Home > Archives > DCS (Archive) > Tools

SMI

Symbolic Model Interface
  Sommaire  

 Manual Pages

Description

The SMI library provides an interface to access finite models builded from Networks of Extended Automata. The models are represented symbolically using Decision Diagrams(DDs). The SMI implements functions to handle model state sets and model transitions. The SMI library use exactly one of the following DD implementation at time:

  • BMDDs - Binary Multivalued Decision Diagrams (local)
  • Cudds - Colorado University Decision Diagram
  • TiGeR - TiGeR Binary Decision Diagrams
  • Bdds - Binary Decision Diagrams (local)

We have been developped two applications using the SMI libraries: evaluator which evaluate mu-calculus formulae on the model and mmg which generate the minimal model w.r.t. some bisimulations. The SMI libraries and the applications are available for SunOS and HP-UX platforms.

Synopsis

  • evaluator [smi-options] [eval-option] name[.exp] [name2]
  • mmg [smi-options] [mmg-options] name[.exp]

The name denotes the use of the followings files to build the symbolic model representation:

  • name.exp-:- model definition
  • name.types -:- model types
  • name.order-:- model variables order

The name2 denote an optionally mu-calculus formula file.

The smi-options available are:

  • -stat print various statistics during computation (not a default option)
  • -mem n allocate n MB of memory for DDs (default n = 8 )
  • -vars v use at maximum v DD variables (default v = 48 )
  • -sift enable the DD variables automatic reordering (not a default option)
  • -sim use the simultaneous composition of automata (not a default option)
  • -front frontier strategy for the computation of reachable states (not a default option)
  • -noreach not compute the reachable states (not a default option)

The eval-options might be one of the following:

  • -eval formula backward evaluation (default option)
  • -path extract an execution path to a satisfying state (not a default option)
  • -inv simple invariant checking (not a default option)

For the mmg-options see Aldebaran manual page.

Syntax for Extended Automata

The extended automata are described using the following context-free grammar :

Ext-Aut ::= [Var-Decl-List] [Ctrl-Thread-List]
Var-Decl-List ::= Var-Decl-List Var-Decl
Ctrl-Thread-List ::= Ctrl-Thread-List Ctrl-Thread

Variable declarations

Var-Decl ::= Var-List ’:’ Type-Name
Var-List ::= Var-List ’,’ Var-Name |Var-Name

Control threads

Ctrl-Thread ::= Thread-Descr [Thread-Trans-List]
Thread-Descr ::= ’des’ ’(’ Init-State ’,’ Trans-Number ’,’States-Number ’)’
Thread-Trans-List ::= Thread-Trans-List Thread-Trans

Thread transitions

Thread-Trans ::= ’(’ Start-State ’,’ [Guard] [Action] [Assign] ’,’ Final-State ’)’
Guard ::= ’[’ Bool-Expr ’]’
Action ::= ’send’ Gate-Name [Out-Expr-List]
’receive’ Gate-Name [In-Var-List]
’i’
Out-Expr-List ::= Out-Expr-List ’!’ Expr
In-Var-List ::= In-Var-List ’?’ Var-Name
Assign ::= Var-Name ’:=’ Expr
Assign Assign | Assign ’;’ Assign | ’{’ Assign ’}’

Expressions

Expr ::= Bool-Expr | Nat-Expr | Enum-Expr
Bool-Expr ::= Var-Name | ’ ’ Bool-Expr
Bool-Expr Bool-Op Bool-Expr | Enum-Expr Rel-Op Enum-Expr | Nat-Expr Rel-Op Nat-Expr
Nat-Expr ::= Var-Name | Nat-Number | Nat-Expr Nat-Op Nat-Expr
Enum-Expr ::= Var-Name | Enum-Item-Name | Enum-Op Enum-Expr

Operators

Bool-Op ::= ’\/’ ’/\’ ’=>’ ’<=>’
Rel-Op ::= ’=’ ’<=’ ’>=’ ’>’ ’<’ ’<>’
Nat-Op ::= ’+’ ’-’ ’*’ ’/’ ’%’
Enum-Op ::= ’succ’ ’pred’

Syntax for Data Types

Type-Defs ::= [Nat-Def] [Enum-Def-List]
Nat-Def ::= ’nat’ ’{’ Nat-Range ’}’
Nat-Range ::= Nat-Number
Enum-Def-List ::= Enum-Def-List Enum-Def
Enum-Def ::= ’enum’ Enum-Name ’{’ Enum-Item-List ’}’
Enum-Item-List ::= Enum-Item-List ’,’ Enum-Item-Name| Enum-Item-Name ’,’ Enum-Item-Name
Enum-Name ::= Identifier
Enum-Item-Name ::= Identifier

Syntax for Variable Ordering

The variables and thread control states order used to build the symbolic model can be specified using an external file, which must respect the following syntax :

Order ::= [ Order-Item-List ]
Order-Item-List ::= Order-Item-List Order-Item
Order-Item ::= Aut-Name ’:’ Var-Name | Aut-Name ’:’ Thread-Id
Aut-Name ::= Identifier
Var-Name ::= Identifier
Thread-Id ::= Nat-Number

 Contact

For more information, contact Marius Dorel Bozga


New publications