;; 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) ;; counter of correct processes in accept state (declare-fun IKA () Int) ;; conter of processes in initial state (declare-fun IKI () Int) ;; counterof processes in received-init state (declare-fun IKR () Int) ;; counter of processes in sent-echo state (declare-fun IKS () Int) ;; ;; parameters used in unsafe formula (declare-fun FK0 () Int) (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) ;; ;; RI(x) is the state of received init for x (declare-fun $RI (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)) (and (= IKA 1) (>= IKS (- (- N $T) 1)) (= N (+ IKA (+ IKS (+ IKI IKR)))) ) (= IK1 (card ((x Int)) (= ($F x) 1)) ) (= IK0 (card ((x Int)) (= ($F x) 0)) ) (= IKA (card ((x Int)) (and (= ($F x) 0) (= ($AC x) 1) (= ($SE x) 1) (= ($IT x) 0) (= ($RI x) 0) ) )) (= IKI (card ((x Int)) (and (= ($IT x) 1) (= ($RI x) 0) (= ($SE x) 0) (= ($AC x) 0) ) )) (= IKR (card ((x Int)) (and (= ($RI x) 1) (= ($IT x) 0) (= ($SE x) 0) (= ($AC x) 0) ) )) (= IKS (card ((x Int)) (and (= ($SE x) 1) (= ($IT x) 0) (= ($RI x) 0) (= ($AC x) 0) ) )) (forall ((x Int)) (= ($EF x) 0) ) )) ;; DECLARE UNSAFE FORMULA (unsafe (and (and (= pc 1) (>= $G 2) ) (> FK0 0) (> FK1 0) (= FK0 (card ((x Int)) (and (> ($AC x) 1) (= ($F x) 0) ) ) ) (= FK1 (card ((x Int)) (and (= ($AC x) 0) (= ($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)) (= ((primed $RI) x) ($RI 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 ; RI->SE (forall ((x Int)) (=> (and (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N (* 2 $T))) (< (+ $KE ($EF x)) (- N $T)) ) (and (= ((primed $RI) x) ($RI x)) (= ((primed $SE) x) 1) (= ((primed $AC) x) ($AC x)) (= ((primed $IT) x) ($IT x)) ) ) ) ;; ;; transition IT->AC ; RI->AC (forall ((x Int)) (=> (and (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N $T)) ) (and (= ((primed $RI) x) ($RI x)) (= ((primed $SE) x) 1) (= ((primed $AC) x) 1) (= ((primed $IT) x) ($IT x)) ) ) ) ;; ;; transition SE->AC (forall ((x Int)) (=> (and (= ($SE x) 1) (>= (+ $KE ($EF x)) (- N $T)) ) (and (= ((primed $RI) x) ($RI x)) (= ((primed $SE) x) ($SE x)) (= ((primed $AC) x) 1) (= ((primed $IT) x) ($IT x)) ) ) ) ;; ;; transition IT->RI: we assume it already done beforehand. Initialization reproduces all cases of init received by any number of nodes ;; otherwise (forall ((x Int)) (=> (and (not (and (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N (* 2 $T))) (< (+ $KE ($EF x)) (- N $T)) ) ) (not (and (= ($SE x) 0) (>= (+ $KE ($EF x)) (- N $T)) ) ) (not (and (= ($SE x) 1) (>= (+ $KE ($EF x)) (- N $T)) ) ) ) (and (= ((primed $RI) x) ($RI x)) (= ((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)) ) ) ))) ;;Declare invariants (invariant (exists ( ($IA0 Int) ($IA1 Int) ($IS0 Int) ($IS1 Int) ($IF1 Int) ($IF0 Int) ($IR1 Int) ($IR0 Int) ($IE Int) ($ISC Int) ($IAD Int) ($IAU Int) ($ISa Int) ($ISb Int) ($ISc Int) ($ISd Int)) ; (and (= (+ $IR0 $IR1) N) (= (+ $IS0 $IS1) N) (= (+ $IA0 $IA1) N) (= (+ $IF0 $IF1) N) (>= $IF1 0) (< (* 3 $IF1) N) (> (* 3 $IF0) (* 2 N)) (= $IE N) (= (+ $ISa $ISb $ISc $ISd) N) (>= $G 0) (<= $G 1) (> (* 3 (+ $ISc 1)) (* 2 N)) (or (and (= pc 1) (= $G 0) (= $IA1 1) ) (and (= pc 1) (= $G 1) (=> (> $IAU 0) (<= (* 3 $ISC) N) ) (=> (> $IAD 0) (> (* 3 $ISC) N)) ) (and (= pc 2) (= $G 0) (= $IE N) (= $IA1 1) ) (and (= pc 2) (= $G 1) (= $IE N) (=> (> $IAU 0) (<= (* 3 $ISC) N) ) (=> (> $IAD 0) (> (* 3 $ISC) N)) ) ) (= $IA0 (card ((x Int)) (= ($AC x) 0) )) (= $IA1 (card ((x Int)) (= ($AC x) 1) )) (= $IS0 (card ((x Int)) (= ($SE x) 0) )) (= $IS1 (card ((x Int)) (= ($SE x) 1) )) (= $IF1 (card ((x Int)) (= ($F x) 1) )) (= $IF0 (card ((x Int)) (= ($F x) 0) )) (= $IR1 (card ((x Int)) (= ($RI x) 1) )) (= $IR0 (card ((x Int)) (= ($RI x) 0) )) (= $IE (card ((x Int)) (and (>= ($EF x) 0) (< (* 3 ($EF x)) N)) )) (= $ISC (card ((x Int)) (and (= ($SE x) 1) (= ($F x) 0)) )) (= $IAD (card ((x Int)) (and (= ($AC x) 1) (= ($F x) 0)) )) (= $IAU (card ((x Int)) (and (= ($AC x) 0) (= ($F x) 0)) )) (= $ISa (card ((x Int)) (and (= ($IT x) 1) (= ($SE x) 0) (= ($RI x) 0) (= ($AC x) 0)) )) (= $ISb (card ((x Int)) (and (= ($IT x) 0) (= ($SE x) 0) (= ($RI x) 1) (= ($AC x) 0)) )) (= $ISc (card ((x Int)) (and (= ($IT x) 0) (= ($SE x) 1) (= ($RI x) 0) (= ($AC x) 0)) )) (= $ISd (card ((x Int)) (and (= ($IT x) 0) (= ($SE x) 1) (= ($RI x) 0) (= ($AC x) 1) (= ($F x) 0)) )) )) ;;This is optional (just in case an invariant is known) ;;One should supply one declaration for each location following the general syntax instructions above )