automaton_G.jl 14.1 KB
Newer Older
1

2

3
function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
4
5
6
7
8
    # 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."
    
9
    # Locations
10
    locations = [:l0, :l1, :l2, :l3, :l4]
11
12

    # Invariant predicates
13
    @everywhere true_inv_predicate(x::Vector{Int}) = true 
14
15
16
    Λ_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))
17
18
    
    ## Init and final loc
19
20
    locations_init = [:l0]
    locations_final = [:l2]
21
22

    ## Map of automaton variables
23
24
    map_var_automaton_idx = Dict{VariableAutomaton,Int}(:tprime => 1, :in => 2,
                                                        :n => 3,  :d => 4, :isabs => 5)
25
26

    ## Flow of variables
27
28
29
30
31
    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])
32
33

    ## Edges
34
35
36
37
    map_edges = Dict{Location, Dict{Location, Vector{Edge}}}()
    for loc in locations 
        map_edges[loc] = Dict{Location, Vector{Edge}}()
    end
38

39
    idx_obs_var = getfield(m, :map_var_idx)[sym_obs]
40
41
42
43
44
45
46
    idx_var_n = map_var_automaton_idx[:n] 
    idx_var_d = map_var_automaton_idx[:d] 
    idx_var_isabs = map_var_automaton_idx[:isabs] 
    idx_var_in = map_var_automaton_idx[:in] 
    idx_var_tprime = map_var_automaton_idx[:tprime]

    nbr_rand = rand(1:100000)
47
48
    basename_func = "$(replace(m.name, ' '=>'_'))_$(nbr_rand)"
    basename_func = replace(basename_func, '-'=>'_')
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
    sym_isabs_func = Symbol(m.isabsorbing)
    func_name(type_func::Symbol, from_loc::Location, to_loc::Location, edge_number::Int) = 
    Symbol("$(type_func)_aut_G_$(basename_func)_$(from_loc)$(to_loc)_$(edge_number)$(type_func == :us ? "!" : "")")
    meta_elementary_functions = quote
        @everywhere istrue(val::Float64) = convert(Bool, val)
        # l0 loc
        # l0 => l1
        @everywhere $(func_name(:cc, :l0, :l1, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = true
        @everywhere $(func_name(:us, :l0, :l1, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l1")); 
         setindex!(getfield(S, :values), 0, $(idx_var_d));
         setindex!(getfield(S, :values), x[$(idx_obs_var)], $(idx_var_n));
         setindex!(getfield(S, :values), true, $(idx_var_in));
         setindex!(getfield(S, :values), getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x), $(idx_var_isabs)))

        # l1 => l3
        @everywhere $(func_name(:cc, :l1, :l3, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        getfield(S, :time) <= $t1 && 
        getfield(S, :values)[$(idx_var_n)] < $x1 || getfield(S, :values)[$(idx_var_n)] > $x2
        @everywhere $(func_name(:us, :l1, :l3, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l3")); 
         setindex!(getfield(S, :values), min(abs($x1 - getfield(S, :values)[$(idx_var_n)]), abs($x2 - getfield(S, :values)[$(idx_var_n)])), $(idx_var_d));
         setindex!(getfield(S, :values), false, $(idx_var_in)))

        @everywhere $(func_name(:cc, :l1, :l3, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (getfield(S, :time) <= $t1) && 
        ($x1 <= getfield(S, :values)[$(idx_var_n)] <= $x2)
        @everywhere $(func_name(:us, :l1, :l3, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l3")); 
         setindex!(getfield(S, :values), 0, $(idx_var_d));
         setindex!(getfield(S, :values), false, $(idx_var_in)))

        @everywhere $(func_name(:cc, :l1, :l3, 3))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(getfield(S, :values)[$(idx_var_in)]) && 
        ($t1 <= getfield(S, :time) <= $t2) && 
        ($x1 <= getfield(S, :values)[$(idx_var_n)] <= $x2)
        @everywhere $(func_name(:us, :l1, :l3, 3))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l3")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] * (getfield(S, :time) - $t1), $(idx_var_d));
         setindex!(getfield(S, :values), 0.0, $(idx_var_tprime)))

        @everywhere $(func_name(:cc, :l1, :l3, 4))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(getfield(S, :values)[$(idx_var_in)]) && 
        ($t1 <= getfield(S, :time) <= $t2) && 
        ($x1 <= getfield(S, :values)[$(idx_var_n)] <= $x2)
        @everywhere $(func_name(:us, :l1, :l3, 4))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l3")); 
         setindex!(getfield(S, :values), 0.0, $(idx_var_tprime)))

        # l1 => l4
        @everywhere $(func_name(:cc, :l1, :l4, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(getfield(S, :values)[$(idx_var_in)]) && 
        ($t1 <= getfield(S, :time) <= $t2) && 
        (getfield(S, :values)[$(idx_var_n)] < $x1 || getfield(S, :values)[$(idx_var_n)] > $x2)
        @everywhere $(func_name(:us, :l1, :l4, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l4")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] + getfield(S, :values)[$(idx_var_d)] * (getfield(S, :time) - $t1), $(idx_var_d)))

        @everywhere $(func_name(:cc, :l1, :l4, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(getfield(S, :values)[$(idx_var_in)]) && 
        ($t1 <= getfield(S, :time) <= $t2) && 
        (getfield(S, :values)[$(idx_var_n)] < $x1 || getfield(S, :values)[$(idx_var_n)] > $x2)
        @everywhere $(func_name(:us, :l1, :l4, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l4")))


        # l1 => l2
116
        #=
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
        @everywhere $(func_name(:cc, :l1, :l2, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(getfield(S, :values)[$(idx_var_in)]) && 
        getfield(S, :time) >= $t2
        @everywhere $(func_name(:us, :l1, :l2, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l2")))

        @everywhere $(func_name(:cc, :l1, :l2, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(getfield(S, :values)[$(idx_var_in)]) && 
        getfield(S, :time) >= $t2
        @everywhere $(func_name(:us, :l1, :l2, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l2")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] * ($t2 - $t1), $(idx_var_d)))

        @everywhere $(func_name(:cc, :l1, :l2, 3))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(getfield(S, :values)[$(idx_var_isabs)]) && 
        getfield(S, :time) <= $t1
        @everywhere $(func_name(:us, :l1, :l2, 3))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l2")); 
         setindex!(getfield(S, :values), ($t2 - $t1) * min(abs($x1 - getfield(S, :values)[$(idx_var_n)]), abs($x2 - getfield(S, :values)[$(idx_var_n)])), $(idx_var_d)))

        @everywhere $(func_name(:cc, :l1, :l2, 4))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(getfield(S, :values)[$(idx_var_isabs)]) && 
        ($t1 <= getfield(S, :time) <= $t2)
        @everywhere $(func_name(:us, :l1, :l2, 4))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l2")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] + ($t2 - getfield(S, :time)) * min(abs($x1 - getfield(S, :values)[$(idx_var_n)]), abs($x2 - getfield(S, :values)[$(idx_var_n)])), $(idx_var_d)))
143
        =#
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161

        # l3 => l1
        @everywhere $(func_name(:cc, :l3, :l1, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = true
        @everywhere $(func_name(:us, :l3, :l1, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l1")); 
         setindex!(getfield(S, :values), x[$(idx_obs_var)], $(idx_var_n));
         setindex!(getfield(S, :values), getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x), $(idx_var_isabs)))

        # l4 => l1
        @everywhere $(func_name(:cc, :l4, :l1, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = true
        @everywhere $(func_name(:us, :l4, :l1, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l1")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] + getfield(S, :values)[$(idx_var_tprime)] * min(abs($x1 - getfield(S, :values)[$(idx_var_n)]), abs($x2 - getfield(S, :values)[$(idx_var_n)])), $(idx_var_d));
         setindex!(getfield(S, :values), 0.0, $(idx_var_tprime));
         setindex!(getfield(S, :values), x[$(idx_obs_var)], $(idx_var_n));
         setindex!(getfield(S, :values), true, $(idx_var_in));
         setindex!(getfield(S, :values), getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x), $(idx_var_isabs)))

162
        # l3 => l2
163
164
        @everywhere $(func_name(:cc, :l3, :l2, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(getfield(S, :values)[$(idx_var_in)]) && 
165
        (getfield(S, :time) >= $t2 || istrue(getfield(S, :values)[$(idx_var_isabs)]))
166
167
168
169
170
171
        @everywhere $(func_name(:us, :l3, :l2, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l2"));
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] * ($t2 - $t1), $(idx_var_d)))

        @everywhere $(func_name(:cc, :l3, :l2, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(getfield(S, :values)[$(idx_var_in)]) && 
172
        (getfield(S, :time) >= $t2 || istrue(getfield(S, :values)[$(idx_var_isabs)]))
173
174
175
176
177
        @everywhere $(func_name(:us, :l3, :l2, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (setfield!(S, :loc, Symbol("l2")))

        # l4 => l2
        @everywhere $(func_name(:cc, :l4, :l2, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
Bentriou Mahmoud's avatar
Bentriou Mahmoud committed
178
        (istrue(getfield(S, :values)[$(idx_var_isabs)]))
179
        @everywhere $(func_name(:us, :l4, :l2, 1))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
Bentriou Mahmoud's avatar
Bentriou Mahmoud committed
180
181
182
183
184
185
186
        (setfield!(S, :loc, Symbol("l2")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] + ($t2 - getfield(S, :time)) * min(abs($x1 - getfield(S, :values)[$(idx_var_n)]), abs($x2 - getfield(S, :values)[$(idx_var_n)])), $(idx_var_d));
         setindex!(getfield(S, :values), 0.0, $(idx_var_tprime)))

        @everywhere $(func_name(:cc, :l4, :l2, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
        (getfield(S, :time) >= $t2)
        @everywhere $(func_name(:us, :l4, :l2, 2))(S::StateLHA, x::Vector{Int}, p::Vector{Float64}) = 
187
188
189
        (setfield!(S, :loc, Symbol("l2")); 
         setindex!(getfield(S, :values), getfield(S, :values)[$(idx_var_d)] + getfield(S, :values)[$(idx_var_tprime)] * min(abs($x1 - getfield(S, :values)[$(idx_var_n)]), abs($x2 - getfield(S, :values)[$(idx_var_n)])), $(idx_var_d));
         setindex!(getfield(S, :values), 0.0, $(idx_var_tprime)))
Bentriou Mahmoud's avatar
Bentriou Mahmoud committed
190
 
191
192
    end
    eval(meta_elementary_functions)
193
194

    # l0 loc
195
    # l0 => l1
196
    edge1 = Edge(nothing, getfield(Main, func_name(:cc, :l0, :l1, 1)), getfield(Main, func_name(:us, :l0, :l1, 1)))
197
    map_edges[:l0][:l1] = [edge1]
198
199

    # l1 loc
200
    # l1 => l3
201
202
203
204
    edge1 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l3, 1)), getfield(Main, func_name(:us, :l1, :l3, 1)))
    edge2 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l3, 2)), getfield(Main, func_name(:us, :l1, :l3, 2)))
    edge3 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l3, 3)), getfield(Main, func_name(:us, :l1, :l3, 3)))
    edge4 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l3, 4)), getfield(Main, func_name(:us, :l1, :l3, 4)))
205
    map_edges[:l1][:l3] = [edge1, edge2, edge3, edge4]
206

207
    # l1 => l4
208
209
    edge1 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l4, 1)), getfield(Main, func_name(:us, :l1, :l4, 1)))
    edge2 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l4, 2)), getfield(Main, func_name(:us, :l1, :l4, 2)))
210
    map_edges[:l1][:l4] = [edge1, edge2]
211
212
   
    # l1 => l2
213
    #=
214
215
216
217
    edge1 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l2, 1)), getfield(Main, func_name(:us, :l1, :l2, 1)))
    edge2 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l2, 2)), getfield(Main, func_name(:us, :l1, :l2, 2)))
    edge3 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l2, 3)), getfield(Main, func_name(:us, :l1, :l2, 3)))
    edge4 = Edge(nothing, getfield(Main, func_name(:cc, :l1, :l2, 4)), getfield(Main, func_name(:us, :l1, :l2, 4)))
218
    map_edges[:l1][:l2] = [edge1, edge2, edge3, edge4]
219
    =#
220
221

    # l3 loc
222
    # l3 => l1
223
    edge1 = Edge([:ALL], getfield(Main, func_name(:cc, :l3, :l1, 1)), getfield(Main, func_name(:us, :l3, :l1, 1)))
224
    map_edges[:l3][:l1] = [edge1]
225

226
    # l3 => l2
227
228
    edge1 = Edge(nothing, getfield(Main, func_name(:cc, :l3, :l2, 1)), getfield(Main, func_name(:us, :l3, :l2, 1)))
    edge2 = Edge(nothing, getfield(Main, func_name(:cc, :l3, :l2, 2)), getfield(Main, func_name(:us, :l3, :l2, 2)))
229
    map_edges[:l3][:l2] = [edge1, edge2]
230
231

    # l4 loc
232
    # l4 => l1
233
    edge1 = Edge([:ALL], getfield(Main, func_name(:cc, :l4, :l1, 1)), getfield(Main, func_name(:us, :l4, :l1, 1)))
234
    map_edges[:l4][:l1] = [edge1]
235

236
    # l4 => l2
237
238
    edge1 = Edge(nothing, getfield(Main, func_name(:cc, :l4, :l2, 1)), getfield(Main, func_name(:us, :l4, :l2, 1)))
    edge2 = Edge(nothing, getfield(Main, func_name(:cc, :l4, :l2, 2)), getfield(Main, func_name(:us, :l4, :l2, 2)))
Bentriou Mahmoud's avatar
Bentriou Mahmoud committed
239
    map_edges[:l4][:l2] = [edge1,edge2]
240
241

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

244
    A = LHA("G property", m.transitions, locations, Λ_F, locations_init, locations_final, 
245
            map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
246
    return A
247
   
248
249
250
251
end

export create_automaton_G