automaton_G.jl 7.62 KB
Newer Older
1
2
3
4

function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, str_obs::String)
    @assert str_obs in m.g
    # Locations
5
    locations = ["l0", "l1", "l2", "l3", "l4"]
6
7
8
9
10
11
12
13

    # 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
14
15
    locations_init = ["l0"]
    locations_final = ["l2"]
16
17

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

    ## Flow of variables
22
    flow = Dict{VariableAutomaton,Vector{Float64}}("l0" => [0.0,0.0,0.0,0.0,0.0], 
23
24
25
26
                                                     "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
    us_aut_G_l0l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
37
38
39
40
41
        (S.loc = "l1"; 
         S["d"] = 0; 
         S["n"] = get_value(A, x, str_obs); 
         S["in"] = true; 
         S["isabs"] = m.isabsorbing(m.p,x))
42
43
44
45
46
47
    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) = 
48
49
        S.time <= A.constants.t1 && 
        S["n"] < A.constants.x1 || S["n"] > A.constants.x2
50
    us_aut_G_l1l3_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
51
        (S.loc = "l3"; 
52
         S["d"] = min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])); 
53
         S["in"] = false)
54
    edge1 = Edge([nothing], cc_aut_G_l1l3_1, us_aut_G_l1l3_1!)
55
56
57

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

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

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

    tuple = ("l1", "l2")
105
106
    cc_aut_G_l1l2_1(A::LHA, S::StateLHA) = 
        istrue(S["in"]) && 
107
        S.time >= A.constants.t2
108
109
    us_aut_G_l1l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2")
110
    edge1 = Edge([nothing], cc_aut_G_l1l2_1, us_aut_G_l1l2_1!)
111
112
    cc_aut_G_l1l2_2(A::LHA, S::StateLHA) = 
        !istrue(S["in"]) && 
113
        S.time >= A.constants.t2
114
115
    us_aut_G_l1l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
116
         S["d"] = S["d"] * (A.constants.t2 - A.constants.t1))
117
    edge2 = Edge([nothing], cc_aut_G_l1l2_2, us_aut_G_l1l2_2!)
118
119
    cc_aut_G_l1l2_3(A::LHA, S::StateLHA) = 
        istrue(S["isabs"]) && 
120
        S.time <= A.constants.t1
121
122
    us_aut_G_l1l2_3!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
123
124
         S["d"] = (A.constants.t2 - A.constants.t1) *
                   min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])))
125
126
127
    edge3 = Edge([nothing], cc_aut_G_l1l2_3, us_aut_G_l1l2_3!)
    cc_aut_G_l1l2_4(A::LHA, S::StateLHA) = 
        istrue(S["isabs"]) && 
128
        (A.constants.t1 <= S.time <= A.constants.t2)
129
130
    us_aut_G_l1l2_4!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2"; 
131
132
         S["d"] += (A.constants.t2 - S.time) * 
                    min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])))
133
134
135
    edge4 = Edge([nothing], cc_aut_G_l1l2_4, us_aut_G_l1l2_4!)
    
    map_edges[tuple] = [edge1, edge2, edge3, edge4]
136
137
138
139

    # l3 loc
    tuple = ("l3", "l1")
    cc_aut_G_l3l1_1(A::LHA, S::StateLHA) = true
140
141
142
143
    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))
144
145
146
147
    edge1 = Edge(["ALL"], cc_aut_G_l3l1_1, us_aut_G_l3l1_1!)
    map_edges[tuple] = [edge1]

    tuple = ("l3", "l2")
148
    cc_aut_G_l3l2_2(A::LHA, S::StateLHA) = 
149
        istrue(S["in"]) && 
150
        S.time >= A.constants.t2
151
152
    us_aut_G_l3l2_2!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2";
153
         S["d"] = S["d"] * (A.constants.t2 - A.constants.t1))
154
    edge2 = Edge([nothing], cc_aut_G_l3l2_2, us_aut_G_l3l2_2!)
155
156
    cc_aut_G_l3l2_1(A::LHA, S::StateLHA) = 
        !istrue(S["in"]) && 
157
        S.time >= A.constants.t2
158
159
160
    us_aut_G_l3l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
        (S.loc = "l2")
    edge1 = Edge([nothing], cc_aut_G_l3l2_1, us_aut_G_l3l2_1!)
161
 
162
    map_edges[tuple] = [edge1, edge2]
163
164
165
166

    # l4 loc
    tuple = ("l4", "l1")
    cc_aut_G_l4l1_1(A::LHA, S::StateLHA) = true
167
    us_aut_G_l4l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
168
        (S.loc = "l1"; 
169
         S["d"] += S["tprime"] * min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])); 
170
         S["tprime"] = 0.0; 
171
172
173
         S["n"] = get_value(A, x, str_obs); 
         S["in"] = true; 
         S["isabs"] = m.isabsorbing(m.p,x))
174
175
176
177
    edge1 = Edge(["ALL"], cc_aut_G_l4l1_1, us_aut_G_l4l1_1!)
    map_edges[tuple] = [edge1]

    tuple = ("l4", "l2")
178
    cc_aut_G_l4l2_1(A::LHA, S::StateLHA) = 
179
        (S.time >= A.constants.t2)
180
    us_aut_G_l4l2_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
181
        (S.loc = "l2"; 
182
         S["d"] +=  S["tprime"] * min(abs(A.constants.x1 - S["n"]), abs(A.constants.x2 - S["n"])); 
183
         S["tprime"] = 0.0)
184
    edge1 = Edge([nothing], cc_aut_G_l4l2_1, us_aut_G_l4l2_1!)
185
    
186
    map_edges[tuple] = [edge1]
187
188

    ## Constants
189
    constants = (x1 = x1, x2 = x2, t1 = t1, t2 = t2)
190

191
192
    A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final, 
            map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
193
    return A
194
   
195
196
197
198
end

export create_automaton_G