Revision 4f3cc9f3
Added by Pierre-Loïc Garoche over 9 years ago
| ex3_correct.smt2 | ||
|---|---|---|
| 4 | 4 |
(declare-var COUNTER.X Bool) |
| 5 | 5 |
(declare-var COUNTER.reset Bool) |
| 6 | 6 |
(declare-var COUNTER.C Int) |
| 7 |
(declare-var COUNTER.COUNTER.__COUNTER_1_c Int)
|
|
| 8 |
(declare-var COUNTER.COUNTER.__COUNTER_1_x Int)
|
|
| 7 |
(declare-var COUNTER.__COUNTER_1_c Int) |
|
| 8 |
(declare-var COUNTER.__COUNTER_1_x Int) |
|
| 9 | 9 |
(declare-var COUNTER.PC Int) |
| 10 | 10 |
(declare-rel COUNTER_init (Int Int Bool Bool Int Int)) |
| 11 | 11 |
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int)) |
| ... | ... | |
| 14 | 14 |
(and (= COUNTER.PC COUNTER.init) |
| 15 | 15 |
(= COUNTER.C (ite COUNTER.reset COUNTER.init |
| 16 | 16 |
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC))) |
| 17 |
(= COUNTER.COUNTER.__COUNTER_1_x COUNTER.C)
|
|
| 17 |
(= COUNTER.__COUNTER_1_x COUNTER.C) |
|
| 18 | 18 |
) |
| 19 |
(COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_x)
|
|
| 19 |
(COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_x) |
|
| 20 | 20 |
)) |
| 21 | 21 |
|
| 22 | 22 |
(rule (=> |
| 23 |
(and (= COUNTER.PC COUNTER.COUNTER.__COUNTER_1_c)
|
|
| 23 |
(and (= COUNTER.PC COUNTER.__COUNTER_1_c) |
|
| 24 | 24 |
(= COUNTER.C (ite COUNTER.reset COUNTER.init |
| 25 | 25 |
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC))) |
| 26 |
(= COUNTER.COUNTER.__COUNTER_1_x COUNTER.C)
|
|
| 26 |
(= COUNTER.__COUNTER_1_x COUNTER.C) |
|
| 27 | 27 |
) |
| 28 |
(COUNTER_step COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_c COUNTER.COUNTER.__COUNTER_1_x)
|
|
| 28 |
(COUNTER_step COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.__COUNTER_1_c COUNTER.__COUNTER_1_x)
|
|
| 29 | 29 |
)) |
| 30 | 30 |
|
| 31 | 31 |
; speed |
| ... | ... | |
| 33 | 33 |
(declare-var speed.second Bool) |
| 34 | 34 |
(declare-var speed.late Bool) |
| 35 | 35 |
(declare-var speed.early Bool) |
| 36 |
(declare-var speed.speed.__speed_3_c Bool)
|
|
| 37 |
(declare-var speed.speed.__speed_6_c Bool)
|
|
| 36 |
(declare-var speed.__speed_3_c Bool) |
|
| 37 |
(declare-var speed.__speed_6_c Bool) |
|
| 38 | 38 |
(declare-var speed.ni_4.COUNTER.__COUNTER_1_c Int) |
| 39 |
(declare-var speed.speed.__speed_3_x Bool)
|
|
| 40 |
(declare-var speed.speed.__speed_6_x Bool)
|
|
| 39 |
(declare-var speed.__speed_3_x Bool) |
|
| 40 |
(declare-var speed.__speed_6_x Bool) |
|
| 41 | 41 |
(declare-var speed.ni_4.COUNTER.__COUNTER_1_x Int) |
| 42 | 42 |
(declare-var speed.__speed_1 Bool) |
| 43 | 43 |
(declare-var speed.__speed_2 Bool) |
| ... | ... | |
| 55 | 55 |
(= speed.__speed_1 (and speed.beacon (not speed.second))) |
| 56 | 56 |
(= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0))) |
| 57 | 57 |
(COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x) |
| 58 |
(= speed.__speed_7 speed.speed.__speed_6_c)
|
|
| 58 |
(= speed.__speed_7 speed.__speed_6_c) |
|
| 59 | 59 |
(= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0) |
| 60 | 60 |
(<= speed.diff (- 10)))) |
| 61 | 61 |
(= speed.late false) |
| 62 |
(= speed.__speed_4 speed.speed.__speed_3_c)
|
|
| 62 |
(= speed.__speed_4 speed.__speed_3_c) |
|
| 63 | 63 |
(= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0) |
| 64 | 64 |
(>= speed.diff 10))) |
| 65 | 65 |
(= speed.early false) |
| 66 |
(= speed.speed.__speed_6_x speed.late)
|
|
| 67 |
(= speed.speed.__speed_3_x speed.early)
|
|
| 66 |
(= speed.__speed_6_x speed.late) |
|
| 67 |
(= speed.__speed_3_x speed.early) |
|
| 68 | 68 |
) |
| 69 |
(speed_init speed.beacon speed.second speed.late speed.early speed.speed.__speed_3_x speed.speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 69 |
(speed_init speed.beacon speed.second speed.late speed.early speed.__speed_3_x speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 70 | 70 |
)) |
| 71 | 71 |
|
| 72 | 72 |
(rule (=> |
| ... | ... | |
| 74 | 74 |
(= speed.__speed_1 (and speed.beacon (not speed.second))) |
| 75 | 75 |
(= speed.incr (ite speed.__speed_1 1 (ite speed.__speed_2 2 0))) |
| 76 | 76 |
(COUNTER_step 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_c speed.ni_4.COUNTER.__COUNTER_1_x) |
| 77 |
(= speed.__speed_7 speed.speed.__speed_6_c)
|
|
| 77 |
(= speed.__speed_7 speed.__speed_6_c) |
|
| 78 | 78 |
(= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0) |
| 79 | 79 |
(<= speed.diff (- 10)))) |
| 80 | 80 |
(= speed.late speed.__speed_8) |
| 81 |
(= speed.__speed_4 speed.speed.__speed_3_c)
|
|
| 81 |
(= speed.__speed_4 speed.__speed_3_c) |
|
| 82 | 82 |
(= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0) |
| 83 | 83 |
(>= speed.diff 10))) |
| 84 | 84 |
(= speed.early speed.__speed_5) |
| 85 |
(= speed.speed.__speed_6_x speed.late)
|
|
| 86 |
(= speed.speed.__speed_3_x speed.early)
|
|
| 85 |
(= speed.__speed_6_x speed.late) |
|
| 86 |
(= speed.__speed_3_x speed.early) |
|
| 87 | 87 |
) |
| 88 |
(speed_step speed.beacon speed.second speed.late speed.early speed.speed.__speed_3_c speed.speed.__speed_6_c speed.ni_4.COUNTER.__COUNTER_1_c speed.speed.__speed_3_x speed.speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 88 |
(speed_step speed.beacon speed.second speed.late speed.early speed.__speed_3_c speed.__speed_6_c speed.ni_4.COUNTER.__COUNTER_1_c speed.__speed_3_x speed.__speed_6_x speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 89 | 89 |
)) |
| 90 | 90 |
|
| 91 | 91 |
; top |
| 92 | 92 |
(declare-var top.beacon Bool) |
| 93 | 93 |
(declare-var top.second Bool) |
| 94 | 94 |
(declare-var top.OK Bool) |
| 95 |
(declare-var top.top.__top_1_c Bool)
|
|
| 95 |
(declare-var top.__top_1_c Bool) |
|
| 96 | 96 |
(declare-var top.ni_1.speed.__speed_3_c Bool) |
| 97 | 97 |
(declare-var top.ni_1.speed.__speed_6_c Bool) |
| 98 | 98 |
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int) |
| 99 |
(declare-var top.top.__top_1_x Bool)
|
|
| 99 |
(declare-var top.__top_1_x Bool) |
|
| 100 | 100 |
(declare-var top.ni_1.speed.__speed_3_x Bool) |
| 101 | 101 |
(declare-var top.ni_1.speed.__speed_6_x Bool) |
| 102 | 102 |
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int) |
| ... | ... | |
| 108 | 108 |
(rule (=> |
| 109 | 109 |
(and (speed_init top.beacon top.second top.late top.early top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x) |
| 110 | 110 |
(= top.OK true) |
| 111 |
(= top.top.__top_1_x top.early)
|
|
| 111 |
(= top.__top_1_x top.early) |
|
| 112 | 112 |
) |
| 113 |
(top_init top.beacon top.second top.OK top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 113 |
(top_init top.beacon top.second top.OK top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x) |
|
| 114 | 114 |
)) |
| 115 | 115 |
|
| 116 | 116 |
(rule (=> |
| 117 | 117 |
(and (speed_step top.beacon top.second top.late top.early top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x) |
| 118 |
(= top.OK (or (not top.top.__top_1_c) (not top.late)))
|
|
| 119 |
(= top.top.__top_1_x top.early)
|
|
| 118 |
(= top.OK (or (not top.__top_1_c) (not top.late))) |
|
| 119 |
(= top.__top_1_x top.early) |
|
| 120 | 120 |
) |
| 121 |
(top_step top.beacon top.second top.OK top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 121 |
(top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 122 | 122 |
)) |
| 123 | 123 |
|
| 124 | 124 |
; Collecting semantics with main node top |
| ... | ... | |
| 129 | 129 |
(rule INIT_STATE) |
| 130 | 130 |
(rule (=> |
| 131 | 131 |
(and INIT_STATE |
| 132 |
(top_init top.beacon top.second top.OK top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 132 |
(top_init top.beacon top.second top.OK top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x) |
|
| 133 | 133 |
) |
| 134 |
(MAIN top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x top.OK)
|
|
| 134 |
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x top.OK) |
|
| 135 | 135 |
)) |
| 136 | 136 |
|
| 137 | 137 |
; Inductive def |
| 138 | 138 |
(declare-var dummy Bool) |
| 139 | 139 |
(rule (=> |
| 140 |
(and (MAIN top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c dummy)
|
|
| 141 |
(top_step top.beacon top.second top.OK top.top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 140 |
(and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c dummy) |
|
| 141 |
(top_step top.beacon top.second top.OK top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 142 | 142 |
) |
| 143 |
(MAIN top.top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x top.OK)
|
|
| 143 |
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x top.OK) |
|
| 144 | 144 |
)) |
| 145 | 145 |
|
| 146 | 146 |
; Property def |
| 147 | 147 |
(declare-rel ERR ()) |
| 148 | 148 |
(rule (=> |
| 149 | 149 |
(and (not (= top.OK true)) |
| 150 |
(MAIN top.top.__top_1_c top.ni_1.speed.__speed_3_c
|
|
| 150 |
(MAIN top.__top_1_c top.ni_1.speed.__speed_3_c |
|
| 151 | 151 |
top.ni_1.speed.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.OK)) |
| 152 | 152 |
ERR)) |
| 153 | 153 |
(query ERR) |
Also available in: Unified diff
Is it working?