Revision 4f3cc9f3
Added by Pierre-Loïc Garoche over 9 years ago
| ex3.smt2 | ||
|---|---|---|
| 54 | 54 |
(and (= speed.__speed_2 (and speed.second (not speed.beacon))) |
| 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 |
(COUNTER_init 0 speed.incr (or speed.beacon speed.second) 0 speed.diff speed.__COUNTER_1_x)
|
|
| 57 |
(COUNTER_init 0 speed.incr (or speed.beacon speed.second) false speed.diff speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 58 | 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 |
(= speed.late 0)
|
|
| 61 |
(= speed.late false)
|
|
| 62 | 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 |
(= speed.early 0)
|
|
| 65 |
(= speed.early false)
|
|
| 66 | 66 |
(= speed.__speed_6_x speed.late) |
| 67 | 67 |
(= speed.__speed_3_x speed.early) |
| 68 | 68 |
) |
| ... | ... | |
| 73 | 73 |
(and (= speed.__speed_2 (and speed.second (not speed.beacon))) |
| 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 |
(COUNTER_step 0 speed.incr (or speed.beacon speed.second) 0 speed.diff speed.__COUNTER_1_c speed.__COUNTER_1_x)
|
|
| 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 | 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)))) |
| ... | ... | |
| 95 | 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 |
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int) |
|
| 98 |
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c Int)
|
|
| 99 | 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 |
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int) |
|
| 102 |
(declare-var top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x Int)
|
|
| 103 | 103 |
(declare-var top.early Bool) |
| 104 | 104 |
(declare-var top.late Bool) |
| 105 | 105 |
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int)) |
| 106 | 106 |
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int)) |
| 107 | 107 |
|
| 108 | 108 |
(rule (=> |
| 109 |
(and (speed_init top.beacon top.second top.late top.early top.__speed_3_x top.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 110 |
(= top.OK 1)
|
|
| 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.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 110 |
(= top.OK true)
|
|
| 111 | 111 |
(= top.__top_1_x top.early) |
| 112 | 112 |
) |
| 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) |
|
| 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.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 114 | 114 |
)) |
| 115 | 115 |
|
| 116 | 116 |
(rule (=> |
| 117 |
(and (speed_step top.beacon top.second top.late top.early top.__speed_3_c top.__speed_6_c top.ni_1.ni_4.COUNTER.__COUNTER_1_c top.__speed_3_x top.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 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.speed.ni_4.COUNTER.__COUNTER_1_c top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 118 | 118 |
(= top.OK (or (not top.__top_1_c) (not top.late))) |
| 119 | 119 |
(= top.__top_1_x top.early) |
| 120 | 120 |
) |
| 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)
|
|
| 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.speed.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.speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 122 | 122 |
)) |
| 123 | 123 |
|
| 124 |
; Collecting semantics with main node top |
|
| 125 |
|
|
| 126 |
(declare-rel MAIN (Bool Bool Bool Int Bool)) |
|
| 127 |
; Initial set |
|
| 128 |
(declare-rel INIT_STATE ()) |
|
| 129 |
(rule INIT_STATE) |
|
| 130 |
(rule (=> |
|
| 131 |
(and INIT_STATE |
|
| 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.speed.ni_4.COUNTER.__COUNTER_1_x) |
|
| 133 |
) |
|
| 134 |
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK) |
|
| 135 |
)) |
|
| 136 |
|
|
| 137 |
; Inductive def |
|
| 138 |
(declare-var dummy Bool) |
|
| 139 |
(rule (=> |
|
| 140 |
(and (MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.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.speed.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.speed.ni_4.COUNTER.__COUNTER_1_x) |
|
| 142 |
) |
|
| 143 |
(MAIN top.__top_1_x top.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_x top.OK) |
|
| 144 |
)) |
|
| 145 |
|
|
| 146 |
; Property def |
|
| 147 |
(declare-rel ERR ()) |
|
| 148 |
(rule (=> |
|
| 149 |
(and (not (= top.OK true)) |
|
| 150 |
(MAIN top.__top_1_c top.ni_1.speed.__speed_3_c top.ni_1.speed.__speed_6_c top.ni_1.speed.ni_4.COUNTER.__COUNTER_1_c)) |
|
| 151 |
ERR)) |
|
| 152 |
(query ERR) |
|
Also available in: Unified diff
Is it working?