Project

General

Profile

Revision f19eb2fd ex3.smt2

View differences:

ex3.smt2
1 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_reset (Int Int Bool Bool Int Int))
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 11
(declare-rel COUNTER_step (Int Int Bool Bool Int Int Int))
12 12

  
13 13
(rule (=> 
......
29 29
))
30 30

  
31 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_reset (Bool Bool Bool Bool Bool Bool Int))
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 51
(declare-rel speed_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Int))
52 52

  
53 53
(rule (=> 
......
89 89
))
90 90

  
91 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_reset (Bool Bool Bool Bool Bool Bool Int))
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 106
(declare-rel top_step (Bool Bool Bool Bool Bool Bool Int Bool Bool Bool Int))
107 107

  
108 108
(rule (=> 

Also available in: Unified diff