SA Tool

  1. News
  2. About
  3. Usage
  4. Input Format
  5. Source Code
  6. Contact
  7. Related Papers

News

23rd of June 2011: Bugfix: initial relation for upward simulation was not set up correctly.
25th of February 2011: Feature: output format improved (by Ondrej Lengal).
3rd of February 2011: Bugfix: usage info was printed even in the case of correct invocation.
28th of January 2011: Bugfix: relation not updated correctly during initialisation phase.

About

SA tool is a utility for computing simulations over labelled transition systems (LTS) and tree automata (TA) based on the paper presented at MEMICS'09.

Usage

The program can be used in 3 different ways:
  1. LTS Simulation. In this case the program computes simulation over an LTS. An LTS is encoded as a tree automaton containing only unary transitions (representing an LTS) and leaf transitions (representing initial states).
    usage: sa lts <file>
  2. Downward Simulation. In this case the program computes downward simulation over a TA.
    usage: sa ta-down <file>
  3. Upward Simulation. In this case the program computes upward simulation over a TA.
    usage: sa ta-up <file>

Input Format

The program expects an input to be formated in Timbuk style:
<file>            : 'Ops' <label_list> <automaton> <automaton> ... 

<label_list>      : <label_decl> <label_decl> ... // a list of label declarations

<label_decl>      : string ':' int // a symbol declaration (the name and the arity)

<automaton>       : 'Automaton' string 'States' <state_list> 'Final States' <state_list> 'Transitions' <transition_list>

<state_list>      : <state> <state> ... // a list of states

<state>           : string // the name of a state

<transition_list> : <transition> <transition> ... // a list of transitions

<transition>      : <label> '(' <state> ',' <state> ',' ... ')' '->' <state> // a transition

<label>           : string // the name of a label
An example could look like this:
Ops a:0 b:1 c:2

Automaton A
States q0 q1 q2
Final States q2 
Transitions
a() -> q0
b(q0) -> q1
c(q1, q1) -> q1
c(q1, q1) -> q2
c(q2, q2) -> q2

Source Code

The program is written in OCaml which is required to compile the source code. It is licensed under GPL.

Contact

If you have further questions, do not hesitate to contact authors (Lukas Holik, Jiri Simacek).

[1]
Holik Lukas, Simacek Jiri: Optimizing an LTS-Simulation Algorithm, In: 5th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, Znojmo, CZ, FI MU, 2009, s. 93-101, ISBN 978-80-8734-204-6
[2]
Holik Lukas, Simacek Jiri: Optimizing an LTS-Simulation Algorithm, FIT-TR-2009-03, Brno, CZ, 2009, p. 17