Interface Program_Implementor

All Known Implementing Classes:

ProgramImplementation

public abstract interface Program_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

java.util.Stack	exploreImp(State s, java.util.Hashtable states)
boolean	isDeadlockedImp(State s)
void	printImp()
boolean	producesTransitionImp(Transition t)
boolean	solveDeadlockImp(State s, Invariant inv, java.util.Hashtable states, SafetySpecification spec, Program fitp)
boolean	solveDeadlockMoreImp(State s, Invariant inv, java.util.Hashtable states, SafetySpecification spec, Program fitp, java.util.Hashtable recStates)

Method Detail

exploreImp

public java.util.Stack exploreImp(State s,
                                  java.util.Hashtable states)

solveDeadlockImp

public boolean solveDeadlockImp(State s,
                                Invariant inv,
                                java.util.Hashtable states,
                                SafetySpecification spec,
                                Program fitp)

solveDeadlockMoreImp

public boolean solveDeadlockMoreImp(State s,
                                    Invariant inv,
                                    java.util.Hashtable states,
                                    SafetySpecification spec,
                                    Program fitp,
                                    java.util.Hashtable recStates)

producesTransitionImp

public boolean producesTransitionImp(Transition t)

isDeadlockedImp

public boolean isDeadlockedImp(State s)

printImp

public void printImp()