automaton_G.jl 10.6 KB
Newer Older
1

2
3
function create_automaton_G(m::ContinuousTimeModel, x1::Float64, x2::Float64, t1::Float64, t2::Float64, sym_obs::VariableModel)
    @assert sym_obs in m.g
4
    # Locations
5
    locations = [:l0, :l1, :l2, :l3, :l4]
6
7

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

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

    ## Flow of variables
22
23
24
25
26
    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])
27
28

    ## Edges
29
30
31
32
    map_edges = Dict{Location, Dict{Location, Vector{Edge}}}()
    for loc in locations 
        map_edges[loc] = Dict{Location, Vector{Edge}}()
    end
33
34
35
    @everywhere istrue(val::Float64) = convert(Bool, val)

    sym_isabs_func = Symbol(m.isabsorbing)
36
37

    # l0 loc
38
    tuple = (:l0, :l1)
39
40
    @everywhere cc_aut_G_l0l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
    @everywhere us_aut_G_l0l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
41
42
        (S.loc = :l1; 
         S[:d] = 0; 
43
         S[:n] = get_value(S, x, $(Meta.quot(sym_obs))); 
44
         S[:in] = true; 
45
46
         S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l0l1_1), getfield(Main, :us_aut_G_l0l1_1!))
47
    map_edges[:l0][:l1] = [edge1]
48
49

    # l1 loc
50
    tuple = (:l1, :l3)
51
    @everywhere cc_aut_G_l1l3_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
52
53
        getfield(S, :time) <= constants[:t1] && 
        S[:n] < constants[:x1] || S[:n] > constants[:x2]
54
    @everywhere us_aut_G_l1l3_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
55
        (S.loc = :l3; 
56
         S[:d] = min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); 
57
         S[:in] = false)
58
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_1), getfield(Main, :us_aut_G_l1l3_1!))
59

60
    @everywhere cc_aut_G_l1l3_3(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
61
         !istrue(S[:in]) && 
62
63
         (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
         (constants[:x1] <= S[:n] <= constants[:x2])
64
    @everywhere us_aut_G_l1l3_3!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
65
        (S.loc = :l3; 
66
         S[:d] = S[:d] * (getfield(S, :time) - constants[:t1]); 
67
         S[:tprime] = 0.0)
68
    edge3 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_3), getfield(Main, :us_aut_G_l1l3_3!))
69
   
70
    @everywhere cc_aut_G_l1l3_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
71
72
        (getfield(S, :time) <= constants[:t1]) && 
        (constants[:x1] <= S[:n] <= constants[:x2])
73
    @everywhere us_aut_G_l1l3_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
74
75
76
        (S.loc = :l3; 
         S[:d] = 0; 
         S[:in] = false)
77
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_2), getfield(Main, :us_aut_G_l1l3_2!))
78

79
    @everywhere cc_aut_G_l1l3_4(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
80
        istrue(S[:in]) && 
81
82
        (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
        (constants[:x1] <= S[:n] <= constants[:x2])
83
    @everywhere us_aut_G_l1l3_4!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
84
85
        (S.loc = :l3; 
         S[:tprime] = 0.0)
86
    edge4 = Edge([nothing], getfield(Main, :cc_aut_G_l1l3_4), getfield(Main, :us_aut_G_l1l3_4!))
87
    
88
    map_edges[:l1][:l3] = [edge1, edge2, edge3, edge4]
89

90
    tuple = (:l1, :l4)
91
    @everywhere cc_aut_G_l1l4_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
92
        !istrue(S[:in]) && 
93
94
        (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
        (S[:n] < constants[:x1] || S[:n] > constants[:x2])
95
    @everywhere us_aut_G_l1l4_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
96
        (S.loc = :l4; 
97
         S[:d] += S[:d] * (getfield(S, :time) - constants[:t1]))
98
99
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l1l4_1), getfield(Main, :us_aut_G_l1l4_1!))
    @everywhere cc_aut_G_l1l4_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
100
        istrue(S[:in]) && 
101
102
        (constants[:t1] <= getfield(S, :time) <= constants[:t2]) && 
        (S[:n] < constants[:x1] || S[:n] > constants[:x2])
103
    @everywhere us_aut_G_l1l4_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
104
        (S.loc = :l4)
105
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l1l4_2), getfield(Main, :us_aut_G_l1l4_2!))
106
107
    
    map_edges[:l1][:l4] = [edge1, edge2]
108

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

    # l3 loc
143
    tuple = (:l3, :l1)
144
145
    @everywhere cc_aut_G_l3l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
    @everywhere us_aut_G_l3l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
146
        (S.loc = :l1; 
147
148
149
         S[:n] = get_value(S, x, $(Meta.quot(sym_obs))); 
         S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))
    edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l3l1_1), getfield(Main, :us_aut_G_l3l1_1!))
150
151
    
    map_edges[:l3][:l1] = [edge1]
152

153
    tuple = (:l3, :l2)
154
    @everywhere cc_aut_G_l3l2_2(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
155
        istrue(S[:in]) && 
156
        getfield(S, :time) >= constants[:t2]
157
    @everywhere us_aut_G_l3l2_2!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
158
        (S.loc = :l2;
159
         S[:d] = S[:d] * (constants[:t2] - constants[:t1]))
160
161
    edge2 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_2), getfield(Main, :us_aut_G_l3l2_2!))
    @everywhere cc_aut_G_l3l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
162
        !istrue(S[:in]) && 
163
        getfield(S, :time) >= constants[:t2]
164
    @everywhere us_aut_G_l3l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
165
        (S.loc = :l2)
166
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l3l2_1), getfield(Main, :us_aut_G_l3l2_1!))
167
 
168
    map_edges[:l3][:l2] = [edge1, edge2]
169
170

    # l4 loc
171
    tuple = (:l4, :l1)
172
173
    @everywhere cc_aut_G_l4l1_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = true
    @everywhere us_aut_G_l4l1_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
174
        (S.loc = :l1; 
175
         S[:d] += S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); 
176
         S[:tprime] = 0.0; 
177
         S[:n] = get_value(S, x, $(Meta.quot(sym_obs))); 
178
         S[:in] = true; 
179
180
         S[:isabs] = getfield(Main, $(Meta.quot(sym_isabs_func)))(p, x))
    edge1 = Edge([:ALL], getfield(Main, :cc_aut_G_l4l1_1), getfield(Main, :us_aut_G_l4l1_1!))
181
182
    
    map_edges[:l4][:l1] = [edge1]
183

184
    tuple = (:l4, :l2)
185
    @everywhere cc_aut_G_l4l2_1(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
186
        (getfield(S, :time) >= constants[:t2])
187
    @everywhere us_aut_G_l4l2_1!(S::StateLHA, constants::Dict{Symbol,Float64}, x::Vector{Int}, p::Vector{Float64}) = 
188
        (S.loc = :l2; 
189
         S[:d] +=  S[:tprime] * min(abs(constants[:x1] - S[:n]), abs(constants[:x2] - S[:n])); 
190
         S[:tprime] = 0.0)
191
    edge1 = Edge([nothing], getfield(Main, :cc_aut_G_l4l2_1), getfield(Main, :us_aut_G_l4l2_1!))
192
    
193
    map_edges[:l4][:l2] = [edge1]
194
195

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

198
    A = LHA("G property", m.transitions, locations, Λ_F, locations_init, locations_final, 
199
            map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
200
    return A
201
   
202
203
204
205
end

export create_automaton_G