|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectde.upb.swt.mcie.mc.Model
public abstract class Model
Abstract class for a model on which model checking should be performed.
When converting a temporal Formula
to
an ROBDD, it refers to the procedures of this class.
Formula
Field Summary | |
---|---|
private boolean |
abort
Indicates that the current model checking operation on this model should be aborted; |
Constructor Summary | |
---|---|
Model()
|
Method Summary | |
---|---|
void |
abort()
Initiates abortion of the model checking operation on this model |
void |
clearHashTables()
If the model maintains hash tables, calling this method will clear all hash tables (if possible). |
ROBDD |
computeReachable()
Sometimes model checking procedures are more efficient, when the reachable states of the model are calculated first and used in the model checking procedures. |
ROBDD |
eg(ROBDD f)
Standard implementation of the operation EG f. |
ROBDD |
er(ROBDD f1,
ROBDD f2)
Standard implementation of the operation E[ f1 R f2 ]. |
ROBDD |
eu(ROBDD f1,
ROBDD f2)
Standard implementation of the operation E[ f1 U f2 ]. |
abstract ROBDD |
ex(ROBDD f)
Must implement the EX operator for this particular model. |
abstract Context |
getContext()
Must implement an operation that returns the Context associated with this
model. |
boolean |
isValid(ROBDD f)
Checks whether f is valid in the system. |
Methods inherited from class java.lang.Object |
---|
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
---|
private boolean abort
Constructor Detail |
---|
public Model()
Method Detail |
---|
public abstract Context getContext()
Context
associated with this
model.
public abstract ROBDD ex(ROBDD f)
f
- a set of states represented as an ROBDD
public ROBDD eu(ROBDD f1, ROBDD f2)
f1
- the first argument for the operation represented as ROBDDf2
- the second argument for the operation represented as ROBDD
public ROBDD eg(ROBDD f)
f
- the argument for the operation represented as ROBDD
public ROBDD er(ROBDD f1, ROBDD f2)
f1
- the first argument for the operation represented as an ROBDDf2
- the second argument for the operation represented as an ROBDD
public void clearHashTables()
public ROBDD computeReachable()
IncorrectUseException
is thrown.
public boolean isValid(ROBDD f)
IncorrectUseException
is thrown.
f
- a set represented as an ROBDD
public void abort()
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |