Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_gain_test_uK_order / gain_test_uK_order.smt2 @ 6c3ea955

History | View | Annotate | Download (3.48 KB)

1
; gain_test_uK_order
2
(declare-var gain_test_uK_order.In7_1_1 Real)
3
(declare-var gain_test_uK_order.In7_1_2 Real)
4
(declare-var gain_test_uK_order.In7_1_3 Real)
5
(declare-var gain_test_uK_order.In7_1_4 Real)
6
(declare-var gain_test_uK_order.In7_1_5 Real)
7
(declare-var gain_test_uK_order.In7_1_6 Real)
8
(declare-var gain_test_uK_order.Out7_1_1 Real)
9
(declare-var gain_test_uK_order.Out7_1_2 Real)
10
(declare-var gain_test_uK_order.Out7_1_3 Real)
11
(declare-var gain_test_uK_order.Out7_1_4 Real)
12
(declare-var gain_test_uK_order.ni_0._arrow._first_c Bool)
13
(declare-var gain_test_uK_order.ni_0._arrow._first_m Bool)
14
(declare-var gain_test_uK_order.ni_0._arrow._first_x Bool)
15
(declare-var gain_test_uK_order.Gain6_1_1 Real)
16
(declare-var gain_test_uK_order.Gain6_1_2 Real)
17
(declare-var gain_test_uK_order.Gain6_1_3 Real)
18
(declare-var gain_test_uK_order.Gain6_1_4 Real)
19
(declare-var gain_test_uK_order.__gain_test_uK_order_1 Bool)
20
(declare-var gain_test_uK_order.i_virtual_local Real)
21
(declare-rel gain_test_uK_order_reset (Bool Bool))
22
(declare-rel gain_test_uK_order_step (Real Real Real Real Real Real Real Real Real Real Bool Bool))
23

    
24
(rule (=> 
25
  (and 
26
       
27
       (= gain_test_uK_order.ni_0._arrow._first_m true)
28
  )
29
  (gain_test_uK_order_reset gain_test_uK_order.ni_0._arrow._first_c
30
                            gain_test_uK_order.ni_0._arrow._first_m)
31
))
32

    
33
(rule (=> 
34
  (and (= gain_test_uK_order.ni_0._arrow._first_m gain_test_uK_order.ni_0._arrow._first_c)
35
       (and (= gain_test_uK_order.__gain_test_uK_order_1 (ite gain_test_uK_order.ni_0._arrow._first_m true false))
36
            (= gain_test_uK_order.ni_0._arrow._first_x false))
37
       (and (or (not (= gain_test_uK_order.__gain_test_uK_order_1 true))
38
               (= gain_test_uK_order.i_virtual_local 0.0))
39
            (or (not (= gain_test_uK_order.__gain_test_uK_order_1 false))
40
               (= gain_test_uK_order.i_virtual_local 1.0))
41
       )
42
       (= gain_test_uK_order.Gain6_1_4 (+ (+ (* gain_test_uK_order.In7_1_4 2.00000000) (* gain_test_uK_order.In7_1_5 4.00000000)) (* gain_test_uK_order.In7_1_6 6.00000000)))
43
       (= gain_test_uK_order.Out7_1_4 gain_test_uK_order.Gain6_1_4)
44
       (= gain_test_uK_order.Gain6_1_3 (+ (+ (* gain_test_uK_order.In7_1_4 1.00000000) (* gain_test_uK_order.In7_1_5 3.00000000)) (* gain_test_uK_order.In7_1_6 5.00000000)))
45
       (= gain_test_uK_order.Out7_1_3 gain_test_uK_order.Gain6_1_3)
46
       (= gain_test_uK_order.Gain6_1_2 (+ (+ (* gain_test_uK_order.In7_1_1 2.00000000) (* gain_test_uK_order.In7_1_2 4.00000000)) (* gain_test_uK_order.In7_1_3 6.00000000)))
47
       (= gain_test_uK_order.Out7_1_2 gain_test_uK_order.Gain6_1_2)
48
       (= gain_test_uK_order.Gain6_1_1 (+ (+ (* gain_test_uK_order.In7_1_1 1.00000000) (* gain_test_uK_order.In7_1_2 3.00000000)) (* gain_test_uK_order.In7_1_3 5.00000000)))
49
       (= gain_test_uK_order.Out7_1_1 gain_test_uK_order.Gain6_1_1)
50
       )
51
  (gain_test_uK_order_step gain_test_uK_order.In7_1_1
52
                           gain_test_uK_order.In7_1_2
53
                           gain_test_uK_order.In7_1_3
54
                           gain_test_uK_order.In7_1_4
55
                           gain_test_uK_order.In7_1_5
56
                           gain_test_uK_order.In7_1_6
57
                           gain_test_uK_order.Out7_1_1
58
                           gain_test_uK_order.Out7_1_2
59
                           gain_test_uK_order.Out7_1_3
60
                           gain_test_uK_order.Out7_1_4
61
                           gain_test_uK_order.ni_0._arrow._first_c
62
                           gain_test_uK_order.ni_0._arrow._first_x)
63
))
64