de.upb.swt.mcie.mc
Class FairModel

java.lang.Object
  extended by de.upb.swt.mcie.mc.Model
      extended by de.upb.swt.mcie.mc.FairModel

public class FairModel
extends Model

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.

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

model

private Model model
The underlying model (without fairness).


fairness

private ROBDD[] fairness
An array of ROBDDs representing the fairness conditions.


fair

private ROBDD fair
The set of all states in which a fair path starts.

Constructor Detail

FairModel

public FairModel(Context context)
Constructs an empty fair Model. All states are initial states, the transition relation is empty, and the set of all states is also the (only) fairness condition.


FairModel

public FairModel(Model model,
                 ROBDD[] fairness)
Constructs a fair model from some model and from a set of fairness conditions.

Parameters:
model - the underlying model
fairness - an array of fairness conditions
Method Detail

getContext

public Context getContext()
Returns the context associated with this fair model structure.

Specified by:
getContext in class Model
Returns:
the context

eg

public ROBDD eg(ROBDD f)
Implements the operation EG considering the fairness conditions.

Overrides:
eg in class Model
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)
Implements the operation ER considering the fairness conditions.

Overrides:
er in class Model
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 f1 ER f1 is valid represented as an ROBDD

eu

public ROBDD eu(ROBDD f1,
                ROBDD f2)
Implements the operation EU considering the fairness conditions.

Overrides:
eu in class Model
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 f1 EU f1 is valid represented as an ROBDD

ex

public ROBDD ex(ROBDD f)
Implements the operation EX considering the fairness conditions.

Specified by:
ex in class Model
Parameters:
f - the argument for the operation represented as ROBDD
Returns:
the states in which EX f is valid represented as an ROBDD

reachable

public ROBDD reachable()
Computes the reachable states of the fair model.

Returns:
the reachable states of the Kripke structure represented as an ROBDD

isValid

public boolean isValid(ROBDD f)
Checks whether all initial states are contained in the set f. This formalizes the validity of a formula in a system.

Overrides:
isValid in class Model
Parameters:
f - a set represented as an ROBDD
Returns:
true, if the initial states are a subset of f

computeReachable

public ROBDD computeReachable()
Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state. Sometimes this reduction helps to significantly improve the performance of the model checking algorithms. On the other hand, calculating the reachable states may be quite inefficient. Whether this method should or should not be applied prior to the invocation of the model checking procedures strongly depends on the application. Typically, this will be decided by the user.

Overrides:
computeReachable in class Model
Returns:
the set of reachable states of the model

abort

public void abort()
Description copied from class: Model
Initiates abortion of the model checking operation on this model

Overrides:
abort in class Model