Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_subsystem_mask_test / subsystem_mask_test.smt2 @ 6c3ea955

History | View | Annotate | Download (7.98 KB)

1
; subsystem_mask_test_Subsystem
2
(declare-var subsystem_mask_test_Subsystem.In1_1_1 Real)
3
(declare-var subsystem_mask_test_Subsystem.Out1_1_1 Bool)
4
(declare-var subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c Real)
5
(declare-var subsystem_mask_test_Subsystem.ni_2._arrow._first_c Bool)
6
(declare-var subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m Real)
7
(declare-var subsystem_mask_test_Subsystem.ni_2._arrow._first_m Bool)
8
(declare-var subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_x Real)
9
(declare-var subsystem_mask_test_Subsystem.ni_2._arrow._first_x Bool)
10
(declare-var subsystem_mask_test_Subsystem.DetectChange_1_1 Bool)
11
(declare-var subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_1 Bool)
12
(declare-var subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_3 Real)
13
(declare-rel subsystem_mask_test_Subsystem_reset (Real Bool Real Bool))
14
(declare-rel subsystem_mask_test_Subsystem_step (Real Bool Real Bool Real Bool))
15

    
16
(rule (=> 
17
  (and 
18
       (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c)
19
       (= subsystem_mask_test_Subsystem.ni_2._arrow._first_m true)
20
  )
21
  (subsystem_mask_test_Subsystem_reset subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c
22
                                       subsystem_mask_test_Subsystem.ni_2._arrow._first_c
23
                                       subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m
24
                                       subsystem_mask_test_Subsystem.ni_2._arrow._first_m)
25
))
26

    
27
(rule (=> 
28
  (and (= subsystem_mask_test_Subsystem.ni_2._arrow._first_m subsystem_mask_test_Subsystem.ni_2._arrow._first_c)
29
       (and (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_1 (ite subsystem_mask_test_Subsystem.ni_2._arrow._first_m true false))
30
            (= subsystem_mask_test_Subsystem.ni_2._arrow._first_x false))
31
       (and (or (not (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_1 true))
32
               (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_3 0.00000000))
33
            (or (not (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_1 false))
34
               (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_3 subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c))
35
       )
36
       (= subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_x subsystem_mask_test_Subsystem.In1_1_1)
37
       (= subsystem_mask_test_Subsystem.DetectChange_1_1 (not (= subsystem_mask_test_Subsystem.In1_1_1 subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_3)))
38
       (= subsystem_mask_test_Subsystem.Out1_1_1 subsystem_mask_test_Subsystem.DetectChange_1_1)
39
       )
40
  (subsystem_mask_test_Subsystem_step subsystem_mask_test_Subsystem.In1_1_1
41
                                      subsystem_mask_test_Subsystem.Out1_1_1
42
                                      subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c
43
                                      subsystem_mask_test_Subsystem.ni_2._arrow._first_c
44
                                      subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_x
45
                                      subsystem_mask_test_Subsystem.ni_2._arrow._first_x)
46
))
47

    
48
; subsystem_mask_test
49
(declare-var subsystem_mask_test.In1_1_1 Real)
50
(declare-var subsystem_mask_test.Out4_1_1 Bool)
51
(declare-var subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c Real)
52
(declare-var subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_c Bool)
53
(declare-var subsystem_mask_test.ni_1._arrow._first_c Bool)
54
(declare-var subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m Real)
55
(declare-var subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_m Bool)
56
(declare-var subsystem_mask_test.ni_1._arrow._first_m Bool)
57
(declare-var subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_x Real)
58
(declare-var subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_x Bool)
59
(declare-var subsystem_mask_test.ni_1._arrow._first_x Bool)
60
(declare-var subsystem_mask_test.Subsystem_1_1 Bool)
61
(declare-var subsystem_mask_test.__subsystem_mask_test_1 Bool)
62
(declare-var subsystem_mask_test.i_virtual_local Real)
63
(declare-rel subsystem_mask_test_reset (Real Bool Bool Real Bool Bool))
64
(declare-rel subsystem_mask_test_step (Real Bool Real Bool Bool Real Bool Bool))
65

    
66
(rule (=> 
67
  (and 
68
       
69
       (= subsystem_mask_test.ni_1._arrow._first_m true)
70
       (subsystem_mask_test_Subsystem_reset subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c
71
                                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_c
72
                                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m
73
                                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_m)
74
  )
75
  (subsystem_mask_test_reset subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c
76
                             subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_c
77
                             subsystem_mask_test.ni_1._arrow._first_c
78
                             subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m
79
                             subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_m
80
                             subsystem_mask_test.ni_1._arrow._first_m)
81
))
82

    
83
(rule (=> 
84
  (and (= subsystem_mask_test.ni_1._arrow._first_m subsystem_mask_test.ni_1._arrow._first_c)
85
       (and (= subsystem_mask_test.__subsystem_mask_test_1 (ite subsystem_mask_test.ni_1._arrow._first_m true false))
86
            (= subsystem_mask_test.ni_1._arrow._first_x false))
87
       (and (or (not (= subsystem_mask_test.__subsystem_mask_test_1 true))
88
               (= subsystem_mask_test.i_virtual_local 0.0))
89
            (or (not (= subsystem_mask_test.__subsystem_mask_test_1 false))
90
               (= subsystem_mask_test.i_virtual_local 1.0))
91
       )
92
       (and (= subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c)
93
            (= subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_m subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_c)
94
            )
95
       (subsystem_mask_test_Subsystem_step subsystem_mask_test.In1_1_1
96
                                           subsystem_mask_test.Subsystem_1_1
97
                                           subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_m
98
                                           subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_m
99
                                           subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_x
100
                                           subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_x)
101
       (= subsystem_mask_test.Out4_1_1 subsystem_mask_test.Subsystem_1_1)
102
       )
103
  (subsystem_mask_test_step subsystem_mask_test.In1_1_1
104
                            subsystem_mask_test.Out4_1_1
105
                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_c
106
                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_c
107
                            subsystem_mask_test.ni_1._arrow._first_c
108
                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.__subsystem_mask_test_Subsystem_2_x
109
                            subsystem_mask_test.ni_0.subsystem_mask_test_Subsystem.ni_2._arrow._first_x
110
                            subsystem_mask_test.ni_1._arrow._first_x)
111
))
112