Generating The Program State

In principle, we identify each program state by a specific valuation to the program variables. In practice, we generate a Java file that specifies a class State. The State class includes all the program variables as its state variables. Moreover, the State class has extra state variables to store more information about a state. For example, we have a Boolean variable invariant in the State class that shows if an instance of the State class is an invariant state. We present a partial structure of the State class as follows.

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
public class State \{ 
 
 int stateno;
	 int vars[]; 
	 int no_vars; 
	 State next; 
	 LinkedList out_ptransitions; 
	 LinkedList in_ptransitions; 
	 LinkedList out_ftransitions; 
	 LinkedList in_ftransitions; 
	 boolean invariant; 
	 boolean ms; 

public int getValue (int i)  \{
	 if( (i < no_vars) && (i >= 0) )  \{
	 	 return vars[i];   \}
	 else  \{
	 	 System.out.println("Erroneous variable no" );  \} 
	 return Parameters.INVALID_VALUE; 
   \} 
 
 
public void setValue (int i, int v) \{ 
	 if( (i < no_vars) && (i >= 0) )  \{ 
	 	 vars[i] = v;    \} 
	 else   \{ 
	 	 System.out.println("Erroneous variable no" ); \} 
 \} 

public void markInvariant() \{ 
	 invariant = true; 
  \} 
 
public boolean isInvariant() \{
	 return invariant;
   \}     
 
public boolean is_ms() \{ 
	 return ms;
   \} 
 
public void set_ms()  \{
	 ms = true;
   \} 

public LinkedList getInFaultTransitions() \{
	 return in_ftransitions;
  \} 
 
public LinkedList getOutFaultTransitions() \{
	 return out_ftransitions;
 \} 
 
public LinkedList getInProgramTransitions() \{
	 return in_ptransitions; 
  \} 
 
public LinkedList getOutProgramTransitions() \{ 
	 return out_ptransitions;
  \}

As we can observe in the State class, we have a set of methods for manipulating the state variables of the State class. Also, we have a set of methods for extracting information about an instance of the State class (e.g., isInvariant() method). Each instance of the State class has four sets of transitions: input program transitions, input fault transitions, output program transitions, and output fault transitions. Observe that there exist some methods for the manipulation of these transitions.