Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_flattening_2_test / flattening_2_test.smt2 @ 6c3ea955

History | View | Annotate | Download (3.46 KB)

1
; flattening_2_test
2
(declare-var flattening_2_test.In1_1_1 Real)
3
(declare-var flattening_2_test.Out1_1_1 Real)
4
(declare-var flattening_2_test.Out2_2_1 Real)
5
(declare-var flattening_2_test.Out3_3_1 Real)
6
(declare-var flattening_2_test.__flattening_2_test_2_c Real)
7
(declare-var flattening_2_test.ni_0._arrow._first_c Bool)
8
(declare-var flattening_2_test.__flattening_2_test_2_m Real)
9
(declare-var flattening_2_test.ni_0._arrow._first_m Bool)
10
(declare-var flattening_2_test.__flattening_2_test_2_x Real)
11
(declare-var flattening_2_test.ni_0._arrow._first_x Bool)
12
(declare-var flattening_2_test.Subsystem_Constant_1_1 Real)
13
(declare-var flattening_2_test.Subsystem_Gain_1_1 Real)
14
(declare-var flattening_2_test.Subsystem_Subsystem1_Gain_1_1 Real)
15
(declare-var flattening_2_test.Subsystem_Sum_1_1 Real)
16
(declare-var flattening_2_test.UnitDelay_1_1 Real)
17
(declare-var flattening_2_test.__flattening_2_test_1 Bool)
18
(declare-var flattening_2_test.i_virtual_local Real)
19
(declare-rel flattening_2_test_reset (Real Bool Real Bool))
20
(declare-rel flattening_2_test_step (Real Real Real Real Real Bool Real Bool))
21

    
22
(rule (=> 
23
  (and 
24
       (= flattening_2_test.__flattening_2_test_2_m flattening_2_test.__flattening_2_test_2_c)
25
       (= flattening_2_test.ni_0._arrow._first_m true)
26
  )
27
  (flattening_2_test_reset flattening_2_test.__flattening_2_test_2_c
28
                           flattening_2_test.ni_0._arrow._first_c
29
                           flattening_2_test.__flattening_2_test_2_m
30
                           flattening_2_test.ni_0._arrow._first_m)
31
))
32

    
33
(rule (=> 
34
  (and (= flattening_2_test.ni_0._arrow._first_m flattening_2_test.ni_0._arrow._first_c)
35
       (and (= flattening_2_test.__flattening_2_test_1 (ite flattening_2_test.ni_0._arrow._first_m true false))
36
            (= flattening_2_test.ni_0._arrow._first_x false))
37
       (and (or (not (= flattening_2_test.__flattening_2_test_1 false))
38
               (and (= flattening_2_test.i_virtual_local 1.0)
39
                    (= flattening_2_test.UnitDelay_1_1 flattening_2_test.__flattening_2_test_2_c)
40
                    ))
41
            (or (not (= flattening_2_test.__flattening_2_test_1 true))
42
               (and (= flattening_2_test.i_virtual_local 0.0)
43
                    (= flattening_2_test.UnitDelay_1_1 0.00000000)
44
                    ))
45
       )
46
       (= flattening_2_test.__flattening_2_test_2_x flattening_2_test.In1_1_1)
47
       (= flattening_2_test.Subsystem_Constant_1_1 1.00000000)
48
       (= flattening_2_test.Subsystem_Sum_1_1 (+ (+ flattening_2_test.UnitDelay_1_1 flattening_2_test.UnitDelay_1_1) flattening_2_test.Subsystem_Constant_1_1))
49
       (= flattening_2_test.Subsystem_Subsystem1_Gain_1_1 (* 0.50000000 flattening_2_test.UnitDelay_1_1))
50
       (= flattening_2_test.Subsystem_Gain_1_1 (* 0.50000000 flattening_2_test.UnitDelay_1_1))
51
       (= flattening_2_test.Out3_3_1 flattening_2_test.Subsystem_Subsystem1_Gain_1_1)
52
       (= flattening_2_test.Out2_2_1 flattening_2_test.Subsystem_Sum_1_1)
53
       (= flattening_2_test.Out1_1_1 flattening_2_test.Subsystem_Gain_1_1)
54
       )
55
  (flattening_2_test_step flattening_2_test.In1_1_1
56
                          flattening_2_test.Out1_1_1
57
                          flattening_2_test.Out2_2_1
58
                          flattening_2_test.Out3_3_1
59
                          flattening_2_test.__flattening_2_test_2_c
60
                          flattening_2_test.ni_0._arrow._first_c
61
                          flattening_2_test.__flattening_2_test_2_x
62
                          flattening_2_test.ni_0._arrow._first_x)
63
))
64