Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_constant_test_order / constant_test_order.smt2 @ 6c3ea955

History | View | Annotate | Download (3.74 KB)

1
; constant_test_order
2
(declare-var constant_test_order.i_virtual Real)
3
(declare-var constant_test_order.Out7_1_1 Real)
4
(declare-var constant_test_order.Out7_1_2 Real)
5
(declare-var constant_test_order.Out7_1_3 Real)
6
(declare-var constant_test_order.Out7_1_4 Real)
7
(declare-var constant_test_order.Out7_1_5 Real)
8
(declare-var constant_test_order.Out7_1_6 Real)
9
(declare-var constant_test_order.Out1_2_1 Real)
10
(declare-var constant_test_order.Out1_2_2 Real)
11
(declare-var constant_test_order.ni_0._arrow._first_c Bool)
12
(declare-var constant_test_order.ni_0._arrow._first_m Bool)
13
(declare-var constant_test_order.ni_0._arrow._first_x Bool)
14
(declare-var constant_test_order.Constant1_1_1 Real)
15
(declare-var constant_test_order.Constant1_1_2 Real)
16
(declare-var constant_test_order.Constant6_1_1 Real)
17
(declare-var constant_test_order.Constant6_1_2 Real)
18
(declare-var constant_test_order.Constant6_1_3 Real)
19
(declare-var constant_test_order.Constant6_1_4 Real)
20
(declare-var constant_test_order.Constant6_1_5 Real)
21
(declare-var constant_test_order.Constant6_1_6 Real)
22
(declare-var constant_test_order.__constant_test_order_1 Bool)
23
(declare-var constant_test_order.i_virtual_local Real)
24
(declare-rel constant_test_order_reset (Bool Bool))
25
(declare-rel constant_test_order_step (Real Real Real Real Real Real Real Real Real Bool Bool))
26

    
27
(rule (=> 
28
  (and 
29
       
30
       (= constant_test_order.ni_0._arrow._first_m true)
31
  )
32
  (constant_test_order_reset constant_test_order.ni_0._arrow._first_c
33
                             constant_test_order.ni_0._arrow._first_m)
34
))
35

    
36
(rule (=> 
37
  (and (= constant_test_order.ni_0._arrow._first_m constant_test_order.ni_0._arrow._first_c)
38
       (and (= constant_test_order.__constant_test_order_1 (ite constant_test_order.ni_0._arrow._first_m true false))
39
            (= constant_test_order.ni_0._arrow._first_x false))
40
       (and (or (not (= constant_test_order.__constant_test_order_1 true))
41
               (= constant_test_order.i_virtual_local 0.0))
42
            (or (not (= constant_test_order.__constant_test_order_1 false))
43
               (= constant_test_order.i_virtual_local 1.0))
44
       )
45
       (= constant_test_order.Constant6_1_6 6.00000000)
46
       (= constant_test_order.Out7_1_6 constant_test_order.Constant6_1_6)
47
       (= constant_test_order.Constant6_1_5 5.00000000)
48
       (= constant_test_order.Out7_1_5 constant_test_order.Constant6_1_5)
49
       (= constant_test_order.Constant6_1_4 4.00000000)
50
       (= constant_test_order.Out7_1_4 constant_test_order.Constant6_1_4)
51
       (= constant_test_order.Constant6_1_3 3.00000000)
52
       (= constant_test_order.Out7_1_3 constant_test_order.Constant6_1_3)
53
       (= constant_test_order.Constant6_1_2 2.00000000)
54
       (= constant_test_order.Out7_1_2 constant_test_order.Constant6_1_2)
55
       (= constant_test_order.Constant6_1_1 1.00000000)
56
       (= constant_test_order.Out7_1_1 constant_test_order.Constant6_1_1)
57
       (= constant_test_order.Constant1_1_2 2.00000000)
58
       (= constant_test_order.Out1_2_2 constant_test_order.Constant1_1_2)
59
       (= constant_test_order.Constant1_1_1 1.00000000)
60
       (= constant_test_order.Out1_2_1 constant_test_order.Constant1_1_1)
61
       )
62
  (constant_test_order_step constant_test_order.i_virtual
63
                            constant_test_order.Out7_1_1
64
                            constant_test_order.Out7_1_2
65
                            constant_test_order.Out7_1_3
66
                            constant_test_order.Out7_1_4
67
                            constant_test_order.Out7_1_5
68
                            constant_test_order.Out7_1_6
69
                            constant_test_order.Out1_2_1
70
                            constant_test_order.Out1_2_2
71
                            constant_test_order.ni_0._arrow._first_c
72
                            constant_test_order.ni_0._arrow._first_x)
73
))
74