git repositories

ltsmin-pbes – LTSmin with PBES language module.

Installation

Download, build and install mCRL2, revision 11119 or later:

svn checkout https://svn.win.tue.nl/repos/MCRL2/trunk mcrl2-11119 -r 11119
cd mcrl2-11119
wget http://www.cs.utwente.nl/~kant/git/files/mcrl2-svn-diff-rev-11119.diff
patch -p0 -i mcrl2-svn-diff-rev-11119.diff
cmake . -DMCRL2_ENABLE_GUI_TOOLS=OFF -DMCRL2_ENABLE_EXPERIMENTAL=ON -DCMAKE_INSTALL_PREFIX=<prefix>
make && make install

Now download and install LTSmin with the PBES language module (which is now part of the next branch of the official LTSmin repository):

git clone -b next http://fmt.cs.utwente.nl/tools/scm/ltsmin.git
cd ltsmin
git submodule update --init
./ltsminreconf
./configure --with-mcrl2=<prefix> --prefix=<prefix>
make && make install

Usage

You can use the PBES language module for explicit generation tools using the following commands:

# Explicit instantiation to a parity game:
pbes2lts-seq -c -rgs --write-state <spec>.pbes <lts>.dir
# Explicit distributed instantiation to a parity game:
pbes2lts-dist --workers=<workers> -rgs -c --write-state <spec>.pbes <lts>.dir
# Translate from the .dir file format to the file format used by the PGSolver tool:
ltsmin-convert --rdwr <lts>.dir <game>.pg

The explicit parity games can be solved by, e.g., the PGSolver tool or the pbespgsolve tool from the mCRL2 toolset.

The symbolic tools (based on MDDs) for the PBES language module can be used as follows:

# Symbolic instantiation to a parity game:
pbes2lts-sym -rgs --order=chain-prev --saturation=sat-like --save-sat-levels <spec>.pbes
# Symbolic instantiation and solving:
pbes2lts-sym --pg-solve -rgs --order=chain-prev --saturation=sat-like --save-sat-levels <spec>.pbes
# Symbolic instantiation and save to a file:
pbes2lts-sym --pg-write=<game>.spg [other options] <spec>.pbes
# Symbolic solving:
spgsolver <game>.spg