Translation Tool for LTS BMC
This archive contains the tool for translating LTS models to Boolean
Circuits modeling path executions of bounded length. The tool
is in the file "lts.static". In addition, a python script called "prep.py"
is provided for LTSs needing preprocessing.
Usage
Its usage is as follows:
./lts.static -b num -n -g filename1, ... , filenameN > result
where
"-b num" is the length of the executions.
"-n" creates a circuit modeling path executions.
"-g" adds the global synchronization check.
filename an LTS file.
For instance to create the circuit modeling path executions
of length 1 of the example elev_3 (should be satisfiable) the command is.
./lts.static -b 1 -n -g elev_3_pp/*.lts > elev_3.1.n.SAT
The archive is available here
If you want to comment / need additional information contact the author
Toni Jussila