;; This line starting with ;; is a comment ;; This file describes the Byzantine Broadcast Primitive ;; This is the informal specification of the protocol ;; Rounds are executed in a synchronous lock-step way by all processes ;; initialization: RI(x)=1 for all corrects; AC(x)= -1; ;; round r starts here ;; 1- corrects send echo to all 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} < N-T ;; =================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 (declare-fun IK0 () Int) (declare-fun IK1 () Int) (declare-fun IK2 () Int) (declare-fun IK3 () Int) (declare-fun IK4 () Int) ;; parameters used in unsafe formula (declare-fun FK () Int) ;; DECLARE GLOBAL VARIABLES ;; Global variables identifiers starts with $ ;; ;; program counter (declare-fun pc () Int) ;; ;; r is the round counter (declare-fun $r () Int) ;; ;; s is the session number (declare-fun $s () Int) ;; ;; T is the maximum number of faulty processes (declare-fun $T () Int) ;; ;; G indicates whether at least one round has been executed (declare-fun $G () Int) ;; DECLARE LOCAL VARIABLES (i.e. array variables) ;; Local variables identifiers also starts with $ ;; ;; I(x) is the state of init for x (declare-fun $I (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) ;; ;; CI(x) is the number of init received by correct processes (declare-fun $CI (Int) Int) ;; ;; CE(x) is the number of init received by correct processes (declare-fun $CE (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 ;; we want to say that there there are K1, K0 processes (whose sum is N) giving the number of the x's failing throughout the run ;; the arrays SE, AC, RI are initialized to 0 ; (and (= pc 1) (and (= $r 0) (= $s 1) (>= $T 1) (> N (* 2 $T)) (= $G 0) (= (+ IK1 IK0) N) (<= IK1 $T) (>= IK1 0) (>= IK2 (+ IK1 1)) (= (+ IK3 IK4) N) ) (= IK1 (card ((x Int)) (= ($F x) 1)) ) (= IK0 (card ((x Int)) (= ($F x) 0)) ) (= IK2 (card ((x Int)) (and (= ($F x) 0) (= ($I x) $s)) )) (= IK3 (card ((x Int)) (= ($I x) 0))) (= IK4 (card ((x Int)) (= ($I x) $s))) (forall ((x Int)) (and (= ($SE x) 0) (= ($AC x) 0) (= ($CI x) 0) (= ($CE x) 0) ) ) )) ;; DECLARE UNSAFE FORMULA (unsafe (and (= pc 1) (= $G 1) (and (> FK 0) ) (= FK (card ((x Int)) (and (= ($AC x) 0) (= ($F x) 0) ) ) ) )) ;;Declare transition from location 1 to location 2 ;; selection of echos received from faulty processes (different number for each correct process) (transition :name t1 (exists (($K1 Int) ($K2 Int) ($K3 Int) ($K4 Int)) (and (and (= pc 1) (= (primed pc) 2) (= (primed $r) $r) (= (primed $s) $s) ) (and (>= $K1 0) (>= $K2 0) (>= $K3 0) (>= $K4 0) (= (primed $G) $G) (= (primed $T) $T) ) ;; (= $K1 (card ((x Int)) (and (= ($F x) 0) (= ($I x) $s)) ) ) (= $K2 (card ((x Int)) (and (= ($F x) 0) (= ($SE x) $s)) ) ) (= $K3 (card ((x Int)) (and (= ($F x) 1) (= ($I x) $s)) ) ) (= $K4 (card ((x Int)) (and (= ($F x) 1) (= ($SE x) $s)) ) ) ;; (forall ((x Int)) (=> (= ($F x) 0) (and (>= ((primed $CI) x) $K1) (<= ((primed $CI) x) (+ $K1 $K3)) (>= ((primed $CE) x) $K2) (<= ((primed $CE) x) (+ $K2 $K4))) )) (forall ((x Int)) (=> (= ($F x) 1) (and (>= ((primed $CI) x) 0) (<= ((primed $CI) x) (+ $K1 $K3)) (>= ((primed $CE) x) 0) (<= ((primed $CE) x) (+ $K2 $K4))) )) ;; the other values stay the same (forall ((x Int)) (and (= ((primed $I) x) ($I x)) (= ((primed $SE) x) ($SE x)) (= ((primed $AC) x) ($AC x)) (= ((primed $F) x) ($F x)) ) ) ))) ;; Declare transition form location 2 back to location 1 ;; reception of echoes and appropriate state transitions ;; correct processes may only evolve from SE to AC state (transition :name t2 (exists (($K1 Int)) (and (and (= pc 2) (= (primed pc) 1)) (= (primed $r) (+ $r 1)) (= (primed $s) $s) (and (= (primed $T) $T) (= (primed $G) 1) (>= $K1 0) ) ;; (= $K1 (card ((x Int)) (= ($F x) 1) ) ) (forall ((x Int)) (=> (>= ($CI x) (+ $K1 1)) (and (= ((primed $SE) x) $s) (= ((primed $AC) x) $s) (= ((primed $I) x) ($I x)) ) ) ) (forall ((x Int)) (=> (and (< ($CI x) (+ $K1 1)) (>= ($CE x) 1)) (and (= ((primed $SE) x) $s) (= ((primed $AC) x) $s) (= ((primed $I) x) ($I x)) ) ) ) (forall ((x Int)) (=> (and (not (>= ($CI x) (+ $K1 1))) (not (and (< ($CI x) (+ $K1 1)) (>= ($CE x) 1) ))) (and (= ((primed $I) x) ($I x)) (= ((primed $AC) x) ($AC x)) (= ((primed $SE) x) ($SE x)) ) )) ;; ;; the other values stay the same (forall ((x Int)) (and (= ((primed $F) x) ($F x)) (= ((primed $CI) x) ($CI x)) (= ((primed $CE) x) ($CE x)) ) ) ))) (declare-fun c1 () Int) ;;Declare invariants (invariant (exists (($IF0 Int) ($IF1 Int) ($IAC Int) ($ICI Int) ($IIC Int) ) (and (= (+ $IF0 $IF1) N) (>= $IF1 0) (<= $IF1 $T) (>= $T 1) (> N (* 2 $T)) (>= $r 0) (= $s 1) (>= $IIC (+ $IF1 1)) (or (and (= pc 1) (= $G 0) (= $IAC $IF0) (= $ICI 0) ) (and (= pc 2) (>= $G 0) (= $ICI $IF0) (>= $IAC 0) (<= $IAC $IF0) ) (and (= pc 1) (= $G 1) (=> (> $IAC 0) (< $IIC 1)) (=> (= $IIC 0) (= $IAC $IF0)) ) ) (= $IF0 (card ((x Int)) (= ($F x) 0) )) (= $IF1 (card ((x Int)) (= ($F x) 1) )) (= $IAC (card ((x Int)) (and (= ($AC x) 0) (= ($F x) 0)) )) (= $ICI (card ((x Int)) (and (= ($F x) 0) (>= ($CI x) (+ $IF1 1))) )) (= $IIC (card ((x Int)) (and (= ($I x) $s) (= ($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 )