Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_ref_subsystem_sub_test / ref_subsystem_sub_test.smt2 @ 6c3ea955

History | View | Annotate | Download (1.9 KB)

1
; 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.ni_0._arrow._first_c Bool)
5
(declare-var ref_subsystem_sub_test.ni_0._arrow._first_m Bool)
6
(declare-var ref_subsystem_sub_test.ni_0._arrow._first_x Bool)
7
(declare-var ref_subsystem_sub_test.Product_1_1 Real)
8
(declare-var ref_subsystem_sub_test.__ref_subsystem_sub_test_1 Bool)
9
(declare-var ref_subsystem_sub_test.i_virtual_local Real)
10
(declare-rel ref_subsystem_sub_test_reset (Bool Bool))
11
(declare-rel ref_subsystem_sub_test_step (Real Real Bool Bool))
12

    
13
(rule (=> 
14
  (and 
15
       
16
       (= ref_subsystem_sub_test.ni_0._arrow._first_m true)
17
  )
18
  (ref_subsystem_sub_test_reset ref_subsystem_sub_test.ni_0._arrow._first_c
19
                                ref_subsystem_sub_test.ni_0._arrow._first_m)
20
))
21

    
22
(rule (=> 
23
  (and (= ref_subsystem_sub_test.ni_0._arrow._first_m ref_subsystem_sub_test.ni_0._arrow._first_c)
24
       (and (= ref_subsystem_sub_test.__ref_subsystem_sub_test_1 (ite ref_subsystem_sub_test.ni_0._arrow._first_m true false))
25
            (= ref_subsystem_sub_test.ni_0._arrow._first_x false))
26
       (and (or (not (= ref_subsystem_sub_test.__ref_subsystem_sub_test_1 true))
27
               (= ref_subsystem_sub_test.i_virtual_local 0.0))
28
            (or (not (= ref_subsystem_sub_test.__ref_subsystem_sub_test_1 false))
29
               (= ref_subsystem_sub_test.i_virtual_local 1.0))
30
       )
31
       (= ref_subsystem_sub_test.Product_1_1 (* ref_subsystem_sub_test.In1_1_1 ref_subsystem_sub_test.In1_1_1))
32
       (= ref_subsystem_sub_test.Out1_1_1 ref_subsystem_sub_test.Product_1_1)
33
       )
34
  (ref_subsystem_sub_test_step ref_subsystem_sub_test.In1_1_1
35
                               ref_subsystem_sub_test.Out1_1_1
36
                               ref_subsystem_sub_test.ni_0._arrow._first_c
37
                               ref_subsystem_sub_test.ni_0._arrow._first_x)
38
))
39