The tool expects the input to be written to stdin
in the xmts
file format, which is described here: xmts-specification, and outputs the result to stdout
. A simple example of the textual representation of an input system is here and more can be found in the downloaded package.
The algorithm is selected via the -a
flag and additional parameters can be passed via the -p
flag. The initial states are passed to the algorithms as starting
points. Furthermore the arity and supported types of an algorithm can be
queried by passing -q
.
Currently the following algorithms are exposed via the command-line interface.
CompositionDMTS
(Parameters: synchronising alphabet for the two systems)CompositionMTS
(Parameters: synchronising alphabet for the two systems)Conjunction
Consistency
DeterministicHullBMTS
DeterministicHullMTS
LTLChecker
(Parameters: LTL Formula to be checked)MaxImplementation
ModalRefinementFixedPoint
ModalRefinementQSat
Quotient
Examples
Query Algorithm Information
[motras-algorithms]$ java -jar motras-algorithms.jar -q -a ModalRefinementQSat Arity: 2 Supported Types: [mts, dmts, bmts, pmts]
Constructing the Deterministic Hull (MTS Version)
Let's assume the following transition system is saved in the file non_deterministic_mts.xmts.
mts non_deterministic_mts [ initial_state s1 action a action b state s1 [ obligation a.s2 & b.s3 a -> s2 a -> s3 b -> s3 ] state s2 [ b -> s4 ] state s3 [ a -> s3 a -> s2 ] state s4 ]
The deterministic Hull is simply created by piping the file to stdin
of the tool.
[motras-algorithms]$ cat non_deterministic_mts.xmts | java -jar motras-algorithms.jar -a DeterministicHullMTS
Which then yields the following result.
mts deterministicHull[ initial_state s1 action b action a state s1[ obligation (b.s3 & a.s2_s3) b -> s3 a -> s2_s3 ] state s3[ a -> s2_s3 ] state s2_s3[ b -> s4 a -> s2_s3 ] state s4 ]
Checking Modal Refinement
We now check modal refinement on two systems contained in the traffic examples directory.
[motras-algorithms]$ cat simple1.xmts param2.xmts | java -jar motras-algorithms.jar -a ModalRefinementQSat true [motras-algorithms]$ cat simple1.xmts simple2.xmts | java -jar motras-algorithms.jar -a ModalRefinementQSat false
Checking a LTL Formula
This example is taken from here.
[motras-algorithms]$ cat CoffeeAndTeaDMTS.xmts | java -jar motras-algorithms.jar -a LTLChecker -p "G ! coffee" true