;; ;; ELENA - 11 nov. 2015 ;; ;; This file describes consensus protocol "One Third" ;; Safety of IRREVOCABILITY property ;; ;; This is the informal specification of the protocol (we assume that the value to be decided is either 1 or 0) ;; Rounds are executed in a synchronous lock-step way by all processes ;; initialization: H(x) \in {0,1}; Dec(x)= (- 1); ;; round r starts here ;; 1-send H(x) to all processes ;; 2-if x got more than 2/3 messages then { ;; H(x) := the least most often received value ;; } ;; if more than 2/3 values received are equal to H(x){ ;; Dec(x):= x ;; } ;; round r ends here ;; unsafe condition #({x|Rev(x)=1})>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 (declare-fun IK1 () Int) (declare-fun IK2 () Int) ;; parameters used in unsafe formula (declare-fun FD1 () Int) (declare-fun FH1 () Int) (declare-fun FD2 () Int) (declare-fun FH2 () Int) ;; Declare global variables ;; Global variables identifiers starts with $ ;; r is the round counter ;; (declare-fun $r () Int) ;; program counter (declare-fun pc () Int) ;; Declare local variables (i.e. array variables) ;; Local variables identifiers also starts with $ ;; ;; H(x) is the value held by x (declare-fun $H (Int) Int) ;; ;;R2(x) is the number of messages received by x with content 2 (declare-fun $R2 (Int) Int) ;; ;;R1(x) is the number of messages received by x with content 1 (declare-fun $R1 (Int) Int) ;; ;;Dec(x) is the value decided by x (declare-fun $Dec (Int) Int) ;; Rev(x) is 1 when x has changed/revoked its decision (declare-fun $Rev (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 (whose sum is N) giving the number of the x's initially holding 1, 0 ;; the arrays H0, H1 are initialized to 0 and the array Dec is initialized to (- 1) ; (and (= pc 1) (and (= $r 0) (= (+ IK1 IK2) N) (<= (* 3 IK1) (* N 2)) (<= (* 3 IK2) (* N 2)) ) (= IK1 (card ((x Int)) (= ($H x) 1)) ) (= IK2 (card ((x Int)) (= ($H x) 2)) ) (forall ((x Int)) (and (= ($R2 x) 0) (= ($R1 x) 0) (= ($Dec x) 0) (= ($Rev x) 0)) ) )) ;; Declare unsafe formula (unsafe (and (= pc 1) (or (and (> FD1 0) (<= (* 3 FH1) (* 2 N)) ) (and (> FD2 0) (<= (* 3 FH2) (* 2 N)) ) ) (= FD1 (card ((x Int)) (= ($Dec x) 1)) ) (= FH1 (card ((x Int)) (= ($H x) 1)) ) (= FD2 (card ((x Int)) (= ($Dec x) 2)) ) (= FH2 (card ((x Int)) (= ($H x) 2)) ) )) ;;Declare transition from location 1 to location 2 (transition :name t1 (exists (($K2 Int) ($K1 Int)) (and (and (= pc 1) (= (primed pc) 2)) (and (>= $K2 0) (>= $K1 0) (= (primed $r) $r)) (= $K1 (card ((x Int)) (= ($H x) 1)) ) (= $K2 (card ((x Int)) (= ($H x) 2)) ) (forall ((x Int)) (and (>= ((primed $R1) x) 0) (<= ((primed $R1) x) $K1) (>= ((primed $R2) x) 0) (<= ((primed $R2) x) $K2) ) ) ;; the other values stay the same (forall ((x Int)) (and (= ((primed $Dec) x) ($Dec x)) (= ((primed $H) x) ($H x) ) (= ((primed $Rev) x) ($Rev x) ) ) ) ))) ;;Declare transition from location 2 to location 1 (transition :name t2 (and (and (= pc 2) (= (primed pc) 1)) (= (primed $r) (+ $r 1)) ;; (forall ((x Int)) (=> (and (> (* 3 (+ ($R2 x) ($R1 x))) (* 2 N)) (> ($R2 x) ($R1 x)) ) (and (= ((primed $H) x) 2) (= ((primed $Dec) x) ($Dec x)) (= ((primed $Rev) x) ($Rev x))) ) ) (forall ((x Int)) (=> (and (> (* 3 (+ ($R2 x) ($R1 x))) (* 2 N)) (<= ($R2 x) ($R1 x)) ) (and (= ((primed $H) x) 1) (= ((primed $Dec) x) ($Dec x)) (= ((primed $Rev) x) ($Rev x))) ) ) (forall ((x Int)) (=> (and (not (and (> (* 3 (+ ($R2 x) ($R1 x))) (* 2 N)) (> ($R2 x) ($R1 x)) )) (not (and (> (* 3 (+ ($R2 x) ($R1 x))) (* 2 N)) (<= ($R2 x) ($R1 x)) ))) (and (= ((primed $H) x) ($H x)) (= ((primed $Dec) x) ($Dec x)) (= ((primed $Rev) x) ($Rev x))) ) ) ;; ;; WITH NO REVOKE (forall ((x Int)) (=> (and (= ($H x) 2) (> (* 3 ($R2 x)) (* 2 N)) (= ($Dec x) 0)) (and (= ((primed $Dec) x) 2) (= ((primed $Rev) x) 0) (= ((primed $H) x) ($H x))) ) ) (forall ((x Int)) (=> (and (= ($H x) 1) (> (* 3 ($R1 x)) (* 2 N)) (= ($Dec x) 0)) (and (= ((primed $Dec) x) 1) (= ((primed $Rev) x) 0) (= ((primed $H) x) ($H x))) ) ) ;; ;; WITH REVOKE (forall ((x Int)) (=> (and (= ($H x) 2) (> (* 3 ($R2 x)) (* 2 N)) (= ($Dec x) 1)) (and (= ((primed $Dec) x) 2) (= ((primed $Rev) x) 1) (= ((primed $H) x) ($H x)) ) ) ) (forall ((x Int)) (=> (and (= ($H x) 1) (> (* 3 ($R1 x)) (* 2 N)) (= ($Dec x) 2)) (and (= ((primed $Dec) x) 1) (= ((primed $Rev) x) 1) (= ((primed $H) x) ($H x)) ) ) ) ;; (forall ((x Int)) (=> (and (not (and (= ($H x) 2) (> (* 3 ($R2 x)) (* 2 N)) (= ($Dec x) 0)) ) (not (and (= ($H x) 1) (> (* 3 ($R1 x)) (* 2 N)) (= ($Dec x) 0)) ) (not (and (= ($H x) 2) (> (* 3 ($R2 x)) (* 2 N)) (= ($Dec x) 1)) ) (not (and (= ($H x) 1) (> (* 3 ($R1 x)) (* 2 N)) (= ($Dec x) 2)) ) ) (and (= ((primed $Dec) x) ($Dec x)) (= ((primed $Rev) x) ($Rev x)) (= ((primed $H) x) ($H x)) ) ) ) ;; ;; the other values stay the same (forall ((x Int)) (and (= ((primed $R1) x) ((primed $R1) x)) (= ((primed $R2) x) ($R2 x)) ) ) )) ;;Declare invariants (invariant (exists (($ID1 Int) ($ID2 Int) ($IH1 Int) ($IH2 Int) ($IR1 Int) ($IR2 Int) ($Irv Int)) ; (and (= (+ $IH2 $IH1) N) (or (and (= pc 1) (=> (> $ID1 0) (> (* 3 $IH1) (* 2 N))) (=> (> $ID2 0) (> (* 3 $IH2) (* 2 N))) (= $Irv 0) ) (and (= pc 2) (=> (> $ID1 0) (> (* 3 $IH1) (* 2 N))) (=> (> $ID2 0) (> (* 3 $IH2) (* 2 N))) (= N $IR1) (= N $IR2) (= $Irv 0) ) ) (= $ID1 (card ((x Int)) (= ($Dec x) 1)) ) (= $ID2 (card ((x Int)) (= ($Dec x) 2)) ) (= $IH1 (card ((x Int)) (= ($H x) 1)) ) (= $IH2 (card ((x Int)) (= ($H x) 2)) ) (= $IR1 (card ((x Int)) (<= ($R1 x) $IH1)) ) (= $IR2 (card ((x Int)) (<= ($R2 x) $IH2)) ) (= $Irv (card ((x Int)) (> ($Rev 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 )