Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / models / model_simple.ml @ 9c654082

History | View | Annotate | Download (2.28 KB)

1
open Datatype
2
open SF
3

    
4
let name = "simple"
5

    
6
let condition x = condition {
7
  expr = Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true));
8
  cinputs = [];
9
  coutputs = [];
10
  cvariables = [];
11
}
12
  
13
  let action _ = no_action
14

    
15
let model : prog_t =
16
    let state_main = "main" in
17
    let state_a = "a" in
18
    let state_a1 = "a1" in
19
    let state_b = "b" in
20

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

    
26
    let tA = {
27
      event = no_event;
28
      condition = condition "cond_tA";
29
      condition_act = action "condact_tA";
30
      transition_act = action "transact_tA";
31
      dest = DPath [state_main;state_a];
32
    }
33
    in
34
    let tB = {
35
      event = no_event;
36
      condition = condition "cond_tB";
37
      condition_act = action "condact_tB";
38
      transition_act = action "transact_tB";
39
      dest = DPath [state_main;state_b];
40
    }
41
    in
42
    let tA1 = {
43
      event = no_event;
44
      condition = condition "cond_tA1";
45
      condition_act = action "condact_tA1";
46
      transition_act = action "transact_tA1";
47
      dest = DPath [state_main;state_a;state_a1];
48
    }
49
    in
50

    
51

    
52
    let def_a = {
53
      state_actions = actions_a;
54
      outer_trans = [tB];
55
      inner_trans = [];
56
      internal_composition = Or ([tA1], [state_a1])
57
    }
58
    in
59
    let def_a1 = {
60
      state_actions = actions_a1;
61
      outer_trans = [tB];
62
      inner_trans = [];
63
      internal_composition = Or ([], [])
64
    }
65
    in
66
    let def_b = {
67
      state_actions = actions_b;
68
      outer_trans = [tA1];
69
      inner_trans = [];
70
      internal_composition = Or ([], [])
71
    }
72
    in
73
    let def_main = {
74
      state_actions = actions_main;
75
      outer_trans = [];
76
      inner_trans = [];
77
      internal_composition = Or ([tA], [state_a; state_b])
78
    }
79
    in
80
    let src = [State([state_main;state_a], def_a);
81
	       State([state_main;state_a;state_a1], def_a1);
82
	       State([state_main;state_b], def_b);
83
	       State([state_main], def_main);
84
	      ]
85
    in
86
    Program (state_main, src, [])
87

    
88
let traces : trace_t list = [[None; None]]