automaton_G.jl 8.25 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, str_obs::String)
    @assert str_obs in m.g
    # Locations
    l_loc = ["l0", "l1", "l2", "l3", "l4"]

    # Invariant predicates
    true_inv_predicate = (A::LHA, S:: StateLHA) -> return true 
    Λ_F = Dict("l0" => true_inv_predicate, "l1" => true_inv_predicate,
               "l2" => true_inv_predicate, "l3" => true_inv_predicate, 
               "l4" => true_inv_predicate)
    
    ## Init and final loc
    l_loc_init = ["l0"]
    l_loc_final = ["l2"]

    ## Map of automaton variables
    map_var_automaton_idx = Dict{VariableAutomaton,Int}("t'" => 1, "in" => 2,
19
                                                         "n" => 3,  "d" => 4, "isabs" => 5)
20
21

    ## Flow of variables
22
23
24
25
26
    l_flow = Dict{VariableAutomaton,Vector{Float64}}("l0" => [0.0,0.0,0.0,0.0,0.0], 
                                                     "l1" => [0.0,0.0,0.0,0.0,0.0], 
                                                     "l2" => [0.0,0.0,0.0,0.0,0.0], 
                                                     "l3" => [0.0,0.0,0.0,0.0,0.0], 
                                                     "l4" => [1.0,0.0,0.0,0.0,0.0])
27
28
29
30

    ## Edges
    map_edges = Dict{Tuple{Location,Location}, Vector{Edge}}()

31
    istrue(val::Float64) = convert(Bool, val)
32
33
34
35

    # l0 loc
    tuple = ("l0", "l1")
    cc_aut_G_l0l1_1(A::LHA, S::StateLHA) = true
36
37
    us_aut_G_l0l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
    (S.loc = "l1"; S["d"] = 0; S["n"] = get_value(A, x, str_obs); S["in"] = true; S["isabs"] = m.isabsorbing(m.p,x))
38
39
40
41
42
43
    edge1 = Edge([nothing], cc_aut_G_l0l1_1, us_aut_G_l0l1_1!)
    map_edges[tuple] = [edge1]

    # l1 loc
    tuple = ("l1", "l3")
    cc_aut_G_l1l3_1(A::LHA, S::StateLHA) = 
44
45
        (S.time < A.l_ctes["t1"] && 
         (S["n"] < A.l_ctes["x1"] || S["n"] > A.l_ctes["x2"]))
46
    us_aut_G_l1l3_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
47
48
49
        (S.loc = "l3"; 
         S["d"] = min(abs(A.l_ctes["x1"] - S["n"]), abs(A.l_ctes["x2"] - S["n"])); 
         S["in"] = false)
50
    edge1 = Edge([nothing], cc_aut_G_l1l3_1, us_aut_G_l1l3_1!)
51
52
53
54
55
56
57
58
59
60
61

    cc_aut_G_l1l3_3(A::LHA, S::StateLHA) = 
         !istrue(S["in"]) && 
         (A.l_ctes["t1"] <= S.time <= A.l_ctes["t2"]) && 
         (A.l_ctes["x1"] <= S["n"] <= A.l_ctes["x2"])
    us_aut_G_l1l3_3!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l3"; 
         S["d"] = S["d"] * (S.time - A.l_ctes["t1"]); 
         S["t'"] = 0.0)
    edge3 = Edge([nothing], cc_aut_G_l1l3_3, us_aut_G_l1l3_3!)
   
62
    cc_aut_G_l1l3_2(A::LHA, S::StateLHA) = 
63
64
        (S.time <= A.l_ctes["t1"]) && 
        (A.l_ctes["x1"] <= S["n"] <= A.l_ctes["x2"])
65
    us_aut_G_l1l3_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
66
67
68
        (S.loc = "l3"; 
         S["d"] = 0; 
         S["in"] = false)
69
    edge2 = Edge([nothing], cc_aut_G_l1l3_2, us_aut_G_l1l3_2!)
70

71
    cc_aut_G_l1l3_4(A::LHA, S::StateLHA) = 
72
73
74
75
76
77
        istrue(S["in"]) && 
        (A.l_ctes["t1"] <= S.time <= A.l_ctes["t2"]) && 
        (A.l_ctes["x1"] <= S["n"] <= A.l_ctes["x2"])
    us_aut_G_l1l3_4!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l3"; 
         S["t'"] = 0.0)
78
    edge4 = Edge([nothing], cc_aut_G_l1l3_4, us_aut_G_l1l3_4!)
79
    
80
81
82
83
    map_edges[tuple] = [edge1, edge2, edge3, edge4]

    tuple = ("l1", "l4")
    cc_aut_G_l1l4_1(A::LHA, S::StateLHA) = 
84
85
86
87
88
89
        !istrue(S["in"]) && 
        (A.l_ctes["t1"] <= S.time <= A.l_ctes["t2"]) && 
        (S["n"] < A.l_ctes["x1"] || S["n"] > A.l_ctes["x2"])
    us_aut_G_l1l4_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l4"; 
         S["d"] += S["d"] * (S.time - A.l_ctes["t1"]))
90
91
    edge1 = Edge([nothing], cc_aut_G_l1l4_1, us_aut_G_l1l4_1!)
    cc_aut_G_l1l4_2(A::LHA, S::StateLHA) = 
92
93
94
95
96
        istrue(S["in"]) && 
        (A.l_ctes["t1"] <= S.time <= A.l_ctes["t2"]) && 
        (S["n"] < A.l_ctes["x1"] || S["n"] > A.l_ctes["x2"])
    us_aut_G_l1l4_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l4")
97
98
99
100
    edge2 = Edge([nothing], cc_aut_G_l1l4_2, us_aut_G_l1l4_2!)
    map_edges[tuple] = [edge1, edge2]

    tuple = ("l1", "l2")
101
102
103
104
105
    cc_aut_G_l1l2_1(A::LHA, S::StateLHA) = 
        istrue(S["in"]) && 
        S.time >= A.l_ctes["t2"]
    us_aut_G_l1l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2")
106
    edge1 = Edge([nothing], cc_aut_G_l1l2_1, us_aut_G_l1l2_1!)
107
108
109
110
111
112
    cc_aut_G_l1l2_2(A::LHA, S::StateLHA) = 
        !istrue(S["in"]) && 
        S.time >= A.l_ctes["t2"]
    us_aut_G_l1l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
         S["d"] = S["d"] * (A.l_ctes["t2"] - A.l_ctes["t1"]))
113
114
115
116
117
118
    edge2 = Edge([nothing], cc_aut_G_l1l2_2, us_aut_G_l1l2_2!)
    map_edges[tuple] = [edge1, edge2]

    # l3 loc
    tuple = ("l3", "l1")
    cc_aut_G_l3l1_1(A::LHA, S::StateLHA) = true
119
120
121
122
    us_aut_G_l3l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l1"; 
         S["n"] = get_value(A, x, str_obs); 
         S["isabs"] = m.isabsorbing(m.p,x))
123
124
125
126
    edge1 = Edge(["ALL"], cc_aut_G_l3l1_1, us_aut_G_l3l1_1!)
    map_edges[tuple] = [edge1]

    tuple = ("l3", "l2")
127
128
129
130
131
    cc_aut_G_l3l2_1(A::LHA, S::StateLHA) = 
        istrue(S["in"]) && 
        (S.time >= A.l_ctes["t2"] || istrue(S["isabs"]))
    us_aut_G_l3l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2")
132
    edge1 = Edge([nothing], cc_aut_G_l3l2_1, us_aut_G_l3l2_1!)
133
134
135
136
137
138
    cc_aut_G_l3l2_2(A::LHA, S::StateLHA) = 
        !istrue(S["in"]) && 
        (S.time >= A.l_ctes["t2"] || istrue(S["isabs"]))
    us_aut_G_l3l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2";
         S["d"] = S["d"] * (A.l_ctes["t2"] - A.l_ctes["t1"]))
139
    edge2 = Edge([nothing], cc_aut_G_l3l2_2, us_aut_G_l3l2_2!)
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
    cc_aut_G_l3l2_3(A::LHA, S::StateLHA) = 
        istrue(S["isabs"]) && 
        S.time <= A.l_ctes["t1"]
    us_aut_G_l3l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
         S["d"] = S["d"] * (A.l_ctes["t2"] - A.l_ctes["t1"]))
    edge3 = Edge([nothing], cc_aut_G_l3l2_3, us_aut_G_l3l2_3!)
    cc_aut_G_l3l2_4(A::LHA, S::StateLHA) = 
        istrue(S["isabs"]) && 
        S.time >= A.l_ctes["t1"]
    us_aut_G_l3l2_4!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
         S["d"] += (A.l_ctes["t2"] - A.l_ctes["t1"]) * 
                    min(abs(S["n"] - A.l_ctes["x1"]), abs(S["n"] - A.l_ctes["x2"])))
    edge4 = Edge([nothing], cc_aut_G_l3l2_4, us_aut_G_l3l2_4!)
 
    map_edges[tuple] = [edge1, edge2, edge3, edge4]
157
158
159
160

    # l4 loc
    tuple = ("l4", "l1")
    cc_aut_G_l4l1_1(A::LHA, S::StateLHA) = true
161
    us_aut_G_l4l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
162
163
164
165
166
167
        (S.loc = "l1"; 
         S["d"] += S["t'"] * min(abs(A.l_ctes["x1"] - S["n"]), abs(A.l_ctes["x2"] - S["n"])); 
         S["t'"] = 0.0; 
         S["n"] = get_value(A, x, str_obs); 
         S["in"] = true; 
         S["isabs"] = m.isabsorbing(m.p,x))
168
169
170
171
    edge1 = Edge(["ALL"], cc_aut_G_l4l1_1, us_aut_G_l4l1_1!)
    map_edges[tuple] = [edge1]

    tuple = ("l4", "l2")
172
173
    cc_aut_G_l4l2_1(A::LHA, S::StateLHA) = 
        (S.time >= A.l_ctes["t2"] || istrue(S["isabs"]))
174
    us_aut_G_l4l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
175
176
177
        (S.loc = "l2"; 
         S["d"] +=  S["t'"] * min(abs(A.l_ctes["x1"] - S["n"]), abs(A.l_ctes["x2"] - S["n"])); 
         S["t'"] = 0.0)
178
    edge1 = Edge([nothing], cc_aut_G_l4l2_1, us_aut_G_l4l2_1!)
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
    cc_aut_G_l4l2_2(A::LHA, S::StateLHA) = 
        istrue(S["isabs"]) && 
        S.time <= A.l_ctes["t1"]
    us_aut_G_l4l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
         S["d"] = S["d"] * (A.l_ctes["t2"] - A.l_ctes["t1"]))
    edge2 = Edge([nothing], cc_aut_G_l4l2_2, us_aut_G_l4l2_2!)
    cc_aut_G_l4l2_3(A::LHA, S::StateLHA) = 
        istrue(S["isabs"]) && 
        S.time >= A.l_ctes["t1"]
    us_aut_G_l4l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
         S["d"] += (A.l_ctes["t2"] - A.l_ctes["t1"]) * 
                    min(abs(S["n"] - A.l_ctes["x1"]), abs(S["n"] - A.l_ctes["x2"])))
    edge3 = Edge([nothing], cc_aut_G_l4l2_3, us_aut_G_l4l2_3!)
    
    map_edges[tuple] = [edge1, edge2, edge3]
196
197
198
199
200
201
202

    ## Constants
    l_ctes = Dict{String,Float64}("x1" => x1, "x2" => x2, "t1" => t1, "t2" => t2)

    A = LHA(m.l_transitions, l_loc, Λ_F, l_loc_init, l_loc_final, 
            map_var_automaton_idx, l_flow, map_edges, l_ctes, m.map_var_idx)
    return A
203
   
204
205
206
207
end

export create_automaton_G