MoTraS

(c) Nikola BeneŇ°, xbenes3 (-at-) fi.muni.cz

Description

MoTraS is a prototype tool for verification of (disjunctive) modal transition systems.

Download

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.)

Installation Instructions

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

Usage

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

where

output_option is one (and only one) of other_options are: Examples of usage can be found in section Examples below.

Input Language

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: (The 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.

Examples

The Coffee Machine

The input DMTS file (cmachine.dmts):

  Idle = coin.Select
  Select = { tea.Work | coffee.Work } + ?hotChocolate.Work
  Work = output.Idle
This 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.png
This 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.dmts
and 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.I1
This 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.png
This 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.dmts
The 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.I1
We can also draw the minimized implementation:
  motras -S Idle -r g_not_coffee.rabin -m cmachine.dmts | dot -Tpng > cmachine_impl_m.png
This yields cmachine_impl_m.png.

The Power Station

The input MTS file (pstation.mts):

  S = low.T + high.U
  T = ?half.S + ?repair.S
  U = full.S
We can create the graph:
  motras -d S pstation.mts | dot -Tpng > pstation.png
with the result: pstation.png. We wish to verify the formula:
F G (! repair & ! half & F full) | F G (! full & F half) | G (F repair & F high)
(Here, we use & to denote conjunction and | to denote disjunction.) Supplying this formula to ltl2dstar gives the following Rabin automaton: ps_formula.rabin. We then use:
  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.I8
We may again draw the implementation:
  motras -S S -r ps_formula.rabin -f pstation.mts | dot -Tpng > ps_impl.png
This 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.I1
Graphical 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.png
This gives: pstation_dmts.png.

The Simple Counterexample

(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.N
The formula is G a, the corresponding Rabin automaton is ce.rabin. Using:
  motras -s M -r ce.rabin -f ce.mts
We 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.mts
giving:
  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. nil). This implementation satisfies (vacuously) all LTL formulae.