Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_bus_test / bus_test.smt2 @ 6c3ea955

History | View | Annotate | Download (2.29 KB)

1
; bus_test
2
(declare-var bus_test.In1_1_1 Real)
3
(declare-var bus_test.In2_1_1 Real)
4
(declare-var bus_test.In3_1_1 Real)
5
(declare-var bus_test.Out4_1_1 Real)
6
(declare-var bus_test.Out5_2_1 Real)
7
(declare-var bus_test.ni_0._arrow._first_c Bool)
8
(declare-var bus_test.ni_0._arrow._first_m Bool)
9
(declare-var bus_test.ni_0._arrow._first_x Bool)
10
(declare-var bus_test.BusAssignment_1_1 Real)
11
(declare-var bus_test.BusAssignment_1_2 Real)
12
(declare-var bus_test.BusAssignment_1_3 Real)
13
(declare-var bus_test.BusCreator_1_1 Real)
14
(declare-var bus_test.BusCreator_1_2 Real)
15
(declare-var bus_test.BusCreator_1_3 Real)
16
(declare-var bus_test.BusSelector_1_1 Real)
17
(declare-var bus_test.BusSelector_2_1 Real)
18
(declare-var bus_test.__bus_test_1 Bool)
19
(declare-var bus_test.i_virtual_local Real)
20
(declare-rel bus_test_reset (Bool Bool))
21
(declare-rel bus_test_step (Real Real Real Real Real Bool Bool))
22

    
23
(rule (=> 
24
  (and 
25
       
26
       (= bus_test.ni_0._arrow._first_m true)
27
  )
28
  (bus_test_reset bus_test.ni_0._arrow._first_c
29
                  bus_test.ni_0._arrow._first_m)
30
))
31

    
32
(rule (=> 
33
  (and (= bus_test.ni_0._arrow._first_m bus_test.ni_0._arrow._first_c)
34
       (and (= bus_test.__bus_test_1 (ite bus_test.ni_0._arrow._first_m true false))
35
            (= bus_test.ni_0._arrow._first_x false))
36
       (and (or (not (= bus_test.__bus_test_1 true))
37
               (= bus_test.i_virtual_local 0.0))
38
            (or (not (= bus_test.__bus_test_1 false))
39
               (= bus_test.i_virtual_local 1.0))
40
       )
41
       (= bus_test.BusCreator_1_2 bus_test.In2_1_1)
42
       (= bus_test.BusAssignment_1_2 bus_test.BusCreator_1_2)
43
       (= bus_test.BusSelector_2_1 bus_test.BusAssignment_1_2)
44
       (= bus_test.Out5_2_1 bus_test.BusSelector_2_1)
45
       (= bus_test.BusAssignment_1_1 bus_test.In3_1_1)
46
       (= bus_test.BusSelector_1_1 bus_test.BusAssignment_1_1)
47
       (= bus_test.Out4_1_1 bus_test.BusSelector_1_1)
48
       (= bus_test.BusCreator_1_3 bus_test.In3_1_1)
49
       (= bus_test.BusCreator_1_1 bus_test.In1_1_1)
50
       (= bus_test.BusAssignment_1_3 bus_test.In2_1_1)
51
       )
52
  (bus_test_step bus_test.In1_1_1
53
                 bus_test.In2_1_1
54
                 bus_test.In3_1_1
55
                 bus_test.Out4_1_1
56
                 bus_test.Out5_2_1
57
                 bus_test.ni_0._arrow._first_c
58
                 bus_test.ni_0._arrow._first_x)
59
))
60