User Tools

Site Tools


wonham:tools

Supervisory control tools

The supervisory control tools or svctools is a collection of Python tools to create, manipulate, and visualize state machines, in particular Wonham state machines with controllable and uncontrollable transitions.

  • File format The file formats used by the svctools
  • sctool The Python variant of Wonham's tct tool
  • ads2stm Convert Wonham's tct tool .ads output file to a .stm file
  • ads2sup Synthesize a supervisor using Wonham's tct tool from .ads files (only for Linux systems)
  • gen-chi Generate Chi 1.0 recursion definition code from a .stm file
  • gen-dot Convert a .stm file to a graph suitable as input for the dot program of Graphviz to render 2D pictures
  • stm2ads Convert a .stm file to an .ads suitable as input for Wonham's tct tool
  • stm2fsm Convert a .stm file to a graph .fsm format suitable for rendering 3D pictures and examining the state space.
  • wmod2ads Convert a .wmod file to multiple .ads files

Version history

Version Date News Download
0.18 2009-06-25 ads2sup: Fixed some typos. ; ads2sup: Fixed some wrong information in the generated input templates. ; wmod2ads: No longer use event number 0, as some tooling can't handle it. ; wmod2ads: Added --overwrite (-w) option to overwrite files without asking. ; wmod2ads: No longer crash with stack trace, but show user friendly error messages. ; wmod2ads: If one or more events are not used in a plant, the application no longer quits with an error message. Instead, a warning is displayed and the application continues. svctools-0.18.tar.gz
0.17 2008-10-06 Fixed bug and now allow commands with whitespaces in ads2sup svctools-0.17.tar.gz
0.16 2008-09-05 Added optional command in ads2sup for defining the location of the 'tct' program svctools-0.16.tar.gz
0.15 2008-06-05 Updated support for 'waters' format, added 'wmod2ads' and 'ads2sup' programs svctools-0.15.tar.gz
0.14 2008-01-21 Fixed bug in FSM file generation (SVCtools issue #9, reported by P.Thijs)
0.13 2007-04-25 Removed PLY from the package (now an external dependency) svctools-0.13.tar.gz
0.12 2007-04-11 Added export to 'waters' format (R.Theunissen)
0.11 2006-07-06 Fix for displaying marker states as requested in http://devel.se.wtb.tue.nl/trac/svctools/ticket/1 svctools-0.11.tar.gz
0.10 2006-06-15 Switched from SPARK to PLY parser
0.9 2006-06-09 A few less typo's than in 0.8
0.8 2006-06-08 selfloop now has two arguments, one for adding controllable events, and one for adding uncontrollable events. Added copying of marker states from ADS. Component name is set in sctool when saving in STM format not available
0.7 2006-06-06 Bugfix for __copy__() on sets; renamed .txt format to .sct
0.6 2006-06-02 Added --show-state option to gen-chi
0.5 2006-05-23 Added stm2fsm convertor
0.4 2006-05-18 Bugfix, saved .txt files can now also be loaded again
0.3 2006-05-18 Added stm2ads conversion tool
0.2 2006-05-17 Fixed bug in sync command of sctool
0.1 2006-05-17 Initial release

Visualisation tools

A picture says a thousand words, and this certainly holds for state machines. The easiest path is from the .stm file format via the gen-dot and dot programs to a two-dimensional picture with states and arrows.

For larger state spaces, the above path becomes less useful. You can then switch to more advanced visualisation tools to help you analyse the state space from the .stm file format via the stm2fsm convertor, and one of the tools listed below:

ads2stm

The ads2stm utility converts the .ads output file from Wonham's tct tool to a state machine file. You must choose to create the .ads file from the tct tool's menu. The .stm file format is used as input for several other tools, such as the gen-chi and the gen-dot utilities.

Usage:

ads2stm  [options] [ads-file [stm-file]]

with options:

   --help, -h                            Online help
   --input=file.ads, -i file.ads         Read file.ads as input
   --output=file.stm, -o file.stm        Write output to file.stm

Example: ads2stm -i controller.ads -o controller.stm

ads2sup

With the ads2sup utility it is possible to synthesize automatically supervisors using Wonham's tct tool. You must create an inputfile were you define the order of tct commands for the synthesis.

Usage:

ads2sup [options] input-file

with options:

    --ads=file        -a file     Location ADS-index file
    --no_execution    -e          Disables the execution of the commands
    --help            -h          Online help
    --label=file      -l file     Location label-file
    --template=name   -t name     Generate template input-file

Example: ads2sup -a ads_index -l label_file.lbl input

Example of an input file:

% Convert ads-files to des-files
ADS2DES

% Create one plant model (P)
SYNC: Automaton_1, Automaton_2, P

% Add selfloops for the unused events at requirements
ALLEVENTS: P, P_events
SYNC: Automaton_3, P_events, Automaton_3
SYNC: Automaton_4, P_events, Automaton_4

% Create on requirement model (R)
MEET: Automaton_3, Automaton_4, R

% Minimize the models
MINSTATE: P, P
MINSTATE: R, R

% Synthesize a supervisor (S)
SUPCON: P, R, S

% Minimize the supervisor
MINSTATE: S, S

% Check if the alphabet of the supervisor and the plant are the same
ALLEVENTS: S, S_events
ISOMORPH: P_events, S_events

Example of an ADS-index file:

{
    '1' : ('PLANT', 'Automaton_1') ,
    '2' : ('PLANT', 'Automaton_2') ,
    '3' : ('SPEC', 'Automaton_3') ,
    '4' : ('SPEC', 'Automaton_4') ,
}

Example of a label file:

{
    '1' : 'Controllable_event_1' ,
    '3' : 'Controllable_event_2' ,
    '4' : 'Uncontrollable_event_1' ,
    '6' : 'Uncontrollable_event_2' ,
}

gen-chi

Wonham's tct tool is used to design a supervisory controller, which is the description of a state machine. This state machine should be translated to, for instance, a chi 1.0 implementation before you can use it. To simplify this translation the gen-chi utility (located in directory /opt/se/bin/) may be used. It uses recursion definitions (mode) to create the chi state machine part of the controller implementation. Keep in mind that recursion definitions are only available in the Python version of the chi compiler, not in the C version.

Usage:

gen-chi [options] [stm-file [label-file [chi-file]]]

with options:

    --help, -h               Online help
    --show-state, -s         Output state name upon entrance (at run time)
    --input=STM, -i STM      Read STM as input
    --label=LABEL, -l LABEL  Use file LABEL for event label translations
    --output=CHI, -o CHI     Write output to file CHI

Example: gen-chi -i example.stm -l example.lbl -o example.chi

The label file file.lbl is a normal ASCII file with on each line an event number, followed by the chi code that has to be inserted for that event. Both items are seperated with a colon (:).

Example:

0 : a!x
1 : b!y
2 : c?x

shows a label file with three event labels (0,1, and 2) with their corresponding chi code snippets that should be executed when the transition takes place.

To obtain a trace of the states being visited as the state machine is being executed, you can add the –show-state option. The program then generates additional print statements that output the name of the state at the moment the state is entered. In this way you can observe which states are visited, which may be helpful for example in debugging.

gen-dot

The gen-dot program reads a state machine file (a .stm file), and generates a graph in dot format, the file format of many visualization programs in Graphviz. By processing the output further, a (2D) picture of the state machine can easily be obtained.

Usage:

gen-dot [options] stm-file [component]

stm-file must be replaced by the name of the .stm file. If the file contains more than one component, the last argument may be used to select which component should be converted.

Options:

    --help, -h                 Online help
    --output=FILE, -o FILE     Write output to FILE
    --papersize=SIZE, -p SIZE  Set papersize to SIZE
Currently supported papersizes: A4, B4

If an output file is specified in the options, output is written to that file. If no output file has been specified, output is written to the stdout. In the latter case, you can redicrect the output to a file using the redirection mechanism of the shell, like gen-dot example.stm > example.dot.

stm2ads

The stm2ads convertor converts a statemachine .stm file back to .ads format. The latter has much more restrictions, so not all statemachine files are acceptable.

The program tries to create a similar file in the sense that numbers in states and events are preserved. For example, state “S123” in the .stm file is mapped to state number 123 in the .ads file. Due to this mapping, it is not allowed to have two state names with the same number at the end in the .stm file. For similar reasons, actions labels that end with a number should be odd, and events that end with a number should be even.

All states, actions, and events without any number get an arbitrary free number.

Usage:

stm2ads [options] [stm-file [ads-file]]

Options:

    --help, -h               Online help
    --input=STM, -i STM      Read STM as input
    --output=ADS, -o ADS     Write output to file ADS

stm2fsm

For large state machines, a 2D picture as generated by for example dot becomes too crowded. The Visualisation group of the department of Informatica is doing research to overcome these problems. They also develop tools for viewing and examining large state spaces, in particular FSMView and NoodleView. Both tools accept the FSM file format. A more experimental tool is StateVis. This tool also accepts the FSM format.

The stm2fsm convertor takes a .stm file, and generates such a .fsm file, so the (generated) Wonham state machine can be viewed and examined in 3D. At the moment, the convertor generates a file with four properties for each state:

  1. stateName, name of the state
  2. marked, is the state a marker state?
  3. fanIn, the number of ingoing transitions of a state
  4. fanOut, the number of outgoing transitions of a state

In addition, actions (controllable events in Wonham) are labelled “action(label)”, and events (uncontrollable events in Wonham) are labelled “event(label)”, where label is the label identifier of the action or event.

If you like to have other properties, please ask. Also, the authors of the viewing tools are interested in your experiences (both good and bad), so they can improve their tools.

Usage:

stm2fsm stm-file fsm-file

wmod2ads

The wmod2ads utility converts .wmod files to multiple .ads files

Usage:

wmod2ads [options] wmod-file

with options:

    --help    -h          Online help
    --output  -o folder   Name output folder

Example: wmod2ads -o outputfolder inputfile.wmod

wonham/tools.txt · Last modified: Friday, 19 February 2010 : 08:11:29 by dhendriks