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
PROCESS_0_MOVED
public static final byte PROCESS_0_MOVED
- teat
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
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)