de.upb.swt.mcie.mc
Class Transitionsystem

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

public class Transitionsystem
extends Model

Implements a transition system. A transition system consists of an initial condition and a set of transitions (each of which is defined by a transition relation). By exploiting ChangeSets, this partitioning of the transition relation significantly increases the efficiency of the model checking procedures.

The Parser provides a method parseTransitionsystem for compiling a textual representation into a transition system.

Author:
Ekkart Kindler, kindler@upb.de
See Also:
Parser

Field Summary
private  ChangeSet[] changeSets
          An array of ChangeSets representing those variables that may change in the corresponding transition.
private  Context context
          The context associated with this transition system.
private  ROBDD init
          The ROBDD representing the initial condition.
private  ROBDD reachable
          The reachable states of this transition system.
private  ROBDD[] transitions
          An array of ROBDDs representing the transitions.
 
Constructor Summary
Transitionsystem(Context context)
          Constructs an empty transition structure.
Transitionsystem(Context context, ROBDD init, ROBDD[] transitions, ChangeSet[] changeSets)
          Constructs a transition structure from the provided ROBDDs for the initial condition and an array of transition relation (along with the set of variables that may be change by a transition).
 
Method Summary
 void clearHashTables()
          Clears all hash tables associated with this model.
 ROBDD computeReachable()
          Returns the reachable states of the transition system.
 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 a fair transition systems.
 
Methods inherited from class de.upb.swt.mcie.mc.Model
abort, eg, er, eu
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Field Detail

context

private Context context
The context associated with this transition system.


init

private ROBDD init
The ROBDD representing the initial condition.


transitions

private ROBDD[] transitions
An array of ROBDDs representing the transitions.


changeSets

private ChangeSet[] changeSets
An array of ChangeSets representing those variables that may change in the corresponding transition.


reachable

private ROBDD reachable
The reachable states of this transition system.

Constructor Detail

Transitionsystem

public Transitionsystem(Context context)
Constructs an empty transition structure. All states are initial states and there is a single empty transition.


Transitionsystem

public Transitionsystem(Context context,
                        ROBDD init,
                        ROBDD[] transitions,
                        ChangeSet[] changeSets)
Constructs a transition structure from the provided ROBDDs for the initial condition and an array of transition relation (along with the set of variables that may be change by a transition).

Parameters:
init - the initial condition
transitions - an array of the transitions
changeSets - an array representing
Method Detail

getContext

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

Specified by:
getContext in class Model
Returns:
the context

ex

public ROBDD ex(ROBDD f)
Implements the operation EX.

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

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()
Returns the reachable states of the transition system. The computed reachable states can also be used for the model checking operations.

Overrides:
computeReachable in class Model
Returns:
the reachable states of the transition system

clearHashTables

public void clearHashTables()
Clears all hash tables associated with this model. In particular, it clears the hash tables of the context of this transition system and all changesets of the transitions.

Overrides:
clearHashTables in class Model

main

public static void main(java.lang.String[] args)
The main method that is invoked when the model checker is started for a fair transition systems. Upon start, the model checker expects two string arguments, which are two file names. The first name refers to the file with a fair transition system, which must have the following form:

( < state formula > , { < transition formula > , ... , < transition formula > } , { < state formula > , ... , < state formula > } )

The first state formula represents the initial state, the transition formulas in braces represent the transitions of the system, and the state formulas in braces represent the set of fairness conditions.

The second name refers to a file with a comma separated list of temporal 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.