Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_demux_test / demux_test.smt2 @ 6c3ea955

History | View | Annotate | Download (2.59 KB)

1
; demux_test
2
(declare-var demux_test.In1_1_1 Real)
3
(declare-var demux_test.In1_1_2 Real)
4
(declare-var demux_test.In2_1_1 Real)
5
(declare-var demux_test.In2_1_2 Real)
6
(declare-var demux_test.In2_1_3 Real)
7
(declare-var demux_test.Out1_1_1 Real)
8
(declare-var demux_test.Out2_2_1 Real)
9
(declare-var demux_test.Out3_3_1 Real)
10
(declare-var demux_test.Out4_4_1 Real)
11
(declare-var demux_test.Out4_4_2 Real)
12
(declare-var demux_test.ni_0._arrow._first_c Bool)
13
(declare-var demux_test.ni_0._arrow._first_m Bool)
14
(declare-var demux_test.ni_0._arrow._first_x Bool)
15
(declare-var demux_test.Demux1_1_1 Real)
16
(declare-var demux_test.Demux1_2_1 Real)
17
(declare-var demux_test.Demux1_2_2 Real)
18
(declare-var demux_test.Demux_1_1 Real)
19
(declare-var demux_test.Demux_2_1 Real)
20
(declare-var demux_test.__demux_test_1 Bool)
21
(declare-var demux_test.i_virtual_local Real)
22
(declare-rel demux_test_reset (Bool Bool))
23
(declare-rel demux_test_step (Real Real Real Real Real Real Real Real Real Real Bool Bool))
24

    
25
(rule (=> 
26
  (and 
27
       
28
       (= demux_test.ni_0._arrow._first_m true)
29
  )
30
  (demux_test_reset demux_test.ni_0._arrow._first_c
31
                    demux_test.ni_0._arrow._first_m)
32
))
33

    
34
(rule (=> 
35
  (and (= demux_test.ni_0._arrow._first_m demux_test.ni_0._arrow._first_c)
36
       (and (= demux_test.__demux_test_1 (ite demux_test.ni_0._arrow._first_m true false))
37
            (= demux_test.ni_0._arrow._first_x false))
38
       (and (or (not (= demux_test.__demux_test_1 true))
39
               (= demux_test.i_virtual_local 0.0))
40
            (or (not (= demux_test.__demux_test_1 false))
41
               (= demux_test.i_virtual_local 1.0))
42
       )
43
       (= demux_test.Demux1_2_2 demux_test.In2_1_3)
44
       (= demux_test.Out4_4_2 demux_test.Demux1_2_2)
45
       (= demux_test.Demux1_2_1 demux_test.In2_1_2)
46
       (= demux_test.Out4_4_1 demux_test.Demux1_2_1)
47
       (= demux_test.Demux1_1_1 demux_test.In2_1_1)
48
       (= demux_test.Out3_3_1 demux_test.Demux1_1_1)
49
       (= demux_test.Demux_2_1 demux_test.In1_1_2)
50
       (= demux_test.Out2_2_1 demux_test.Demux_2_1)
51
       (= demux_test.Demux_1_1 demux_test.In1_1_1)
52
       (= demux_test.Out1_1_1 demux_test.Demux_1_1)
53
       )
54
  (demux_test_step demux_test.In1_1_1
55
                   demux_test.In1_1_2
56
                   demux_test.In2_1_1
57
                   demux_test.In2_1_2
58
                   demux_test.In2_1_3
59
                   demux_test.Out1_1_1
60
                   demux_test.Out2_2_1
61
                   demux_test.Out3_3_1
62
                   demux_test.Out4_4_1
63
                   demux_test.Out4_4_2
64
                   demux_test.ni_0._arrow._first_c
65
                   demux_test.ni_0._arrow._first_x)
66
))
67