Skip to content

MM2 Example: CTL model checking

Jump to bottom
AnnelineD edited this page Feb 25, 2026 · 10 revisions

We implement Computation Tree Logic (CTL) model checking in MM2 over a Kripke model.

To test the implementation, we use the rocket model from Wojciech Jamroga's Logical Methods for Specification and Verification of Multi-Agent Systems (see p. 32 for a graphical representation of the model).

The CTL checker is not limited to this example: you can include your own transition system and CTL formulas to experiment with other models.

To run the checker, concatenate the transition system definition and the CTL model-checking code, and execute them together. To run the included tests, simply concatenate the test code as well.

We implement a minimal set of CTL operators and derive the remaining operators from this core fragment.

  • Minimal operator set:
    • atomic proposition
    • negation (~)
    • conjunction (&)
    • EX
    • EU
    • EG

All other CTL operators are derived from this core set (and are unfolded accordingly in the MM2 code):

  • All other operations can be derived from these basic operators (which the MM2 code also does):
    • p -> q ≡ ~p v q
    • EF(p) ≡ E[true U p]
    • AX(p) ≡ ~(EX(~p))
    • AF(p) ≡ ~(EG(~p))
    • AG(p) ≡ ~E[trueU~p]
    • A[pUq] ≡ ~E[~qU(~p&~q)]&~EG~q
;==========================================================
;               KRIPKE MODEL AND STATEMENTS
;==========================================================
;----------------------------------------------------------
; 1. ROCKET DOMAIN KRIPKE MODEL
;----------------------------------------------------------
(t 1 1) (t 1 2) (t 1 5) (t 1 6)
(t 2 2) (t 2 3) (t 2 6)
(t 3 3) (t 3 4)
(t 4 4) (t 4 1)
(t 5 5) (t 5 6) (t 5 1) (t 5 2)
(t 6 6) (t 6 2) (t 6 7)
(t 7 7) (t 7 8) (t 7 11) (t 7 12)
(t 8 8) (t 8 5) (t 8 12)
(t 9 9) (t 9 10)
(t 10 10) (t 10 11)
(t 11 11) (t 11 7) (t 11 8) (t 11 12)
(t 12 12) (t 12 8) (t 12 9)

(eval 1 roL) (eval 1 nofuel) (eval 1 caL)
(eval 2 roL) (eval 2 fuelOK) (eval 2 caL)
(eval 3 roP) (eval 3 nofuel) (eval 3 caL)
(eval 4 roP) (eval 4 fuelOK) (eval 4 caL)
(eval 5 roL) (eval 5 nofuel) (eval 5 caR)
(eval 6 roL) (eval 6 fuelOK) (eval 6 caR)
(eval 7 roP) (eval 7 nofuel) (eval 7 caR)
(eval 8 roP) (eval 8 fuelOK) (eval 8 caR)
(eval 9 roL) (eval 9 nofuel) (eval 9 caP)
(eval 10 roL) (eval 10 fuelOK) (eval 10 caP)
(eval 11 roP) (eval 11 nofuel) (eval 11 caP)
(eval 12 roP) (eval 12 fuelOK) (eval 12 caP)


;----------------------------------------------------------
; CTL STATEMENTS TO CHECK
;----------------------------------------------------------
(to_check ((fuelOK) EU ((caR) & (EX(caP)))))    ; 2, 6, 7, 8, 12
(to_check (AG((~(fuelOK)) -> (EF(fuelOK)))))    ; all


;==========================================================
;                   CTL MODEL CHECKING
;==========================================================
; By Anneline Daggelinckx


; Overview of the code
; 1. Arithmetic Operations                                  (data)
; 2. Preprocessing: build a dependency graph of todos       (exec (0 ...))
; 3. Unfold derived CTL operators into basic-operator todos (exec (1 ...))
; 4. Generate execution statements from todos using CTL operator algorithms    (exec (2 ...))
; 5. CTL operator model-checking algorithms                 (data)


;----------------------------------------------------------
; 1. ARITHMETIC OPERATIONS
;----------------------------------------------------------

(succ 0 1) (succ 1 2) (succ 2 3) (succ 3 4) (succ 4 5) (succ 5 6) (succ 6 7) (succ 7 8) (succ 8 9) (succ 9 10) (succ 10 11)
(succ 11 12) (succ 12 13) (succ 13 14) (succ 14 15) (succ 15 16) (succ 16 17) (succ 17 18) (succ 18 19) (succ 19 20)


(arith (1 - 0 = 1)) (arith (1 - 1 = 0))
(arith (2 - 0 = 2)) (arith (2 - 1 = 1)) (arith (2 - 2 = 0))
(arith (3 - 0 = 3)) (arith (3 - 1 = 2)) (arith (3 - 2 = 1)) (arith (3 - 3 = 0))
(arith (4 - 0 = 4)) (arith (4 - 1 = 3)) (arith (4 - 2 = 2)) (arith (4 - 3 = 1)) (arith (4 - 4 = 0))
(arith (5 - 0 = 5)) (arith (5 - 1 = 4)) (arith (5 - 2 = 3)) (arith (5 - 3 = 2)) (arith (5 - 4 = 1)) (arith (5 - 5 = 0))
(arith (6 - 0 = 6)) (arith (6 - 1 = 5)) (arith (6 - 2 = 4)) (arith (6 - 3 = 3)) (arith (6 - 4 = 2)) (arith (6 - 5 = 1)) (arith (6 - 6 = 0))
(arith (7 - 0 = 7)) (arith (7 - 1 = 6)) (arith (7 - 2 = 5)) (arith (7 - 3 = 4)) (arith (7 - 4 = 3)) (arith (7 - 5 = 2)) (arith (7 - 6 = 1)) (arith (7 - 7 = 0))
(arith (8 - 0 = 8)) (arith (8 - 1 = 7)) (arith (8 - 2 = 6)) (arith (8 - 3 = 5)) (arith (8 - 4 = 4)) (arith (8 - 5 = 3)) (arith (8 - 6 = 2)) (arith (8 - 7 = 1)) (arith (8 - 8 = 0))
(arith (9 - 0 = 9)) (arith (9 - 1 = 8)) (arith (9 - 2 = 7)) (arith (9 - 3 = 6)) (arith (9 - 4 = 5)) (arith (9 - 5 = 4)) (arith (9 - 6 = 3)) (arith (9 - 7 = 2)) (arith (9 - 8 = 1)) (arith (9 - 9 = 0))
(arith (10 - 0 = 10)) (arith (10 - 1 = 9)) (arith (10 - 2 = 8)) (arith (10 - 3 = 7)) (arith (10 - 4 = 6)) (arith (10 - 5 = 5)) (arith (10 - 6 = 4)) (arith (10 - 7 = 3)) (arith (10 - 8 = 2)) (arith (10 - 9 = 1)) (arith (10 - 10 = 0))


;----------------------------------------------------------
; 2. PREPROCESSING
; Number each layer of the CTL formula so we can work inside → outside.
; Example: model check ((fuelOK) EU (~caR))
;   (todo (0 0) (caR))
;   (todo (1 0) (fuelOK))
;   (todo (1 0) (~(caR)))
;   (todo (2 0) ((fuelOK) EU (~(caR))))
;----------------------------------------------------------
; 2.0 Initialize dependency graph               (wanted ...)
; 2.1 Expand dependency graph iteratively       (wanted ...)
; 2.2 Count the number of layers of the dependency graph    (total ...)
; 2.3 Turn the dependency graph upside down because we want to work inside → outside (todo ...)
;----------------------------------------------------------


; initialize dependency graph
; (to_check ((fuelOK) EU (~(caR)))) -> (wanted 1 ((fuelOK) EU (~(caR))))
(exec (0 0 0 0) (, (to_check $f)) (, (wanted 1 $f)))

; (wanted 1 ((fuelOK) EU (~(caR))))
;          |
;          v
; (wanted 1 ((fuelOK) EU (~(caR))))
; (wanted 2 (fuelOK)) (wanted 2 (~(caR)))
; (wanted 3 (caR))
(exec (0 1 0 1)     ; iterative exec statement
	(, (exec (0 1 0 $d) $ps $ts) (succ $d $e) (wanted $d $_))
	(,
		(exec (0 1 0 0) (, (wanted $d ($o $x))) (, (wanted $e $x)))
		(exec (0 1 0 0) (, (wanted $d ($x $o $y))) (, (wanted $e $x) (wanted $e $y)))
		(exec (0 1 0 $e) $ps $ts)
	)
)

; count the number of layers such that we can use it to turn the graph upside down
(exec (0 2 0 0)
	(, (wanted $i $_))
	(O (count (total $c) $c $i))
)

; Re-index layers so evaluation proceeds inside → outside
; Use tuples such that we can insert todos when unfolding derived operators
; (wanted 1 ((fuelOK) EU (~(caR))))
; (wanted 2 (fuelOK)) (wanted 2 (~(caR)))
; (wanted 3 (caR))
;           |
;           v
; (todo (0 0) (caR))
; (todo (1 0) (fuelOK)) (todo (1 0) (~(caR)))
; (todo (2 0) ((fuelOK) EU (~(caR))))
(exec (0 3 0 0)
	(, (wanted $i $p) (total $t) (arith ($t - $i = $j)))
	(O (+ (todo ($j 0) $p)) (- (wanted $i $p)) (- (total $t)))
)


;----------------------------------------------------------
; 3. UNFOLD DERIVED CTL OPERATORS INTO BASIC OPERATORS
; Example:
;   (todo (5 0) (AX(p)))
;           |
;           v
;   (todo (5 0) (~p))
;   (todo (5 1) (EX(~p)))
;   (todo (5 2) (~(EX(~p))))
;   (todo (5 3) (AX(p)))
;----------------------------------------------------------

; p -> q ≡ (~p) v q
(exec (1 0 0 0)
    (,
        (todo ($x1 $x2) ($p -> $q))
        (succ $x2 $x21)
		(succ $x21 $x22)
		(succ $x22 $x23)
    )
    (O
        (+ (todo ($x1 $x21) (~ $p)))
        (+ (todo ($x1 $x22) ((~ $p) v $q)))
        (- (todo ($x1 $x2) ($p -> $q)))
        (+ (todo ($x1 $x23) ($p -> $q)))
    )
)

; EF(p) ≡ E[true U p]
(exec (1 0 0 0) (, (todo ($x1 0) (EF $p)))
	(O
		(+ (todo ($x1 0) ((true) EU $p)))
		(- (todo ($x1 0) (EF $p)))
		(+ (todo ($x1 1) (EF $p)))
	)
)

; AX(p) ≡ ~(EX(~p))
(exec (1 0 0 0)
	(,
		(todo ($x1 $x2) (AX $p))
		(succ $x2 $x21)
		(succ $x21 $x22)
		(succ $x22 $x23)
	)
	(O
		(- (todo ($x1 $x2) (AX $p)))
		(+ (todo ($x1 $x2) (~ $p)))
		(+ (todo ($x1 $x21) (EX(~ $p))))
		(+ (todo ($x1 $x22) (~ (EX(~ $p)))))
		(+ (todo ($x1 $x23) (AX $p)))
	)
)


; AF(p) ≡ ~(EG(~p))
(exec (1 0 0 0)
	(,
		(todo ($x1 $x2) (AF $p))
		(succ $x2 $x21)
		(succ $x21 $x22)
		(succ $x22 $x23)
	)
	(O
		(- (todo ($x1 $x2) (AF $p)))
		(+ (todo ($x1 $x2) (~ $p)))
		(+ (todo ($x1 $x21) (EG(~ $p))))
		(+ (todo ($x1 $x22) (~ (EG(~ $p)))))
		(+ (todo ($x1 $x23) (AF $p)))
	)
)

; AG(p) ≡ ~E[trueU~p]
(exec (1 0 0 0)
	(,
		(todo ($x1 $x2) (AG $p))
		(succ $x2 $x21)
		(succ $x21 $x22)
		(succ $x22 $x23)
	)
	(O
		(- (todo ($x1 $x2) (AG $p)))
		(+ (todo ($x1 $x2) (~ $p)))
		(+ (todo ($x1 $x21) ((true) EU (~ $p))))
		(+ (todo ($x1 $x22) (~ ((true) EU (~ $p)))))
		(+ (todo ($x1 $x23) (AG $p)))
	)
)


; A[pUq] ≡ ~E[~qU((~p)&(~q))]&(~EG(~q))
(exec (1 0 0 0)
	(,
		(todo ($x1 $x2) ($p AU $q))
		(succ $x2 $x21)
		(succ $x21 $x22)
		(succ $x22 $x23)
		(succ $x23 $x24)
		(succ $x24 $x25)
	)
	(O
		(- (todo ($x1 $x2) ($p AU $q)))
		(+ (todo ($x1 $x2) (~ $p)))
		(+ (todo ($x1 $x2) (~ $q)))
		(+ (todo ($x1 $x21) ((~ $p)&(~ $q))))
		(+ (todo ($x1 $x21) (EG(~ $q))))
		(+ (todo ($x1 $x22) ((~q) EU ((~ p)&(~ q)))))
		(+ (todo ($x1 $x22) (~ (EG(~ $q)))))
		(+ (todo ($x1 $x23) (~ ((~$q) EU ((~ $p)&(~ $q))))))
		(+ (todo ($x1 $x24) ((~ ((~$q) EU ((~ $p)&(~ $q)))) & (~ (EG(~ $q))))))
		(+ (todo ($x1 $x25) ($p AU $q)))
	)
)

;----------------------------------------------------------
; 4. TURN TODOS INTO EXEC STATEMENTS
; Generate execution statements from todos using the (check ...) statements from section 5
;----------------------------------------------------------

; in all states true is true
(exec (2 0 0 0) (, (eval $s $_)) (, (true (true) $s)))

; propositions
(exec (2 0 0 0)
	(, (todo ($x1 $x2) ($p)) ((check ($p) ($x1 $x2)) $ps $ts))
	(O (+ (exec (3 $x1 $x2 0) $ps $ts)) (- (todo ($x1 $x2) ($p))))
)

; unary operators
(exec (2 0 0 0)
	(, (todo ($x1 $x2) ($o $p)) ((check ($o $p) ($x1 $x2)) $ps $ts))
	(O (+ (exec (3 $x1 $x2 0) $ps $ts)) (- (todo ($x1 $x2) ($o $p))))
)

; binary operators
(exec (2 0 0 0)
	(, (todo ($x1 $x2) ($p1 $o $p2)) ((check ($p1 $o $p2) ($x1 $x2)) $ps $ts))
	(O (+ (exec (3 $x1 $x2 0) $ps $ts)) (- (todo ($x1 $x2) ($p1 $o $p2))))
)


;----------------------------------------------------------
; 5. CTL OPERATOR MODEL-CHECKING ALGORITHMS
;----------------------------------------------------------
; 5.1 Basic operators
; 5.2 Derived operators
;----------------------------------------------------------


;-- BASIC OPERATORS --------------------------------------

; PROPOSITION
; Sat(p)={s∣p∈eval(s)}

((check ($p) $x)
	(, (eval $s $p))
	(, (true ($p) $s))
)

; NEGATION
; Sat(~ψ)=S∖Sat(ψ)

((check (~ $p) ($x1 $x2))
	(, (eval $s1 $_))
	(O
		(+ (true (~ $p) $s1))
		(+ (exec (3 0 0 0)      ; Ensure removal of invalidated states takes priority
			(, (true $p $s2))
			(O (- (true (~ $p) $s2))))
		)
	)
)


; CONJUNCTION
; Sat(ψ1&ψ2)=Sat(ψ1)∩Sat(ψ2)

((check ($p1 & $p2) $x)
	(, (true $p1 $s) (true $p2 $s))
	(, (true ($p1 & $p2) $s))
)


; DISJUNCTION
; (this is strictly speaking not a basic operator, but easy to define)
((check ($p1 v $p2) ($x1 $x2))
	(, (true $p1 $s1) (true $p2 $s2))
	(, (true ($p1 v $p2) $s1) (true ($p1 v $p2) $s2))
)


; EX
; Sat(EXψ)={s1∣∃s2:(s1,s2)∈R&s2∈Sat(ψ)}

((check (EX $p) $x)
	(, (t $s1 $s2) (true $p $s2))
	(, (true (EX $p) $s1))
)


; EU
; Least fixpoint computation:
;   W0 = Sat(p2)
;   W(i+1) = Wi ∪ { s | s ∈ Sat(p1) ∧ ∃s' ∈ Wi : (s,s') ∈ R }
; Stops when no new states are added.


; iteration stop criterion -> no new states added!

((check ($p1 EU $p2) ($x1 $x2))
	(, (true $p2 $t))
	(,
		(true ($p1 EU $p2) $t)
		(new ($p1 EU $p2) $t)
		(exec (3 $x1 $x2 1)
			(,
				(exec (3 $x1 $x2 1) $ps $ts)
				(true $p1 $s) (t $s $sp) (true ($p1 EU $p2) $sp)
				(true ($p1 EU $p2) $v) (new ($p1 EU $p2) $_))
			(O
				(+ (true ($p1 EU $p2) $s))
				(+ (new ($p1 EU $p2) $s))
				(- (new ($p1 EU $p2) $v))
				(+ (exec (3 $x1 $x2 1) $ps $ts))
			)
		)
	)
)


; EG
; W0=Sat(ψ)
; W(i+1)={s∈Wi∣∃s′∈Wi:(s,s′)∈R}

((check (EG $p) ($x1 $x2))
	(, $_)
	(,
		(WIP (EG $p))
        (exec (3 $x1 0 0) (, (true $p $s)) (, (temp Z (EG $p) $s)))
		(exec (3 $x1 1 Z)
            (, (exec (3 $x1 1 $l) $ps $ts) (temp $l (EG $p) $s) (temp $l (EG $p) $t) (t $s $t) (WIP (EG $p)))
            (,
                (temp (S $l) (EG $p) $s)
                (exec (3 $x1 0 1) (, (temp (S $l) (EG $p) $s1)) (O (hash (h (S $l) (EG $p) $h) $h $s1)))
                (exec (3 $x1 0 2) (, (temp $l (EG $p) $s2)) (O (hash (h $l (EG $p) $h) $h $s2)))
                (exec (3 $x1 0 3) (, (h (S $l) (EG $p) $h1) (h $l (EG $p) $h1)) (O (- (WIP (EG $p)))
                                    (+ (exec (3 0 0 0) (, (temp $l (EG $p) $s5)) (, (true (EG $p) $s5))))
                                    (+ (exec (3 0 0 1) (, (h $x (EG $p) $y) (temp $m (EG $p) $v)) (O (- (h $x (EG $p) $y)) (- (temp $m (EG $p) $v)))))))
                (exec (3 $x1 1 (S $l)) $ps $ts)
            )
        )
	)
)

;-- Derived operators -------------------------------------
; p -> q ≡ ~p v q
((check ($p -> $q) ($x1 $x2))
	(, (true ((~ $p) v $q) $s))
	(, (true ($p -> $q) $s))
)


; EFp≡E[true U p]
((check (EF $p) ($x1 $x2))
	(, (true ((true) EU $p) $s))
	(, (true (EF $p) $s))
)

; -> AX(p)≡~(EX(~p))
((check (AX $p) ($x1 $x2))
	(, (true (~ (EX(~ $p))) $s))
	(, (true (AX $p) $s))
)


; -> AFp≡~(EG(~p))
((check (AF $p) ($x1 $x2))
	(, (true (~ (EG(~ $p))) $s))
	(, (true (AF $p) $s))
)

; -> AGp≡~E[trueU~p]
((check (AG $p) ($x1 $x2))
	(, (true (~ ((true) EU (~ $p))) $s))
	(, (true (AG $p) $s))
)


; A[p1Up2]≡ ~E[~p2U(~p1&~p2)]&~EG~p2
((check ($p AU $q) ($x1 $x2))
	(, (true ((~ ((~$q) EU ((~ $p)&(~ $q)))) & (~ (EG(~ $q)))) $s))
	(, (true ($p AU $q) $s))
)
Optional: tests

(to_check (caR)) (solution (caR) 5) (solution (caR) 6) (solution (caR) 7) (solution (caR) 8)

(to_check ((caR))) ; 1, 2, 3, 4, 9, 10, 11, 12 (solution ((caR)) 1) (solution ((caR)) 2) (solution ((caR)) 3) (solution ((caR)) 4) (solution ((caR)) 9) (solution ((caR)) 10) (solution ((caR)) 11) (solution (~(caR)) 12)

(to_check ((nevertrue))) ; all (solution ((nevertrue)) 1) (solution ((nevertrue)) 2) (solution ((nevertrue)) 3) (solution ((nevertrue)) 4) (solution ((nevertrue)) 5) (solution ((nevertrue)) 6) (solution ((nevertrue)) 7) (solution ((nevertrue)) 8) (solution ((nevertrue)) 9) (solution ((nevertrue)) 10) (solution ((nevertrue)) 11) (solution (~(nevertrue)) 12)

(to_check ((caR) & (fuelOK))) ; 6, 8 (solution ((caR) & (fuelOK)) 6) (solution ((caR) & (fuelOK)) 8)

(to_check (EX(caR))) ; 1, 2, 5, 6, 7, 8, 11, 12 (solution (EX(caR)) 1) (solution (EX(caR)) 2) (solution (EX(caR)) 5) (solution (EX(caR)) 6) (solution (EX(caR)) 7) (solution (EX(caR)) 8) (solution (EX(caR)) 11) (solution (EX(caR)) 12)

(to_check ((fuelOK) EU (caR))) ; 2, 5, 6, 7, 8, 12 (solution ((fuelOK) EU (caR)) 2) (solution ((fuelOK) EU (caR)) 5) (solution ((fuelOK) EU (caR)) 6) (solution ((fuelOK) EU (caR)) 7) (solution ((fuelOK) EU (caR)) 8) (solution ((fuelOK) EU (caR)) 12)

(to_check ((caR) EU (caL))) ; 1, 2, 3, 4, 5, 6, 7, 8 (solution ((caR) EU (caL)) 1) (solution ((caR) EU (caL)) 2) (solution ((caR) EU (caL)) 3) (solution ((caR) EU (caL)) 4) (solution ((caR) EU (caL)) 5) (solution ((caR) EU (caL)) 6) (solution ((caR) EU (caL)) 7) (solution ((caR) EU (caL)) 8)

(to_check (EG(fuelOK))) ; 2, 4, 6, 8, 10, 12 (solution (EG(fuelOK)) 2) (solution (EG(fuelOK)) 4) (solution (EG(fuelOK)) 6) (solution (EG(fuelOK)) 8) (solution (EG(fuelOK)) 10) (solution (EG(fuelOK)) 12)

(to_check (EF(caR))) ; all (solution (EF(caR)) 1) (solution (EF(caR)) 2) (solution (EF(caR)) 3) (solution (EF(caR)) 4) (solution (EF(caR)) 5) (solution (EF(caR)) 6) (solution (EF(caR)) 7) (solution (EF(caR)) 8) (solution (EF(caR)) 9) (solution (EF(caR)) 10) (solution (EF(caR)) 11) (solution (EF(caR)) 12)

(to_check (AX(roL))) ; 1, 5, 9 (solution (AX(roL)) 1) (solution (AX(roL)) 5) (solution (AX(roL)) 9)

(to_check (AF(caR))) ; 5, 6, 7, 8 (solution (AF(caR)) 5) (solution (AF(caR)) 6) (solution (AF(caR)) 7) (solution (AF(caR)) 8)

(to_check (AG((roL) v (caL)))) ; none

(to_check (AG((roL) v (roP)))) ; all (solution (AG((roL) v (roP))) 1) (solution (AG((roL) v (roP))) 2) (solution (AG((roL) v (roP))) 3) (solution (AG((roL) v (roP))) 4) (solution (AG((roL) v (roP))) 5) (solution (AG((roL) v (roP))) 6) (solution (AG((roL) v (roP))) 7) (solution (AG((roL) v (roP))) 8) (solution (AG((roL) v (roP))) 9) (solution (AG((roL) v (roP))) 10) (solution (AG((roL) v (roP))) 11) (solution (AG((roL) v (roP))) 12)

(to_check ((roL) -> (caL))) ; 1, 2, 3, 4, 7, 8, 11, 12 (solution ((roL) -> (caL)) 1) (solution ((roL) -> (caL)) 2) (solution ((roL) -> (caL)) 3) (solution ((roL) -> (caL)) 4) (solution ((roL) -> (caL)) 7) (solution ((roL) -> (caL)) 8) (solution ((roL) -> (caL)) 11) (solution ((roL) -> (caL)) 12)

; checks whether each EG is handled independently! (to_check ((EG(roL)) & (EG(caR)))) (solution ((EG (roL)) & (EG (caR))) 5) (solution ((EG (roL)) & (EG (caR))) 6)

(to_check ((fuelOK) EU ((caR) & (EX(caP))))) ; 2, 6, 7, 8, 12 (solution ((fuelOK) EU ((caR) & (EX(caP)))) 2) (solution ((fuelOK) EU ((caR) & (EX(caP)))) 6) (solution ((fuelOK) EU ((caR) & (EX(caP)))) 7) (solution ((fuelOK) EU ((caR) & (EX(caP)))) 8) (solution ((fuelOK) EU ((caR) & (EX(caP)))) 12)

(to_check (AG((caR) -> (AF(caP))))) ; none

(to_check (AG(((fuelOK)) -> (EF(fuelOK))))) ; all (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 1) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 2) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 3) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 4) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 5) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 6) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 7) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 8) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 9) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 10) (solution (AG(((fuelOK)) -> (EF(fuelOK)))) 11) (solution (AG((~(fuelOK)) -> (EF(fuelOK)))) 12)

; symmetric difference ; (A U B) \ (A /\ B) (exec (6 0 0 0) (, (to_check $p1) (true $p1 $s1)) (O (+ (MISTAKE $p1 $s1))) )

(exec (6 0 0 0) (, (to_check $p1) (solution $p1 $s1)) (O (+ (MISTAKE $p1 $s1))) )

(exec (6 1 0 0) (, (to_check $p) (true $p $s) (solution $p $s)) (O (- (MISTAKE $p $s))) )

Full program output 
(arith (1 - 0 = 1))
(arith (1 - 1 = 0))
(arith (2 - 0 = 2))
(arith (2 - 1 = 1))
(arith (2 - 2 = 0))
(arith (3 - 0 = 3))
(arith (3 - 1 = 2))
(arith (3 - 2 = 1))
(arith (3 - 3 = 0))
(arith (4 - 0 = 4))
(arith (4 - 1 = 3))
(arith (4 - 2 = 2))
(arith (4 - 3 = 1))
(arith (4 - 4 = 0))
(arith (5 - 0 = 5))
(arith (5 - 1 = 4))
(arith (5 - 2 = 3))
(arith (5 - 3 = 2))
(arith (5 - 4 = 1))
(arith (5 - 5 = 0))
(arith (6 - 0 = 6))
(arith (6 - 1 = 5))
(arith (6 - 2 = 4))
(arith (6 - 3 = 3))
(arith (6 - 4 = 2))
(arith (6 - 5 = 1))
(arith (6 - 6 = 0))
(arith (7 - 0 = 7))
(arith (7 - 1 = 6))
(arith (7 - 2 = 5))
(arith (7 - 3 = 4))
(arith (7 - 4 = 3))
(arith (7 - 5 = 2))
(arith (7 - 6 = 1))
(arith (7 - 7 = 0))
(arith (8 - 0 = 8))
(arith (8 - 1 = 7))
(arith (8 - 2 = 6))
(arith (8 - 3 = 5))
(arith (8 - 4 = 4))
(arith (8 - 5 = 3))
(arith (8 - 6 = 2))
(arith (8 - 7 = 1))
(arith (8 - 8 = 0))
(arith (9 - 0 = 9))
(arith (9 - 1 = 8))
(arith (9 - 2 = 7))
(arith (9 - 3 = 6))
(arith (9 - 4 = 5))
(arith (9 - 5 = 4))
(arith (9 - 6 = 3))
(arith (9 - 7 = 2))
(arith (9 - 8 = 1))
(arith (9 - 9 = 0))
(arith (10 - 0 = 10))
(arith (10 - 1 = 9))
(arith (10 - 2 = 8))
(arith (10 - 3 = 7))
(arith (10 - 4 = 6))
(arith (10 - 5 = 5))
(arith (10 - 6 = 4))
(arith (10 - 7 = 3))
(arith (10 - 8 = 2))
(arith (10 - 9 = 1))
(arith (10 - 10 = 0))
(to_check (AG ((~ (fuelOK)) -> (EF (fuelOK)))))
(to_check ((fuelOK) EU ((caR) & (EX (caP)))))
((EG iter (step 1)) (, (t $a $b) (Q1 $b) (Q1 $a) (Q1 $c)) (O (+ (to delete $c)) (- (to delete $a)) (- (WIP))))
((EG iter (step 2)) (, (to delete $a)) (O (- (Q1 $a)) (- (to delete $a)) (+ (WIP))))
((check ($a) $b) (, (eval $c $a)) (, (true ($a) $c)))
((check (~ $a) ($b $c)) (, (eval $d $e)) (O (+ (true (~ $a) $d)) (+ (exec (3 0 0 0) (, (true $a $f)) (O (- (true (~ $a) $f)))))))
((check (AF $a) ($b $c)) (, (true (~ (EG (~ $a))) $d)) (, (true (AF $a) $d)))
((check (AG $a) ($b $c)) (, (true (~ ((true) EU (~ $a))) $d)) (, (true (AG $a) $d)))
((check (AX $a) ($b $c)) (, (true (~ (EX (~ $a))) $d)) (, (true (AX $a) $d)))
((check (EF $a) ($b $c)) (, (true ((true) EU $a) $d)) (, (true (EF $a) $d)))
((check (EG $a) ($b $c)) (, (true $a $d)) (, (Q1 $d) (WIP) (exec (3 $b $c 3) (, (exec (3 $b $c 3) $e $f) (WIP) ((EG iter (step $g)) $h $i)) (, (exec (3 $b $c $g) $h $i) (exec (3 $b $c 3) $e $f))) (exec (3 $b $c 4) (, (Q1 $j)) (O (+ (true (EG $a) $j)) (- (Q1 $j))))))
((check (EX $a) $b) (, (t $c $d) (true $a $d)) (, (true (EX $a) $c)))
((check ($a & $b) $c) (, (true $a $d) (true $b $d)) (, (true ($a & $b) $d)))
((check ($a v $b) ($c $d)) (, (true $a $e) (true $b $f)) (, (true ($a v $b) $e) (true ($a v $b) $f)))
((check ($a -> $b) ($c $d)) (, (true ((~ $a) v $b) $e)) (, (true ($a -> $b) $e)))
((check ($a AU $b) ($c $d)) (, (true ((~ ((~$q) EU ((~ $a) & (~ $b)))) & (~ (EG (~ $b)))) $e)) (, (true ($a AU $b) $e)))
((check ($a EU $b) ($c $d)) (, (true $b $e)) (, (true ($a EU $b) $e) (new ($a EU $b) $e) (exec (3 $c $d 1) (, (exec (3 $c $d 1) $f $g) (true $a $h) (t $h $i) (true ($a EU $b) $i) (true ($a EU $b) $j) (new ($a EU $b) $x10)) (O (+ (true ($a EU $b) $h)) (+ (new ($a EU $b) $h)) (- (new ($a EU $b) $j)) (+ (exec (3 $c $d 1) $f $g))))))
(t 1 1)
(t 1 2)
(t 1 5)
(t 1 6)
(t 2 2)
(t 2 3)
(t 2 6)
(t 3 3)
(t 3 4)
(t 4 1)
(t 4 4)
(t 5 1)
(t 5 2)
(t 5 5)
(t 5 6)
(t 6 2)
(t 6 6)
(t 6 7)
(t 7 7)
(t 7 8)
(t 7 11)
(t 7 12)
(t 8 5)
(t 8 8)
(t 8 12)
(t 9 9)
(t 9 10)
(t 10 10)
(t 10 11)
(t 11 7)
(t 11 8)
(t 11 11)
(t 11 12)
(t 12 8)
(t 12 9)
(t 12 12)
(eval 1 caL)
(eval 1 roL)
(eval 1 nofuel)
(eval 2 caL)
(eval 2 roL)
(eval 2 fuelOK)
(eval 3 caL)
(eval 3 roP)
(eval 3 nofuel)
(eval 4 caL)
(eval 4 roP)
(eval 4 fuelOK)
(eval 5 caR)
(eval 5 roL)
(eval 5 nofuel)
(eval 6 caR)
(eval 6 roL)
(eval 6 fuelOK)
(eval 7 caR)
(eval 7 roP)
(eval 7 nofuel)
(eval 8 caR)
(eval 8 roP)
(eval 8 fuelOK)
(eval 9 caP)
(eval 9 roL)
(eval 9 nofuel)
(eval 10 caP)
(eval 10 roL)
(eval 10 fuelOK)
(eval 11 caP)
(eval 11 roP)
(eval 11 nofuel)
(eval 12 caP)
(eval 12 roP)
(eval 12 fuelOK)
(succ 0 1)
(succ 1 2)
(succ 2 3)
(succ 3 4)
(succ 4 5)
(succ 5 6)
(succ 6 7)
(succ 7 8)
(succ 8 9)
(succ 9 10)
(succ 10 11)
(succ 11 12)
(succ 12 13)
(succ 13 14)
(succ 14 15)
(succ 15 16)
(succ 16 17)
(succ 17 18)
(succ 18 19)
(succ 19 20)
(true (caP) 9)
(true (caP) 10)
(true (caP) 11)
(true (caP) 12)
(true (caR) 5)
(true (caR) 6)
(true (caR) 7)
(true (caR) 8)
(true (true) 1)
(true (true) 2)
(true (true) 3)
(true (true) 4)
(true (true) 5)
(true (true) 6)
(true (true) 7)
(true (true) 8)
(true (true) 9)
(true (true) 10)
(true (true) 11)
(true (true) 12)
(true (fuelOK) 2)
(true (fuelOK) 4)
(true (fuelOK) 6)
(true (fuelOK) 8)
(true (fuelOK) 10)
(true (fuelOK) 12)
(true (~ (fuelOK)) 1)
(true (~ (fuelOK)) 3)
(true (~ (fuelOK)) 5)
(true (~ (fuelOK)) 7)
(true (~ (fuelOK)) 9)
(true (~ (fuelOK)) 11)
(true (~ (~ (fuelOK))) 2)
(true (~ (~ (fuelOK))) 4)
(true (~ (~ (fuelOK))) 6)
(true (~ (~ (fuelOK))) 8)
(true (~ (~ (fuelOK))) 10)
(true (~ (~ (fuelOK))) 12)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 1)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 2)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 3)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 4)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 5)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 6)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 7)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 8)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 9)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 10)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 11)
(true (~ ((true) EU (~ ((~ (fuelOK)) -> (EF (fuelOK)))))) 12)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 1)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 2)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 3)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 4)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 5)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 6)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 7)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 8)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 9)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 10)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 11)
(true (AG ((~ (fuelOK)) -> (EF (fuelOK)))) 12)
(true (EF (fuelOK)) 1)
(true (EF (fuelOK)) 2)
(true (EF (fuelOK)) 3)
(true (EF (fuelOK)) 4)
(true (EF (fuelOK)) 5)
(true (EF (fuelOK)) 6)
(true (EF (fuelOK)) 7)
(true (EF (fuelOK)) 8)
(true (EF (fuelOK)) 9)
(true (EF (fuelOK)) 10)
(true (EF (fuelOK)) 11)
(true (EF (fuelOK)) 12)
(true (EX (caP)) 7)
(true (EX (caP)) 8)
(true (EX (caP)) 9)
(true (EX (caP)) 10)
(true (EX (caP)) 11)
(true (EX (caP)) 12)
(true ((caR) & (EX (caP))) 7)
(true ((caR) & (EX (caP))) 8)
(true ((true) EU (fuelOK)) 1)
(true ((true) EU (fuelOK)) 2)
(true ((true) EU (fuelOK)) 3)
(true ((true) EU (fuelOK)) 4)
(true ((true) EU (fuelOK)) 5)
(true ((true) EU (fuelOK)) 6)
(true ((true) EU (fuelOK)) 7)
(true ((true) EU (fuelOK)) 8)
(true ((true) EU (fuelOK)) 9)
(true ((true) EU (fuelOK)) 10)
(true ((true) EU (fuelOK)) 11)
(true ((true) EU (fuelOK)) 12)
(true ((fuelOK) EU ((caR) & (EX (caP)))) 2)
(true ((fuelOK) EU ((caR) & (EX (caP)))) 6)
(true ((fuelOK) EU ((caR) & (EX (caP)))) 7)
(true ((fuelOK) EU ((caR) & (EX (caP)))) 8)
(true ((fuelOK) EU ((caR) & (EX (caP)))) 12)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 1)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 2)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 3)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 4)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 5)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 6)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 7)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 8)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 9)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 10)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 11)
(true ((~ (fuelOK)) -> (EF (fuelOK))) 12)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 1)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 2)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 3)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 4)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 5)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 6)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 7)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 8)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 9)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 10)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 11)
(true ((~ (~ (fuelOK))) v (EF (fuelOK))) 12)

Clone this wiki locally