Current version of MoTraS can be found here: motras.tgz.

In order to perform LTL model checking, you need to use ltl2dstar to transform the LTL formula into a Rabin automaton.

(Several Rabin automata already created using the ltl2dstar tool are presented in the Examples section below.)

Download the tgz archive above. Unpack it. Run make. (Note:
The Makefile assumes
the `gcc`

compiler. If you want to use another C++ compiler,
you have to change the CXX variable in the Makefile.)

tar xzvf motras.tgz cd motras make

motras [output_option] [-r rabin_automaton_file] [other_options] [dmts_defs_file]

where

`dmts_defs_file`

is a text file containing the definitions of (D)MTS processes, the format of the file is described below, in section Input Language; if the file is omitted, the definitions are read from the standard input`-r rabin_automaton_file`

is a text file containing the description of a Rabin automaton; the Rabin automaton has to be in the output format of the ltl2dstar tool

`output_option`

is one (and only one) of
`-d process_name`

– output the reachable state space of process`process_name`

in the Graphviz DOT language.`-p process_name`

(needs`-r`

to be specified) – output the product of the process`process_name`

and the Rabin automaton in the Graphviz DOT language.`-s process_name`

(needs`-r`

to be specified) – solve the Rabin game, i.e. determine, whether there is an implementation of`process_name`

satisfying the formula given by the Rabin automaton; output a YES/NO answer and if the answer is YES, output an implementation in the input format (see below)`-S process_name`

similar to`-s`

above, the YES/NO answer is output to stderr, the implementation is in the Graphviz DOT language.

`other_options`

are:
`-f`

if possible, transform the process given by`-d`

,`-p`

,`-s`

or`-S`

into a DMTS process that has exactly all the deadlock-free implementations of the original process; if that is impossible (i.e. all implementations of the given process have a reachable deadlock), print a message that no deadlock-free implementations of the given process exist`-m`

(only makes sense with`-s`

and`-S`

) minimizes the produced implementation (using bisimulation quotienting)

The input language is a process-algebra-like language.

There are two types of identifiers: process names and action names.
All identifiers consist of a sequence of alphanumeric characters
and underscores, the process names start with
an *upper case letter*, the action names start with
a *lower case letter*. Thus, e.g. `SomeProcess`

is a process name, while `someAction`

is an action
name.

The input file may contain one or more definitions. Every definition is of the following form:

<process_name> = <process_definition>where process definition is one of the following:

- a process with one may transition:

`? action . NextProcess`

- a process with one must transition to one target
(and the corresponding may transition):

`action . NextProcess`

- a process with one must (hyper)transition with several targets
(and the corresponding may transitions):

`{ action1 . NP1 | action2 . NP2 |`

...`| action`

*n*`. NP`

*n*`}`

- a process with several transitions of the above types:

`<transition1> +`

...`+ <transition`

*n*`>`

`NextProcess`

may be either a process name,
or again a process definition, thus allowing such definitions as:
`S = a.b.S`

)
There is a special process name 0 (the number zero), representing
*nil*, the process with no transitions.

The input DMTS file (cmachine.dmts):

Idle = coin.Select Select = { tea.Work | coffee.Work } + ?hotChocolate.Work Work = output.IdleThis is a simple example of a drink vending machine specification. The specification states that the machine has to provide at least one of coffee or tea, and may optionally provide hot chocolate.

We can draw the coffee machine using DOT like this:

motras -d Idle cmachine.dmts | dot -Tpng > cmachine.pngThis draws the state space reachable from process

`Idle`

in the DOT language, then uses DOT to produce a drawing
(cmachine.png).
We may be also interested in asking whether there is an implementation
of the coffee machine that never produces coffee. This requirement
may be written in LTL as *G ! coffee* (where *G*
is the *globally* temporal operator and *!*
is used here to signify negation). Using
ltl2dstar with this formula as the
input, we get the following Rabin automaton:
g_not_coffee.rabin. We may then use:

motras -s Idle -r g_not_coffee.rabin cmachine.dmtsand we get the following answer:

The answer is YES, there is an implementation of Idle that satisfies the condition given by the Rabin automaton. I0 = coin.I1 I1 = tea.I3 I3 = output.I5 I5 = coin.I1This means that such implementation exists and the tool has provided us with one such implementation (the starting process of the implementation is always

`I0`

). We can also draw the implementation using
DOT:motras -S Idle -r g_not_coffee.rabin cmachine.dmts | dot -Tpng > cmachine_impl.pngThis gives us cmachine_impl.png.

Clearly, this implementation can be minimized using bisimulation
quotienting. We tell MoTraS to apply bisimulation quotienting with the
option `-m`

:

motras -s Idle -r g_not_coffee.rabin -m cmachine.dmtsThe output is then:

The answer is YES, there is an implementation of Idle that satisfies the condition given by the Rabin automaton. I0 = coin.I2 I1 = output.I0 I2 = tea.I1We can also draw the minimized implementation:

motras -S Idle -r g_not_coffee.rabin -m cmachine.dmts | dot -Tpng > cmachine_impl_m.pngThis yields cmachine_impl_m.png.

The input MTS file (pstation.mts):

S = low.T + high.U T = ?half.S + ?repair.S U = full.SWe can create the graph:

motras -d S pstation.mts | dot -Tpng > pstation.pngwith the result: pstation.png. We wish to verify the formula:

(Here, we useF G (! repair & ! half & F full) | F G (! full & F half) | G (F repair & F high)

motras -s S -r ps_formula.rabin -f pstation.mts(Note that we used the

`-f`

option here, as we
are only interested in deadlock-free implementations.) We get the following
output:The answer is YES, there is an implementation of S that satisfies the condition given by the Rabin automaton. I0 = low.I1 + high.I2 I1 = repair.I5 I2 = full.I6 I5 = low.I7 + high.I8 I6 = low.I1 + high.I2 I7 = half.I10 I8 = full.I11 I10 = low.I7 + high.I8 I11 = low.I12 + high.I8 I12 = repair.I15 I15 = low.I7 + high.I8We may again draw the implementation:

motras -S S -r ps_formula.rabin -f pstation.mts | dot -Tpng > ps_impl.pngThis gives: ps_impl.png. Using minimization (

`-m`

option) we get:I0 = low.I3 + high.I1 I1 = full.I0 I2 = half.I4 I3 = repair.I4 I4 = low.I2 + high.I1Graphical representation: ps_impl_m.png.

Note about the `-f`

option: internally,
the input MTS process is transformed into a DMTS process
which has exactly all deadlock-free implementations as the original one.
We may draw this DMTS using:

motras -d S -f pstation.mts | dot -Tpng > pstation_dmts.pngThis gives: pstation_dmts.png.

(This is the counterexample from our paper
*Modal Transition Systems: Composition and LTL Model Checking*.)

The input (ce.mts):

M = ?a.N N = a.N + b.NThe formula is

motras -s M -r ce.rabin -f ce.mtsWe get the answer:

The answer is NO, no implementation of M satisfies the condition given by the Rabin automaton.(As we used the

`-f`

option, this answer means that there are
no deadlock-free implementations of `M`

satisfying
the condition.) We may, however, try omitting the `-f`

option:motras -s M -r ce.rabin ce.mtsgiving:

The answer is YES, there is an implementation of M that satisfies the condition given by the Rabin automaton. There exists an implementation with no transitions.We are thus given the answer YES. Instead of obtaining an implementation satisfying the formula, we are given the information that there exists an implementation with no transitions (e.g.