Interface Graph_Implementor

All Known Implementing Classes:
GraphImplementation

public abstract interface Graph_Implementor

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 analyzeImp()
           
 void closeDebugFile()
           
 void expandImp(Program p, Fault f)
           
 int getNumStates()
           
 State getState(State s)
           
 void identify_msImp(SafetySpecification spec)
           
 void markInvariantStatesImp(Invariant inv)
           
 java.util.Vector printImp(java.lang.String processIndex, java.lang.String actionName)
           
 void printInvariant()
           
 void removeViolatingProgramTransitionsImp(SafetySpecification spec)
           
 void solveDeadlocksImp(Program pnew, Program pold, SafetySpecification spec, Invariant inv)
           
 

Method Detail

expandImp

public void expandImp(Program p,
                      Fault f)

identify_msImp

public void identify_msImp(SafetySpecification spec)

removeViolatingProgramTransitionsImp

public void removeViolatingProgramTransitionsImp(SafetySpecification spec)

markInvariantStatesImp

public void markInvariantStatesImp(Invariant inv)

solveDeadlocksImp

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

printImp

public java.util.Vector printImp(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()

analyzeImp

public void analyzeImp()