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) |
|
| 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) |
| src/horn_backend.ml | ||
|---|---|---|
| 28 | 28 |
let pp_var fmt id = Format.pp_print_string fmt id.var_id |
| 29 | 29 |
|
| 30 | 30 |
|
| 31 |
let prefix prefix x = if prefix = "" then x else prefix ^ "." ^ x |
|
| 32 |
let rename_machine p = rename (fun n -> prefix p n) |
|
| 31 |
let concat prefix x = if prefix = "" then x else prefix ^ "." ^ x |
|
| 32 |
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
|
| 33 |
let rename_machine p = rename (fun n -> concat p n) |
|
| 33 | 34 |
let rename_machine_list p = List.map (rename_machine p) |
| 34 | 35 |
|
| 35 |
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
|
| 36 | 36 |
let rename_current = rename (fun n -> n ^ "_c") |
| 37 | 37 |
let rename_current_list = List.map rename_current |
| 38 | 38 |
let rename_next = rename (fun n -> n ^ "_x") |
| ... | ... | |
| 43 | 43 |
List.find (fun m -> m.mname.node_id = node_name) machines |
| 44 | 44 |
|
| 45 | 45 |
let full_memory_vars machines machine = |
| 46 |
let rec aux fst prefix_s m =
|
|
| 47 |
(rename_machine_list (if fst then prefix else prefix ^ "." ^ m.mname.node_id) m.mmemory) @
|
|
| 46 |
let rec aux fst prefix m = |
|
| 47 |
(rename_machine_list (if fst then prefix else concat prefix m.mname.node_id) m.mmemory) @
|
|
| 48 | 48 |
List.fold_left (fun accu (id, (n, _)) -> |
| 49 | 49 |
let name = node_name n in |
| 50 | 50 |
if name = "_arrow" then accu else |
| 51 | 51 |
let machine_n = get_machine machines name in |
| 52 |
( aux false (prefix_s ^ "." ^ id) machine_n ) @ accu
|
|
| 52 |
( aux false (concat prefix (if fst then id else concat m.mname.node_id id)) machine_n ) @ accu
|
|
| 53 | 53 |
) [] (m.minstances) |
| 54 | 54 |
in |
| 55 | 55 |
aux true machine.mname.node_id machine |
| ... | ... | |
| 85 | 85 |
|
| 86 | 86 |
(* Used to print boolean constants *) |
| 87 | 87 |
let pp_horn_tag fmt t = |
| 88 |
pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
|
|
| 88 |
pp_print_string fmt (if t = tag_true then "true" else if t = tag_false then "false" else t)
|
|
| 89 | 89 |
|
| 90 | 90 |
(* Prints a constant value *) |
| 91 | 91 |
let rec pp_horn_const fmt c = |
| ... | ... | |
| 110 | 110 |
| StateVar v -> |
| 111 | 111 |
if Types.is_array_type v.var_type |
| 112 | 112 |
then assert false |
| 113 |
else pp_var fmt ((if is_lhs then rename_next else rename_current) self v)
|
|
| 113 |
else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
|
|
| 114 | 114 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl |
| 115 | 115 |
|
| 116 | 116 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
| ... | ... | |
| 161 | 161 |
(Utils.fprintf_list ~sep:" " (pp_horn_val self (pp_horn_var m))) (List.map (fun v -> LocalVar v) outputs) |
| 162 | 162 |
(Utils.pp_final_char_if_non_empty " " outputs) |
| 163 | 163 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
| 164 |
(rename_next_list m.mname.node_id (full_memory_vars machines i target_machine))
|
|
| 164 |
rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))
|
|
| 165 | 165 |
) |
| 166 | 166 |
else |
| 167 | 167 |
Format.fprintf fmt "(%s_step %a%t%a%t%a)" |
| ... | ... | |
| 172 | 172 |
(Utils.pp_final_char_if_non_empty " " outputs) |
| 173 | 173 |
(Utils.fprintf_list ~sep:" " pp_var) ( |
| 174 | 174 |
|
| 175 |
(rename_current_list m.mname.node_id (full_memory_vars machines i target_machine)) @
|
|
| 176 |
(rename_next_list m.mname.node_id (full_memory_vars machines i target_machine))
|
|
| 175 |
(rename_machine_list (concat m.mname.node_id i) (rename_current_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine))) @
|
|
| 176 |
(rename_machine_list (concat m.mname.node_id i) (rename_next_list (* concat m.mname.node_id i *) (full_memory_vars machines target_machine)))
|
|
| 177 | 177 |
) |
| 178 | 178 |
|
| 179 | 179 |
end |
| ... | ... | |
| 280 | 280 |
Format.fprintf fmt "; Collecting semantics with main node %s@.@." node; |
| 281 | 281 |
(* We print the types of the main node "memory tree" TODO: add the output *) |
| 282 | 282 |
let main_memory_next = |
| 283 |
(rename_next_list machine.mname.node_id (full_memory_vars machines "" machine))
|
|
| 283 |
(rename_next_list (* machine.mname.node_id *) (full_memory_vars machines machine))
|
|
| 284 | 284 |
in |
| 285 | 285 |
let main_memory_current = |
| 286 |
(rename_current_list machine.mname.node_id (full_memory_vars machines "" machine))
|
|
| 286 |
(rename_current_list (* machine.mname.node_id *) (full_memory_vars machines machine))
|
|
| 287 | 287 |
in |
| 288 | 288 |
Format.fprintf fmt "(declare-rel MAIN (%a Bool))@." |
| 289 | 289 |
(Utils.fprintf_list ~sep:" " pp_type) |
| src/main_lustre_compiler.ml | ||
|---|---|---|
| 258 | 258 |
let fmt = Format.std_formatter in |
| 259 | 259 |
Horn_backend.translate fmt basename normalized_prog machine_code |
| 260 | 260 |
end |
| 261 |
| _ -> assert false |
|
| 261 | 262 |
in |
| 262 | 263 |
report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@."); |
| 263 | 264 |
(* We stop the process here *) |
Also available in: Unified diff
Is it working?