;; This line starting with ;; is a comment ;; This file describes the Byzantine Broadcast Primitive ;; RELAY property - safe version ;; ;; This is the informal specification of the protocol ;; Rounds are executed in a synchronous lock-step way by all processes ;; initialization: IT(x)=1 for all corrects; AC(x)= 0; ;; round r starts here ;; 1- we compute a random number of echoes sent by faulty processes ;; 2-if x got more than 1/3 echoes then its sends echo ;; if more than 2/3 echoes received then AC(x)=1 ;; round r ends here ;; unsafe condition #{x| AC(x)=1 \wedge F(x)=0} >0 ;; =================VARIABLE DECLARATIONS=================== ;; DECLARE GLOBAL PARAMETERS ;; ;; N is the dimension of the system (declare-system-size N) ;; ;; parameters used only in the initial or in the final formula must be declared here ;; parameters used in initial formula ;; conuters of faulty and correct processes (declare-fun IK1 () Int) (declare-fun IK0 () Int) ;; conter of processes in initial state (declare-fun IKI () Int) ;; ;; parameters used in unsafe formula (declare-fun FK1 () Int) ;; DECLARE GLOBAL VARIABLES ;; Global variables identifiers starts with $ ;; ;; program counter (declare-fun pc () Int) ;; ;; r is the round counter (declare-fun $r () Int) ;; ;; T is the maximum number of faulty processes (declare-fun $T () Int) ;; ;; G is the flag indicating that at least one round has been executed (declare-fun $G () Int) ;; DECLARE LOCAL VARIABLES (i.e. array variables) ;; Local variables identifiers also starts with $ ;; ;; IT(x) is the initial state for x (declare-fun $IT (Int) Int) ;; ;; SE(x) is the state of sent echo for x (declare-fun $SE (Int) Int) ;; ;; AC(x) is the value decided by x (declare-fun $AC (Int) Int) ;; ;; F(x) is a flag indicating whether x is faulty (declare-fun $F (Int) Int) ;; ;; EF(x) is the number of echos sent by faulty processes (declare-fun $EF (Int) Int) ;; =========GENERAL SYNTAX INSTRUCTIONS============ ;; Each of initial, unsafe, transition, invariants formulae have five parts: ;; 0) pc_counter specification (this is an Integer giving the location) ;; 1) Local parameters declarations (parameters used only in the formula are declared - they are existentially quantified) ;; local parameters identifiers starts with $ ;; 2) SMT-LIB quantifier-free formula containing parameters (local or global) ;; 3) universally quantified formula ;; (forall ((x Int)) \phi) ;; where \phi is an SMT-LIB quiantifier-free formula containing parameters (local or global) as well as terms $A, $A' ;; denoting the value of the array $A, $A' computed at the entry x ;; 4) cardinality constraInts ;; a = #{x | \phi} ;; where a is a parameter (local or global) or a global variable and \phi is an SMT quantifier-free formula as above ;; =====BODY DECLARATIONS============== ;; DECLARE INITIAL FORMULA (initial ;; conters IK1, IK0 allow to select faulty processes ; (and (= pc 1) (and (= $r 1) (>= $T 1) (> N (* 3 $T)) (= $G 0) ) (and (= (+ IK1 IK0) N) (<= IK1 $T) (>= IK1 0) (>= IK0 0)) (= IK1 (card ((x Int)) (= ($F x) 1)) ) (= IK0 (card ((x Int)) (= ($F x) 0)) ) (forall ((x Int)) (and (= ($EF x) 0) (= ($IT x) 0) (= ($SE x) 0) (= ($AC x) 0)) ) )) ;; DECLARE UNSAFE FORMULA (unsafe (and (and (= pc 1) (>= $G 2) ) (> FK1 0) (= FK1 (card ((x Int)) (and (= ($AC x) 1) (= ($F x) 0) ) ) ) )) ;;Declare transition from location 1 to location 2 ;; selection of echoes received from faulty processes (different number for each correct process) (transition :name t1 (exists (($K Int)) (and (and (= pc 1) (= (primed pc) 2)) (and (>= $K 0) (= (primed $r) $r) (= (primed $T) $T) (= (primed $G) $G) ) ;; the value $EF' is nondeterministically taken to be a number less or equal to the number of faulty processes (= $K (card ((x Int)) (= ($F x) 1)) ) (forall ((x Int)) (and (<= ((primed $EF) x) $K) (>= ((primed $EF) x) 0) ) ) ;; the other values stay the same (forall ((x Int)) (and (= ((primed $IT) x) ($IT x)) (= ((primed $SE) x) ($SE x)) (= ((primed $AC) x) ($AC x)) (= ((primed $F) x) ($F x)) ) ) ))) ;; Declare transition from location 2 to location 3 ;; reception of echoes and appropriate state transitions ;; transitions possibile: IT->SE, IT->AC, SE->AC, IT->RI, RI->SE, RI->AC (transition :name t2 (exists (($KE Int)) (and (and (= pc 2) (= (primed pc) 1)) (and (= (primed $r) (+ $r 1)) (= (primed $T) $T) (> $KE 0) (= (primed $G) (+ $G 1)) ) ;; KE counts the number of echoes sent by correct processes (= $KE (card ((x Int)) (and (= ($SE x) 1) (= ($F x) 0)) )) ;; the values are updated according to the protocol's rules ;; ;; transition IT->SE correct procs (forall ((x Int)) (=> (and (= ($F x) 0) (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N (* 2 $T))) (< (+ $KE ($EF x)) (- N $T)) ) (and (= ((primed $SE) x) 1) (= ((primed $AC) x) 0) (= ((primed $IT) x) 0) ) ) ) ;; ;; transition IT->AC correct procs (forall ((x Int)) (=> (and (= ($F x) 0) (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N $T)) ) (and (= ((primed $SE) x) 1) (= ((primed $AC) x) 1) (= ((primed $IT) x) 0) ) ) ) ;; ;; transition SE->AC correct procs (forall ((x Int)) (=> (and (= ($F x) 0) (= ($SE x) 1) (>= (+ $KE ($EF x)) (- N $T)) ) (and (= ((primed $SE) x) 1) (= ((primed $AC) x) 1) (= ((primed $IT) x) 0) ) ) ) ;; ;; transition IT->RI->SE: we assume it already done before. Initialization reproduces all cases of init received by any number of nodes; those that receive init send Echo, the other procs stay in IT ;; ;; otherwise (forall ((x Int)) (=> (and (not (and (= ($F x) 0) (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N (* 2 $T))) (< (+ $KE ($EF x)) (- N $T)) ) ) (not (and (= ($F x) 0) (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N $T)) ) ) (not (and (= ($F x) 0) (= ($SE x) 1) (>= (+ $KE ($EF x)) (- N $T)) ) ) ) (and (= ((primed $SE) x) ($SE x)) (= ((primed $AC) x) ($AC x)) (= ((primed $IT) x) ($IT x)) ) ) ) ;; ;; the other values stay the same (forall ((x Int)) (and (= ((primed $F) x) ($F x)) (= ((primed $EF) x) ($EF x)) ) ) ))) (invariant (exists (($IF0 Int) ($IF1 Int) ($IAU Int) ($IAC Int) ($ICE Int) ($ISC Int) ) (and (= (+ $IF0 $IF1) N) (>= $IF1 0) (<= $IF1 $T) (>= $T 1) (> N (* 3 $T)) (>= $r 1) (= $ICE N) (= $ISC 0) (= (+ $IAC $IAU) $IF0) (or (and (= pc 1) (= $G 0) (= $IAC 0) (= $IAU $IF0) ) (and (= pc 2) (= $G 0) (= $IAC 0) (= $IAU $IF0) ) (and (= pc 1) (= $G 1) (= $IAC 0) (= $IAU $IF0) ) (and (= pc 2) (= $G 1) (= $IAC 0) (= $IAU $IF0) ) (and (= pc 1) (>= $G 2) (=> (> $IAU 0) (<= (* 3 $ISC) N) ) (=> (> $IAC 0) (> (* 3 $ISC) N)) ) (and (= pc 2) (>= $G 2) (= $IAU $IF0) (= $IAC 0) ) ) (= $IF0 (card ((x Int)) (= ($F x) 0) )) (= $IF1 (card ((x Int)) (= ($F x) 1) )) (= $IAU (card ((x Int)) (and (= ($AC x) 0) (= ($F x) 0)) )) (= $IAC (card ((x Int)) (and (= ($AC x) 1) (= ($F x) 0)) )) (= $ICE (card ((x Int)) (and (>= ($EF x) 0) (<= ($EF x) $IF1)) )) (= $ISC (card ((x Int)) (and (= ($F x) 0) (= ($SE x) 1)) )) )) ;;This is optional (just in case an invariant is known) ;;One should supply one declaration for each location following the general syntax instructions above )