A B C D E F G H I M O P Q R S T V W

A

AbstractAction - class AbstractAction.

This class models the reachability graph of a program.

AbstractAction() - Constructor for class AbstractAction

AbstractFault - class AbstractFault.

This class models the reachability graph of a program.

AbstractFault() - Constructor for class AbstractFault

AbstractGuard - class AbstractGuard.

This class models the reachability graph of a program.

AbstractGuard() - Constructor for class AbstractGuard

AbstractInvariant - class AbstractInvariant.

This class models the reachability graph of a program.

AbstractInvariant() - Constructor for class AbstractInvariant

AbstractProcess - class AbstractProcess.

AbstractProcess() - Constructor for class AbstractProcess

AbstractProgram - class AbstractProgram.

AbstractReachabilityGraph - class AbstractReachabilityGraph.

This class models the reachability graph of a program.

AbstractSafetySpecification - class AbstractSafetySpecification.

This class models the reachability graph of a program.

AbstractSafetySpecification() - Constructor for class AbstractSafetySpecification

AbstractState - class AbstractState.

This class models the reachability graph of a program.

AbstractState() - Constructor for class AbstractState

AbstractStatement - class AbstractStatement.

This class models the reachability graph of a program.

AbstractStatement() - Constructor for class AbstractStatement

AbstractTransition - class AbstractTransition.

This class models the reachability graph of a program.

AbstractTransition() - Constructor for class AbstractTransition

AbstractVariable - class AbstractVariable.

This class models the reachability graph of a program.

AbstractVariable() - Constructor for class AbstractVariable

addInFaultTransition(FaultTransition) - Method in class AbstractState

addInFaultTransition(FaultTransition) - Method in class State

addInProgramTransition(ProgramTransition) - Method in class AbstractState

addInProgramTransition(ProgramTransition) - Method in class State

addOutFaultTransition(FaultTransition) - Method in class AbstractState

addOutFaultTransition(FaultTransition) - Method in class State

addOutProgramTransition(ProgramTransition) - Method in class AbstractState

addOutProgramTransition(ProgramTransition) - Method in class State

analyze() - Method in class AbstractReachabilityGraph

analyzeImp() - Method in class GraphImplementation

analyzeImp() - Method in interface Graph_Implementor

B

breakCycle(Hashtable) - Method in class GraphImplementation

C

close() - Method in class OutputFile

closeDebugFile() - Method in class AbstractReachabilityGraph

closeDebugFile() - Method in class GraphImplementation

closeDebugFile() - Method in interface Graph_Implementor

combine(Minterm, Minterm, int) - Method in class QuineMac

CommandHandler - class CommandHandler.

CommandHandler(Program, Program, Fault, LinkedList, SafetySpecification, Invariant) - Constructor for class CommandHandler

compare(Minterm, Minterm) - Method in class QuineMac

CompareResult - class CompareResult.

This class models the reachability graph of a program.

CompareResult(boolean, int) - Constructor for class CompareResult

Creates new CompareResult

Component - class Component.

Component(Object, Method[], int, Node, Vector) - Constructor for class Component

computeList(MintermList, boolean) - Method in class QuineMac

ComputePredicate() - Method in class PredicateMaker

containsInvariantImp(Hashtable) - Method in class GraphImplementation

D

DeadlockResolver - class DeadlockResolver.

This class models the reachability graph of a program.

DeadlockResolver() - Constructor for class DeadlockResolver

DeadlockResolver1 - class DeadlockResolver1.

This class models the reachability graph of a program.

DeadlockResolver1(GraphImplementation, Program, Program, SafetySpecification, Invariant) - Constructor for class DeadlockResolver1

Creates new DeadlockResolver1

DeadlockResolver2 - class DeadlockResolver2.

DeadlockResolver2(GraphImplementation, Program, Program, SafetySpecification, Invariant) - Constructor for class DeadlockResolver2

Creates new DeadlockResolver1

detectCycle(State, Hashtable) - Method in class GraphImplementation

detectNonProgressCycle(State, Hashtable) - Method in class GraphImplementation

dfs_detectCycle(State, Hashtable) - Method in class GraphImplementation

E

emptyHashTable(Hashtable) - Method in class GraphImplementation

equals(State) - Method in class AbstractState

equals(State) - Method in class State

error(String) - Method in class CommandHandler

evaluate(Stack, State, Hashtable) - Method in class AbstractStatement

exec() - Method in class QuineMac

expand(Program, Fault) - Method in class AbstractReachabilityGraph

expandImp(Program, Fault) - Method in class GraphImplementation

expandImp(Program, Fault) - Method in interface Graph_Implementor

explore(Stack, State, Hashtable) - Method in class AbstractProcess

explore(Stack, State, Hashtable) - Method in class Component

exploreImp(State, Hashtable) - Method in class ProgramImplementation

exploreImp(State, Hashtable) - Method in interface Program_Implementor

F

factoryMethod(int) - Method in class ProgramImplementation_Concrete_Creator

factoryMethod(int) - Method in class ProgramImplementation_Creator

factoryMethod(int) - Method in class Program_Concrete_Creator

factoryMethod(int) - Method in class Program_Creator

factoryMethod(int, LinkedList) - Method in class ReachabilityGraph_Concrete_Creator

factoryMethod(int, LinkedList) - Method in class ReachabilityGraph_Creator

Fault - class Fault.

Fault() - Constructor for class Fault

FaultTransition - class FaultTransition.

This class models the reachability graph of a program.

G

getDestination() - Method in class AbstractTransition

getDestination() - Method in class Transition

getDomain(int) - Static method in class State

getDomSize() - Method in class Minterm

getEquivalentStates(Vector) - Method in class State

getGeneratingProgramStatement() - Method in class ProgramTransition

getInFaultTransitions() - Method in class State

getInProgramTransitions() - Method in class State

getMatch() - Method in class Minterm

getMatchList() - Method in class QuineMac

getNum() - Method in class AbstractVariable

getNumStates() - Method in class AbstractReachabilityGraph

getNumStates() - Method in class GraphImplementation

getNumStates() - Method in interface Graph_Implementor

getOutFaultTransitions() - Method in class State

getOutProgramTransitions() - Method in class State

getPosition() - Method in class CompareResult

getResult() - Method in class CompareResult

getSize() - Method in class Minterm

getSource() - Method in class AbstractTransition

getSource() - Method in class Transition

getState(State) - Method in class AbstractReachabilityGraph

getState(State) - Method in class GraphImplementation

getState(State) - Method in interface Graph_Implementor

getStateno() - Method in class AbstractState

getStateno() - Method in class State

getStates() - Method in class GraphImplementation

getValue(int) - Method in class AbstractState

getValue(int) - Method in class State

getVar_no() - Method in class AbstractVariable

Graph_Implementor - interface Graph_Implementor.

This class models the reachability graph of a program.

GraphImplementation - class GraphImplementation.

This class models the reachability graph of a program.

GraphImplementation(LinkedList) - Constructor for class GraphImplementation

GraphImplementation1 - class GraphImplementation1.

This class models the reachability graph of a program.

GraphImplementation1(LinkedList) - Constructor for class GraphImplementation1

GraphImplementation2 - class GraphImplementation2.

GraphImplementation2(LinkedList) - Constructor for class GraphImplementation2

H

hasCycles() - Method in class DeadlockResolver2

hasOutProgramTransition(ProgramTransition) - Method in class AbstractState

hasOutProgramTransition(ProgramTransition) - Method in class State

I

identify_ms(SafetySpecification) - Method in class AbstractReachabilityGraph

identify_msImp(SafetySpecification) - Method in class GraphImplementation

identify_msImp(SafetySpecification) - Method in interface Graph_Implementor

InitialStates - class InitialStates.

InitialStates() - Constructor for class InitialStates

Invariant - class Invariant.

Invariant() - Constructor for class Invariant

is_ms() - Method in class AbstractState

is_ms() - Method in class State

isDeadlocked() - Method in class AbstractState

isDeadlocked() - Method in class State

isDeadlocked(State) - Method in class AbstractProcess

isDeadlocked(State) - Method in class AbstractProgram

isDeadlocked(State) - Method in class Component

isDeadlockedImp(State) - Method in class ProgramImplementation

isDeadlockedImp(State) - Method in interface Program_Implementor

isInvariant() - Method in class AbstractState

isInvariant() - Method in class State

M

main(String[]) - Static method in class Tool

markInvariant() - Method in class AbstractState

markInvariant() - Method in class State

markInvariantStates(Invariant) - Method in class AbstractReachabilityGraph

markInvariantStatesImp(Invariant) - Method in class GraphImplementation

markInvariantStatesImp(Invariant) - Method in interface Graph_Implementor

minListSize() - Method in class MintermList

Minterm - class Minterm.

This class models the reachability graph of a program.

Minterm(String[], int, int[]) - Constructor for class Minterm

Creates new Minterm

MintermList - class MintermList.

This class models the reachability graph of a program.

MintermList(int) - Constructor for class MintermList

Creates new MintermList

MinToString(Minterm) - Method in class QuineMac

mList - Variable in class MintermList

O

OutputFile - class OutputFile.

OutputFile(String) - Constructor for class OutputFile

Creates new OutputFile

OutputGenerator - class OutputGenerator.

OutputGenerator() - Constructor for class OutputGenerator

P

Parameters - class Parameters.

Parameters() - Constructor for class Parameters

PredicateMaker - class PredicateMaker.

This class models the reachability graph of a program.

PredicateMaker(MintermList, int) - Constructor for class PredicateMaker

Creates new PredicateMaker

PrimeImplicants - class PrimeImplicants.

This class models the reachability graph of a program.

PrimeImplicants() - Constructor for class PrimeImplicants

Creates new PrimeImplicants

print() - Method in class AbstractFault

print() - Method in class AbstractGuard

print() - Method in class AbstractInvariant

print() - Method in class AbstractProcess

print() - Method in class AbstractProgram

print() - Method in class AbstractSafetySpecification

print() - Method in class AbstractTransition

print() - Method in class Component

print() - Method in class Fault

print() - Method in class FaultTransition

print() - Method in class Minterm

print() - Method in class MintermList

print() - Method in class ProgramTransition

print() - Method in class SafetySpecification

print() - Method in class Transition

print(String) - Method in class AbstractTransition

print(String) - Method in class FaultTransition

print(String) - Method in class ProgramTransition

print(String) - Method in class Transition

print(String, String) - Method in class AbstractReachabilityGraph

print(String, String, String[], Vector) - Method in class AbstractTransition

print(String, String, String[], Vector) - Method in class FaultTransition

print(String, String, String[], Vector) - Method in class ProgramTransition

print(String, String, String[], Vector) - Method in class Transition

print(String, String, Vector) - Method in class AbstractState

print(String, String, Vector) - Method in class State

printHashTable(Hashtable, String) - Method in class GraphImplementation

printImp() - Method in class ProgramImplementation

printImp() - Method in interface Program_Implementor

printImp(String, String) - Method in class GraphImplementation

printImp(String, String) - Method in interface Graph_Implementor

printInvariant() - Method in class AbstractReachabilityGraph

printInvariant() - Method in class GraphImplementation

printInvariant() - Method in interface Graph_Implementor

printProcess(String) - Method in class AbstractState

printProcess(String) - Method in class State

printProgram(AbstractReachabilityGraph, OutputFile) - Static method in class OutputGenerator

printViolatingTransitions(SafetySpecification) - Method in class GraphImplementation

This is a test method for debugging.

ProblemSpecific - class ProblemSpecific.

ProblemSpecific() - Constructor for class ProblemSpecific

producesTransition(Transition) - Method in class AbstractProcess

producesTransition(Transition) - Method in class AbstractProgram

producesTransition(Transition) - Method in class Component

producesTransitionImp(Transition) - Method in class ProgramImplementation

producesTransitionImp(Transition) - Method in interface Program_Implementor

Program - class Program.

This class models the reachability graph of a program.

Program_Concrete_Creator - class Program_Concrete_Creator.

This class models the reachability graph of a program.

Program_Concrete_Creator() - Constructor for class Program_Concrete_Creator

Creates new Program_Concrete_Creator

Program_Creator - class Program_Creator.

This class models the reachability graph of a program.

Program_Creator() - Constructor for class Program_Creator

Creates new Program_Creator

Program_Implementor - interface Program_Implementor.

This class models the reachability graph of a program.

Program(ProgramImplementation1) - Constructor for class Program

Creates new Program1

Program(ProgramImplementation2) - Constructor for class Program

Creates new Program1

ProgramImplementation - class ProgramImplementation.

ProgramImplementation_Concrete_Creator - class ProgramImplementation_Concrete_Creator.

This class models the reachability graph of a program.

ProgramImplementation_Concrete_Creator() - Constructor for class ProgramImplementation_Concrete_Creator

Creates new ProgramImplementation_Concrete_Creator

ProgramImplementation_Creator - class ProgramImplementation_Creator.

This class models the reachability graph of a program.

ProgramImplementation_Creator() - Constructor for class ProgramImplementation_Creator

Creates new ProgramImplementation_Creator

ProgramImplementation() - Constructor for class ProgramImplementation

ProgramImplementation1 - class ProgramImplementation1.

ProgramImplementation1() - Constructor for class ProgramImplementation1

ProgramImplementation2 - class ProgramImplementation2.

ProgramImplementation2() - Constructor for class ProgramImplementation2

ProgramTransition - class ProgramTransition.

This class models the reachability graph of a program.

Q

QuineMac - class QuineMac.

This class models the reachability graph of a program.

R

ReachabilityGraph_Concrete_Creator - class ReachabilityGraph_Concrete_Creator.

This class models the reachability graph of a program.

ReachabilityGraph_Concrete_Creator() - Constructor for class ReachabilityGraph_Concrete_Creator

Creates new ReachabilityGraph_Concrete_Creator

ReachabilityGraph_Creator - class ReachabilityGraph_Creator.

This class models the reachability graph of a program.

ReachabilityGraph_Creator() - Constructor for class ReachabilityGraph_Creator

Creates new ReachabilityGraph_Creator

recomputeFaultSpanImp() - Method in class GraphImplementation

removeAnInvariantStateImp(State) - Method in class GraphImplementation

removeAStateImp(State) - Method in class GraphImplementation

removeFirstViolatingProgramTransitionImp(SafetySpecification) - Method in class GraphImplementation

removeInProgramTransition(ProgramTransition) - Method in class AbstractState

removeInProgramTransition(ProgramTransition) - Method in class State

removeOutProgramTransition(ProgramTransition) - Method in class AbstractState

removeOutProgramTransition(ProgramTransition) - Method in class State

removeViolatingProgramTransitions(SafetySpecification) - Method in class AbstractReachabilityGraph

removeViolatingProgramTransitionsImp(SafetySpecification) - Method in class GraphImplementation

removeViolatingProgramTransitionsImp(SafetySpecification) - Method in interface Graph_Implementor

resetInFaultTransitions() - Method in class AbstractState

resetInFaultTransitions() - Method in class State

resetInProgramTransitions() - Method in class AbstractState

resetInProgramTransitions() - Method in class State

Resolve() - Method in class DeadlockResolver

Resolve() - Method in class DeadlockResolver1

Resolve() - Method in class DeadlockResolver2

resolveCycles() - Method in class DeadlockResolver2

run() - Method in class CommandHandler

S

SafetySpecification - class SafetySpecification.

SafetySpecification() - Constructor for class SafetySpecification

satisfies(State) - Method in class AbstractInvariant

satisfies(State) - Method in class Invariant

scanAndSolve(Program, Program, SafetySpecification, Invariant) - Method in class DeadlockResolver

scanAndSolve(Program, Program, SafetySpecification, Invariant) - Method in class DeadlockResolver1

scanAndSolve(Program, Program, SafetySpecification, Invariant) - Method in class DeadlockResolver2

scanAndSolveDeadlocksImp(Program, Program, SafetySpecification, Invariant) - Method in class GraphImplementation

scanAndSolveDeadlocksImp(Program, Program, SafetySpecification, Invariant) - Method in class GraphImplementation2

set_ms() - Method in class AbstractState

set_ms() - Method in class State

setGeneratingProgramStatement(ProgramStatement) - Method in class ProgramTransition

setMatch(boolean) - Method in class Minterm

setStateno(int) - Method in class AbstractState

setStateno(int) - Method in class State

setValue(int, int) - Method in class AbstractState

setValue(int, int) - Method in class State

solveDeadlock(State, Invariant, Hashtable, SafetySpecification, Program) - Method in class AbstractProcess

solveDeadlock(State, Invariant, Hashtable, SafetySpecification, Program) - Method in class AbstractProgram

solveDeadlock(State, Invariant, Hashtable, SafetySpecification, Program) - Method in class Component

solveDeadlockImp(State, Invariant, Hashtable, SafetySpecification, Program) - Method in class ProgramImplementation

solveDeadlockImp(State, Invariant, Hashtable, SafetySpecification, Program) - Method in class ProgramImplementation2

solveDeadlockImp(State, Invariant, Hashtable, SafetySpecification, Program) - Method in interface Program_Implementor

solveDeadlockMore(State, Invariant, Hashtable, SafetySpecification, Program, Hashtable) - Method in class AbstractProgram

solveDeadlockMore(State, Invariant, Hashtable, SafetySpecification, Program, Hashtable) - Method in class Component

solveDeadlockMoreImp(State, Invariant, Hashtable, SafetySpecification, Program, Hashtable) - Method in class ProgramImplementation

solveDeadlockMoreImp(State, Invariant, Hashtable, SafetySpecification, Program, Hashtable) - Method in interface Program_Implementor

solveDeadlocks(Program, Program, SafetySpecification, Invariant) - Method in class AbstractReachabilityGraph

solveDeadlocksImp(Program, Program, SafetySpecification, Invariant) - Method in class GraphImplementation

solveDeadlocksImp(Program, Program, SafetySpecification, Invariant) - Method in class GraphImplementation2

solveDeadlocksImp(Program, Program, SafetySpecification, Invariant) - Method in interface Graph_Implementor

State - class State.

State() - Constructor for class State

State(State) - Constructor for class State

T

Tool - class Tool.

This class models the reachability graph of a program.

Tool() - Constructor for class Tool

toString() - Method in class AbstractState

toString() - Method in class Minterm

toString() - Method in class ProgramTransition

toString() - Method in class State

toString() - Method in class Transition

Transition - class Transition.

This class models the reachability graph of a program.

Transition() - Constructor for class Transition

V

violatesSafety(Transition) - Method in class AbstractSafetySpecification

violatesSafety(Transition) - Method in class SafetySpecification

W

writeLine(String) - Method in class OutputFile

A B C D E F G H I M O P Q R S T V W