SYNOPSIS

A text based intermediate format for PINS models.

DESCRIPTION

An ETF file is a sequence of sections.

  • The first section must be a state section, describing the state vector.

  • The second section must be an edge section, describing the edge labels.

  • There must be a single init section, describing the initial state(s).

  • There can be 0 or more map sections, defining a state label each.

  • There can be 0 or more sort sections, describing the values of sorts.

  • There can be 0 or more trans sections, describing a partition of the transition relation each.

GRAMMAR

etf         ::= state edge ( trans | map | sort )* init ( trans | map | sort )*
state       ::= "begin state"
                opt_decl*
                "end state"
edge        ::= "begin edge"
                declaration*
                "end edge"
init        ::= "begin init"
                number*
                "end init"
map         ::= "begin map" declaration
                mapentry*
                "end map"
trans       ::= "begin trans"
                transentry*
                "end trans"
sort        ::= "begin sort" ident
                value*
                "end ident"
opt_decl    ::= (ident | "_") ":" (ident | "_")
declaration ::= ident ":" ident
mapentry    ::= ( number | "*" ) * ( value | number )
transentry  ::= ((number "/" number)|"*")* ( value | number )*
ident       ::= '_'*[':print:'] ([':print:']*
number      ::= ['0'..'9']+
value       ::= 'see below'

Note that the current parser is line based and requires that every section entry is one line and that the begins and end are also lines. This version supports three kinds of values:

  • A quoted string, e.g., "foo bar" (contained double quotes and backward slashes must be escaped with a backward slash)

  • A hex encoding of a byte string. That is, # followed by pairs of hex digits encoding chars followed by #. E.g., #61FF62FF63#.

EXAMPLE

The LTS

+-------+           +-------+
|+-----+|     a     |       |
|| 0 0 || ------->  |  0 1  |
|+-----+|           |       |
+-------+           +-------+

    |                   |
    |b                  |b
    V                   V
   ___                 ___
  /   \               /___\
 /     \     a       //   \\
|  1 0  | ------->  || 1 1 ||
 \     /             \\___//
  \___/               \___/

with initial state 00 is represented by the ETF specification:

begin state
shape:shape  multiplicity:multiplicity
end state
begin edge
action:action
end edge
begin init
0 0
end init
begin trans
0/1 * 1
end trans
begin trans
* 0/1 0
end trans
begin map shape:shape
0 * "square"
1 * "circle"
end map
begin map multiplicity:multiplicity
0 0 1
0 1 0
1 0 0
1 1 1
end map
begin sort action
"a"
"b"
end sort
begin sort multiplicity
"single"
"double"
end sort

SEE ALSO

ltsmin(7), etf2lts-mpi(1), etf2lts-grey(1), etf-reach(1), etf-convert(1)