-
Notifications
You must be signed in to change notification settings - Fork 4
/
DiscretePost.jl
122 lines (107 loc) · 3.9 KB
/
DiscretePost.jl
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
120
121
122
import LazySets.use_precise_ρ
"""
DiscretePost
Abstract supertype of all discrete post operators.
### Notes
All discrete post operators should provide the following method, in addition
to those provided for general post operators:
```julia
tube⋂inv!(𝒫::DiscretePost, reach_tube::Vector{<:AbstractReachSet{<:LazySet, N}},
invariant, Rsets, start_interval) where {N}
```
"""
abstract type DiscretePost <: PostOperator end
function postprocess(𝒫,
HS,
post_jump,
options,
waiting_list,
passed_list,
target_loc_id,
jumps)
fixpoint_strategy = options[:fixpoint_check]
if fixpoint_strategy == :eager
# eager fixpoint checking
post_jump_filtered =
filter(x -> !isfixpoint(𝒫, x, passed_list, target_loc_id),
post_jump)
else
post_jump_filtered = post_jump
end
if (isempty(post_jump_filtered))
# fixpoint found or transition can never be taken
return
end
# apply clustering
clustered = cluster(𝒫, post_jump_filtered, options)
# push new sets after jump (unless a fixpoint is detected)
for reach_set in clustered
if fixpoint_strategy != :none
if fixpoint_strategy == :lazy &&
isfixpoint(𝒫, reach_set, passed_list, target_loc_id)
continue
end
push!(passed_list[target_loc_id], reach_set)
end
push!(waiting_list, (target_loc_id, reach_set, jumps))
end
end
function cluster(𝒫::DiscretePost,
reach_sets::Vector{RSN},
options::Options) where {SN, RSN<:AbstractReachSet{SN}}
clustering_strategy = options[:clustering]
oa = 𝒫.options[:overapproximation]
if clustering_strategy == :none
# no clustering, keeping original set
return reach_sets
elseif clustering_strategy == :none_oa
# no clustering but overapproximation
return [RSN(overapproximate(set(reach_set), oa),
time_start(reach_set), time_end(reach_set)) for reach_set in reach_sets]
elseif clustering_strategy == :chull
# cluster all sets in a convex hull and overapproximate that set
chull = ConvexHullArray([set(reach_set) for reach_set in reach_sets])
chull_oa = overapproximate(chull, oa)
return [RSN(chull_oa, time_start(reach_sets[1]),
time_end(reach_sets[end]))]
end
end
function isfixpoint(𝒫::DiscretePost,
reach_set::RSN,
passed_list,
loc_id
) where {SN, RSN<:AbstractReachSet{SN}}
@assert passed_list != nothing
if isassigned(passed_list, loc_id)
for other_reach_set in passed_list[loc_id]
if set(reach_set) ⊆ set(other_reach_set)
info("found a fixpoint in some reach tube")
return true
end
end
return false
else
passed_list[loc_id] = Vector{RSN}()
return false
end
end
# default: always apply line search
function use_precise_ρ(𝒫::DiscretePost,
cap::Intersection{N})::Bool where N<:Real
return true
end
# --- default methods for handling assignments ---
# default implementation: use 'apply' from MathematicalSystems
function apply_assignment(𝒫::DiscretePost,
constrained_map::AbstractMap,
R⋂G::LazySet;
kwargs...)
return apply(constrained_map, R⋂G)
end
# for reset maps: return a lazy ResetMap from LazySets
function apply_assignment(𝒫::DiscretePost,
constrained_map::ConstrainedResetMap,
R⋂G::LazySet;
kwargs...)
return LazySets.ResetMap(R⋂G, constrained_map.dict)
end