Project

General

Profile

Download (2.47 KB) Statistics
| Branch: | Tag: | Revision:
1
open Datatype
2
open SF
3

    
4
let name = "medium"
5

    
6
let condition x =
7
  condition
8
    (Corelang.mkexpr Location.dummy_loc
9
       (LustreSpec.Expr_const (Corelang.const_of_bool true)))
10

    
11
let model : prog_t =
12
  let state_main = "main" in
13
  let state_a = "a" in
14
  let state_a1 = "a1" in
15
  let state_b = "b" in
16

    
17
  let actions_main =
18
    state_action (action "emain") (action "dmain") (action "xmain")
19
  in
20
  let actions_a = state_action (action "eA") (action "dA") (action "xA") in
21
  let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in
22
  let actions_b = state_action (action "eB") (action "dB") (action "xB") in
23

    
24
  let tA =
25
    {
26
      event = no_event;
27
      condition = condition "cond_tA";
28
      condition_act = action "condact_tA";
29
      transition_act = action "transact_tA";
30
      dest = DPath [ state_main; state_a ];
31
    }
32
  in
33
  let tJ =
34
    {
35
      event = no_event;
36
      condition = condition "cond_tJ";
37
      condition_act = action "condact_tJ";
38
      transition_act = action "transact_tJ";
39
      dest = DJunction "jmid";
40
    }
41
  in
42
  let tB =
43
    {
44
      event = no_event;
45
      condition = condition "cond_tB";
46
      condition_act = action "condact_tB";
47
      transition_act = action "transact_tB";
48
      dest = DPath [ state_main; state_b ];
49
    }
50
  in
51
  let tA1 =
52
    {
53
      event = no_event;
54
      condition = condition "cond_tA1";
55
      condition_act = action "condact_tA1";
56
      transition_act = action "transact_tA1";
57
      dest = DPath [ state_main; state_a; state_a1 ];
58
    }
59
  in
60

    
61
  let def_a =
62
    {
63
      state_actions = actions_a;
64
      outer_trans = [ tJ ];
65
      inner_trans = [];
66
      internal_composition = Or ([ tA1 ], [ state_a1 ]);
67
    }
68
  in
69
  let def_a1 =
70
    {
71
      state_actions = actions_a1;
72
      outer_trans = [ tB ];
73
      inner_trans = [];
74
      internal_composition = Or ([], []);
75
    }
76
  in
77
  let def_b =
78
    {
79
      state_actions = actions_b;
80
      outer_trans = [ tA1 ];
81
      inner_trans = [];
82
      internal_composition = Or ([], []);
83
    }
84
  in
85
  let def_main =
86
    {
87
      state_actions = actions_main;
88
      outer_trans = [];
89
      inner_trans = [];
90
      internal_composition = Or ([ tA ], [ state_a; state_b ]);
91
    }
92
  in
93
  let src =
94
    [
95
      State ([ state_main; state_a ], def_a);
96
      State ([ state_main; state_a; state_a1 ], def_a1);
97
      State ([ state_main; state_b ], def_b);
98
      State ([ state_main ], def_main);
99
      Junction ("jmid", [ tB ]);
100
    ]
101
  in
102
  Program (state_main, src, [])
103

    
104
let traces : trace_t list = [ [ None; None ] ]
(1-1/3)