Generating The Invariant

Using the invariantCondition specified in the input text file and program variables, the input translator creates the following Java class.

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
public class Invariant \{ 
 
public Invariant()   \{  \} 
 
public boolean satisfies( State s ) \{ 

	 int bi; 
	 int bj; 
	 int bk; 
	 int bg; 
	 int dg; 
	 int di; 
	 int dj; 
	 int dk; 
	 int fi; 
	 int fj; 
	 int fk; 
 
 
	 bi = s.getValue(0); 
	 bj = s.getValue(1); 
	 bk = s.getValue(2); 
	 bg = s.getValue(3); 
	 dg = s.getValue(4); 
	 di = s.getValue(5); 
	 dj = s.getValue(6); 
	 dk = s.getValue(7); 
	 fi = s.getValue(8); 
	 fj = s.getValue(9); 
	 fk = s.getValue(10); 

 if ( {\em invariantCondition} )  
 	 	 return true; 
 
 return false; 
  \} 
 \}

The constructor of this Invariant class is empty. The input translator, declares all program variables in the satisfies method. Then, using the value of the variables in the parameter state of the satisfies method, the membership of the given state to the invariant is determined. As an example, we have shown in the above Java code the structure of the Invariant class that is generated for the Byzantine agreement program introduced in Section 3.2. The invariantCondition specified in the if statement is exactly the same condition specified in the input file in the invariant section.