de.upb.swt.mcie.mc
Class Kripkestructure

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

public class Kripkestructure
extends Model

Implements a Kripke structure. The Kripke structure consists of an initial condition and a transition relation.

The Parser provides a method parseKripkestructure for compiling a textual representation into a Model.

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

Field Summary
private  Context context
          The context associated with this Kripkestructure.
private  ROBDD init
          The ROBDD representing the initial condition.
private  ROBDD reachable
          If calculated already, this represents the reachable states of the Kripke structure.
private  ROBDD relation
          The ROBDD representing the transition relation.
 
Constructor Summary
Kripkestructure(Context context)
          Constructs an empty Kripke structure.
Kripkestructure(Context context, ROBDD init, ROBDD relation)
          Constructs a Kripke structure from the provided ROBDDs for the initial condition and the transition relation.
 
Method Summary
 ROBDD computeReachable()
          Reduces the transition relation of the Kripke structure to the transitions that are reachable from the initial state.
 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 fair Kripke structures.
private  ROBDD reachable()
          Computes the reachable states of the Kripke structure.
 
Methods inherited from class de.upb.swt.mcie.mc.Model
abort, clearHashTables, 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 Kripkestructure.


init

private ROBDD init
The ROBDD representing the initial condition.


relation

private ROBDD relation
The ROBDD representing the transition relation.


reachable

private ROBDD reachable
If calculated already, this represents the reachable states of the Kripke structure.

Constructor Detail

Kripkestructure

public Kripkestructure(Context context)
Constructs an empty Kripke structure. All states are initial states, the transition relation is empty.


Kripkestructure

public Kripkestructure(Context context,
                       ROBDD init,
                       ROBDD relation)
Constructs a Kripke structure from the provided ROBDDs for the initial condition and the transition relation.

Parameters:
init - the initial condition
relation - the transition relation
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

reachable

private ROBDD reachable()
Computes the reachable states of the Kripke structure.

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

main

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

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

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

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