![]() |
![]() |
![]() |
![]() |
![]() |
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.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 |
![]() |
![]() |
![]() |
![]() |