Revision c76f1d66
Added by Pierre-Loïc Garoche over 9 years ago
| ex3.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)) |
| ... | ... | |
| 16 | 16 |
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC))) |
| 17 | 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 (=> |
| ... | ... | |
| 25 | 25 |
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC))) |
| 26 | 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) |
| ... | ... | |
| 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.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 57 |
(COUNTER_init 0 speed.incr (or speed.beacon speed.second) 0 speed.diff speed.__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)))) |
| ... | ... | |
| 66 | 66 |
(= speed.__speed_6_x speed.late) |
| 67 | 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 (=> |
| 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.ni_4.COUNTER.__COUNTER_1_c speed.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 76 |
(COUNTER_step 0 speed.incr (or speed.beacon speed.second) 0 speed.diff speed.__COUNTER_1_c speed.__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)))) |
| ... | ... | |
| 85 | 85 |
(= speed.__speed_6_x speed.late) |
| 86 | 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) |
| ... | ... | |
| 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.ni_1.speed.__speed_3_x top.ni_1.speed.__speed_6_x top.ni_1.ni_4.COUNTER.__COUNTER_1_x)
|
|
| 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 | 110 |
(= top.OK 1) |
| 111 | 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 |
(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)
|
|
| 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)
|
|
| 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.__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 |
; 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.__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 |
) |
|
| 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) |
|
| 135 |
)) |
|
| 136 |
|
|
| 137 |
; Inductive def |
|
| 138 |
(declare-var dummy Bool) |
|
| 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) |
|
| 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) |
|
| 144 |
)) |
|
| 145 |
|
|
| 146 |
; Property def |
|
| 147 |
(declare-rel ERR ()) |
|
| 148 |
(rule (=> |
|
| 149 |
(and (not (= top.OK true)) |
|
| 150 |
(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)) |
|
| 151 |
ERR)) |
|
| 152 |
(query ERR) |
|
| ex3_pourri.smt2 | ||
|---|---|---|
| 1 |
; COUNTER |
|
| 2 |
(declare-var COUNTER.init Int) |
|
| 3 |
(declare-var COUNTER.incr Int) |
|
| 4 |
(declare-var COUNTER.X Bool) |
|
| 5 |
(declare-var COUNTER.reset Bool) |
|
| 6 |
(declare-var COUNTER.C Int) |
|
| 7 |
(declare-var COUNTER.COUNTER.__COUNTER_1_c Int) |
|
| 8 |
(declare-var COUNTER.COUNTER.__COUNTER_1_x Int) |
|
| 9 |
(declare-var COUNTER.PC Int) |
|
| 10 |
(declare-rel COUNTER_init (Int Int Bool Bool Int Int)) |
|
| 11 |
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int)) |
|
| 12 |
|
|
| 13 |
(rule (=> |
|
| 14 |
(and (= COUNTER.PC COUNTER.init) |
|
| 15 |
(= COUNTER.C (ite COUNTER.reset COUNTER.init |
|
| 16 |
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC))) |
|
| 17 |
(= COUNTER.__COUNTER_1_x COUNTER.C) |
|
| 18 |
) |
|
| 19 |
(COUNTER_init COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_x) |
|
| 20 |
)) |
|
| 21 |
|
|
| 22 |
(rule (=> |
|
| 23 |
(and (= COUNTER.PC COUNTER.__COUNTER_1_c) |
|
| 24 |
(= COUNTER.C (ite COUNTER.reset COUNTER.init |
|
| 25 |
(ite COUNTER.X (+ COUNTER.PC COUNTER.incr) COUNTER.PC))) |
|
| 26 |
(= COUNTER.__COUNTER_1_x COUNTER.C) |
|
| 27 |
) |
|
| 28 |
(COUNTER_step COUNTER.init COUNTER.incr COUNTER.X COUNTER.reset COUNTER.C COUNTER.COUNTER.__COUNTER_1_c COUNTER.COUNTER.__COUNTER_1_x) |
|
| 29 |
)) |
|
| 30 |
|
|
| 31 |
; speed |
|
| 32 |
(declare-var speed.beacon Bool) |
|
| 33 |
(declare-var speed.second Bool) |
|
| 34 |
(declare-var speed.late Bool) |
|
| 35 |
(declare-var speed.early Bool) |
|
| 36 |
(declare-var speed.speed.__speed_3_c Bool) |
|
| 37 |
(declare-var speed.speed.__speed_6_c Bool) |
|
| 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) |
|
| 41 |
(declare-var speed.ni_4.COUNTER.__COUNTER_1_x Int) |
|
| 42 |
(declare-var speed.__speed_1 Bool) |
|
| 43 |
(declare-var speed.__speed_2 Bool) |
|
| 44 |
(declare-var speed.__speed_4 Bool) |
|
| 45 |
(declare-var speed.__speed_5 Bool) |
|
| 46 |
(declare-var speed.__speed_7 Bool) |
|
| 47 |
(declare-var speed.__speed_8 Bool) |
|
| 48 |
(declare-var speed.diff Int) |
|
| 49 |
(declare-var speed.incr Int) |
|
| 50 |
(declare-rel speed_init (Bool Bool Bool Bool Bool Bool Int)) |
|
| 51 |
(declare-rel speed_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Int)) |
|
| 52 |
|
|
| 53 |
(rule (=> |
|
| 54 |
(and (= speed.__speed_2 (and speed.second (not speed.beacon))) |
|
| 55 |
(= speed.__speed_1 (and speed.beacon (not speed.second))) |
|
| 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.ni_4.COUNTER.__COUNTER_1_x) |
|
| 58 |
(= speed.__speed_7 speed.__speed_6_c) |
|
| 59 |
(= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0) |
|
| 60 |
(<= speed.diff (- 10)))) |
|
| 61 |
(= speed.late 0) |
|
| 62 |
(= speed.__speed_4 speed.__speed_3_c) |
|
| 63 |
(= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0) |
|
| 64 |
(>= speed.diff 10))) |
|
| 65 |
(= speed.early 0) |
|
| 66 |
(= speed.__speed_6_x speed.late) |
|
| 67 |
(= speed.__speed_3_x speed.early) |
|
| 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) |
|
| 70 |
)) |
|
| 71 |
|
|
| 72 |
(rule (=> |
|
| 73 |
(and (= speed.__speed_2 (and speed.second (not speed.beacon))) |
|
| 74 |
(= speed.__speed_1 (and speed.beacon (not speed.second))) |
|
| 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.ni_4.COUNTER.__COUNTER_1_c speed.ni_4.COUNTER.__COUNTER_1_x) |
|
| 77 |
(= speed.__speed_7 speed.__speed_6_c) |
|
| 78 |
(= speed.__speed_8 (ite speed.__speed_7 (< speed.diff 0) |
|
| 79 |
(<= speed.diff (- 10)))) |
|
| 80 |
(= speed.late speed.__speed_8) |
|
| 81 |
(= speed.__speed_4 speed.__speed_3_c) |
|
| 82 |
(= speed.__speed_5 (ite speed.__speed_4 (> speed.diff 0) |
|
| 83 |
(>= speed.diff 10))) |
|
| 84 |
(= speed.early speed.__speed_5) |
|
| 85 |
(= speed.__speed_6_x speed.late) |
|
| 86 |
(= speed.__speed_3_x speed.early) |
|
| 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) |
|
| 89 |
)) |
|
| 90 |
|
|
| 91 |
; top |
|
| 92 |
(declare-var top.beacon Bool) |
|
| 93 |
(declare-var top.second Bool) |
|
| 94 |
(declare-var top.OK Bool) |
|
| 95 |
(declare-var top.top.__top_1_c Bool) |
|
| 96 |
(declare-var top.ni_1.speed.__speed_3_c Bool) |
|
| 97 |
(declare-var top.ni_1.speed.__speed_6_c Bool) |
|
| 98 |
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_c Int) |
|
| 99 |
(declare-var top.top.__top_1_x Bool) |
|
| 100 |
(declare-var top.ni_1.speed.__speed_3_x Bool) |
|
| 101 |
(declare-var top.ni_1.speed.__speed_6_x Bool) |
|
| 102 |
(declare-var top.ni_1.ni_4.COUNTER.__COUNTER_1_x Int) |
|
| 103 |
(declare-var top.early Bool) |
|
| 104 |
(declare-var top.late Bool) |
|
| 105 |
(declare-rel top_init (Bool Bool Bool Bool Bool Bool Int)) |
|
| 106 |
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int)) |
|
| 107 |
|
|
| 108 |
(rule (=> |
|
| 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 |
(= top.OK 1) |
|
| 111 |
(= top.__top_1_x top.early) |
|
| 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) |
|
| 114 |
)) |
|
| 115 |
|
|
| 116 |
(rule (=> |
|
| 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_1_c) (not top.late))) |
|
| 119 |
(= top.__top_1_x top.early) |
|
| 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) |
|
| 122 |
)) |
|
| 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.__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 |
) |
|
| 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) |
|
| 135 |
)) |
|
| 136 |
|
|
| 137 |
; Inductive def |
|
| 138 |
(declare-var dummy Bool) |
|
| 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) |
|
| 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) |
|
| 144 |
)) |
|
| 145 |
|
|
| 146 |
; Property def |
|
| 147 |
(declare-rel ERR ()) |
|
| 148 |
(rule (=> |
|
| 149 |
(and (not (= top.OK true)) |
|
| 150 |
(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)) |
|
| 151 |
ERR)) |
|
| 152 |
(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) |
|
| 33 |
let rename_machine_list p = List.map (rename_machine p) |
|
| 34 |
|
|
| 31 | 35 |
let rename f = (fun v -> {v with var_id = f v.var_id } )
|
| 32 |
let rename_current prefix = rename (fun n -> prefix ^ "." ^ n ^ "_c") |
|
| 33 |
let rename_current_list prefix = List.map (rename_current prefix) |
|
| 34 |
let rename_next prefix = rename (fun n -> prefix ^ "." ^ n ^ "_x") |
|
| 35 |
let rename_next_list prefix = List.map (rename_next prefix) |
|
| 36 |
let rename_machine prefix = rename (fun n -> prefix ^ "." ^ n) |
|
| 37 |
let rename_machine_list prefix = List.map (rename_machine prefix) |
|
| 36 |
let rename_current = rename (fun n -> n ^ "_c") |
|
| 37 |
let rename_current_list = List.map rename_current |
|
| 38 |
let rename_next = rename (fun n -> n ^ "_x") |
|
| 39 |
let rename_next_list = List.map rename_next |
|
| 40 |
|
|
| 38 | 41 |
|
| 39 | 42 |
let get_machine machines node_name = |
| 40 | 43 |
List.find (fun m -> m.mname.node_id = node_name) machines |
| 41 | 44 |
|
| 42 |
let full_memory_vars machines prefix machine = |
|
| 43 |
let rec aux prefix m = |
|
| 44 |
let pref x = if prefix = "" then x else prefix ^ "." ^ x in |
|
| 45 |
(rename_machine_list (pref m.mname.node_id) m.mmemory) @ |
|
| 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 | 48 |
List.fold_left (fun accu (id, (n, _)) -> |
| 47 | 49 |
let name = node_name n in |
| 48 | 50 |
if name = "_arrow" then accu else |
| 49 | 51 |
let machine_n = get_machine machines name in |
| 50 |
( aux (pref id) machine_n ) @ accu
|
|
| 52 |
( aux false (prefix_s ^ "." ^ id) machine_n ) @ accu
|
|
| 51 | 53 |
) [] (m.minstances) |
| 52 | 54 |
in |
| 53 |
aux prefix machine
|
|
| 55 |
aux true machine.mname.node_id machine
|
|
| 54 | 56 |
|
| 55 | 57 |
let machine_vars machines m = |
| 56 | 58 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
| 57 | 59 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@ |
| 58 |
(rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @
|
|
| 59 |
(rename_next_list m.mname.node_id (full_memory_vars machines "" m))
|
|
| 60 |
(rename_current_list (full_memory_vars machines m)) @
|
|
| 61 |
(rename_next_list (full_memory_vars machines m))
|
|
| 60 | 62 |
|
| 61 | 63 |
let step_vars machines m = |
| 62 | 64 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
| 63 | 65 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@ |
| 64 |
(rename_current_list m.mname.node_id (full_memory_vars machines "" m)) @
|
|
| 65 |
(rename_next_list m.mname.node_id (full_memory_vars machines "" m))
|
|
| 66 |
(rename_current_list (full_memory_vars machines m)) @
|
|
| 67 |
(rename_next_list (full_memory_vars machines m))
|
|
| 66 | 68 |
|
| 67 | 69 |
let init_vars machines m = |
| 68 | 70 |
(rename_machine_list m.mname.node_id m.mstep.step_inputs)@ |
| 69 | 71 |
(rename_machine_list m.mname.node_id m.mstep.step_outputs)@ |
| 70 |
(rename_next_list m.mname.node_id (full_memory_vars machines "" m)) |
|
| 71 |
|
|
| 72 |
(rename_next_list (full_memory_vars machines m)) |
|
| 72 | 73 |
|
| 73 | 74 |
(********************************************************************************************) |
| 74 | 75 |
(* Instruction Printing functions *) |
| ... | ... | |
| 110 | 111 |
if Types.is_array_type v.var_type |
| 111 | 112 |
then assert false |
| 112 | 113 |
else pp_var fmt ((if is_lhs then rename_next else rename_current) self v) |
| 113 |
| Fun (n, vl) -> Format.fprintf fmt "(%a)" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
|
|
| 114 |
| Fun (n, vl) -> Format.fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
|
|
| 114 | 115 |
|
| 115 | 116 |
(* Prints a [value] indexed by the suffix list [loop_vars] *) |
| 116 | 117 |
let rec pp_value_suffix self pp_value fmt value = |
Also available in: Unified diff
Working on bugs
git-svn-id: https://cavale.enseeiht.fr/svn/lustrec/lustre_compiler/branches/horn_encoding@149 041b043f-8d7c-46b2-b46e-ef0dd855326e