Translation Tool for LTS BMC
This archive contains the tool for translating LTS models to Boolean
Circuits modeling step and process executions of bounded length. The tool
is in the file "lts.static".
Usage
Its usage is as follows:
./lts.static -b num -o | -p filename1, ... , filenameN > result
where
"-b num" is the length of the executions.
"-o" creates a circuit modeling step executions.
"-p" creates a circuit modeling process executions.
filename an LTS file.
For instance to create the circuit modeling process executions
of length 3 of the example elev_1 (should be satisfiable) the command is.
./lts.static -b 3 -p elev_1/*.lts > elev_1.3.p.SAT
The archive is available here
If you want to comment / need additional information contact the author
Toni Jussila