Project

General

Profile

Download (2.29 KB) Statistics
| Branch: | Tag: | Revision:
1 2de7fa82 ploc
open Datatype
2 8446bf03 ploc
open Basetypes
3 2de7fa82 ploc
open SF
4
5
let name = "simple"
6
7 9c654082 ploc
let condition x = condition {
8 8446bf03 ploc
  expr = Corelang.mkexpr Location.dummy_loc (Lustre_types.Expr_const (Corelang.const_of_bool true));
9 9c654082 ploc
  cinputs = [];
10
  coutputs = [];
11
  cvariables = [];
12
}
13
  
14 69c96b6c ploc
  let action _ = no_action
15 b06b7b77 Christophe Garion
16 2de7fa82 ploc
let model : prog_t =
17
    let state_main = "main" in
18
    let state_a = "a" in
19
    let state_a1 = "a1" in
20
    let state_b = "b" in
21
22
    let actions_main = state_action (action "emain") (action "dmain") (action "xmain") in
23
    let actions_a = state_action (action "eA") (action "dA") (action "xA") in
24
    let actions_a1 = state_action (action "eA1") (action "dA1") (action "xA1") in
25
    let actions_b = state_action (action "eB") (action "dB") (action "xB") in
26
27
    let tA = {
28
      event = no_event;
29
      condition = condition "cond_tA";
30
      condition_act = action "condact_tA";
31
      transition_act = action "transact_tA";
32
      dest = DPath [state_main;state_a];
33
    }
34
    in
35
    let tB = {
36
      event = no_event;
37
      condition = condition "cond_tB";
38
      condition_act = action "condact_tB";
39
      transition_act = action "transact_tB";
40
      dest = DPath [state_main;state_b];
41
    }
42
    in
43
    let tA1 = {
44
      event = no_event;
45
      condition = condition "cond_tA1";
46
      condition_act = action "condact_tA1";
47
      transition_act = action "transact_tA1";
48
      dest = DPath [state_main;state_a;state_a1];
49
    }
50
    in
51
52
53
    let def_a = {
54
      state_actions = actions_a;
55
      outer_trans = [tB];
56
      inner_trans = [];
57
      internal_composition = Or ([tA1], [state_a1])
58
    }
59
    in
60
    let def_a1 = {
61
      state_actions = actions_a1;
62
      outer_trans = [tB];
63
      inner_trans = [];
64
      internal_composition = Or ([], [])
65
    }
66
    in
67
    let def_b = {
68
      state_actions = actions_b;
69
      outer_trans = [tA1];
70
      inner_trans = [];
71
      internal_composition = Or ([], [])
72
    }
73
    in
74
    let def_main = {
75
      state_actions = actions_main;
76
      outer_trans = [];
77
      inner_trans = [];
78
      internal_composition = Or ([tA], [state_a; state_b])
79
    }
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
	      ]
86
    in
87 b06b7b77 Christophe Garion
    Program (state_main, src, [])
88 2de7fa82 ploc
89
let traces : trace_t list = [[None; None]]