de.upb.swt.mcie.mc
Class Model

java.lang.Object
  extended by de.upb.swt.mcie.mc.Model
Direct Known Subclasses:
FairModel, Kripkestructure, Transitionsystem

public abstract class Model
extends java.lang.Object

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.

Author:
Ekkart Kindler, kindler@upb.de
See Also:
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

abort

private boolean abort
Indicates that the current model checking operation on this model should be aborted;

Constructor Detail

Model

public Model()
Method Detail

getContext

public abstract Context getContext()
Must implement an operation that returns the Context associated with this model.

Returns:
the context

ex

public abstract ROBDD ex(ROBDD f)
Must implement the EX operator for this particular model.

Parameters:
f - a set of states represented as an ROBDD
Returns:
the set of predecessors of f in this model

eu

public ROBDD eu(ROBDD f1,
                ROBDD f2)
Standard implementation of the operation E[ f1 U f2 ]. The implementation is based on the method ex that must be implemented for each subclass.

Parameters:
f1 - the first argument for the operation represented as ROBDD
f2 - the second argument for the operation represented as ROBDD
Returns:
the states in which E[ f1 U f2 ] is valid represented as an ROBDD

eg

public ROBDD eg(ROBDD f)
Standard implementation of the operation EG f. The implementation is based on the method ex that must be implemented for each subclass.

Parameters:
f - the argument for the operation represented as ROBDD
Returns:
the states in which EG f is valid represented as an ROBDD

er

public ROBDD er(ROBDD f1,
                ROBDD f2)
Standard implementation of the operation E[ f1 R f2 ]. The implementation is based on the method ex that must be implemented for each subclass.

Parameters:
f1 - the first argument for the operation represented as an ROBDD
f2 - the second argument for the operation represented as an ROBDD
Returns:
the states in which E[ f1 R f2 ] is valid represented as an ROBDD

clearHashTables

public void clearHashTables()
If the model maintains hash tables, calling this method will clear all hash tables (if possible).


computeReachable

public 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. This mode can be invoked by this procedure (if implemented by the model). Note that this method might not be implemented for some models; in this case, an IncorrectUseException is thrown.

Returns:
the set of reachable states of the model

isValid

public boolean isValid(ROBDD f)
Checks whether f is valid in the system. Typically, the initial states must be a subset of f. Note that this method might not be implemented for some models; in this case, an IncorrectUseException is thrown.

Parameters:
f - a set represented as an ROBDD
Returns:
true, if f is valid for the system

abort

public void abort()
Initiates abortion of the model checking operation on this model