|
||||||||||
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.Kripkestructure
public class Kripkestructure
Implements a Kripke structure. The Kripke structure consists of an initial condition and a transition relation.
The Parser
provides a method
parseKripkestructure
for compiling a textual representation into a Model.
Parser
Field Summary | |
---|---|
private Context |
context
The context associated with this Kripkestructure. |
private ROBDD |
init
The ROBDD representing the initial condition. |
private ROBDD |
reachable
If calculated already, this represents the reachable states of the Kripke structure. |
private ROBDD |
relation
The ROBDD representing the transition relation. |
Constructor Summary | |
---|---|
Kripkestructure(Context context)
Constructs an empty Kripke structure. |
|
Kripkestructure(Context context,
ROBDD init,
ROBDD relation)
Constructs a Kripke structure from the provided ROBDDs for the initial condition and the transition relation. |
Method Summary | |
---|---|
ROBDD |
computeReachable()
Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state. |
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 fair Kripke structures. |
private ROBDD |
reachable()
Computes the reachable states of the Kripke structure. |
Methods inherited from class de.upb.swt.mcie.mc.Model |
---|
abort, clearHashTables, 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 relation
private ROBDD reachable
Constructor Detail |
---|
public Kripkestructure(Context context)
public Kripkestructure(Context context, ROBDD init, ROBDD relation)
init
- the initial conditionrelation
- the transition relationMethod 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
private ROBDD reachable()
public boolean isValid(ROBDD f)
isValid
in class Model
f
- a set represented as an ROBDD
public ROBDD computeReachable()
computeReachable
in class Model
public static void main(java.lang.String[] args)
( < state formula > , < transition formula > , { < state formula > , ... , < state formula > } )
The first state formula represents the initial state, the transition formula represents the transition relation, the state formulas in braces represent the set of fairness conditions.
The second name refers to a file with a comma separated list of 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 |