;; This line starting with ;; is a comment ;; This file describes the U_{T, E, alpha} algorithm ;; INTEGRITY property - UNsafe version for byzantine failures ;; P^{U,safe} predicate guaranteed, alpha = 1 ;; ;; =================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 IK1 () Int) (declare-fun IK2 () 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) ;; ;; Phi is the fase counter (declare-fun $phi () Int) ;; DECLARE LOCAL VARIABLES (i.e. array variables) ;; Local variables identifiers also starts with $ ;; ;; X(x) is the value held by x, in {1,2}; the default value is 2 (declare-fun $X (Int) Int) ;; ;; V(x) is the vote expressed by x -> 0 for ? vote (declare-fun $V (Int) Int) ;; ;; D(x) is the decision taken by x -> 0 for no decision (yet) (declare-fun $D (Int) Int) ;; ;; C1(x) number of msgs received with value / vote 1 (declare-fun $C1 (Int) Int) ;; ;; C2(x) number of messages received with value / vote 2 (declare-fun $C2 (Int) Int) ;; ;; C0(x) number of messages received with vote ? (0) (declare-fun $C0 (Int) Int) ;; ;; B12(x) number of messages with value/vote 1 from nodes with value/vote 2 (declare-fun $B12 (Int) Int) ;; ;; B21(x) number of messages with value/vote 2 from nodes with value/vote 1 (declare-fun $B21 (Int) Int) ;; ;; B10 (declare-fun $B10 (Int) Int) ;; ;; B20 (declare-fun $B20 (Int) Int) ;; ;; B01 (declare-fun $B01 (Int) Int) ;; ;; B02 (declare-fun $B02 (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) (= $phi 1) (= IK2 0) (= IK1 N) ) (= IK1 (card ((x Int)) (= ($X x) 1)) ) (= IK2 (card ((x Int)) (= ($X x) 2)) ) (forall ((x Int)) (and (= ($V x) 0) (= ($D x) 0) (= ($C1 x) 0) (= ($C2 x) 0) (= ($C0 x) 0) (= ($B12 x) 0) (= ($B21 x) 0) (= ($B10 x) 0) (= ($B20 x) 0) (= ($B01 x) 0) (= ($B02 x) 0) )) )) ;; DECLARE UNSAFE FORMULA (unsafe (and (= pc 1) (> FK1 0) (= FK1 (card ((x Int)) (> ($D x) 1) ) ) )) ;;Declare transition from location 1 to location 2 ;; selection of messages received from processes (different number for each correct process) ;; C1 for value 1; C2 for value 2; B1 byzantine for value 1; B2 byzantine for value 2 (transition :name t1 (exists (($K1 Int) ($K2 Int) ) (and (and (= pc 1) (= (primed pc) 2)) (and (>= $K1 0) (>= $K2 0) (= (primed $r) $r) (= (primed $phi) $phi) ) (= $K1 (card ((x Int)) (= ($X x) 1)) ) (= $K2 (card ((x Int)) (= ($X x) 2)) ) (forall ((x Int)) (and (<= ((primed $C1) x) $K1) (>= ((primed $C1) x) 0) (<= ((primed $C2) x) $K2) (>= ((primed $C2) x) 0) (>= ((primed $B21) x) 0) (>= ((primed $B12) x) 0) (<= ((primed $B21) x) $K1) (<= ((primed $B12) x) $K2) (<= (+ ((primed $C1) x) ((primed $B21) x)) $K1) (<= (+ ((primed $C2) x) ((primed $B12) x)) $K2) (<= (+ ((primed $C1) x) ((primed $C2) x) ((primed $B12) x) ((primed $B21) x)) N) (<= (+ ((primed $B12) x) ((primed $B21) x)) 1) ) ) ;; the other values stay the same (forall ((x Int)) (and (= ((primed $X) x) ($X x)) (= ((primed $V) x) ($V x)) (= ((primed $D) x) ($D x)) (= ((primed $C0) x) ($C0 x)) (= ((primed $B10) x) ($B10 x)) (= ((primed $B20) x) ($B20 x)) (= ((primed $B01) x) ($B01 x)) (= ((primed $B02) x) ($B02 x)) ) ) ))) ;; Declare transition from location 2 to location 3 ;; reception of messages and appropriate state transitions (transition :name t2 (and (and (= pc 2) (= (primed pc) 3)) (and (= (primed $r) (+ $r 1)) (= (primed $phi) $phi) ) ;; lines 8-9 pseudo-code (forall ((x Int)) (=> (> (* 2 (+ ($C1 x) ($B12 x))) (+ N 2)) (= ((primed $V) x) 1))) (forall ((x Int)) (=> (> (* 2 (+ ($C2 x) ($B21 x))) (+ N 2)) (= ((primed $V) x) 2))) (forall ((x Int)) (=> (and (not (> (* 2 (+ ($C1 x) ($B12 x))) (+ N 2))) (not (> (* 2 (+ ($C2 x) ($B21 x))) (+ N 2)))) (= ((primed $V) x) 0) )) ;; ;; the other values stay the same (forall ((x Int)) (and (= ((primed $X) x) ($X x)) (= ((primed $D) x) ($D x)) (= ((primed $C1) x) ($C1 x)) (= ((primed $C2) x) ($C2 x)) (= ((primed $C0) x) ($C0 x)) (= ((primed $B12) x) ($B12 x)) (= ((primed $B21) x) ($B21 x)) (= ((primed $B10) x) ($B10 x)) (= ((primed $B20) x) ($B20 x)) (= ((primed $B01) x) ($B01 x)) (= ((primed $B02) x) ($B02 x)) ) ) )) ;; Declare transition from location 3 to location 4 ;; selection of messages received from processes (different number for each correct process) ;; C_i according to value / vote as said above (transition :name t3 (exists (($K1 Int) ($K2 Int) ($K0 Int) ) (and (and (= pc 3) (= (primed pc) 4)) (and (= (primed $r) $r) (= (primed $phi) $phi) (>= $K1 0) (>= $K2 0) (>= $K0 0) ) (= $K1 (card ((x Int)) (= ($V x) 1) ) ) (= $K2 (card ((x Int)) (= ($V x) 2) ) ) (= $K0 (card ((x Int)) (= ($V x) 0) ) ) (forall ((x Int)) (and (>= ((primed $C1) x) 0) (>= ((primed $C2) x) 0) (>= ((primed $C0) x) 0) (<= ((primed $C1) x) $K1) (<= ((primed $C2) x) $K2) (<= ((primed $C0) x) $K0) (>= ((primed $B12) x) 0) (>= ((primed $B21) x) 0) (>= ((primed $B10) x) 0)(>= ((primed $B20) x) 0) (>= ((primed $B01) x) 0) (>= ((primed $B02) x) 0) (<= ((primed $B12) x) $K2) (<= ((primed $B21) x) $K1) (<= ((primed $B10) x) $K0) (<= ((primed $B20) x) $K0)(<= ((primed $B01) x) $K1) (<= ((primed $B02) x) $K2)(<= (+ ((primed $B12) x) ((primed $B21) x) ((primed $B10) x) ((primed $B20) x) ((primed $B01) x) ((primed $B02) x)) 1) (<= (+ ((primed $C1) x) ((primed $B01) x) ((primed $B21) x)) $K1) (<= (+ ((primed $C2) x) ((primed $B02) x) ((primed $B12) x)) $K2) (<= (+ ((primed $C0) x) ((primed $B10) x) ((primed $B20) x)) $K0) (<= (+ ((primed $C1) x) ((primed $C2) x) ((primed $C0) x) ((primed $B12) x) ((primed $B21) x) ((primed $B10) x) ((primed $B20) x) ((primed $B01) x) ((primed $B02) x)) N) ) ) ;; the other values stay the same (forall ((x Int)) (and (= ((primed $X) x) ($X x)) (= ((primed $V) x) ($V x)) (= ((primed $D) x) ($D x)) ) ) ))) ;; Declare transition from location 4 back to location 1 ;; reception of messages and appropriate state transitions (transition :name t4 (and (and (= pc 4) (= (primed pc) 1)) (and (= (primed $r) 1) (= (primed $phi) (+ $phi 1)) ) ;; line 14-17 pseudo-code (forall ((x Int)) (=> (>= (+ ($C1 x) ($B12 x) ($B10 x)) 1) (= ((primed $X) x) 1))) (forall ((x Int)) (=> (>= (+ ($C2 x) ($B21 x) ($B20 x)) 1) (= ((primed $X) x) 2))) (forall ((x Int)) (=> (and (not (>= (+ ($C1 x) ($B12 x) ($B10 x)) 1)) (not (>= (+ ($C2 x) ($B21 x) ($B20 x)) 1))) (= ((primed $X) x) 2))) ;; ;; line 18-19 pseudo-code (forall ((x Int)) (=> (> (* 2 (+ ($C1 x) ($B12 x) ($B10 x))) (+ N 2)) (= ((primed $D) x) 1))) (forall ((x Int)) (=> (> (* 2 (+ ($C2 x) ($B21 x) ($B20 x))) (+ N 2)) (= ((primed $D) x) 2))) (forall ((x Int)) (=> (and (not (> (* 2 (+ ($C1 x) ($B12 x) ($B10 x))) (+ N 2))) (not (> (* 2 (+ ($C2 x) ($B21 x) ($B20 x))) (+ N 2))) ) (= ((primed $D) x) ($D x)) )) ;; ;; line 20 (forall ((x Int)) (and (= ((primed $V) x) 0) (= ((primed $C1) x) 0) (= ((primed $C2) x) 0) (= ((primed $C0) x) 0) (= ((primed $B12) x) 0) (= ((primed $B21) x) 0) (= ((primed $B10) x) 0) (= ((primed $B20) x) 0) (= ((primed $B01) x) 0) (= ((primed $B02) x) 0) ) ) )) ;;Declare invariants (invariant (= 1 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 ;;To be done for this protocol )