Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_flattening_1_test / flattening_1_test.smt2 @ 6c3ea955

History | View | Annotate | Download (4.85 KB)

1
; flattening_1_test
2
(declare-var flattening_1_test.In1_1_1 Real)
3
(declare-var flattening_1_test.In3_1_1 Real)
4
(declare-var flattening_1_test.Out1_1_1 Real)
5
(declare-var flattening_1_test.Out2_2_1 Real)
6
(declare-var flattening_1_test.__flattening_1_test_2_c Real)
7
(declare-var flattening_1_test.ni_0._arrow._first_c Bool)
8
(declare-var flattening_1_test.__flattening_1_test_2_m Real)
9
(declare-var flattening_1_test.ni_0._arrow._first_m Bool)
10
(declare-var flattening_1_test.__flattening_1_test_2_x Real)
11
(declare-var flattening_1_test.ni_0._arrow._first_x Bool)
12
(declare-var flattening_1_test.Subsystem_Gain_1_1 Real)
13
(declare-var flattening_1_test.Subsystem_SubSub1_Sum1_1_1 Real)
14
(declare-var flattening_1_test.Subsystem_SubSub1_Sum_1_1 Real)
15
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_D1_1_1 Real)
16
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainAC1_1_1_1 Real)
17
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainAC2_1_1_1 Real)
18
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainBD1_1_1_1 Real)
19
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainBD2_1_1_1 Real)
20
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_Sum1_1_1 Real)
21
(declare-var flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_Sum2_1_1 Real)
22
(declare-var flattening_1_test.__flattening_1_test_1 Bool)
23
(declare-var flattening_1_test.i_virtual_local Real)
24
(declare-rel flattening_1_test_reset (Real Bool Real Bool))
25
(declare-rel flattening_1_test_step (Real Real Real Real Real Bool Real Bool))
26

    
27
(rule (=> 
28
  (and 
29
       (= flattening_1_test.__flattening_1_test_2_m flattening_1_test.__flattening_1_test_2_c)
30
       (= flattening_1_test.ni_0._arrow._first_m true)
31
  )
32
  (flattening_1_test_reset flattening_1_test.__flattening_1_test_2_c
33
                           flattening_1_test.ni_0._arrow._first_c
34
                           flattening_1_test.__flattening_1_test_2_m
35
                           flattening_1_test.ni_0._arrow._first_m)
36
))
37

    
38
(rule (=> 
39
  (and (= flattening_1_test.ni_0._arrow._first_m flattening_1_test.ni_0._arrow._first_c)
40
       (and (= flattening_1_test.__flattening_1_test_1 (ite flattening_1_test.ni_0._arrow._first_m true false))
41
            (= flattening_1_test.ni_0._arrow._first_x false))
42
       (and (or (not (= flattening_1_test.__flattening_1_test_1 true))
43
               (= flattening_1_test.i_virtual_local 0.0))
44
            (or (not (= flattening_1_test.__flattening_1_test_1 false))
45
               (= flattening_1_test.i_virtual_local 1.0))
46
       )
47
       (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainBD1_1_1_1 (* 1.00000000 flattening_1_test.In3_1_1))
48
       (and (or (not (= flattening_1_test.__flattening_1_test_1 true))
49
               (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_D1_1_1 0.00000000))
50
            (or (not (= flattening_1_test.__flattening_1_test_1 false))
51
               (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_D1_1_1 flattening_1_test.__flattening_1_test_2_c))
52
       )
53
       (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainAC1_1_1_1 (* (- 1.00000000) flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_D1_1_1))
54
       (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_Sum1_1_1 (+ flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainAC1_1_1_1 flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainBD1_1_1_1))
55
       (= flattening_1_test.__flattening_1_test_2_x flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_Sum1_1_1)
56
       (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainBD2_1_1_1 (* 0.00000000 flattening_1_test.In3_1_1))
57
       (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainAC2_1_1_1 (* 1.00000000 flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_D1_1_1))
58
       (= flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_Sum2_1_1 (+ flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainAC2_1_1_1 flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_GainBD2_1_1_1))
59
       (= flattening_1_test.Subsystem_Gain_1_1 (* 0.50000000 flattening_1_test.In1_1_1))
60
       (= flattening_1_test.Subsystem_SubSub1_Sum_1_1 (- flattening_1_test.Subsystem_Gain_1_1 flattening_1_test.Subsystem_SubSub1_TransferFcn_pp_Sum2_1_1))
61
       (= flattening_1_test.Subsystem_SubSub1_Sum1_1_1 flattening_1_test.Subsystem_Gain_1_1)
62
       (= flattening_1_test.Out2_2_1 flattening_1_test.Subsystem_SubSub1_Sum1_1_1)
63
       (= flattening_1_test.Out1_1_1 flattening_1_test.Subsystem_SubSub1_Sum_1_1)
64
       )
65
  (flattening_1_test_step flattening_1_test.In1_1_1
66
                          flattening_1_test.In3_1_1
67
                          flattening_1_test.Out1_1_1
68
                          flattening_1_test.Out2_2_1
69
                          flattening_1_test.__flattening_1_test_2_c
70
                          flattening_1_test.ni_0._arrow._first_c
71
                          flattening_1_test.__flattening_1_test_2_x
72
                          flattening_1_test.ni_0._arrow._first_x)
73
))
74