User Tools

Site Tools


wonham:tools

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
wonham:tools [Thursday, 25 June 2009 : 16:20:08]
dhendriks Fixed option name formatting
wonham:tools [Friday, 19 February 2010 : 08:11:29] (current)
dhendriks Updated 'dev' to 'devel'
Line 1: Line 1:
 +====== Supervisory control tools ======
 +The //​supervisory control tools// or //​svctools//​ is a collection of [[http://​www.python.org/​|Python]] tools to create, manipulate, and visualize state machines, in particular Wonham state machines with controllable and uncontrollable transitions.
  
 +  * [[creating_and_editing_state_machines|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 [[http://​www.graphviz.org|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. | {{:​wonham:​svctools-0.18.tar.gz|svctools-0.18.tar.gz}}|
 +|   ​0.17 ​ | 2008-10-06 | Fixed bug and now allow commands with whitespaces in ads2sup | {{:​wonham:​svctools-0.17.tar.gz|svctools-0.17.tar.gz}}|
 +|   ​0.16 ​ | 2008-09-05 | Added optional command in ads2sup for defining the location of the '​tct'​ program | {{:​wonham:​svctools-0.16.tar.gz|svctools-0.16.tar.gz}} |
 +|   ​0.15 ​ | 2008-06-05 | Updated support for '​waters'​ format, added '​wmod2ads'​ and '​ads2sup'​ programs | {{:​wonham:​svctools-0.15.tar.gz|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) | {{:​wonham:​svctools-0.13.tar.gz|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]] | {{:​wonham:​svctools-0.11.tar.gz|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:  ​
 +  * [[http://​www.mcrl2.org/​wiki/​index.php|LTSView (part of mCRL2)]]
 +  * [[http://​www.win.tue.nl/​~fvham/​fsm|FSMView]]
 +  * [[http://​www.win.tue.nl/​~apretori/​noodleview/​index.html|NoodleView]]
 +  * [[http://​www.win.tue.nl/​~apretori/​diagraphica/​index.html|Diagraphica]]
 +  * [[http://​www.win.tue.nl/​~apretori/​statevis/​index.html|StateVis]]
 +
 +
 +===== 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:
 +<​code>​
 +ads2stm ​ [options] [ads-file [stm-file]]
 +</​code>​
 +with options:
 +<​code>​
 +   ​--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
 +</​code>​
 +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:
 +<​code>​
 +ads2sup [options] input-file
 +</​code>​
 +with options:
 +<​code>​
 +    --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
 +</​code>​
 +Example: ''​ ads2sup -a ads_index -l label_file.lbl input''​
 +
 +Example of an input file: 
 +<​code>​
 +% 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
 +</​code>​
 +
 +Example of an ADS-index file:
 +<​code>​
 +{
 +    '​1'​ : ('​PLANT',​ '​Automaton_1'​) ,
 +    '​2'​ : ('​PLANT',​ '​Automaton_2'​) ,
 +    '​3'​ : ('​SPEC',​ '​Automaton_3'​) ,
 +    '​4'​ : ('​SPEC',​ '​Automaton_4'​) ,
 +}
 +</​code>​
 +
 +Example of a label file:
 +<​code>​
 +{
 +    '​1'​ : '​Controllable_event_1'​ ,
 +    '​3'​ : '​Controllable_event_2'​ ,
 +    '​4'​ : '​Uncontrollable_event_1'​ ,
 +    '​6'​ : '​Uncontrollable_event_2'​ ,
 +}
 +</​code>​
 +
 +
 +===== 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 [[http://​seweb.se.wtb.tue.nl/​documentation/​manuals/​chi10/​refman-r813/​ch05.html#​id2786831|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:
 +<​code>​
 +gen-chi [options] [stm-file [label-file [chi-file]]]
 +</​code>​
 +with options:
 +<​code>​
 +    --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
 +</​code>​
 +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:
 +<​code>​
 +0 : a!x
 +1 : b!y
 +2 : c?x
 +</​code>​
 +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 [[http://​www.graphviz.org/​|Graphviz]]. By processing the output further, a (2D) picture of the state machine can easily be obtained.
 +
 +Usage:
 +<​code>​
 +gen-dot [options] stm-file [component]
 +</​code>​
 +''​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:
 +<​code>​
 +    --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
 +</​code>​
 +
 +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:
 +<​code>​
 +stm2ads [options] [stm-file [ads-file]]
 +</​code>​
 +
 +Options:
 +<​code>​
 +    --help, -h               ​Online help
 +    --input=STM,​ -i STM      Read STM as input
 +    --output=ADS,​ -o ADS     Write output to file ADS
 +</​code>​
 +
 +
 +===== stm2fsm =====
 +For large state machines, a 2D picture as generated by for example ''​dot''​ becomes too crowded. The [[http://​w3.win.tue.nl/​nl/​de_faculteit/​capaciteitsgroepen/​informatica/​vis/​|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 [[http://​www.win.tue.nl/​~fvham/​fsm|FSMView]] and [[http://​www.win.tue.nl/​~apretori/​noodleview/​index.html|NoodleView]]. Both tools accept the FSM file format.
 +A more experimental tool is [[http://​www.win.tue.nl/​~apretori/​statevis/​index.html|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:
 +
 +  - //​stateName//,​ name of the state
 +  - //marked//, is the state a marker state?
 +  - //fanIn//, the number of ingoing transitions of a state
 +  - //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:
 +<​code>​
 +stm2fsm stm-file fsm-file
 +</​code>​
 +
 +
 +===== wmod2ads =====
 +The ''​wmod2ads''​ utility converts ''​.wmod''​ files to multiple ''​.ads''​ files
 +
 +Usage:
 +<​code>​
 +wmod2ads [options] wmod-file
 +</​code>​
 +with options:
 +<​code>​
 +    --help ​   -h          Online help
 +    --output ​ -o folder ​  Name output folder
 +</​code>​
 +Example: ''​ wmod2ads -o outputfolder inputfile.wmod''​
wonham/tools.txt · Last modified: Friday, 19 February 2010 : 08:11:29 by dhendriks