Generating The Safety Specification

The structure of the SafetySpecification class is very similar to the structure of the Invariant class. The only difference is that in the SafetySpecification class, we need to check the validity of a given transition instead of checking the membership of a given state to the invariant.

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
public class SafetySpecification \{ 
 
LinkedList predicate_list; 
 
public SafetySpecification()   \{  \} 
 
public boolean violatesSafety( Transition t ) \{  
	 State source = t.getSource(); 
	 State dest = t.getDestination(); 
	 int bis; 
	 int bjs; 
	 int bks; 
	 int bgs; 
	 int dgs; 
	 int dis; 
	 int djs; 
	 int dks; 
	 int fis; 
	 int fjs; 
	 int fks; 
 
 
	 int bid; 
	 int bjd; 
	 int bkd; 
	 int bgd; 
	 int dgd; 
	 int did; 
	 int djd; 
	 int dkd; 
	 int fid; 
	 int fjd; 
	 int fkd; 
 
 
	 bis = source.getValue(0); 
	 bjs = source.getValue(1); 
	 bks = source.getValue(2); 
	 bgs = source.getValue(3); 
	 dgs = source.getValue(4); 
	 dis = source.getValue(5); 
	 djs = source.getValue(6); 
	 dks = source.getValue(7); 
	 fis = source.getValue(8); 
	 fjs = source.getValue(9); 
	 fks = source.getValue(10); 
 
 
	 bid = dest.getValue(0); 
	 bjd = dest.getValue(1); 
	 bkd = dest.getValue(2); 
	 bgd = dest.getValue(3); 
	 dgd = dest.getValue(4); 
	 did = dest.getValue(5); 
	 djd = dest.getValue(6); 
	 dkd = dest.getValue(7); 
	 fid = dest.getValue(8); 
	 fjd = dest.getValue(9); 
	 fkd = dest.getValue(10); 
 
 
 if ( {\em destinationCondition} )  	 return true; 
 
 if ({\em relationCondition} )	 	 return true; 
 
 return false; 
  \} 
 
public void print()  \{ 	 \} 
 \}

As an example, we have shown in the above Java code the structure of the SafetySpecification class that is generated for the Byzantine agreement program introduced in Section 3.2. The destinationCondition and relationCondition specified in the if statements are exactly the same condition specified in the input file in the specification section.