Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_ref_subsystem_test / ref_subsystem_test.smt2 @ 6c3ea955

History | View | Annotate | Download (3.05 KB)

1 6c3ea955 bourbouh
; ref_subsystem_sub_test
2
(declare-var ref_subsystem_sub_test.In1_1_1 Real)
3
(declare-var ref_subsystem_sub_test.Out1_1_1 Real)
4
(declare-var ref_subsystem_sub_test.Product_1_1 Real)
5
(declare-rel ref_subsystem_sub_test (Real Real))
6
(rule (=> 
7
  (and (= ref_subsystem_sub_test.Product_1_1 (* ref_subsystem_sub_test.In1_1_1 ref_subsystem_sub_test.In1_1_1))
8
       (= ref_subsystem_sub_test.Out1_1_1 ref_subsystem_sub_test.Product_1_1)
9
       )
10
  (ref_subsystem_sub_test ref_subsystem_sub_test.In1_1_1 ref_subsystem_sub_test.Out1_1_1)
11
))
12
13
; ref_subsystem_test_Subsystem
14
(declare-var ref_subsystem_test_Subsystem.In1_1_1 Real)
15
(declare-var ref_subsystem_test_Subsystem.Out1_1_1 Real)
16
(declare-var ref_subsystem_test_Subsystem.block_Subsystem_1_1 Real)
17
(declare-rel ref_subsystem_test_Subsystem (Real Real))
18
(rule (=> 
19
  (and (ref_subsystem_sub_test ref_subsystem_test_Subsystem.In1_1_1
20
                               ref_subsystem_test_Subsystem.block_Subsystem_1_1)
21
       (= ref_subsystem_test_Subsystem.Out1_1_1 ref_subsystem_test_Subsystem.block_Subsystem_1_1)
22
       )
23
  (ref_subsystem_test_Subsystem ref_subsystem_test_Subsystem.In1_1_1 ref_subsystem_test_Subsystem.Out1_1_1)
24
))
25
26
; ref_subsystem_test
27
(declare-var ref_subsystem_test.In1_1_1 Real)
28
(declare-var ref_subsystem_test.Out1_1_1 Real)
29
(declare-var ref_subsystem_test.ni_0._arrow._first_c Bool)
30
(declare-var ref_subsystem_test.ni_0._arrow._first_m Bool)
31
(declare-var ref_subsystem_test.ni_0._arrow._first_x Bool)
32
(declare-var ref_subsystem_test.Gain_1_1 Real)
33
(declare-var ref_subsystem_test.Subsystem_1_1 Real)
34
(declare-var ref_subsystem_test.__ref_subsystem_test_1 Bool)
35
(declare-var ref_subsystem_test.i_virtual_local Real)
36
(declare-rel ref_subsystem_test_reset (Bool Bool))
37
(declare-rel ref_subsystem_test_step (Real Real Bool Bool))
38
39
(rule (=> 
40
  (and 
41
       
42
       (= ref_subsystem_test.ni_0._arrow._first_m true)
43
  )
44
  (ref_subsystem_test_reset ref_subsystem_test.ni_0._arrow._first_c
45
                            ref_subsystem_test.ni_0._arrow._first_m)
46
))
47
48
(rule (=> 
49
  (and (= ref_subsystem_test.ni_0._arrow._first_m ref_subsystem_test.ni_0._arrow._first_c)
50
       (and (= ref_subsystem_test.__ref_subsystem_test_1 (ite ref_subsystem_test.ni_0._arrow._first_m true false))
51
            (= ref_subsystem_test.ni_0._arrow._first_x false))
52
       (and (or (not (= ref_subsystem_test.__ref_subsystem_test_1 true))
53
               (= ref_subsystem_test.i_virtual_local 0.0))
54
            (or (not (= ref_subsystem_test.__ref_subsystem_test_1 false))
55
               (= ref_subsystem_test.i_virtual_local 1.0))
56
       )
57
       (= ref_subsystem_test.Gain_1_1 (* 1.00000000 ref_subsystem_test.In1_1_1))
58
       (ref_subsystem_test_Subsystem ref_subsystem_test.Gain_1_1
59
                                     ref_subsystem_test.Subsystem_1_1)
60
       (= ref_subsystem_test.Out1_1_1 ref_subsystem_test.Subsystem_1_1)
61
       )
62
  (ref_subsystem_test_step ref_subsystem_test.In1_1_1
63
                           ref_subsystem_test.Out1_1_1
64
                           ref_subsystem_test.ni_0._arrow._first_c
65
                           ref_subsystem_test.ni_0._arrow._first_x)
66
))