Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / src / models / model_simple.ml @ 2de7fa82

History | View | Annotate | Download (2.06 KB)

1
open Datatype
2
open SF
3

    
4
let name = "simple"
5

    
6
 
7
let model : prog_t =
8
    let state_main = "main" in
9
    let state_a = "a" in
10
    let state_a1 = "a1" in
11
    let state_b = "b" in
12

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

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

    
43

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

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