git repositories

ltsmin-pbes – LTSmin with PBES language module.


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

svn checkout mcrl2-11119 -r 11119
cd mcrl2-11119
patch -p0 -i mcrl2-svn-diff-rev-11119.diff
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
cd ltsmin
git submodule update --init
./configure --with-mcrl2=<prefix> --prefix=<prefix>
make && make install


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