|
||||||||||
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.FairModel
public class FairModel
Implements a fair model based on some other model. It basically adds a set of
fairness conditions, which must be valid infinitely often on each fair path. The
model checking methods are implemented in such a way that only fair paths are
taken into account. Note that this works with any correct implementation of
Model
.
The Parser
provides a method
parseFairKripkestructure
for compiling a textual representation into a fair
Kripke structure and a method
parseFairTransitionsystem
for compiling a fair transition system.
Parser
Field Summary | |
---|---|
private ROBDD |
fair
The set of all states in which a fair path starts. |
private ROBDD[] |
fairness
An array of ROBDDs representing the fairness conditions. |
private Model |
model
The underlying model (without fairness). |
Constructor Summary | |
---|---|
FairModel(Context context)
Constructs an empty fair Model. |
|
FairModel(Model model,
ROBDD[] fairness)
Constructs a fair model from some model and from a set of fairness conditions. |
Method Summary | |
---|---|
void |
abort()
Initiates abortion of the model checking operation on this model |
ROBDD |
computeReachable()
Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state. |
ROBDD |
eg(ROBDD f)
Implements the operation EG considering the fairness conditions. |
ROBDD |
er(ROBDD f1,
ROBDD f2)
Implements the operation ER considering the fairness conditions. |
ROBDD |
eu(ROBDD f1,
ROBDD f2)
Implements the operation EU considering the fairness conditions. |
ROBDD |
ex(ROBDD f)
Implements the operation EX considering the fairness conditions. |
Context |
getContext()
Returns the context associated with this fair model structure. |
boolean |
isValid(ROBDD f)
Checks whether all initial states are contained in the set f. |
ROBDD |
reachable()
Computes the reachable states of the fair model. |
Methods inherited from class de.upb.swt.mcie.mc.Model |
---|
clearHashTables |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
private Model model
private ROBDD[] fairness
private ROBDD fair
Constructor Detail |
---|
public FairModel(Context context)
public FairModel(Model model, ROBDD[] fairness)
model
- the underlying modelfairness
- an array of fairness conditionsMethod Detail |
---|
public Context getContext()
getContext
in class Model
public ROBDD eg(ROBDD f)
eg
in class Model
f
- the argument for the operation represented as ROBDD
public ROBDD er(ROBDD f1, ROBDD f2)
er
in class Model
f1
- the first argument for the operation represented as ROBDDf2
- the second argument for the operation represented as ROBDD
public ROBDD eu(ROBDD f1, ROBDD f2)
eu
in class Model
f1
- the first argument for the operation represented as ROBDDf2
- the second argument for the operation represented as ROBDD
public ROBDD ex(ROBDD f)
ex
in class Model
f
- the argument for the operation represented as ROBDD
public 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 void abort()
Model
abort
in class Model
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |