Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / tools / stateflow / models / model_simple.ml @ 69c96b6c

History | View | Annotate | Download (2.21 KB)

1
open Datatype
2
open SF
3

    
4
let name = "simple"
5

    
6
  let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
7
  let action _ = no_action
8
 
9
let model : prog_t =
10
    let state_main = "main" in
11
    let state_a = "a" in
12
    let state_a1 = "a1" in
13
    let state_b = "b" in
14

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

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

    
45

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

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