Repository navigation
MM2 Example: CTL model checking
AnnelineD edited this page Feb 6, 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).
This CTL checker also works on other models, so feel free to include your own model and CTL statements to check.
Limitations/WIP:
-
At the moment, only a minimal set of CTL operators is implemented:
- atomic proposition
- negation
- conjunction
- EX
- EU
- EG
All other operations can be derived from these primitives:
- EFφ ≡ E[true U φ]
- AX(φ) ≡ ¬(EX(¬φ))
- AFφ ≡ ¬(EG(¬φ))
- AGφ ≡ ¬E[trueU¬φ]
- A[φ1Uφ2] ≡ ¬E[¬φ2U(¬φ1∧¬φ2)]∧¬EG¬φ2
-
Currently, users must manually construct a dependency graph for the CTL formula to be checked.
- e.g., for the formula (¬ (roL))∧(¬(caL)), the dependency graph must be written as:
- (todo 1 (roL))
- (todo 1 (caL))
- (todo 2 (¬ (roL)))
- (todo 2 (¬ (caL)))
- (todo 3 ((¬ (roL))∧(¬(caL))))
- e.g., for the formula (¬ (roL))∧(¬(caL)), the dependency graph must be written as:
Both of the above limitations are work in progress. These features will be added soon (in the coming days)!
;==========================================================
; 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 0 0 0) (, (wanted $d ($o $x))) (, (wanted $e $x)))
(exec (0 0 0 0) (, (wanted $d ($x $o $y))) (, (wanted $e $x) (wanted $e $y)))
(exec (0 0 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))
(, (true $p $t))
(,
(Q1 $t) (WIP)
(exec (3 $x1 $x2 3) ;iterative exec
(, (exec (3 $x1 $x2 3) $ps $ts) (WIP) ((EG iter (step $i)) $psi $tsi))
(,
(exec (3 $x1 $x2 $i) $psi $tsi)
(exec (3 $x1 $x2 3) $ps $ts)
)
)
(exec (3 $x1 $x2 4)
(, (Q1 $s))
(O (+ (true (EG $p) $s)) (- (Q1 $s)))
)
)
)
((EG iter (step 1))
(, (t $s $sp) (Q1 $sp) (Q1 $s) (Q1 $v))
(O
(+(to delete $v))
(-(to delete $s))
(- (WIP))
)
)
((EG iter (step 2))
(, (to delete $s))
(O (- (Q1 $s)) (- (to delete $s)) (+ (WIP)))
)
;-- 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))
)
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)