forked from Eelis/hybrid
-
Notifications
You must be signed in to change notification settings - Fork 0
/
abstract.v
340 lines (269 loc) · 11 KB
/
abstract.v
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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
Set Automatic Coercions Import.
Require Import List Bool.
Require Import util list_util stability containers.
Require Import CSetoids.
Require Import Morphisms.
Set Implicit Arguments.
Require Import EquivDec.
Require concrete.
Require Import CoLoR.Util.Vector.VecUtil.
Require Import hybrid.vector_setoid.
Require hybrid.nat_util.
Require Import hybrid.hlist_aux.
Module c := concrete.
Section contents.
Variable chs: concrete.System.
Record Space: Type :=
{ Region: Type
; Region_eq_dec: EquivDec.EqDec Region eq
; regions: ExhaustiveList Region
; NoDup_regions: NoDup regions
; in_region: Container (concrete.Point chs) Region
; in_region_mor: Proper (@cs_eq _ ==> eq ==> iff) in_region
; regions_cover: forall l p, c.invariant (l, p) -> DN (sig (in_region p))
}.
Existing Instance in_region.
Existing Instance Region_eq_dec.
Existing Instance regions.
Existing Instance in_region_mor.
Section space_derivatives.
Variable p: Space.
Definition State := (concrete.Location chs * Region p)%type.
Definition region: State -> Region p := snd.
Definition location: State -> c.Location chs := fst.
Definition states: ExhaustiveList State := @ExhaustivePairList (concrete.Location chs) (Region p) _ _.
Lemma NoDup_states: NoDup (regions p) -> NoDup states.
Proof. apply NoDup_ExhaustivePairList, c.NoDup_locations. Qed.
End space_derivatives.
(* Given two sets of abstraction parameters, we can combine these to make
finer-grained abstraction parameters where each region corresponds to the
intersection of two regions of the respective abstraction parameters.
For instance, for a hybrid system whose continuous state space is the plane,
we could first define abstraction parameters with regions corresponding to X
intervals, then define abstraction parameters with regions corresponding to
Y intervals, and then finally combine these using param_prod below to
produce abstraction parameters with regions corresponding to squares. *)
Section prod_space.
Variables ap ap': Space.
Let in_region p r := in_region ap p (fst r) /\ in_region ap' p (snd r).
Let in_region_mor: Proper (@cs_eq _ ==> eq ==> iff) in_region.
Proof. unfold in_region. intros x x' e r r' e'. rewrite e, e'. split; auto. Qed.
Program Definition regions_cover_prod l p : concrete.invariant (l, p) -> DN (sig (in_region p)) :=
fun H =>
C1 <- contents.regions_cover ap l p H;
C2 <- contents.regions_cover ap' l p H;
return [=(`C1, `C2)=].
Next Obligation.
split; crunch.
Qed.
Definition prod_space: Space := Build_Space _ _
(NoDup_ExhaustivePairList (NoDup_regions ap) (NoDup_regions ap'))
in_region_mor regions_cover_prod.
End prod_space.
(* We generalize the product space above from 2 to arbitrary 'n' dimensions,
hence generalizing abstraction by squares in 2 dimensional space to
abstraction by hyper-cubes in n-dimensional space *)
Section hyper_space.
Variable n : nat.
Variable aps : list Space.
(* [Regions] is formed by an n-product of [Region]s of respective [Space]s,
epxressed with heterogenous list *)
Notation Regions aps := (@hlist _ Region aps).
Fixpoint in_region_aux (aps : list Space) (p : concrete.Point chs) : Regions aps -> Prop :=
match aps as aps return Regions aps -> Prop with
| [] => fun _ => True
| s::ss => fun rs =>
in_region s p (hhd rs) /\ @in_region_aux ss p (htl rs)
end.
Obligation Tactic := crunch.
Program Fixpoint regions_cover_aux (aps : list Space) l p :
concrete.invariant (l, p) -> DN (sig (@in_region_aux aps p)) :=
match aps with
| [] => fun H => return [= HNil (H:=_) =]
| s::ss => fun H =>
C1 <- contents.regions_cover s l p H;
C2 <- @regions_cover_aux ss l p H;
return [= `C1:::`C2 =]
end.
Lemma in_region_aux_morph : Proper (@st_eq _ ==> eq ==> iff) (@in_region_aux aps).
Proof with auto.
repeat intro.
subst.
induction aps. firstorder.
split; intros [H0 H1]; split.
apply (in_region_mor a x y H (refl_equal _))...
apply IHl...
apply (in_region_mor a x y H (refl_equal _))...
apply IHl...
Qed.
Obligation Tactic := program_simpl; auto with typeclass_instances.
Hint Resolve NoDup_regions.
Program Definition hyper_space : Space := @Build_Space (Regions aps) _ _ _
(@in_region_aux aps) in_region_aux_morph (@regions_cover_aux aps).
Next Obligation.
set (w := NoDup_ExhaustiveHList); simpl in w; apply w; auto.
Qed.
End hyper_space.
Variable ap: Space.
Instance abs: Container (c.State chs) (State ap) := fun s s' =>
c.location s = location s' /\ c.point s ∈ region s'.
Hint Unfold abs.
Section CoverRelandsuch.
Context `{Container (c.State chs) C} `{Container (State ap) D} (cs: C) (ss: D).
Definition CompleteCover: Prop := forall s: c.State chs, s ∈ cs -> forall r: State ap, s ∈ r -> r ∈ ss.
Definition SharedCover: Prop := forall s: c.State chs, s ∈ cs -> DN (exists r: State ap, s ∈ r /\ r ∈ ss).
End CoverRelandsuch.
Definition CompleteCoverList (cs: c.State chs -> Prop): Type :=
sig (LazyProp ∘ (CompleteCover cs: list (State ap) -> Prop)).
Section safe.
(* We're looking for a set of abstract states... *)
Variables (reachable: State ap -> Prop)
(* ... that together cover concretely reachable states in a shared manner: *)
(reachable_respect: SharedCover concrete.reachable reachable).
(* Because then, abstract unreachability implies concrete unreachability *)
Lemma safe (s: concrete.State chs): (forall s', s ∈ s' -> ~ reachable s') -> ~ concrete.reachable s.
Proof with eauto.
unfold not.
intros.
apply DN_free, (DN_bind (reachable_respect H0))...
intros [s' [H1 H2]]...
Qed.
(* And consequently, if abstract reachability is overestimatable, reachability of an
overestimatable concrete set is overestimatable: *)
Hint Unfold intersection overlap nonempty.
Context
`(forall s, overestimation (reachable s))
(cstates: concrete.State chs -> Prop)
(astates: CompleteCoverList cstates).
Program Definition some_reachable_1: overestimation (overlap cstates concrete.reachable) :=
@overestimate (exists u, In u (proj1_sig astates) /\ reachable u) overestimate.
Next Obligation. Proof with eauto.
intros [x [Px r]].
apply (@safe x)...
repeat intro.
apply (@overestimation_false (exists u, In u (proj1_sig astates) /\ reachable u) _ H0)...
(* todo: ugly *)
destruct astates.
pose proof (c ())...
Qed.
End safe.
Definition cont_trans (l: c.Location chs): relation (Region ap)
:= fun r r' => exists p q, p ∈ r /\ q ∈ r' /\ c.can_flow chs l p q.
Definition sharing_transition_overestimator (R: relation (concrete.State chs)): Type :=
forall s: State ap, sig (fun l: list (State ap) => LazyProp (NoDup l /\
SharedCover (concrete.invariant ∩ (overlap s ∘ util.flip R)) l)).
(* the invariant part is important because it means the overestimators can use
regions_cover in their correctness proofs (which we do actually need) *)
(* We define abstract versions of initiality, invariance, and guards, suitable
as overestimation predicates. *)
Definition Initial: State ap -> Prop := overlap (@concrete.initial chs).
Definition invariant: State ap -> Prop := overlap (@concrete.invariant chs).
Definition guard (l: concrete.Location chs) (r: Region ap) (l': concrete.Location chs): Prop
:= exists p, p ∈ r /\ concrete.guard _ (l, p) l'.
Record System: Type :=
{ initial_dec: overestimator (overlap (@concrete.initial chs))
; disc_trans_over: sharing_transition_overestimator (@concrete.disc_trans _)
; cont_trans_over: sharing_transition_overestimator (@concrete.cont_trans _)
}.
Variable ahs: System.
Definition trans (b: bool): relation (State ap) :=
fun s1 s2 => s2 ∈ if b then proj1_sig (cont_trans_over ahs s1) else proj1_sig (disc_trans_over ahs s1).
Definition reachable (s: State ap): Prop :=
exists is: State ap,
overestimation_bool (initial_dec ahs is) = true /\ alternate trans is s.
Hint Unfold Initial predicate_container containers.intersection In.
Lemma reachable_alternating_concrete_abstract (i s: c.State chs):
concrete.initial i -> forall b, end_with (@concrete.trans_kind chs) b i s ->
DN (exists is, overestimation_bool (initial_dec ahs is) = true /\
exists s', s ∈ s' /\ end_with trans (negb b) is s').
Proof with eauto; auto 20.
intros H b H0.
induction H0 as [| b i (l, p) H0 IH [l' p']].
destruct s as [l cp].
apply (DN_fmap (regions_cover ap l cp (concrete.invariant_initial chs _ H))).
intros [x i].
exists (l, x).
split.
apply overestimation_true.
exists (l, cp).
auto 20.
exists (l, x)...
apply (DN_bind (IH H)).
intros [ir [H2 [[al r] [[H3 H5] H4]]]]. clear IH.
apply (DN_exists (x := ir)).
apply (DN_liftM2 (@conj _ _))...
simpl in H3. subst.
cut (DN (exists r0, In p' r0 /\ trans (negb b) (al, r) (l', r0))).
intros.
apply (DN_fmap H3).
intros [x [H6 H7]].
exists (l', x).
eauto 30.
destruct b; simpl in H0 |- *.
unfold trans.
destruct (disc_trans_over ahs (al, r)).
simpl.
destruct l...
unfold SharedCover in H6.
unfold In at 1 in H6.
unfold predicate_container in H6.
simpl in H1.
cut (DN (exists r: State ap, In (l', p') r /\ In r x)).
intro.
apply (DN_fmap H7).
intro.
destruct H8.
destruct H8.
exists (region x0).
destruct H8.
split...
destruct x0.
simpl in H8. subst...
apply H6.
split...
destruct H1. intuition.
exists (al, p)...
unfold trans.
destruct cont_trans_over.
simpl.
destruct l...
unfold SharedCover, In, predicate_container in H6.
simpl in H1.
cut (DN (exists r : State ap, (l', p') ∈ r /\ r ∈ x)).
intro.
apply (DN_fmap H7). clear H7.
intros [x0 [[H7 H9] H8]].
exists (region x0).
split...
simpl in H7. subst.
destruct x0...
apply H6.
split.
apply concrete.reachable_invariant.
apply -> concrete.alternating_reachable.
hnf.
exists i.
split...
unfold alternate.
exists false.
eauto.
exists (al, p)...
Qed.
Hint Unfold alternate.
Lemma reachable_respect: SharedCover concrete.reachable reachable.
Proof.
unfold SharedCover.
intros.
apply concrete.alternating_reachable in H.
destruct H as [s' [H0 [x0 H1]]].
apply (DN_fmap (@reachable_alternating_concrete_abstract s' s H0 x0 H1)).
intros [x [y [A [B C]]]].
unfold reachable.
eauto 10.
Qed.
Definition some_reachable_2 := @some_reachable_1 reachable reachable_respect.
End contents.
Existing Instance in_region.
Existing Instance Region_eq_dec.
Existing Instance regions.
Existing Instance in_region_mor.