The Specification of Agreement Program

In this section, we present an example of specifying a fault-intolerant program. Specifically, we show how the developers of fault-tolerance can specify an agreement program that consists of a general process and four non-general processes that are perturbed by both Byzantine and failstop faults. The structure of the input text file is as follows:

[commandchars=\\\{\},
       numbers=left,numbersep=3pt, fontsize=\footnotesize,
       xleftmargin=10mm,xrightmargin=10mm]
{\bf  \it program} Byzantine-Failstop
{\bf  \it  var }
{\bf  \it bool} bi; 
{\bf  \it bool} bj; 
{\bf  \it bool} bk;  
{\bf  \it bool} bl;  
{\bf  \it bool} bg;

{\bf  \it int} dg=0, {\bf  \it domain }  0 .. 1;
{\bf  \it int}  di, {\bf  \it domain }  -1 .. 1;  // (di == -1) means process i has not yet decided.
{\bf  \it int}  dj, {\bf  \it domain }  -1 .. 1;
{\bf  \it int}  dk, {\bf  \it domain }  -1 .. 1;
{\bf  \it int}  dl, {\bf  \it domain }  -1 .. 1;

{\bf  \it bool}  fi;
{\bf  \it bool}  fj;
{\bf  \it bool}  fk; 
{\bf  \it bool}  fl; 

{\bf  \it bool}  upi;
{\bf  \it bool}  upj;
{\bf  \it bool}  upk; 
{\bf  \it bool}  upl; 

// The structure of process i.
{\bf  \it  process  } i
{\bf  \it  begin } 
 ((di == -1) && (fi == 0) && (upi == 0)) ->  di = dg ;
| 
((di != -1) && (fi == 0) && (upi == 0)) ->  fi = 1 ;

{\bf  \it read} di, dj, dk, dl, dg, fi, upi, bi;
{\bf  \it write} di, fi;
{\bf  \it end} 

// The structure of process j.
{\bf  \it  process}  j
{\bf  \it  begin}
((dj == -1) && (fj == 0) && (upj == 0)) -> dj = dg;
|
((dj != -1) && (fj == 0) && (upj == 0)) -> fj = 1;

{\bf  \it read} di, dj, dk, dl, dg, fj, upj, bj;
{\bf  \it write} dj, fj;
{\bf  \it end}

// The structure of process k.
{\bf  \it  process}  k
{\bf  \it  begin}
((dk == -1) && (fk == 0) && (upk == 0)) -> dk = dg;
|
((dk != -1) && (fk == 0) && (upk == 0)) -> fk = 1;

{\bf  \it read} di, dj, dk, dl, dg, fk, upk, bk;
{\bf  \it write} dk, fk;
{\bf  \it end}

// The structure of process l.
{\bf  \it  process}  l
{\bf  \it  begin}
((dl == -1) && (fl == 0) && (upl == 0)) -> dl = dg;
|
((dl != -1) && (fl == 0) && (upl == 0)) -> fl = 1;

{\bf  \it read} di, dj, dk, dl, dg, fl, upl, bl;
{\bf  \it write} dl, fl;
{\bf  \it end}

// Faults are represented as a process.

{\bf  \it fault } FailstopAndByzantine
{\bf  \it  begin}
((upi == 1)&&(upj == 1)&&(upk == 1)&&(upl == 1)) -> upi = 0, upj = 0, 
                                                    upk = 0, upl = 0,
|
((bi == 0)&&(bj == 0)&&(bk == 0)&&(bl == 0)&&(bg == 0)) -> bi = 1, bj = 1, 
                                                   bk = 1, bl = 1, bg = 1,
|
((bi == 1)) -> di = 1 , di =0 , 
|
((bj == 1)) -> dj = 1 , dj =0 , 
|
((bk == 1)) -> dk = 1 , dk =0 , 
|
((bl == 1)) -> dl = 1 , dl =0 , 
|
((bg == 1)) -> dg = 1 , dg =0 ,
{\bf  \it end}

// The invariant of the program.
{\bf  \it invariant }
( (
  ((bg==0) &&
        (((bi == 1) && (bj == 0)&& (bk == 0)&& (bl == 0)) ||
         ((bj == 1) && (bi == 0)&& (bk == 0)&& (bl == 0)) ||
         ((bk == 1) && (bj == 0)&& (bi == 0)&& (bl == 0)) ||
         ((bl == 1) && (bj == 0)&& (bk == 0)&& (bi == 0)) ||
         ((bi == 0) && (bj == 0)&& (bk == 0)&& (bl == 0)) ) &&
         ((bi==1)||(di==-1)||(di==dg))&&
         ((bj==1)||(dj==-1)||(dj==dg))&&
         ((bk==1)||(dk==-1)||(dk==dg))&&
         ((bl==1)||(dl==-1)||(dl==dg))&&
         ((bi==1)||(fi==0)||(di!=-1) )&&
         ((bj==1)||(fj==0)||(dj!=-1) )&&
         ((bk==1)||(fk==0)||(dk!=-1) )&&
         ((bl==1)||(fl==0)||(dl!=-1) ) ) ||

  ((bg==1)&& (bi==0)&&(bj==0)&&(bk==0)&&(bl==0)&& (
         ( (((upi == 1) && (upj == 1)&& (upk == 1)&& (upl == 1)))  &&
                                   ((di==dj)&&(dj==dk)&&(dk==dl)&&(di!=-1)) ) || 
         ( (((upi == 1) && (upj == 1)&& (upk == 1)&& (upl == 0)))  &&
                                             ((di==dj)&&(dj==dk)&&(di!=-1)) ) ||
         ( (((upi == 1) && (upj == 1)&& (upk == 0)&& (upl == 1)))  &&
                                             ((di==dj)&&(dj==dl)&&(di!=-1)) ) ||
         ( (((upi == 1) && (upj == 0)&& (upk == 1)&& (upl == 1)))  &&
                                             ((di==dk)&&(dk==dl)&&(di!=-1)) ) ||
         ( (((upi == 0) && (upj == 1)&& (upk == 1)&& (upl == 1)))  &&
                                             ((dj==dk)&&(dk==dl)&&(dj!=-1)) ) 
         )) 
          )
         &&
         (
         ((upi == 0) && (upj == 1) && (upk ==1) && (upl == 1)) ||
         ((upi == 1) && (upj == 0) && (upk ==1) && (upl == 1)) ||
         ((upi == 1) && (upj == 1) && (upk ==0) && (upl == 1)) ||
         ((upi == 1) && (upj == 1) && (upk ==1) && (upl == 0)) ||
         ((upi == 1) && (upj == 1) && (upk ==1) && (upl == 1))   ))   

// The specification of the program is specified in three parts starting with
// {\it specification} keyword.

{\bf  \it specification}

// The {\it source} part identifies a set of states that every transition 
// originating at them violates safety.

 {\bf  \it noSource }

// The {\it destination} part identifies a set of states that every
// transition reaching them violates safety.

{\bf  \it destination }
(
( (bid == 0) && (bjd == 0) && (upid == 1) && (upjd == 1) && (did != -1) &&
                     (djd != -1) && (did != djd) && (fid == 1)  && (fjd == 1)) ||
( (bid == 0) && (bkd == 0) && (upid == 1) && (upkd == 1) && (did != -1) && 
                     (dkd != -1) && (did != dkd) && (fid == 1) && (fkd == 1)) ||
( (bid == 0) && (bld == 0) && (upid == 1) && (upld == 1) && (did != -1) && 
                      (dld != -1) && (did != dld) && (fid == 1) && (fld == 1)) ||
( (bjd == 0) && (bkd == 0) && (upkd == 1) && (upjd == 1) && (djd != -1) && 
                      (dkd != -1) && (djd != dkd) && (fjd == 1) && (fkd == 1)) ||
( (bjd == 0) && (bld == 0) && (upld == 1) && (upjd == 1) && (djd != -1) && 
                      (dld != -1) && (djd != dld) && (fjd == 1) && (fld == 1)) ||
( (bkd == 0) && (bld == 0) && (upkd == 1) && (upld == 1) && (dkd != -1) && 
                       (dld != -1) && (dkd != dld) && (fkd == 1) && (fld == 1)) ||

((bgd == 0) && (bid == 0)  && (did != -1) && (did != dgd) && (fid == 1)) ||
((bgd == 0) && (bjd == 0)  && (djd != -1) && (djd != dgd) && (fjd == 1)) ||
((bgd == 0) && (bkd == 0)  && (dkd != -1) && (dkd != dgd) && (fkd == 1)) ||
((bgd == 0) && (bld == 0)  && (dld != -1) && (dld != dgd) && (fld == 1))
)

// The {\it relation} part identifies a set of transitions that violate safety.

{\bf  \it relation }
((((bis == 0)&& (bid == 0) &&  (fis == 1) && (dis != did))) ||
            (((bjs == 0) && (bjd == 0) && (fjs == 1) && (djs != djd)))||
            (((bks == 0) && (bkd == 0) && (fks == 1) && (dks != dkd)))||
            (((bls == 0) && (bld == 0) && (fls == 1) && (dls != dld)))||
            (((bis == 0) && (bid == 0) && (fis == 1) && (fid == 0)))||
            (((bjs == 0) && (bjd == 0) && (fjs == 1) && (fjd == 0)))||
            (((bks == 0) && (bkd == 0) && (fks == 1) && (fkd == 0)))||
            (((bls == 0) && (bld == 0) && (fls == 1) && (fld == 0)))) 

// The {\it init} section is used for specifying the initial states.

{\bf  \it init }

// Each initial state is specified using the {\it state} keyword.

{\bf  \it state }
bi = 0; bj = 0; bk = 0; bl = 0; bg = 0; dg = 0; di = -1; dj = -1; dk = -1; bl = -1;
fi = 0; fj = 0; fk = 0; fl = 0; upi = 1; upj = 1; upk = 1; upl = 1;


{\bf  \it state }
bi = 0; bj = 0; bk = 0; bl = 0; bg = 0; dg = 1; di = -1; dj = -1; dk = -1; bl = -1;
fi = 0; fj = 0; fk = 0; fl = 0; upi = 1; upj = 1; upk = 1; upl = 1;