automaton_G.jl 7.71 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

    # Invariant predicates
    true_inv_predicate = (A::LHA, S:: StateLHA) -> return true 
9
10
11
    Λ_F = Dict(:l0 => true_inv_predicate, :l1 => true_inv_predicate,
               :l2 => true_inv_predicate, :l3 => true_inv_predicate, 
               :l4 => 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
    istrue(val::Float64) = convert(Bool, val)
34
35

    # l0 loc
36
    tuple = (:l0, :l1)
37
    cc_aut_G_l0l1_1(A::LHA, S::StateLHA) = true
38
    us_aut_G_l0l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
39
40
41
42
43
        (S.loc = :l1; 
         S[:d] = 0; 
         S[:n] = get_value(A, x, str_obs); 
         S[:in] = true; 
         S[:isabs] = m.isabsorbing(m.p,x))
44
    edge1 = Edge([nothing], cc_aut_G_l0l1_1, us_aut_G_l0l1_1!)
45
    map_edges[:l0][:l1] = [edge1]
46
47

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

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

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

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

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

    # l3 loc
141
    tuple = (:l3, :l1)
142
    cc_aut_G_l3l1_1(A::LHA, S::StateLHA) = true
143
    us_aut_G_l3l1_1!(A::LHA, S::StateLHA, x::Vector{Int}) = 
144
145
146
        (S.loc = :l1; 
         S[:n] = get_value(A, x, str_obs); 
         S[:isabs] = m.isabsorbing(m.p,x))
147
    edge1 = Edge(["ALL"], cc_aut_G_l3l1_1, us_aut_G_l3l1_1!)
148
149
    
    map_edges[:l3][:l1] = [edge1]
150

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

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

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

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

196
197
    A = LHA(m.transitions, locations, Λ_F, locations_init, locations_final, 
            map_var_automaton_idx, flow, map_edges, constants, m.map_var_idx)
198
    return A
199
   
200
201
202
203
end

export create_automaton_G