|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.mc.Model
de.upb.swt.mcie.mc.Transitionsystem
public class Transitionsystem
Implements a transition system. A transition system consists of an
initial condition and a set of transitions (each of which is defined
by a transition relation). By exploiting
ChangeSets
, this partitioning
of the transition relation significantly increases the efficiency of the
model checking procedures.
The Parser
provides a method
parseTransitionsystem
for compiling a textual representation into a transition system.
Parser
Field Summary | |
---|---|
private ChangeSet[] |
changeSets
An array of ChangeSets representing those variables that may change in the corresponding transition. |
private Context |
context
The context associated with this transition system. |
private ROBDD |
init
The ROBDD representing the initial condition. |
private ROBDD |
reachable
The reachable states of this transition system. |
private ROBDD[] |
transitions
An array of ROBDDs representing the transitions. |
Constructor Summary | |
---|---|
Transitionsystem(Context context)
Constructs an empty transition structure. |
|
Transitionsystem(Context context,
ROBDD init,
ROBDD[] transitions,
ChangeSet[] changeSets)
Constructs a transition structure from the provided ROBDDs for the initial condition and an array of transition relation (along with the set of variables that may be change by a transition). |
Method Summary | |
---|---|
void |
clearHashTables()
Clears all hash tables associated with this model. |
ROBDD |
computeReachable()
Returns the reachable states of the transition system. |
ROBDD |
ex(ROBDD f)
Implements the operation EX. |
Context |
getContext()
Returns the context associated with this Kripke structure. |
boolean |
isValid(ROBDD f)
Checks whether all initial states are contained in the set f. |
static void |
main(java.lang.String[] args)
The main method that is invoked when the model checker is started for a fair transition systems. |
Methods inherited from class de.upb.swt.mcie.mc.Model |
---|
abort, eg, er, eu |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
private Context context
private ROBDD init
private ROBDD[] transitions
private ChangeSet[] changeSets
private ROBDD reachable
Constructor Detail |
---|
public Transitionsystem(Context context)
public Transitionsystem(Context context, ROBDD init, ROBDD[] transitions, ChangeSet[] changeSets)
init
- the initial conditiontransitions
- an array of the transitionschangeSets
- an array representingMethod Detail |
---|
public Context getContext()
getContext
in class Model
public ROBDD ex(ROBDD f)
ex
in class Model
f
- the argument for the operation represented as ROBDD
public boolean isValid(ROBDD f)
isValid
in class Model
f
- a set represented as an ROBDD
public ROBDD computeReachable()
computeReachable
in class Model
public void clearHashTables()
clearHashTables
in class Model
public static void main(java.lang.String[] args)
( < state formula > , { < transition formula > , ... , < transition formula > } , { < state formula > , ... , < state formula > } )
The first state formula represents the initial state, the transition formulas in braces represent the transitions of the system, and the state formulas in braces represent the set of fairness conditions.
The second name refers to a file with a comma separated list of temporal formulas that are to be checked on the system.
For each formula, it will be printed to the screen, whether it is valid in the system or not. Currently, there is no interaction between the user and the model checker.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |