Generating The Output Generator

After the synthesis framework synthesizes a fault-tolerant program, it has to transform the reachability graph of the fault-tolerant program to guarded commands that are understandable for the user. To achieve this goal, the input translator automatically generates the OutputGenerator class in Java code.

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
public class OutputGenerator \{   
 
	 public OutputGenerator() \{     \}  
 
static void PrintProcess_i(AbstractReachabilityGraph g, 
                               String action, OutputFile outf)\{ 
				.  .  .
		\}
static void PrintProcess_j(AbstractReachabilityGraph g, 
					 String action, OutputFile outf)\{ 
				.  .  .
		\}
static void PrintProcess_k(AbstractReachabilityGraph g, 
					 String action, OutputFile outf)\{ 
				.  .  .
		\}

static public void printFIProgram(AbstractReachabilityGraph g,OutputFile of)\{ 
	 of.writeLine("No. of states: "+g.getNumStates()); 
	 of.writeLine(" "); 
	 of.writeLine("*******  The fault-intolerant program  ********"); 
	 of.writeLine(" "); 
	 of.writeLine("----------  The actions of Process i ----------"); 
	 of.writeLine(" "); 
	 PrintProcess_i(g,"set_di_val0",of); 
	 of.writeLine(" "); 
	 PrintProcess_i(g,"set_di_val1",of); 
	 of.writeLine(" "); 
	 PrintProcess_i(g,"set_fi_val1",of); 
	 of.writeLine(" "); 
	 of.writeLine("----------  The actions of Process j ----------"); 
	 of.writeLine(" "); 
	 PrintProcess_j(g,"set_dj_val0",of); 
	 of.writeLine(" "); 
	 PrintProcess_j(g,"set_dj_val1",of); 
	 of.writeLine(" "); 
	 PrintProcess_j(g,"set_fj_val1",of); 
	 of.writeLine(" "); 
	 of.writeLine("----------  The actions of Process k ----------"); 
	 of.writeLine(" "); 
	 PrintProcess_k(g,"set_dk_val0",of); 
	 of.writeLine(" "); 
	 PrintProcess_k(g,"set_dk_val1",of); 
	 of.writeLine(" "); 
	 PrintProcess_k(g,"set_fk_val1",of); 
	 of.writeLine(" "); 
	 \} 

static public void printFTProgram(AbstractReachabilityGraph g,OutputFile of)\{ 
	 of.writeLine("No. of states: "+g.getNumStates()); 
	 of.writeLine(" "); 
	 of.writeLine("*******  The fault-tolerant program  ********"); 
	 of.writeLine(" "); 
	 of.writeLine("----------  The actions of Process i ----------"); 
	 of.writeLine(" "); 
	 PrintProcess_i(g,"set_di_val0",of); 
	 of.writeLine(" "); 
	 PrintProcess_i(g,"set_di_val1",of); 
	 of.writeLine(" "); 
	 PrintProcess_i(g,"set_fi_val1",of); 
	 of.writeLine(" "); 
	 of.writeLine("----------  The actions of Process j ----------"); 
	 of.writeLine(" "); 
	 PrintProcess_j(g,"set_dj_val0",of); 
	 of.writeLine(" "); 
	 PrintProcess_j(g,"set_dj_val1",of); 
	 of.writeLine(" "); 
	 PrintProcess_j(g,"set_fj_val1",of); 
	 of.writeLine(" "); 
	 of.writeLine("----------  The actions of Process k ----------"); 
	 of.writeLine(" "); 
	 PrintProcess_k(g,"set_dk_val0",of); 
	 of.writeLine(" "); 
	 PrintProcess_k(g,"set_dk_val1",of); 
	 of.writeLine(" "); 
	 PrintProcess_k(g,"set_fk_val1",of); 
	 of.writeLine(" "); 
	 \} 

 \}

The structure of the OutputGenerator class consists of two parts. First, we have a section that includes a method corresponding to each process. For example, for the Byzantine agreement program, the input translator generates three methods corresponding to non-general processes i, j, and k (cf. Section 3.2). In the second part of the code of the OutputGenerator class, the input translator generates two methods respectively for generating the fault-intolerant and the fault-tolerant programs. In each of these section, the methods specified in the first part are invoked to generate the guarded command of each process.