IBM
Contents Index Previous Next



State Space Files


Using the command Save-State-Space, a Labelled Transition System (LTS) representing the state space generated during exhaustive exploration is saved to a file.

Syntax

The syntax of the generated LTS is (using BNF notation):

LTS	 ::=	 `START:' StateId `LTS:' TransList* 
`STATES:' State*

TransList	 ::=	 StateId `:' Event `-' [StateId] (`,' Event 
`-' [StateId])* `;' 

Event	 ::=	 (Output | Input | Timeout | Internal) 

Output	 ::=	 `o(' Signal `,' `"' GraphRef `"' `)' 

Input 	 ::=	 `i(' Signal `,' `"' GraphRef `"' `)'

Timeout	 ::=	 `t(' Timer `)' 

Internal	 ::=	 `x'

State	 ::=	 `*****' StateId `*****' Process*

Process	 ::=	 ProcessName `:' InstanceNo `State:' StateName 
(VariableName `:' Value)* `Input port:[' Signal 
(`,' Signal)* `]' `Timers:{' Timer (`,' Timer)* 
`}' Procedure* 

Procedure	 ::=	 `Procedure' ProcedureName `:' `State:' 
StateName (VariableName `:' Value)*

Signal	 ::=	 SignalName `(' ParameterName (`,' 
ParameterName)* `)'

Timer 	 ::=	 TimerName `(' ParameterName (`,' 
ParameterName)* `)'

Lexical Elements

The lexical elements used above are:

StateId	 	 An integer denoting a system state.

GraphRef	 	 A string denoting a graphical reference to an 
SDL diagram.

ProcessName	 	 An id denoting a process type.

InstanceNo	 	 An integer denoting a process instance.

StateName	 	 An id denoting a state in an SDL process graph.

VariableName	 	 An id denoting a process variable.

Value	 	 A string denoting a value for a variable of any 
defined SDL type.

ProcedureName	 	 An id denoting a procedure.

ParameterName	 	 An id denoting a signal or timer parameter.

Example 341 : A Generated LTS

A simple example of a generated LTS:

START:121 
LTS:
2456:o(sig1(true,3),"5 P1 1 80 100")-43567;
43567:i(sig2(1),"5 P1 1 80 120")-2467,
i(sig2(2),"5 P1 1 100 120")-98567;
121:x-2456;
2467:x-27645;
98567:x-27645;
27645:i(sig2(1),"5 P1 1 80 120")-2467,
i(sig2(2),"5 P1 1 100 120")-98567;
STATES:
***** 121 *****
P1:1 State:idle Parent:null Offspring:null Sender:null i:0 Input port:[ ] Timers:{ }
***** 2456 *****
P1:1 State:idle Parent:null Offspring:null Sender:null i:5 Input port:[ ] Timers:{ }
***** 43567 *****
P1:1 State:s1 Parent:null Offspring:null Sender:null i:5 Input port:[ ] Timers:{ }
***** 2467 *****
P1:1 State:s1 Parent:null Offspring:null Sender:null i:1 Input port:[ ] Timers:{ }
***** 98567 *****
P1:1 State:s1 Parent:null Offspring:null Sender:null i:2 Input port:[ ] Timers:{ }
***** 27645 *****
P1:1 State:s1 Parent:null Offspring:null Sender:ENV i:5 Input port:[ ] Timers:{ }


http://www.ibm.com/rational
Contents Index Previous Next