automaton_G.jl 13.5 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
    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
56
        @everywhere $(func_name(:cc, :l0, :l1, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = true
57
58
        @everywhere $(func_name(:us, :l0, :l1, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, 0, $(idx_var_d));
59
60
         setindex!(S_values, x[$(idx_obs_var)], $(idx_var_n));
         setindex!(S_values, true, $(idx_var_in));
61
62
         setindex!(S_values, getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x), $(idx_var_isabs));
		:l1)
63
64

        # l1 => l3
65
66
67
        @everywhere $(func_name(:cc, :l1, :l3, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        S_time <= $t1 && 
        S_values[$(idx_var_n)] < $x1 || S_values[$(idx_var_n)] > $x2
68
69
70
71
        @everywhere $(func_name(:us, :l1, :l3, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, min(abs($x1 - S_values[$(idx_var_n)]), abs($x2 - S_values[$(idx_var_n)])), $(idx_var_d));
         setindex!(S_values, false, $(idx_var_in));
		:l3)
72
73
74
75

        @everywhere $(func_name(:cc, :l1, :l3, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (S_time <= $t1) && 
        ($x1 <= S_values[$(idx_var_n)] <= $x2)
76
77
78
79
        @everywhere $(func_name(:us, :l1, :l3, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, 0, $(idx_var_d));
         setindex!(S_values, false, $(idx_var_in));
		:l3)
80
81
82
83
84

        @everywhere $(func_name(:cc, :l1, :l3, 3))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(S_values[$(idx_var_in)]) && 
        ($t1 <= S_time <= $t2) && 
        ($x1 <= S_values[$(idx_var_n)] <= $x2)
85
86
87
88
        @everywhere $(func_name(:us, :l1, :l3, 3))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] * (S_time - $t1), $(idx_var_d));
         setindex!(S_values, 0.0, $(idx_var_tprime));
		:l3)
89
90
91
92
93

        @everywhere $(func_name(:cc, :l1, :l3, 4))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(S_values[$(idx_var_in)]) && 
        ($t1 <= S_time <= $t2) && 
        ($x1 <= S_values[$(idx_var_n)] <= $x2)
94
95
96
        @everywhere $(func_name(:us, :l1, :l3, 4))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, 0.0, $(idx_var_tprime));
		:l3)
97
98

        # l1 => l4
99
100
101
102
        @everywhere $(func_name(:cc, :l1, :l4, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(S_values[$(idx_var_in)]) && 
        ($t1 <= S_time <= $t2) && 
        (S_values[$(idx_var_n)] < $x1 || S_values[$(idx_var_n)] > $x2)
103
104
105
        @everywhere $(func_name(:us, :l1, :l4, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] + S_values[$(idx_var_d)] * (S_time - $t1), $(idx_var_d));
		:l4)
106
107
108
109
110

        @everywhere $(func_name(:cc, :l1, :l4, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(S_values[$(idx_var_in)]) && 
        ($t1 <= S_time <= $t2) && 
        (S_values[$(idx_var_n)] < $x1 || S_values[$(idx_var_n)] > $x2)
111
112
        @everywhere $(func_name(:us, :l1, :l4, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (:l4)
113
114
115


        # l1 => l2
116
        #=
117
118
119
        @everywhere $(func_name(:cc, :l1, :l2, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(S_values[$(idx_var_in)]) && 
        S_time >= $t2
120
121
        @everywhere $(func_name(:us, :l1, :l2, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (:l2)
122
123
124
125

        @everywhere $(func_name(:cc, :l1, :l2, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(S_values[$(idx_var_in)]) && 
        S_time >= $t2
126
127
128
        @everywhere $(func_name(:us, :l1, :l2, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] * ($t2 - $t1), $(idx_var_d));
		:l2)
129
130
131
132

        @everywhere $(func_name(:cc, :l1, :l2, 3))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(S_values[$(idx_var_isabs)]) && 
        S_time <= $t1
133
134
135
        @everywhere $(func_name(:us, :l1, :l2, 3))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, ($t2 - $t1) * min(abs($x1 - S_values[$(idx_var_n)]), abs($x2 - S_values[$(idx_var_n)])), $(idx_var_d));
		:l2)
136
137
138
139

        @everywhere $(func_name(:cc, :l1, :l2, 4))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        istrue(S_values[$(idx_var_isabs)]) && 
        ($t1 <= S_time <= $t2)
140
141
142
        @everywhere $(func_name(:us, :l1, :l2, 4))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] + ($t2 - S_time) * min(abs($x1 - S_values[$(idx_var_n)]), abs($x2 - S_values[$(idx_var_n)])), $(idx_var_d));
		:l2)
143
        =#
144
145

        # l3 => l1
146
        @everywhere $(func_name(:cc, :l3, :l1, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = true
147
148
149
150
        @everywhere $(func_name(:us, :l3, :l1, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, x[$(idx_obs_var)], $(idx_var_n));
         setindex!(S_values, getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x), $(idx_var_isabs));
		:l1)
151
152

        # l4 => l1
153
        @everywhere $(func_name(:cc, :l4, :l1, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = true
154
155
        @everywhere $(func_name(:us, :l4, :l1, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] + S_values[$(idx_var_tprime)] * min(abs($x1 - S_values[$(idx_var_n)]), abs($x2 - S_values[$(idx_var_n)])), $(idx_var_d));
156
157
158
         setindex!(S_values, 0.0, $(idx_var_tprime));
         setindex!(S_values, x[$(idx_obs_var)], $(idx_var_n));
         setindex!(S_values, true, $(idx_var_in));
159
160
         setindex!(S_values, getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x), $(idx_var_isabs));
		:l1)
161

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

        @everywhere $(func_name(:cc, :l3, :l2, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        !istrue(S_values[$(idx_var_in)]) && 
        (S_time >= $t2 || istrue(S_values[$(idx_var_isabs)]))
173
174
        @everywhere $(func_name(:us, :l3, :l2, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (:l2)
175
176

        # l4 => l2
177
178
        @everywhere $(func_name(:cc, :l4, :l2, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (istrue(S_values[$(idx_var_isabs)]))
179
180
181
182
        @everywhere $(func_name(:us, :l4, :l2, 1))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] + ($t2 - S_time) * min(abs($x1 - S_values[$(idx_var_n)]), abs($x2 - S_values[$(idx_var_n)])), $(idx_var_d));
         setindex!(S_values, 0.0, $(idx_var_tprime));
		:l2)
183
184
185

        @everywhere $(func_name(:cc, :l4, :l2, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (S_time >= $t2)
186
187
188
189
        @everywhere $(func_name(:us, :l4, :l2, 2))(S_time::Float64, S_values::Vector{Float64}, x::Vector{Int}, p::Vector{Float64}) = 
        (setindex!(S_values, S_values[$(idx_var_d)] + S_values[$(idx_var_tprime)] * min(abs($x1 - S_values[$(idx_var_n)]), abs($x2 - S_values[$(idx_var_n)])), $(idx_var_d));
         setindex!(S_values, 0.0, $(idx_var_tprime));
		:l2)
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