Project

General

Profile

Download (2.3 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustrec
2
open Datatype
3
open Basetypes
4
open SF
5

    
6
let name = "simple"
7

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

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

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

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

    
53

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

    
90
let traces : trace_t list = [[None; None]]
(3-3/4)