Class AbstractReachabilityGraph

java.lang.Object
  |
  +--AbstractReachabilityGraph

public abstract class AbstractReachabilityGraph
extends java.lang.Object

This class models the reachability graph of a program. The reachability graph is a directed graph that contains all the states of the fault-span of a program. This class is the root of the abstract class hierarchy in the Bridge design pattern.

Since:
 

Method Summary
 void analyze()
           
 void closeDebugFile()
           
 void expand(Program p, Fault f)
           
 int getNumStates()
           
 State getState(State s)
           
 void identify_ms(SafetySpecification spec)
           
 void markInvariantStates(Invariant inv)
           
 java.util.Vector print(java.lang.String processIndex, java.lang.String actionName)
           
 void printInvariant()
           
 void removeViolatingProgramTransitions(SafetySpecification spec)
           
 void solveDeadlocks(Program pnew, Program pold, SafetySpecification spec, Invariant inv)
           
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Method Detail

expand

public void expand(Program p,
                   Fault f)

identify_ms

public void identify_ms(SafetySpecification spec)

removeViolatingProgramTransitions

public void removeViolatingProgramTransitions(SafetySpecification spec)

markInvariantStates

public void markInvariantStates(Invariant inv)

solveDeadlocks

public void solveDeadlocks(Program pnew,
                           Program pold,
                           SafetySpecification spec,
                           Invariant inv)

print

public java.util.Vector print(java.lang.String processIndex,
                              java.lang.String actionName)

getNumStates

public int getNumStates()

getState

public State getState(State s)

closeDebugFile

public void closeDebugFile()

printInvariant

public void printInvariant()

analyze

public void analyze()