print · login   

On this page we plan to make scripts available that allow one to translate between different types of models, and to decide whether two models of the same type are equivalent.

StatemachineLib

Statemachinelib is a java library which has two user interface frontends:

  • commandline interface with the 'stm' command and
  • a GUI program called 'StatemachineLib'.

Fig. 1: StatemachineLib GUI

Install the GUI application 'StatemachineLib' and 'stm' command by the installation package:

For both Linux and Macos the 'stm' command is installed at /usr/local/bin/stm. Normally for the bash/zsh shell the path /usr/local/bin/ is in the default $PATH environment variable and therefore the 'stm' command can directly be used after installation.

The libary supports the following :

  • models: DFAs, Moore machines, Mealy machines, interface automata (in the future possibly also EFSMs and register automata)
  • these models:
    • are immutable in java
    • can easily be build in java using a builder
  • export and import for the models to the following file formats : dot, gml, aut, graphml
  • you can customize the import and export by giving your own formatting style for the transition label. For instance for a Mealy machine we could represent the transition label in dot file in several ways :
    • a/b
    • ?a / !b
    • Ia / Ob
  • checking equivalence between models
  • several conversions between models, a described in our paper. Some examples:
    • a DFA can be converted to a Moore machine
    • a Moore machine can be converted into a DFA if we supply accepting and rejecting subsets for the Moore machine outputs
    • a Moore machine can be converted into a Mealy machine
    • a Mealy machine can be converted into a Moore machine
    • a Mealy machine can be converted into an Interface Automaton
    • a (deterministic) Interface Automaton can be converted to a DFA
    • if a Mealy machine is represented as an interface automaton then we can convert it back to a Mealy machine model
    • DFA and Mealy machine models in statemachinelib can be converted to their corresponding models in automatalib which is used by learnlib

The 'stm' commandline tool requires a java 8 installation and can be downloaded as stm.zip. You can install it by just extracting the zip file and putting the 'bin/' subdir to your system's PATH environment variable.

The 'stm' commandline tool supports the following subcommands: (will be extended in the future) 

    $ stm --help

    usage: stm [-h]   ...

    statemachine tool

    named arguments:
      -h, --help             show this help message and exit

    subcommands:

        convert              convert lossless the statemachine representation
        info                 displays information about the statemachine:
                             number of states, number of transitions,  ...

The help for the 'convert' command: 

    $ stm convert --help

    usage: stm convert [-h] {fa2moore,moore2mealy,mealy2moore,mealy2ia}
               inputfile outputfile

    convert lossless the statemachine representation

    positional arguments:
      {fa2moore,moore2mealy,mealy2moore,mealy2ia}
                             type of conversion
      inputfile              input file
      outputfile             output file

    named arguments:
      -h, --help             show this help message and exit

The help for the 'info' command: 

    $ stm info --help
    usage: stm info [-h] {fa,moore,mealy,ia,register} file

    displays information about the statemachine:
    number of states, number of transitions,  ...

    positional arguments:
      {fa,moore,mealy,ia,register}
                             type of statemachine
      file                   model file

    named arguments:
      -h, --help             show this help message and exit

Sut Tool

Using the Sut tool we can easily generate a running SUT from a register model to which you can then communicate over network sockets. By using the CADP tool set it also supports flattening of register models to a fixed integer domain.