automaton_G.jl 10.8 KB
Newer Older
1

2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
@everywhere istrue(val::Float64) = convert(Bool, val)

# Invariant predicate functions
@everywhere true_inv_predicate(x::Vector{Int}) = true 

# l0 loc
# l0 => l1
@everywhere cc_aut_G_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true

# l1 => l3
@everywhere cc_aut_G_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
getfield(S, :time) <= constants[:t1] && 
S[:n] < constants[:x1] || S[:n] > constants[:x2]
@everywhere us_aut_G_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l3; 
 S[:d] = min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); 
 S[:in] = false)

@everywhere cc_aut_G_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(getfield(S, :time) <= constants[:t1]) && 
(constants[:x1] <= S[:n] <= constants[:x2])
@everywhere us_aut_G_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l3; 
 S[:d] = 0; 
 S[:in] = false)

@everywhere cc_aut_G_l1l3_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
!istrue(S[:in]) && 
(constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
(constants[:x1] <= S[:n] <= constants[:x2])
@everywhere us_aut_G_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l3; 
 S[:d] = S[:d] * (getfield(S, :time) - constants[:t1]); 
 S[:tprime] = 0.0)

@everywhere cc_aut_G_l1l3_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
istrue(S[:in]) && 
(constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
(constants[:x1] <= S[:n] <= constants[:x2])
@everywhere us_aut_G_l1l3_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l3; 
 S[:tprime] = 0.0)

# l1 => l4
@everywhere cc_aut_G_l1l4_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
!istrue(S[:in]) && 
(constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
(S[:n] < constants[:x1] || S[:n] > constants[:x2])
@everywhere us_aut_G_l1l4_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l4; 
 S[:d] += S[:d] * (getfield(S, :time) - constants[:t1]))

@everywhere cc_aut_G_l1l4_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
istrue(S[:in]) && 
(constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
(S[:n] < constants[:x1] || S[:n] > constants[:x2])
@everywhere us_aut_G_l1l4_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l4)


# l1 => l2
@everywhere cc_aut_G_l1l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
istrue(S[:in]) && 
getfield(S, :time) >= constants[:t2]
@everywhere us_aut_G_l1l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2)

@everywhere cc_aut_G_l1l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
!istrue(S[:in]) && 
getfield(S, :time) >= constants[:t2]
@everywhere us_aut_G_l1l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2; 
 S[:d] = S[:d] * (constants[:t2] - constants[:t1]))

@everywhere cc_aut_G_l1l2_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
istrue(S[:isabs]) && 
getfield(S, :time) <= constants[:t1]
@everywhere us_aut_G_l1l2_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2; 
 S[:d] = (constants[:t2] - constants[:t1]) *
min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])))

@everywhere cc_aut_G_l1l2_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
istrue(S[:isabs]) && 
(constants[:t1] <= getfield(S, :time) <= constants[:t2])
@everywhere us_aut_G_l1l2_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2; 
 S[:d] += (constants[:t2] - getfield(S, :time)) * 
min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])))

# l3 => l1
@everywhere cc_aut_G_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true

# l4 => l1
@everywhere cc_aut_G_l4l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true

# l2 => l1
@everywhere cc_aut_G_l3l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
istrue(S[:in]) && 
getfield(S, :time) >= constants[:t2]
@everywhere us_aut_G_l3l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2;
 S[:d] = S[:d] * (constants[:t2] - constants[:t1]))

@everywhere cc_aut_G_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
!istrue(S[:in]) && 
getfield(S, :time) >= constants[:t2]
@everywhere us_aut_G_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2)

# l4 => l2
@everywhere cc_aut_G_l4l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(getfield(S, :time) >= constants[:t2])
@everywhere us_aut_G_l4l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
(S.loc = :l2; 
 S[:d] +=  S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); 
 S[:tprime] = 0.0)

120
function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
121
122
123
124
125
    # Requirements for the automaton
    @assert sym_obs in m.g "$(sym_obs) is not observed."
    @assert (x1 <= x2) "x1 > x2 impossible for G automaton."
    @assert (t1 <= t2) "t1 > t2 impossible for G automaton."
    
126
    # Locations
127
    locations = [:l0, :l1, :l2, :l3, :l4]
128
129

    # Invariant predicates
130
131
132
    Λ_F = Dict(:l0 => getfield(Main, :true_inv_predicate), :l1 => getfield(Main, :true_inv_predicate),
               :l2 => getfield(Main, :true_inv_predicate), :l3 => getfield(Main, :true_inv_predicate), 
               :l4 => getfield(Main, :true_inv_predicate))
133
134
    
    ## Init and final loc
135
136
    locations_init = [:l0]
    locations_final = [:l2]
137
138

    ## Map of automaton variables
139
140
    map_var_automaton_idx = Dict{VariableAutomaton,Int}(:tprime => 1, :in => 2,
                                                        :n => 3,  :d => 4, :isabs => 5)
141
142

    ## Flow of variables
143
144
145
146
147
    flow = Dict{Location,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])
148
149

    ## Edges
150
151
152
153
    map_edges = Dict{Location, Dict{Location, Vector{Edge}}}()
    for loc in locations 
        map_edges[loc] = Dict{Location, Vector{Edge}}()
    end
154
155

    sym_isabs_func = Symbol(m.isabsorbing)
156
157
158
159
    idx_obs_var = getfield(m, :map_var_idx)[sym_obs]
    nbr_rand = rand(1:1000)
    basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
    basename_func = replace(basename_func, '-'=>'_')
160
161

    # l0 loc
162
163
164
165
166
167
168
169
170
171
172
    # l0 => l1
    sym_func_us_l0l1_1 = Symbol("us_aut_G_$(basename_func)_l0l1_1!")
    str_us_l0l1_1 = "
    @everywhere $(sym_func_us_l0l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
    (S.loc = :l1; \n
    S[:d] = 0; \n
    S[:n] = x[$(idx_obs_var)]; \n
    S[:in] = true; \n
    S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
    eval(Meta.parse(str_us_l0l1_1))
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l0l1_1), getfield(Main, sym_func_us_l0l1_1))
173
    map_edges[:l0][:l1] = [edge1]
174
175

    # l1 loc
176
    # l1 => l3
177
178
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_1), getfield(Main, :us_aut_G_l1l3_1!))
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_2), getfield(Main, :us_aut_G_l1l3_2!))
179
    edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_3), getfield(Main, :us_aut_G_l1l3_3!))
180
    edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_4), getfield(Main, :us_aut_G_l1l3_4!))
181
    map_edges[:l1][:l3] = [edge1, edge2, edge3, edge4]
182

183
    # l1 => l4
184
185
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l4_1), getfield(Main, :us_aut_G_l1l4_1!))
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l4_2), getfield(Main, :us_aut_G_l1l4_2!))
186
    map_edges[:l1][:l4] = [edge1, edge2]
187
188
   
    # l1 => l2
189
190
191
192
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_1), getfield(Main, :us_aut_G_l1l2_1!))
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_2), getfield(Main, :us_aut_G_l1l2_2!))
    edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_3), getfield(Main, :us_aut_G_l1l2_3!))
    edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1l2_4), getfield(Main, :us_aut_G_l1l2_4!))
193
    map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
194
195

    # l3 loc
196
197
198
199
200
201
202
203
204
    # l3 => l1
    sym_func_us_l3l1_1 = Symbol("us_aut_G_$(basename_func)_l3l1_1!")
    str_us_l3l1_1 = "
    @everywhere $(sym_func_us_l3l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
    (S.loc = :l1; 
    S[:n] = x[$(idx_obs_var)]; 
    S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
    eval(Meta.parse(str_us_l3l1_1))
    edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l3l1_1), getfield(Main, sym_func_us_l3l1_1))
205
    map_edges[:l3][:l1] = [edge1]
206

207
    # l3 => l2
208
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_1), getfield(Main, :us_aut_G_l3l2_1!))
209
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_2), getfield(Main, :us_aut_G_l3l2_2!))
210
    map_edges[:l3][:l2] = [edge1, edge2]
211
212

    # l4 loc
213
214
215
216
217
218
219
220
221
222
223
224
    # l4 => l1
    sym_func_us_l4l1_1 = Symbol("us_aut_G_$(basename_func)_l4l1_1!")
    str_us_l4l1_1 = "
    @everywhere $(sym_func_us_l4l1_1)(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = \n
    (S.loc = :l1; \n
    S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); \n
    S[:tprime] = 0.0; \n
    S[:n] = x[$(idx_obs_var)]; \n
    S[:in] = true; \n
    S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))"
    eval(Meta.parse(str_us_l4l1_1))
    edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l4l1_1), getfield(Main, sym_func_us_l4l1_1))
225
    map_edges[:l4][:l1] = [edge1]
226

227
    # l4 => l2
228
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l4l2_1), getfield(Main, :us_aut_G_l4l2_1!))
229
    map_edges[:l4][:l2] = [edge1]
230
231

    ## Constants
232
    constants = Dict{Symbol,Float64}(:x1 => x1,  :x2 => x2, :t1 => t1, :t2 => t2)
233

234
    A = LHA("G property", m.transitions, locations, Λ_F, locations_init, locations_final, 
235
            map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
236
    return A
237
   
238
239
240
241
end

export create_automaton_G