Beam Search Supplementary Material

Downloads/Links

The latest version of the µCRL toolset for Linux, which includes implementations of minimal-cost search (MCS), g-Synchronised Detailed Beam Search (g-SDBS), and g-Synchronised Flexible Detailed Beam Search (g-SFDBS), can be downloaded here.


Variants of Priority Beam Search (PBS) are as of yet not part of the official release of the µCRL toolset. Version 2.18.5 of the toolset for Linux extended with PBS variants can be downloaded here.


The µCRL specifications and .tbf files of the AIPS 2000 planning problems can be downloaded here.


The µCRL specifications and .tbf files of the Zebra Finch problem can be downloaded here.


The µCRL specifications and .tbf files of the Clinical Chemical Analyser case study can be downloaded here.


The µCRL specifications and .tbf files of the Cannibals & Missionaries problem can be downloaded here.


For instructions how to use the µCRL modelling language see the official website.

How to compile the µCRL toolset

The following is applicable for both the official release and the extended version of the toolset. Unpack the tool archive and cd to the main folder. We recommend compiling the µCRL toolset
by typing the following at the command line (as root):

1. ./configure --enable-development

2. ./make

3. ./make install

How to obtain the .tbf files from the specifications

Although the .tbf files (which are linearised versions of the µCRL specifications)
are provided in the case study packages above, they can be generated
from the µCRL specifications with some additional optimisations, by typing the following
at the command line (for a given specification a.mcrl):

mcrl -stdout -regular2 -nocluster a.mcrl | constelm | sumelm | constelm | stategraph > a.tbf

How to use the exhaustive search algorithms in the µCRL toolset

Given a .tbf file a.tbf, type the following at the command line to run
the different search algorithms (where finished is the action we are looking
for on-the-fly):

Exhaustive breadth-first search (BFS)

instantiators -local -trace -action finished -stop a.tbf

Minimal-cost search (MCS)

instantiators -local -tick -trace -action finished -stop a.tbf

How to use beam search in the µCRL toolset

g-Synchronised (Flexible) Detailed Beam Search (g-S(F)DBS)

The following search algorithms require, in addition to a .tbf file, a heuristic function to guide the search. In the following, we denote such a function with <heur>. Also, a beam width needs to be given. This beam width is a natural number, and we denote it with <β>.

For the different case studies, the following should replace <heur>: g-SDBS can be launched as follows:
instantiators -local -tick -trace -action finished -stop -detailed-expr -beam-width <β> a.tbf <<EOF
<heur>
EOF


A flexible variant can be launched by replacing -beam-width with -beam-width++.

g-Synchronised (Flexible) Priority Beam Search (g-S(F)PBS)

To launch a (flexible) priority beam search, a file describing the priorities of the different actions must be used. In the following, we denote such a file with <priofile>. As in detailed beam search, additionally, a beam width must be given, here called <α>. Finally, the pruning in a priority beam search can be stabilised at a particular search level by setting the stabilisation level, called <l> in the following.

The priority file for the Clinical Chemical Analyser case study can be downloaded here.

g-SPBS can be launched as follows:
instantiators -local -tick -trace -action finished -stop -beam-priority <priofile> beam-width <α> -beam-slevel <l> a.tbf

A flexible variant can be launched by replacing -beam-width with -beam-width++.