Generating The Initial States

In this subsection, we describe the automatic generation of the InitialStates class from input file. In this class, the input translator generates Java code for the creation of a linked list of initial states. The input translator uses the values of the variables from the input file in order to generate code for the instantiation of initial states.

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
public class InitialStates \{

	  public InitialStates() \{ \} 

	 static LinkedList getInputStates()  \{ 
	 	 State s0 = new State();
	 	 	s0.setValue(0,0);
	 	 	s0.setValue(1,0);
	 	 	s0.setValue(2,0);
	 	 	s0.setValue(3,0);
	 	 	s0.setValue(4,0);
	 	 	s0.setValue(5,-1);
	 	 	s0.setValue(6,-1);
	 	 	s0.setValue(7,-1);
	 	 	s0.setValue(8,0);
	 	 	s0.setValue(9,0);
	 	 	s0.setValue(10,0);

	 	 State s1 = new State();
	 	 	s1.setValue(0,0);
	 	 	s1.setValue(1,0);
	 	 	s1.setValue(2,0);
	 	 	s1.setValue(3,0);
	 	 	s1.setValue(4,1);
	 	 	s1.setValue(5,-1);
	 	 	s1.setValue(6,-1);
	 	 	s1.setValue(7,-1);
	 	 	s1.setValue(8,0);
	 	 	s1.setValue(9,0);
	 	 	s1.setValue(10,0);

LinkedList inputstates = new LinkedList();
	 	 	 inputstates.add(s1);
	 	 	 inputstates.add(s0);
	 	 	 return inputstates;
      \} 
 \}

Observe that the getInputStates returns a linked list of states that are used for the expansion of the reachability graph.