varification
Class BaseCaseNextStateGenerator

public class BaseCaseNextStateGenerator
implements NextStateGenerator

Title: Automatic Varfication of two process system

Description: This program will do an automatic varification of the mutual exclusion algorithim as described by the dog problem

Copyright: Copyright (c) 2003

Version:
1.0
Author:
Jonathan Harris
Field Detail

PROCESS_0_MOVED

public static final byte PROCESS_0_MOVED
teat

Constructor Detail

BaseCaseNextStateGenerator

public BaseCaseNextStateGenerator()
this is the default constructor for the base case. The wnats and the turns change at lines 1 and 2 (respectively) for both processes

BaseCaseNextStateGenerator

public BaseCaseNextStateGenerator(byte[] changeWantToTrueAt,
                                  byte[] giveTurnAwayAt,
                                  byte critSecLine)
Now this is a tad tricky because the changeWantToTrueAt array and giveTurnAwayAt array mean slightly different things. for a given process i, if changeWantToTrueAt[i] > lineNumber[i] (i.e. the current line number that i is on) then i wants into the critical section. On the other hand, if a given process is making the transition from giveTurnAwayAt[i] to giveTurnAwayAt[i] + 1, then it changes the turn number to abs(1 - i) (in other words, with 2 processes, and with i = 0, and the turn number currently equal to 1, the turn number would not change, however, if the turn number is equal to 0, then the turn number would be changed to 1. Note that what is going on is that a process is being polite and giving up its turn.
Parameters:
changeWantToTrueAt - the line for a given process i at wich its want changes from false to true (note that this is the transition line, i.e., it changes after said line)
giveTurnAwayAt - this is the line after which a process gives up its turn
critSecLine - this is the line that reperesents the critical section. If 2 states are in this line then the state is a bad state after the critSecLine, the next line number is 0, and turn is set to i and the process i nolonger wants

Method Detail

getNextStates

public ArrayList getNextStates(VertexInfo vi)
currently this is a hardcoded stupid algorithim. Later I would like to do this by passing some sort of input in. The caller is responsible for note that this currently only works for a 2 process system
Parameters:
vi - the soruce VertexInfo object
Returns:
an ArrayList containing new vertex info objects representing the new possible states. The caller should add these to the graph.
Throws:
IllegalStateException - if one of the states generated was illigal

whichStateMoved

public byte whichStateMoved(VertexInfo source,
                            VertexInfo dest,
                            Graph g)
Given 2 states amd a graph this method will tell you which process, if any, actually advances
Parameters:
source - the source state
dest - the destination state
Returns:
0 if process 0 changed, 1 if process 1 changed 2 if both changed -1 if niether changed -2 indicates an error condition...something is really wrong

getStateToAdd

private VertexInfo getStateToAdd(VertexInfo vi,
                                 byte[] lineNumArr,
                                 byte processNum)
this function will return a state to add by increasing the line number and setting the turn as is appropriate
Parameters:
vi - the source VertexInfo object
lineNumArr - the array of line numbers indexed by process
processNum - the process number who's line number will be increased
Returns:
the new state created by increasing a particular line number and setting turn variable correctly

chooseTurn

private byte chooseTurn(VertexInfo viSource,
                        byte processNum,
                        byte newLineNumber)
given a Vertex info object, a process number, and the new line that we will be moving too, this function returns the new turn number (if it changes) note that this is currently for a 2 process system only
Parameters:
viSource - this is the source VertexInfo (from which we are trying to generate new states)
processNum - this is the process number who is changing (or not changing) lines
newLineNumber - this will be the new line number
Returns:
the turn number for the newly generated state

stateOK

public boolean stateOK(VertexInfo vi)
this method will check to see if more then one state is in the critical asection at a time if this is the case the state is not OK
Parameters:
vi - the state to check
Returns:
true if the state is OK, else false

stateOKExceptionThrower

private VertexInfo stateOKExceptionThrower(VertexInfo vi)
This is a simple method that will throw an exception if the state is not OK Otherwise it just returns the vi that was passed in
Parameters:
vi - a VertexInfo Object to check
Returns:
the same VertexInfo that was passed in
Throws:
IllegalStateException - if the state was not OK

getStatesAtLine

private int getStatesAtLine(VertexInfo vi,
                            byte lineNumber)
this method will check how many states are at a given line number
Parameters:
vi - the vertex info object to check
lineNumber - the line number you want to know about
Returns:
the number of states at that line number

processWants

public boolean processWants(VertexInfo vi,
                            int processNumber)
this will test if a given process wants into the critical section
Parameters:
vi - the vertex info
processNumber - the process number
Returns:
true if the process wants in (ie its flag is up)