;; =================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 ;; parameters used in unsafe formula (declare-fun F () Int) ;; Declare global variables ;; Global variables identifiers starts with $ ;; r is the round counter ;; program counter (declare-fun pc () Int) ;; Declare local variables (i.e. array variables) ;; Local variables identifiers also starts with $ ;; ;; H(x) is the location of x (declare-fun $H (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) (forall ((x Int)) (= ($H x) 5 )) )) ;; Declare unsafe formula (unsafe (and (= pc 1) (> F 1) (= F (card ((x Int)) (= ($H x) 1)) ) )) ;;Declare transition (transition :name t1 (exists (($K1 Int) ($K2 Int) ($K3 Int) ($K4 Int) ($K5 Int) ($H1 Int) ($H2 Int) ($H3 Int) ($H4 Int) ($H5 Int) ) (and (and (= pc 1) (= (primed pc) 1)) (and (> $K3 0) (= $H2 $K2) (= (+ $H3 1) $K3) (= $H4 $K4) (= $H1 (+ $K1 1)) ) (= $K1 (card ((x Int)) (= ($H x) 1)) ) (= $K2 (card ((x Int)) (= ($H x) 2)) ) (= $K3 (card ((x Int)) (= ($H x) 3)) ) (= $K4 (card ((x Int)) (= ($H x) 4)) ) (= $K5 (card ((x Int)) (= ($H x) 5)) ) (= $H1 (card ((x Int)) (= ((primed $H) x) 1)) ) (= $H2 (card ((x Int)) (= ((primed $H) x) 2)) ) (= $H3 (card ((x Int)) (= ((primed $H) x) 3)) ) (= $H4 (card ((x Int)) (= ((primed $H) x) 4)) ) (= $H5 (card ((x Int)) (= ((primed $H) x) 5)) ) ))) ;;Declare transition (transition :name t2 (exists (($K1 Int) ($K2 Int) ($K3 Int) ($K4 Int) ($K5 Int) ($H1 Int) ($H2 Int) ($H3 Int) ($H4 Int) ($H5 Int)) (and (and (= pc 1) (= (primed pc) 1)) (and (> $K5 0) (= $H4 (+ $K3 $K4 1)) (= $H2 (+ $K1 $K2)) (= (+ $H5 1) $K5 ) (= $H3 0) (= $H1 0) ) (= $K1 (card ((x Int)) (= ($H x) 1)) ) (= $K2 (card ((x Int)) (= ($H x) 2)) ) (= $K3 (card ((x Int)) (= ($H x) 3)) ) (= $K4 (card ((x Int)) (= ($H x) 4)) ) (= $K5 (card ((x Int)) (= ($H x) 5)) ) (= $H1 (card ((x Int)) (= ((primed $H) x) 1)) ) (= $H2 (card ((x Int)) (= ((primed $H) x) 2)) ) (= $H3 (card ((x Int)) (= ((primed $H) x) 3)) ) (= $H4 (card ((x Int)) (= ((primed $H) x) 4)) ) (= $H5 (card ((x Int)) (= ((primed $H) x) 5)) ) ))) ;;Declare transition (transition :name t3 (exists (($K1 Int) ($K2 Int) ($K3 Int) ($K4 Int) ($K5 Int) ($H1 Int) ($H2 Int) ($H3 Int) ($H4 Int) ($H5 Int)) (and (and (= pc 1) (= (primed pc) 1)) (and (> $K4 0) (= $H3 1) (= $H1 0) (= $H3 0) (= $H2 0) (= $H4 0) (= (+ $H5 1) (+ $K1 $K2 $K3 $K4 $K5)) ) (= $K1 (card ((x Int)) (= ($H x) 1)) ) (= $K2 (card ((x Int)) (= ($H x) 2)) ) (= $K3 (card ((x Int)) (= ($H x) 3)) ) (= $K4 (card ((x Int)) (= ($H x) 4)) ) (= $K5 (card ((x Int)) (= ($H x) 5)) ) (= $H1 (card ((x Int)) (= ((primed $H) x) 1)) ) (= $H2 (card ((x Int)) (= ((primed $H) x) 2)) ) (= $H3 (card ((x Int)) (= ((primed $H) x) 3)) ) (= $H4 (card ((x Int)) (= ((primed $H) x) 4)) ) (= $H5 (card ((x Int)) (= ((primed $H) x) 5)) ) ))) ;;Declare transition (transition :name t4 (exists (($K1 Int) ($K2 Int) ($K3 Int) ($K4 Int) ($K5 Int) ($H1 Int) ($H2 Int) ($H3 Int) ($H4 Int) ($H5 Int)) (and (and (= pc 1) (= (primed pc) 1)) (and (> $K2 0) (= $H3 1) (= $H1 0) (= $H3 0) (= $H2 0) (= $H4 0) (= (+ $H5 1) (+ $K1 $K2 $K3 $K4 $K5)) ) (= $K1 (card ((x Int)) (= ($H x) 1)) ) (= $K2 (card ((x Int)) (= ($H x) 2)) ) (= $K3 (card ((x Int)) (= ($H x) 3)) ) (= $K4 (card ((x Int)) (= ($H x) 4)) ) (= $K5 (card ((x Int)) (= ($H x) 5)) ) (= $H1 (card ((x Int)) (= ((primed $H) x) 1)) ) (= $H2 (card ((x Int)) (= ((primed $H) x) 2)) ) (= $H3 (card ((x Int)) (= ((primed $H) x) 3)) ) (= $H4 (card ((x Int)) (= ((primed $H) x) 4)) ) (= $H5 (card ((x Int)) (= ((primed $H) x) 5)) ) ))) ;;Declare transition (transition :name t5 (exists (($K1 Int) ($K2 Int) ($K3 Int) ($K4 Int) ($K5 Int) ($H1 Int) ($H2 Int) ($H3 Int) ($H4 Int) ($H5 Int)) (and (and (= pc 1) (= (primed pc) 1)) (and (> $K5 0) (= $H3 1) (= $H1 0) (= $H3 0) (= $H2 0) (= $H4 0) (= (+ $H5 1) (+ $K1 $K2 $K3 $K4 $K5)) ) (= $K1 (card ((x Int)) (= ($H x) 1)) ) (= $K2 (card ((x Int)) (= ($H x) 2)) ) (= $K3 (card ((x Int)) (= ($H x) 3)) ) (= $K4 (card ((x Int)) (= ($H x) 4)) ) (= $K5 (card ((x Int)) (= ($H x) 5)) ) (= $H1 (card ((x Int)) (= ((primed $H) x) 1)) ) (= $H2 (card ((x Int)) (= ((primed $H) x) 2)) ) (= $H3 (card ((x Int)) (= ((primed $H) x) 3)) ) (= $H4 (card ((x Int)) (= ((primed $H) x) 4)) ) (= $H5 (card ((x Int)) (= ((primed $H) x) 5)) ) ))) (declare-fun c1 () Int) ;;Declare invariants (invariant (exists (($R Int)) (and (<= $R 1) (= $R (card ((x Int)) (or (= ($H x) 1) (= ($H x) 3) ) )) )) ;;This is optional (just in case an invariant is known) ;;One should supply one declaration for each location following the general syntax instructions above )