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>:
- Cannibals and Missionaries Problem (with <C> the number of cannibals):
CanLeft+MisLeft+(f*(2*<C>))
- Zebra Finch Problem:
(2*LeftGroup)+LeftHusGroup+LeftWifGroup+LeftHusRight+LeftWifRight+LeftYoung
- Clinical Chemical Analyser:
left
- AIPS 2000 Planning Problems:
h
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++.