Welcome to the homepage!

MoTraS is a tool for modal transition systems (MTS), disjunctive MTS and further MTS extensions. It implements relations and operations standard for specification theories as well as deterministic hull (see here), generalized model checking (see here, linking the implementation accessible here with ltl2dstar and LTL2BA) and more. Further, QBF-based refinement checking uses Quantor.

MoTraS is written in Java and is developed at Technical University Munich, Faculty of Informatics, Chair 7.
If you have any questions please contact the authors Jan Kretinsky or Salomon Sickert.
The logo reflects the defining assumption of MTS that whatever is required is also allowed.


(0) News

Update on June 17: link to the xmts specification has been fixed.


(1) Download MoTraS

You can download the tool as an executable and run it using Java 1.7 (note that GUI experiences problems when Java 1.6 is used; tested on Linux, Mac OS and Windows). The algorithms package with the command line interface, linked executables mentioned above, examples and a readme file can be downloaded here. The source files are here. The graphical user interface can be downloaded here. Please read also the disclaimer below. If MoTraS appears not to have any active buttons and looks like this ↓ then Java 1.7 needs to be (re-)installed.

Build Dependencies

In order to build the tool various libraries are needed.

Runtime Dependencies

motras-algorithms requires a recent version of Java, namely Java 7.

Furthermore some algorithms, such as the ModalRefinementQSat and the LTLChecker need external applications, which need to be placed in the lib subdirectory. The name of executable has to match exactly the names listed below. More specifically:

ModalRefinementQSat
LTLChecker


(2) GUI Usage

MoTraS CLI can be invoked and used as described below. To run the GUI, please use the executables in motras_ui/bin for Linux or Windows. The GUI is self-explanatory, but we show a couple of screenshots to explain the functionality. The first one shows the MoTraS basic features: drawing area in the middle and side panels for setting properties (also possible by right-clicking on the drawing area) and calling algorithms. The windows layout can be fully adjusted.

In the next screenshot, one can see two systems displayed at once and each of the windows contains more tabs opened (displayable upon clicking the name of the current systems next to the switch between the visual and source code representation). The refinement checker is called here for the indicated systems.

If an algorithm with only one input system is called, the seocnd argument is grayed out as follows:

Upon calling an algorithm producing a system, a new tab in the current window is created containing the result:

Whenever an exception is encountered, such as external tools aren't available or the input for the algorithm is malformed, e.g. an DMTS is passed instead of an MTS, a red exclamation mark appears at the right bottom of the window. Additional information is revealed by clicking on that icon.


(3) CLI Usage

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.

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

(4) Experiments

Firstly, we compare the performance of the MoTraS and MTSA on modal refinement of MTS. We compare them systems with 500 states, see the table below (computational times in seconds). We consider systems with different sizes of alphabet and branching degrees. We further consider "global" monolithic systems where the transitions are evenly distributed, and "local" systems with several clusters mutually connected with only a few edges. We do not include results for the tool MIO here as there are stack overflows already for systems with less than 150 states, and for systems with 100 states the time is actually more than 3 seconds while MIO reports 0 seconds, see here.

SizeStructureMTSAMoTraS
Alphabet 2, branching 5Global:4.572.23
Local0.340.04
Alphabet 2, branching 10Global:6.628.75
Local:5.996.73
Alphabet 10, branching 5Global:1.460.50
Local:1.540.01
For more details on global and local systems and results on QBF-based refinement, see here. Further, we display the running times for the exponential construction of the deterministic hull for alphabet with two elements:

** Degree: 2
*** Structure: Local
101520255075100
0(0)0(0)0(0)0(0)0.01(0.01)0.02(0.01)0.03(0.02)
*** Structure: Global
101520255075100
0(0)0(0)0.01(0)0.01(0.01)0.26(0.15)2.53(4.65)10.95(9.55)
** Degree: 5
*** Structure: Local
101520255075100
0(0)0(0)0(0)0(0)0(0)0(0)0(0)
*** Structure: Global
101520255075100
0(0)0(0)0(0)0(0)0.02(0.01)0.05(0.02)0.08(0.02)

Experiments conducted for the journal version of our ICTAC'13 paper: The experimental data can be found here

(5) Disclaimer

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS ''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
(Last update: May 23, 2013)