% Short report on results on SAL model and formal verification of:
% 
% A fault-tolerant digital clocking system
%  William M. Daly
%  Albert L. Hopkins, jr.,
%  John F. McKena
%  MIT Draper Lab 
% 
%%  Summary of the result:
% ----------------------
% The proposed clock synchronization algorithm
% is buggy and can not synchronize clocks from
% arbitrary initial configurations if faults are
% assumed byzantine.
% 
% Details:
% --------
% We modeled the proposed algorithm in SAL, as a
% finite state machine.
% 
% Time was abstracted into 4 regions, named
% l, lf, fa, fl.
% Intuitively, 
% "l" represents a small region around the leading edge, 
% "fa" represents a small region around the falling edge,
% "lf" represents the region after l but before fa, and
% "fl" represents the region after fa but before l.
% 
% The system has two parameters:
% f is the number of faulty clocks
% r is the number of non-faulty clocks.
% We verify the system for different values of f and r.
% We assume r+f >= 3*f+1
% 
% The state of the system consists of
% c: ARRAY [1..r] OF BOOLEAN
% ftime, ltime: ARRAY [1..r] OF TIME
% qrmf,qfp1: ARRAY [1..r] OF BOOLEAN	% qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r
% currtime: TIME
% 
% c is the array that stores the clock value for each of 
% the r non-faulty clocks.  The value is either TRUE (1) 
% or FALSE (0).  Note that we do not keep the state of the 
% faulty clocks since it is irrelevant.  This leads to a 
% smaller (and easily model checkable) model.
% 
% currtime holds the value of the current time (l, lf, fa, fl).
% 
% The quorum function
% Q(b,a) is defined so that it has value 1 if a or more its
% b inputs are 1, and is 0 otherwise.
% 
% qfp1 is the quorum function Q(r+f, f+1).
% qrmf is the quorum function Q(r+f, r).
% 
% If clock c[i] sees a falling edge on qfp1 signal, then it
% sets ftime[i] to (current_time + 2 abstract time units).
% If clock c[i] sees a leading edge on qrmf signal, then it
% sets ltime[i] to (current_time + 2 abstract time units).
% There is also an abstract time value called "notset" for the
% case when these arrays have unset values.
% 
% The SAL model then follows the description in the 1973 paper.
% When a clock output changes, it is not allowed to change again
% for an interval t_min, which in our case is 1 abstract time unit.
% 
% We can run the sal symbolic model checker to verify 
% eventuality properties, which state that the system eventually 
% reaches some 'clock synchronized' state.
% We use f = 1 and r = 3.
% 
% For the case when the initial state has 2 clocks at 1
% and 1 clock at 0, then the byzantine faulty 4th clock can
% make the system loop in states that have either
% (2 clocks at 1 and 1 clock at 0)
% or
% (1 clock at 1 and 2 clocks at 0)
% at all times.
% Thus, the good clocks never synchronize.
% 
% Most minor changes to the protocol continue to yield counter-examples
% to the desired clock-sync property.
% It appears to be difficult to fix.
% 

phaseLocking7: CONTEXT = 
BEGIN

 % Time is abstracted into 4 regions
 % l = leading edge ; f = following edge (of desired clock signal)
 TIME: TYPE = { l, lf, fa, fl, notset };
 
 r: NATURAL = 3 ;	% number of NON-FAULTY nodes
 f: NATURAL = 1 ;	% number of faults tolerated

 sum(x: ARRAY [1..r] OF BOOLEAN, n: [0..r], a: [0..r] ): [0..r] = 
  IF n = r THEN a ELSIF x[n+1] THEN sum(x, n+1, a+1) ELSE sum(x, n+1, a) ENDIF;

 % Q_b^r where s is the sum of all 1's in x
 q(b: [1..r], s: [0..r]): [BOOLEAN -> BOOLEAN] = 
  IF (s >= b) THEN { TRUE }
  ELSIF (s + f < b) THEN { FALSE }
  ELSE { TRUE, FALSE } ENDIF ;	 % STUCK AT 1 FAULT - not byzantine

 prev(t: TIME): TIME = 
  IF t = l THEN fl 
  ELSIF t = lf THEN l
  ELSIF t = fa THEN lf
  ELSE fa ENDIF ;

 next(t: TIME): TIME = 
  IF t = l THEN lf 
  ELSIF t = lf THEN fa
  ELSIF t = fa THEN fl
  ELSE l ENDIF ;

 next2(t: TIME): TIME = next(next(t)) ;

 calculator: MODULE = 
 BEGIN
  OUTPUT ftime, ltime: ARRAY [1..r] OF TIME
  OUTPUT qrmf,qfp1: ARRAY [1..r] OF BOOLEAN	% qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r
  INPUT c: ARRAY [1..r] OF BOOLEAN
  INPUT currtime: TIME
  LOCAL smin: [0..r]
  INITIALIZATION
   ftime = [ [i:[1..r]] IF c[i] THEN notset ELSE next(currtime) ENDIF ] ;
   ltime = [ [i:[1..r]] IF c[i] THEN next(currtime) ELSE notset ENDIF ] ;
   qrmf = [ [i:[1..r]] FALSE ];
   qfp1 = [ [i:[1..r]] FALSE ];
  DEFINITION
    smin = sum(c, 0, 0) ;
  TRANSITION
  [
  % currtime = currtime' -->
  TRUE -->
    qrmf' IN { a: ARRAY [1..r] OF BOOLEAN | FORALL (i:[1..r]):
		q(r,smin)(a[i]) } ;
    qfp1' IN { a: ARRAY [1..r] OF BOOLEAN | FORALL (i:[1..r]):
		q(f+1,smin)(a[i]) } ;
    ftime' = [ [i:[1..r]] 
	    IF c[i] THEN notset
  	    ELSIF (qfp1[i] AND qfp1'[i] = FALSE) THEN next2(currtime)
	    ELSE ftime[i] ENDIF ] ;
    ltime' = [ [i:[1..r]] 
	    IF NOT(c[i]) THEN notset
  	    ELSIF (qrmf[i] = FALSE AND qrmf'[i]) THEN next2(currtime)
	    ELSE ltime[i] ENDIF ]
   % []
   % ELSE -->
  ]
 END;

 updater: MODULE = 
 BEGIN
  INPUT ftime, ltime: ARRAY [1..r] OF TIME
  INPUT qrmf,qfp1: ARRAY [1..r] OF BOOLEAN % qrmf = Q_{r-f}^r, qfp1 = Q_{f+1}^r
  OUTPUT currtime: TIME
  LOCAL frozen: ARRAY [1..r] OF TIME 
  LOCAL lastChange: ARRAY [1..r] OF TIME 
  OUTPUT c: ARRAY [1..r] OF BOOLEAN 	% r phase locked clock's
  INITIALIZATION
   currtime = l ;
   frozen = [ [i:[1..r]] currtime ] ;
   lastChange = [ [i:[1..r]] notset ] ;
   %c = [ [i:[1..r]] FALSE ];
   %c = [ [i:[1..r]] IF i=1 THEN TRUE ELSE FALSE ENDIF ];
   c IN { a: ARRAY [1..r] OF BOOLEAN | 2*sum(a,0,0) = 2 } ;
  TRANSITION
  [
   FORALL (i:[1..r]): (NOT(frozen[i] = currtime) OR
    ( NOT(qfp1[i] = FALSE AND qfp1'[i] = TRUE AND NOT(c[i]) ) AND
      NOT(qrmf[i] = TRUE AND qrmf'[i] = FALSE AND c[i]) AND 
      NOT(ftime[i] = currtime AND NOT(c[i])) AND
      NOT(ltime[i] = currtime AND c[i]) )) AND NOT(lastChange[i] = next(currtime)) -->
	currtime' = next(currtime) ;
	frozen' = [ [i:[1..r]] IF frozen[i] = currtime THEN next(currtime)
		ELSE frozen[i] ENDIF ]
   []
   ELSE -->
    c' = [ [i:[1..r]]
	IF frozen[i] = currtime AND qfp1[i] = FALSE AND qfp1'[i] = TRUE AND NOT(c[i])
	THEN TRUE
	ELSIF frozen[i] = currtime AND qrmf[i] = TRUE AND qrmf'[i] = FALSE AND c[i]
	THEN FALSE
    	ELSIF frozen[i] = currtime AND ftime[i] = currtime AND NOT(c[i])
	THEN TRUE
    	ELSIF frozen[i] = currtime AND ltime[i] = currtime AND c[i]
	THEN FALSE
	ELSIF lastChange[i] = next(currtime) THEN NOT(c[i])
	ELSE c[i] ENDIF ] ;
    lastChange' = [ [i:[1..r]]
	IF NOT(c[i] = c'[i]) THEN currtime ELSE lastChange[i] ENDIF ] ;
    frozen' = [ [i:[1..r]]
	IF frozen[i] = currtime AND qfp1[i] = FALSE AND qfp1'[i] = TRUE AND NOT(c[i])
	THEN next(currtime)
	ELSIF frozen[i] = currtime AND qrmf[i] = TRUE AND qrmf'[i] = FALSE AND c[i]
	THEN next(currtime)
    	ELSIF frozen[i] = currtime AND ftime[i] = currtime AND NOT(c[i])
	THEN next(currtime)
    	ELSIF frozen[i] = currtime AND ltime[i] = currtime AND c[i]
	THEN next(currtime)
	ELSE frozen[i] ENDIF ] 
  ]
 END ;

 startup: MODULE = calculator || updater ;

 p1: LEMMA 
  startup |- F ( currtime = fl );

 p2: LEMMA
  % startup |-  F( G ( currtime = fl => (FORALL (i:[1..r]): c[i] = c[1])) ) ;
  startup |-  F( G ( (FORALL (i:[1..r]): c[i] = c[1])) ) ;

 % THIS PROPERTY IS INVALID.
 p22: LEMMA
  startup |-  F ( ((FORALL (i:[1..r]): c[i] = c[1])) ) ;

 p3: LEMMA
  startup |-  ( G ( (currtime = fl) => (sum(c,0,0) <= f OR sum(c,0,0) >= 2*f+1) ) ) ;

 p4: LEMMA
  startup |- G ( (currtime = fl) => (FORALL (j:[1..r]): FORALL (k:[1..r]):
		  c[j] = c[k] ) );

 p5: LEMMA
  startup |- G( FORALL (i:[1..r]): c[i] = FALSE => X(NOT(ftime[i] = prev(currtime)) )) ;
END