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) |
|
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