Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/tools/stateflow/models/model_medium.ml
3 3

  
4 4
let name = "medium"
5 5

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

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

  
14
    let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in
15
    let actions_a = state_action (action "eA") (action "dA") (action "xA") in
16
    let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in
17
    let actions_b = state_action (action "eB") (action "dB") (action "xB") in
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
18 23

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

  
52

  
53
    let def_a = {
61
  let def_a =
62
    {
54 63
      state_actions = actions_a;
55
      outer_trans = [tJ];
64
      outer_trans = [ tJ ];
56 65
      inner_trans = [];
57
      internal_composition = Or ([tA1], [state_a1])
66
      internal_composition = Or ([ tA1 ], [ state_a1 ]);
58 67
    }
59
    in
60
    let def_a1 = {
68
  in
69
  let def_a1 =
70
    {
61 71
      state_actions = actions_a1;
62
      outer_trans = [tB];
72
      outer_trans = [ tB ];
63 73
      inner_trans = [];
64
      internal_composition = Or ([], [])
74
      internal_composition = Or ([], []);
65 75
    }
66
    in
67
    let def_b = {
76
  in
77
  let def_b =
78
    {
68 79
      state_actions = actions_b;
69
      outer_trans = [tA1];
80
      outer_trans = [ tA1 ];
70 81
      inner_trans = [];
71
      internal_composition = Or ([], [])
82
      internal_composition = Or ([], []);
72 83
    }
73
    in
74
    let def_main = {
84
  in
85
  let def_main =
86
    {
75 87
      state_actions = actions_main;
76 88
      outer_trans = [];
77 89
      inner_trans = [];
78
      internal_composition = Or ([tA], [state_a; state_b])
90
      internal_composition = Or ([ tA ], [ state_a; state_b ]);
79 91
    }
80
    in
81
    let src = [State([state_main;state_a], def_a);
82
	       State([state_main;state_a;state_a1], def_a1);
83
	       State([state_main;state_b], def_b);
84
	       State([state_main], def_main);
85
	       Junction("jmid", [tB]);
86
	      ]
87
    in
88
    Program (state_main, src, [])
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, [])
89 103

  
90
let traces : trace_t list = [[None; None]]
104
let traces : trace_t list = [ [ None; None ] ]

Also available in: Unified diff