diff --git a/abstract.v b/abstract.v index 7aa1b78..0a4d7e5 100644 --- a/abstract.v +++ b/abstract.v @@ -1,6 +1,7 @@ Require Import reachability. Require Import List Bool. Require Import util list_util. +Require Import CSetoids. Set Implicit Arguments. Require EquivDec. Require concrete. @@ -32,33 +33,25 @@ Section contents. Implicit Arguments State []. - Record System: Type := + Record Parameters: Type := { Region: Set ; Region_eq_dec: EquivDec.EqDec Region eq ; regions: ExhaustiveList Region ; NoDup_regions: NoDup regions ; in_region: concrete.Point chs -> Region -> Prop - ; select_region: forall l p, concrete.invariant (l, p) -> exists r, in_region p r - ; Initial: State Region -> Prop - := fun s => exists p, in_region p (snd s) /\ concrete.initial (fst s, p) - ; initial_dec: forall s, overestimation (Initial s) - ; disc_trans: State Region -> list (State Region) - ; NoDup_disc_trans: forall s, NoDup (disc_trans s) - ; disc_resp: forall s1 s2 : concrete.State chs, - let (l1, p1) := s1 in - let (l2, p2) := s2 in - concrete.disc_trans s1 s2 -> - forall r1, in_region p1 r1 -> - exists r2, in_region p2 r2 /\ In (l2, r2) (disc_trans (l1, r1)) - ; cont_trans: State Region -> list Region - ; NoDup_cont_trans: forall s, NoDup (cont_trans s) - ; cont_resp: forall l s1 s2, - concrete.can_flow chs l s1 s2 -> - forall r1, in_region s1 r1 -> - exists r2, in_region s2 r2 /\ In r2 (cont_trans (l, r1)) + ; in_region_wd: forall x x', cs_eq x x' -> forall r, in_region x r -> in_region x' r + ; select_region: forall l p, concrete.invariant (l, p) -> sig (in_region p) }. - (* Note that the definition of cont_resp above is no longer the traditional + Variable ap: Parameters. + + Definition ContRespect := + fun (s: State (Region ap)) (l: list (Region ap)) => + forall p, in_region ap p (region s) -> + forall q, concrete.can_flow chs (location s) p q -> + exists r', in_region ap q r' /\ In r' l. + + (* Note that this is no longer the traditional "there is an abstract continuous transition between regions A and B if there is a concrete continuous transition between a point in A and a point in B" @@ -69,23 +62,41 @@ Section contents. The former implies the latter, so the latter is weaker (and therefore better). In particular, the former does not let us avoid drift, while the latter does. *) + Definition DiscRespect := + fun (s: State (Region ap)) (l: list (State (Region ap))) => + forall p1 (s2 : concrete.State chs) , + concrete.disc_trans (fst s, p1) s2 -> + in_region ap p1 (snd s) -> + exists r2, in_region ap (concrete.point s2) r2 /\ In (concrete.location s2, r2) l. + + Definition Initial (s: State (Region ap)): Prop := + exists p, in_region ap p (snd s) /\ concrete.initial (fst s, p). + + Record System: Type := + { initial_dec: forall s, overestimation (Initial s) + ; disc_trans: forall s: State (Region ap), + { l: list (State (Region ap)) | LazyProp (NoDup l /\ DiscRespect s l) } + ; cont_trans: forall s: State (Region ap), + { l: list (Region ap) | LazyProp (NoDup l /\ ContRespect s l) } + }. + Variable ahs: System. - Let State := State (Region ahs). + Let State := State (Region ap). Let c_State := concrete.State chs. Definition abs (s: c_State) (s': State): Prop := concrete.location s = fst s' /\ - in_region ahs (snd s) (snd s'). + in_region ap (snd s) (snd s'). Hint Unfold abs. Definition trans (b : bool) (s1 s2 : State) : Prop := let (l1, p1) := s1 in let (l2, p2) := s2 in if b then - l1 = l2 /\ In p2 (cont_trans _ s1) + l1 = l2 /\ In p2 (proj1_sig (cont_trans ahs s1)) else - In s2 (disc_trans _ s1). + In s2 (proj1_sig (disc_trans ahs s1)). Definition reachable (s : State) : Prop := exists is : State, @@ -99,33 +110,35 @@ Section contents. (exists is, (initial_dec ahs is: bool) = true /\ exists s', abs s s' /\ end_with trans (negb b) is s'). Proof with eauto. intros i s H b H0. - induction H0. + induction H0 as [| b i (l, p) H0 IH [l' p']]. destruct s as [l cp]. - destruct (select_region ahs l cp). + destruct (select_region ap l cp). apply (concrete.invariant_initial chs _ H). exists (l, x). split. apply overestimation_true... exists (l, x)... - intuition. - destruct H2 as [x0 [H2 [x1 [H3 H4]]]]. - exists x0. split... - rewrite negb_involutive in H4. - destruct y. - destruct H3. + destruct IH as [ir [H2 [[al r] [[H3 H5] H4]]]]... + exists ir. split... + pose proof (end_with_next (negb b) H4). clear H4. simpl in H3. subst. - destruct x1 as [l0 r]. - destruct z as [l s0]. - destruct b. - destruct (disc_resp ahs (l0, s) (l, s0) H1 _ H5) as [x2 [H3 H6]]. - exists (l, x2)... + cut (exists r0, in_region ap p' r0 /\ trans (negb b) (al, r) (l', r0)). + intros [x H3]. + exists (l', x). + intuition. + destruct b; simpl in H0 |- *. + destruct (disc_trans ahs (al, r)). + simpl. + destruct l... + destruct (H4 p (l', p') H1 H5)... + destruct (cont_trans ahs (al, r)). + simpl. + destruct l... destruct H1. - destruct (cont_resp ahs H3 r H5) as [x2 [H6 H7]]. - exists (l, x2). - split... - apply end_with_next with (l0, r)... - simpl... + destruct (H4 p H5 _ H7). + exists x0. + intuition. Qed. Lemma reachable_concrete_abstract (s : concrete.State chs) : @@ -150,6 +163,3 @@ End contents. Hint Resolve Region_eq_dec regions: typeclass_instances. Implicit Arguments State []. -Implicit Arguments initial_dec [s]. -Implicit Arguments cont_trans [s]. -Implicit Arguments disc_trans [s]. diff --git a/abstract_as_graph.v b/abstract_as_graph.v index 7b81664..88707b3 100644 --- a/abstract_as_graph.v +++ b/abstract_as_graph.v @@ -7,14 +7,16 @@ Set Implicit Arguments. Section using_duplication. - Variable chs: concrete.System. - Variable ahs: abstract.System chs. + Variables + (chs: concrete.System) + (ap: abstract.Parameters chs) + (ahs: abstract.System ap). Inductive TransKind := Cont | Disc. Instance transKinds: ExhaustiveList TransKind := { exhaustive_list := Cont :: Disc :: [] }. - Proof. destruct x; firstorder. Defined. + Proof. destruct x; clear; firstorder. Defined. Instance TransKind_eq_dec: EquivDec.EqDec TransKind eq. Proof. repeat intro. cut (decision (x = y)). auto. dec_eq. Defined. @@ -22,11 +24,11 @@ Section using_duplication. Definition flip (k: TransKind) := match k with Cont => Disc | Disc => Cont end. - Let a_State := abstract.State chs (abstract.Region ahs). + Let a_State := abstract.State chs (abstract.Region ap). Let V := (TransKind * a_State)%type. - Definition all_abstract_states := @abstract.states chs _ (abstract.regions ahs). + Definition all_abstract_states := @abstract.states chs _ (abstract.regions ap). Definition states_to_verts (s : list a_State) := map (pair Cont) s ++ map (pair Disc) s. @@ -37,8 +39,8 @@ Section using_duplication. match k with | Cont => let (l, r) := s in - map (pair l) (abstract.cont_trans _ s) - | Disc => abstract.disc_trans _ s + map (pair l) (proj1_sig (abstract.cont_trans ahs s)) + | Disc => proj1_sig (abstract.disc_trans ahs s) end. Definition next (v: V) : list V := @@ -49,8 +51,8 @@ Section using_duplication. intros. apply NoDup_map... destruct v. destruct a. destruct t; simpl. apply NoDup_map... - apply abstract.NoDup_cont_trans. - apply abstract.NoDup_disc_trans. + destruct_call abstract.cont_trans. simpl. destruct l0... + destruct_call abstract.disc_trans. simpl. destruct l0... Qed. Lemma NoDup_states_to_verts s : NoDup s -> NoDup (states_to_verts s). @@ -61,12 +63,12 @@ Section using_duplication. Qed. Definition g : digraph.DiGraph := - @digraph.Build (TransKind * abstract.State chs (abstract.Region ahs)) _ _ _ NoDup_next. + @digraph.Build (TransKind * abstract.State chs (abstract.Region ap)) _ _ _ NoDup_next. Lemma respect (s : a_State) : - abstract.reachable _ s -> + abstract.reachable ahs s -> exists k, exists v : digraph.Vertex g, - (abstract.initial_dec chs (snd v): bool) = true /\ + (@abstract.initial_dec chs ap ahs (snd v): bool) = true /\ digraph.reachable v (k, s). Proof with auto. intros s [absS [init [tt reach_alt]]]. @@ -86,12 +88,12 @@ Section using_duplication. Qed. Definition graph_unreachable_prop s (v : digraph.Vertex g) : Prop := - (abstract.initial_dec chs (snd v): bool) = true -> + (@abstract.initial_dec _ _ ahs (snd v): bool) = true -> ~digraph.reachable v (Cont, s) /\ ~digraph.reachable v (Disc, s). Lemma respect_inv (s: a_State) : (forall v: digraph.Vertex g, graph_unreachable_prop s v) -> - ~abstract.reachable _ s. + ~abstract.reachable ahs s. Proof with auto. intros s rc abs_reach. destruct (respect abs_reach) as [tt [v [init reach]]]. @@ -100,21 +102,21 @@ Section using_duplication. Qed. Definition init_verts : list V := - let is_initial v := abstract.initial_dec chs v in + let is_initial v := @abstract.initial_dec chs ap ahs v in let init_states := filter is_initial all_abstract_states in states_to_verts init_states. Lemma init_verts_eq_aux (tt : TransKind) ss : - map (pair tt) (filter (fun v => abstract.initial_dec chs (s:=ahs) v) ss) = - filter (fun s => abstract.initial_dec chs (snd s)) (map (pair tt) ss). + map (pair tt) (filter (fun v => abstract.initial_dec ahs v) ss) = + filter (fun s => abstract.initial_dec ahs (snd s)) (map (pair tt) ss). Proof. induction ss. ref. simpl. - destruct (abstract.initial_dec chs a); destruct x; simpl; rewrite IHss; ref. + destruct (abstract.initial_dec ahs a); destruct x; simpl; rewrite IHss; ref. Qed. Lemma init_verts_eq : init_verts = - filter (fun s => abstract.initial_dec chs (snd s)) + filter (fun s => abstract.initial_dec ahs (snd s)) vertices. Proof. unfold init_verts, states_to_verts. @@ -168,12 +170,12 @@ Section using_duplication. List.existsb (state_reachable reachable_verts) ss. Lemma states_unreachable (P: concrete.State chs -> Prop) (ss : list a_State): - (forall s, P s -> forall r, abstract.abs ahs s r -> In r ss) -> + (forall s, P s -> forall r, abstract.abs ap s r -> In r ss) -> some_reachable ss = false -> forall cs, P cs -> ~ concrete.reachable cs. Proof with auto. intros. - apply (@abstract.safe chs ahs). + apply (@abstract.safe chs ap ahs). unfold some_reachable in H0. intros. intro. diff --git a/abstraction.v b/abstraction.v index 39ee1de..9091969 100644 --- a/abstraction.v +++ b/abstraction.v @@ -5,128 +5,91 @@ Require Import flow. Require concrete abstract. Set Implicit Arguments. Open Local Scope CR_scope. +Require Import EquivDec. Section contents. - (* If we have a suitable set of regions.. *) + Variable (chs: concrete.System) (ap: abstract.Parameters chs). - Context - {Region: Set} - {Region_eq_dec: EquivDec.EqDec Region eq} - {regions: ExhaustiveList Region}. - Variable NoDup_regions: NoDup regions. + Let Location := concrete.Location chs. + Let Point := concrete.Point chs. + Let c_State := concrete.State chs. - (* .. and a concrete system.. *) + Let State := (Location * abstract.Region ap)%type. - Variable conc_sys: concrete.System. - Let Location := concrete.Location conc_sys. - Let Point := concrete.Point conc_sys. - Let c_State := concrete.State conc_sys. - Let State := (Location * Region)%type. - - (* .. and we can express that a concrete point lies in a region.. *) - - Variables - (in_region : concrete.Point conc_sys -> Region -> Prop) - (in_region_wd: forall x x', x [=] x' -> forall r, in_region x r -> in_region x' r). - - (* .. and we can also find regions corresponding to points.. *) - - Variables - (select_region: Point -> Region) - (* (does not have to be constructive, because never used in actual computations) *) - (select_region_wd: forall x x', x [=] x' -> select_region x = select_region x') - (select_region_correct: forall x, concrete.invariant x -> in_region (snd x) (select_region (snd x))). - - Hint Resolve select_region_correct. - - (* .. then we can state abstract region-based versions of initiality- and - transition conditions. These are not necessarily decidable. *) - - Definition initial_condition (s : State) : Prop := - let (l, r) := s in - exists p, in_region p r /\ concrete.initial (l, p). - - Definition cont_trans_cond (l: Location) (r1 r2: Region): Prop := + Definition cont_trans_cond (l: Location) (r1 r2: abstract.Region ap): Prop := exists p, exists q, - in_region p r1 /\ in_region q r2 /\ concrete.cont_trans (l, p) (l, q). + abstract.in_region ap p r1 /\ abstract.in_region ap q r2 /\ concrete.cont_trans (l, p) (l, q). Definition disc_trans_cond (s : State * State): Prop := let (s1, s2) := s in let (l1, r1) := s1 in let (l2, r2) := s2 in exists p, exists q, - in_region p r1 /\ in_region q r2 /\ concrete.disc_trans (l1, p) (l2, q). + abstract.in_region ap p r1 /\ abstract.in_region ap q r2 /\ concrete.disc_trans (l1, p) (l2, q). - Definition Hint (l: Location) (r r': Region): Set := - forall p, in_region p r -> - forall t, '0 <= t -> in_region (concrete.flow conc_sys l p t) r' -> - in_region (concrete.flow conc_sys l p t) r. + Definition Hint (l: Location) (r r': abstract.Region ap): Set := + forall p, abstract.in_region ap p r -> + forall t, '0 <= t -> abstract.in_region ap (concrete.flow chs l p t) r' -> + abstract.in_region ap (concrete.flow chs l p t) r. - Definition AltHint (l: Location) (r r': Region): Set := + Definition AltHint (l: Location) (r r': abstract.Region ap): Set := (forall p: Point, - in_region p r -> + abstract.in_region ap p r -> forall t: Time, - in_region (concrete.flow conc_sys l p t) r' -> t <= '0). + abstract.in_region ap (concrete.flow chs l p t) r' -> t <= '0). Lemma dealt_hint l r r': AltHint l r r' -> Hint l r r'. Proof with auto. repeat intro. set (H p H0 _ H2). clearbody c. clear H. set (snd (CRle_def t ('0)) (conj c H1)). clearbody s. - apply in_region_wd with p... + apply (abstract.in_region_wd ap) with p... simpl bsm. - transitivity (concrete.flow conc_sys l p ('0)). + transitivity (concrete.flow chs l p ('0)). symmetry. apply flow_zero. - destruct (concrete.flow conc_sys l). + destruct (concrete.flow chs l). simpl. apply bsm_wd... symmetry... Qed. - Variable hints: forall (l: Location) (r r': Region), r <> r' -> option (Hint l r r'). + Variable hints: forall (l: Location) (r r': abstract.Region ap), r <> r' -> option (Hint l r r'). Definition dealt_hints (H: forall l r r', r <> r' -> option (AltHint l r r')) l r r' (E: r <> r'): option (Hint l r r') := option_map (@dealt_hint l r r') (H l r r' E). - Definition hints' (l: Location) (r r': Region): - option (forall p, in_region p r -> - forall t, '0 <= t -> in_region (concrete.flow conc_sys l p t) r' -> - in_region (concrete.flow conc_sys l p t) r) := - match Region_eq_dec r r' with + Definition hints' (l: Location) (r r': abstract.Region ap): + option (forall p, abstract.in_region ap p r -> + forall t, '0 <= t -> abstract.in_region ap (concrete.flow chs l p t) r' -> + abstract.in_region ap (concrete.flow chs l p t) r) := + match r == r' with | left _ => None | right E => hints l E end. - Variables - (cont_dec: forall l r r', overestimation (cont_trans_cond l r r')) - (initial_dec: forall s, overestimation (initial_condition s)). + Variable cont_dec: forall l r r', overestimation (cont_trans_cond l r r'). (* Using these, we can define the abstract transitions.. *) - Let cont_trans_b (s : State) (r_dst : Region) : bool := + Let cont_trans_b (s : State) (r_dst : abstract.Region ap) : bool := let (l, r_src) := s in cont_dec l r_src r_dst && negb (hints' l r_src r_dst). - Definition RegionsCoverInvariants : Prop := - forall l p, concrete.invariant (l, p) -> - in_region p (select_region p). - - Variable regions_cover_invariants : RegionsCoverInvariants. - - Add Morphism (concrete.inv_curried conc_sys) + Add Morphism (concrete.inv_curried chs) with signature (@eq _) ==> (@cs_eq _) ==> iff as inv_mor. Proof. intros. apply concrete.invariant_wd; trivial. Qed. - Definition cont_trans (s : State) : list Region := - filter (cont_trans_b s) regions. + Definition raw_cont_trans (s : State) : list (abstract.Region ap) := + filter (cont_trans_b s) (abstract.regions ap). - Lemma cont_refl l r p: in_region p r -> concrete.invariant (l, p) -> In r (cont_trans (l, r)). + Lemma cont_refl l r p: abstract.in_region ap p r -> concrete.invariant (l, p) -> + In r (raw_cont_trans (l, r)). Proof with auto. intros. apply in_filter... @@ -142,9 +105,9 @@ Section contents. intros. simpl. rewrite concrete.curry_inv. - assert (concrete.flow conc_sys l p t [=] p). - transitivity (concrete.flow conc_sys l p ('0))... - set (concrete.flow conc_sys l). + assert (concrete.flow chs l p t [=] p). + transitivity (concrete.flow chs l p ('0))... + set (concrete.flow chs l). clearbody f . destruct f. simpl. @@ -160,82 +123,60 @@ Section contents. rewrite flow_zero... simpl. unfold hints'. - destruct (Region_eq_dec r r)... + destruct (equiv_dec r r)... elimtype False. intuition. Qed. Lemma respects_cont l s1 s2 : concrete.can_flow _ l s1 s2 -> - forall r1, in_region s1 r1 -> - exists r2, in_region s2 r2 /\ In r2 (cont_trans (l, r1)). + forall r1, abstract.in_region ap s1 r1 -> + exists r2, abstract.in_region ap s2 r2 /\ In r2 (raw_cont_trans (l, r1)). Proof with auto with real. - intros l s1 s2 [t [inv flow]] r1 inr1. - set (r2 := select_region s2). - case_eq (hints' l r1 r2); intros. - clear H. - exists r1. + intros l p p' [t [inv f]] r rin. + assert (concrete.invariant (l, p')). + apply (concrete.invariant_wd chs (refl_equal l) _ _ f). + apply inv... + apply -> CRnonNeg_le_zero... + destruct (abstract.select_region ap l p' H) as [r' rin']. + case_eq (hints' l r r'); intros. + exists r. split. - apply in_region_wd with (concrete.flow conc_sys l s1 (`t))... + apply abstract.in_region_wd with (concrete.flow chs l p (`t))... apply i... apply -> CRnonNeg_le_zero... - subst r2. - apply in_region_wd with s2. - symmetry... - apply (select_region_correct (l, s2)). - rewrite concrete.curry_inv. - rewrite <- flow. - apply inv... - apply -> CRnonNeg_le_zero... - apply cont_refl with s1... + apply abstract.in_region_wd with p'... + symmetry... + apply cont_refl with p... rewrite concrete.curry_inv. - rewrite <- (flow_zero (concrete.flow conc_sys l) s1). + rewrite <- (flow_zero (concrete.flow chs l) p). apply inv... apply -> CRnonNeg_le_zero... - exists r2. - split. - apply (select_region_correct (l, s2)). - rewrite concrete.curry_inv. - rewrite <- flow. - apply inv... - apply -> CRnonNeg_le_zero... - unfold cont_trans. + exists r'. + split... + unfold raw_cont_trans. apply in_filter... apply andb_true_intro. split. apply overestimation_true. - exists s1. exists s2. - split... - split. - apply regions_cover_invariants with l. - rewrite concrete.curry_inv. - rewrite <- flow. - apply inv... - apply -> CRnonNeg_le_zero... + exists p. eauto 10. - rewrite H... + rewrite H0... Qed. - Lemma NoDup_cont_trans s : NoDup (cont_trans s). - Proof. unfold cont_trans. auto. Qed. - - Lemma regions_cover_invariant l p: concrete.invariant (l, p) -> exists r, in_region p r. - Proof with auto. - intros. - exists (select_region p). - apply (select_region_correct (l, p))... - Qed. - - Program Definition abstract_system disc_trans respects_disc NoDup_disc_trans - : abstract.System conc_sys := - abstract.Build_System Region_eq_dec regions - NoDup_regions in_region regions_cover_invariant initial_dec disc_trans NoDup_disc_trans - respects_disc cont_trans NoDup_cont_trans respects_cont. - - Next Obligation. Proof with intuition. - destruct (initial_dec x). - destruct x0... - destruct x... + Program Definition cont_trans (s : State): sig + (fun l: list (abstract.Region ap) => LazyProp (NoDup l /\ abstract.ContRespect ap s l)) := + filter (cont_trans_b s) (abstract.regions ap). + Next Obligation. Proof with auto. + split. + apply NoDup_filter, (abstract.NoDup_regions ap). + repeat intro. + destruct (respects_cont H1 _ H0). + destruct H2. + exists x. + split... + unfold raw_cont_trans in H3. + destruct s... Qed. End contents. diff --git a/hs_solver.v b/hs_solver.v index 5208953..346049d 100644 --- a/hs_solver.v +++ b/hs_solver.v @@ -119,7 +119,7 @@ Ltac hs_unfolds := Basics.compose, in_orange, in_osquare, orange_left, orange_right, square_abstraction.in_region, - square_abstraction.absInterval; + square_abstraction.select_region; simpl). Ltac CRle_solve := diff --git a/square_abstraction.v b/square_abstraction.v index 737bd38..3492f7f 100644 --- a/square_abstraction.v +++ b/square_abstraction.v @@ -69,14 +69,20 @@ Section contents. Definition in_region (p: Point) (s: SquareInterval): Prop := in_osquare p (square s). - Variables - (absXinterval: CR -> Xinterval) - (absYinterval: CR -> Yinterval). - - Definition absInterval (p: Point): SquareInterval := - (absXinterval (fst p), absYinterval (snd p)). - - Variable initial: Location -> Xinterval -> Yinterval -> bool. + Lemma in_region_wd x x': x [=] x' -> forall r, in_region x r -> in_region x' r. + Proof with auto. + unfold in_region. + intros. + destruct H0. + destruct r. + simpl in H0, H1. unfold square. simpl. + destruct x. destruct x'. + simpl in H0, H1. + inversion_clear H. + split; simpl. + apply (@in_orange_wd (Xinterval_range x0) (Xinterval_range x0)) with s; try reflexivity... + apply (@in_orange_wd (Yinterval_range y) (Yinterval_range y)) with s0; try reflexivity... + Qed. Variables (xflow yflow: Location -> Flow CRasCSetoid) @@ -94,6 +100,17 @@ Section contents. (concrete_guard: Location * geometry.Point -> Location -> Prop) (reset: Location -> Location -> Point -> Point). + Hypothesis invariant_wd: forall l l', l = l' -> forall p p', p[=]p' -> + (concrete_invariant (l, p) <-> concrete_invariant (l', p')). + + Hypothesis NoDup_locations: NoDup locations. + + Variables + (absXinterval: CR -> Xinterval) + (absYinterval: CR -> Yinterval). + + Variable initial: Location -> Xinterval -> Yinterval -> bool. + Definition abstract_guard (l: Location) (s: SquareInterval) (l': Location): Prop := exists p, geometry.in_osquare p (square s) /\ concrete_guard (l, p) l'. @@ -127,12 +144,7 @@ Ltac bool_contradict id := apply (overestimation_false _ H), osquares_share_point with p... Qed. - Variable invariant_decider: forall s, overestimation (abstract_invariant s). - - Hypothesis invariant_wd: forall l l', l = l' -> forall p p', p[=]p' -> - (concrete_invariant (l, p) <-> concrete_invariant (l', p')). - - Hypothesis NoDup_locations: NoDup locations. + Variable invariant_decider: forall s, overestimation (abstract_invariant s). Variables (reset_x reset_y: Location -> Location -> Reset). @@ -147,17 +159,6 @@ Ltac bool_contradict id := (absXinterval_wd: forall x x', x == x' -> absXinterval x = absXinterval x') (absYinterval_wd: forall y y', y == y' -> absYinterval y = absYinterval y'). - Lemma absInterval_wd (p p': Point): p [=] p' -> absInterval p = absInterval p'. - Proof with auto. - intros. - unfold absInterval. - destruct p. destruct p'. - inversion_clear H. - f_equal. - apply absXinterval_wd... - apply absYinterval_wd... - Qed. - Instance SquareInterval_eq_dec: EquivDec.EqDec SquareInterval eq. repeat intro. cut (decision (x = y)). auto. @@ -171,6 +172,17 @@ Ltac bool_contradict id := (fun l: Location => product_flow (xflow l) (yflow l)) concrete_guard reset. + Program Definition select_region (l: concrete.Location concrete_system) + (p: concrete.Point concrete_system) (I: concrete.invariant (l, p)): sig (in_region p) := + (absXinterval (fst p), absYinterval (snd p)). + Next Obligation. + split; simpl; eauto using absXinterval_correct, absYinterval_correct. + Qed. + + Definition ap: abstract.Parameters concrete_system := + abstract.Build_Parameters concrete_system _ _ + NoDup_squareIntervals in_region in_region_wd select_region. + Section initial_dec. Variables (initial_location: Location) (initial_square: OpenSquare) @@ -183,7 +195,7 @@ Ltac bool_contradict id := Obligation Tactic := idtac. Program Definition initial_dec (eps: Qpos) s: overestimation - (abstraction.initial_condition concrete_system in_region s) := + (abstract.Initial ap s) := (overestimate_conj (osquares_overlap_dec eps (initial_square) (square (snd s))) (weaken_decision (Location_eq_dec (fst s) initial_location))). Next Obligation. Proof with auto. @@ -275,14 +287,14 @@ Ltac bool_contradict id := in flat_map (fun x => filter (fun s => invariant_decider (l', s)) (map (pair x) ys)) xs else []. - Definition disc_trans (eps: Qpos) (s: State): list State := + Definition raw_disc_trans (eps: Qpos) (s: State): list State := let (l, r) := s in flat_map (fun l' => map (pair l') (disc_trans_regions eps l l' r)) locations. - Lemma NoDup_disc_trans eps s: NoDup (disc_trans eps s). + Lemma NoDup_disc_trans eps s: NoDup (raw_disc_trans eps s). Proof with auto. intros. - unfold disc_trans. + unfold raw_disc_trans. destruct s. apply NoDup_flat_map... intros. @@ -314,21 +326,6 @@ Ltac bool_contradict id := destruct (reset_x l x)... Qed. - Lemma in_region_wd x x': x [=] x' -> forall r, in_region x r -> in_region x' r. - Proof with auto. - unfold in_region. - intros. - destruct H0. - destruct r. - simpl in H0, H1. unfold square. simpl. - destruct x. destruct x'. - simpl in H0, H1. - inversion_clear H. - split; simpl. - apply (@in_orange_wd (Xinterval_range x0) (Xinterval_range x0)) with s; try reflexivity... - apply (@in_orange_wd (Yinterval_range y) (Yinterval_range y)) with s0; try reflexivity... - Qed. - Hint Resolve absXinterval_correct absYinterval_correct. Hint Resolve in_map_orange. @@ -337,7 +334,7 @@ Ltac bool_contradict id := let (l2, p2) := s2 in concrete.disc_trans s1 s2 -> forall i1, in_region p1 i1 -> exists i2, in_region p2 i2 /\ - In (l2, i2) (disc_trans eps (l1, i1)). + In (l2, i2) (raw_disc_trans eps (l1, i1)). Proof with simpl; auto. destruct s1. destruct s2. intros. @@ -348,7 +345,7 @@ Ltac bool_contradict id := simpl in H1. subst s0. simpl @fst in H. - unfold disc_trans. + unfold raw_disc_trans. cut (exists i2: SquareInterval, in_region (reset l l0 s) i2 /\ In i2 (disc_trans_regions eps l l0 i1)). intro. @@ -452,10 +449,24 @@ Ltac bool_contradict id := simpl. exists s... split... split... Qed. - Obligation Tactic := idtac. + Program Definition disc_trans (eps: Qpos) (s: State): + sig (fun l: list State => LazyProp (NoDup l /\ abstract.DiscRespect ap s l)) + := raw_disc_trans eps s. + Next Obligation. Proof with auto. + split. + apply NoDup_disc_trans. + repeat intro. + set (respects_disc eps (fst s, p1) s2). + simpl in y. + destruct s2. + destruct (y H0 _ H1). + destruct H2. + destruct s. + eauto. + Qed. Program Definition cont_trans_cond_dec eps l r r': - overestimation (abstraction.cont_trans_cond concrete_system in_region l r r') := + overestimation (abstraction.cont_trans_cond ap l r r') := square_flow_conditions.decide_practical (xflow_invr l) (yflow_invr l) (square r) (square r') eps && invariant_dec eps (l, r) && diff --git a/thermostat/abs.v b/thermostat/abs.v index b42b8e0..68bc8d5 100644 --- a/thermostat/abs.v +++ b/thermostat/abs.v @@ -132,26 +132,32 @@ Proof. hs_solver. Qed. Lemma NoDup_temp_intervals: NoDup temp_intervals. Proof. hs_solver. Qed. -Lemma regions_cover_invariants l p: - invariant (l, p) -> - square_abstraction.in_region ClockInterval_bounds TempInterval_bounds p - (square_abstraction.absInterval absClockInterval absTempInterval p). -Proof with auto. - destruct p. - unfold invariant. - unfold square_abstraction.in_region, square_abstraction.absInterval, - absClockInterval, absTempInterval. - simplify_hyps. simplify_proj. split... +Lemma absClockInterval_correct p l (i: invariant (l, p)): + in_orange (ClockInterval_bounds (absClockInterval (fst p))) (fst p). +Proof. + intros. + unfold absClockInterval. + destruct_call s_absClockInterval. + destruct i; auto. Qed. -Definition Region: Set := prod ClockInterval TempInterval. +Lemma absTempInterval_correct p l (i: invariant (l, p)): + in_orange (TempInterval_bounds (absTempInterval (snd p))) (snd p). +Proof. + intros. + unfold absTempInterval. + destruct_call s_absTempInterval. + destruct i; auto. +Qed. -Let in_region := square_abstraction.in_region ClockInterval_bounds TempInterval_bounds. +Definition ap: abstract.Parameters conc.system := + @square_abstraction.ap _ _ _ _ _ _ _ _ _ + NoDup_clock_intervals NoDup_temp_intervals + _ _ _ _ _ _ _ _ _ _ _ _ _ absClockInterval_correct absTempInterval_correct. -Definition in_region_wd: forall (x x': concrete.Point conc_thermo.system), - x[=]x' -> forall r, in_region x r -> in_region x' r - := @square_abstraction.in_region_wd _ _ Location - _ _ _ _ _ _ ClockInterval_bounds TempInterval_bounds. +Definition Region: Set := prod ClockInterval TempInterval. + +Let in_region := abstract.in_region ap. (* Abstracted initial: *) @@ -167,8 +173,11 @@ Proof. simpl. rewrite H2. auto. Qed. -Let initial_dec := square_abstraction.initial_dec - ClockInterval_bounds TempInterval_bounds _ _ initial_representative . +Let initial_dec := @square_abstraction.initial_dec + _ _ _ _ _ _ _ _ _ NoDup_clock_intervals NoDup_temp_intervals + _ _ _ _ _ _ initial_invariant _ _ invariant_wd NoDup_locations + _ _ absClockInterval_correct absTempInterval_correct + _ _ initial_representative. (* Abstracted invariant: *) @@ -212,75 +221,55 @@ Let guard_dec := square_abstraction.guard_dec (* Hints: *) -Definition he (f: Flow CRasCSetoid) (flow_inc: forall x, strongly_increasing (f x)) (t: Time) (x b: CR): - b <= x -> f x t <= b -> t <= '0. -Proof with auto. - intros. - apply (@strongly_increasing_inv_mild (f x) (flow_inc x))... - rewrite (flow_zero f). - apply CRle_trans with b... -Qed. - -Definition clock_hints (l: Location) (r r': Region): r <> r' -> option - (abstraction.AltHint conc_thermo.system in_region l r r'). +Definition clock_hints (l: Location) (r r': Region): r <> r' -> + option (abstraction.AltHint ap l r r'). Proof with auto. - intros. + intros l [ci ti] [ci' ti'] H. unfold abstraction.AltHint, in_region, square_abstraction.in_region, square_abstraction.square, in_osquare. - simpl. - destruct r. destruct r'. - unfold in_orange at 1 3. - unfold ClockInterval_bounds. - simpl. - destruct (ClockInterval_qbounds c). - destruct (ClockInterval_qbounds c0). - destruct x. destruct x0. - destruct o1. destruct o4. - simpl. - destruct (Qeq_dec q q0). - constructor. - intros. - destruct H0. destruct H1. destruct H0. destruct H1. - apply (@he (clock_flow l) ) with (fst p) ('q)... - simpl. - rewrite q1... - exact None. - exact None. - exact None. + simpl abstract.in_region. + unfold square_abstraction.in_region, in_osquare, + in_orange at 1 3, ClockInterval_bounds. + simpl @fst. simpl @snd. + destruct (ClockInterval_qbounds ci) as [[ci_lo ci_hi] ci_le]. + destruct (ClockInterval_qbounds ci') as [[ci'_lo ci'_hi] ci'_le]. + destruct ci_lo; [idtac | exact None]. + destruct ci'_hi; [idtac | exact None]. + destruct (Qeq_dec q q0) as [A|B]; [idtac | exact None]. + apply Some. + intros p [[H0 H4] H2] t [[H1 H5] H3]. + apply (strongly_increasing_inv_mild) with (clock_flow l (fst p))... + rewrite flow_zero. + apply CRle_trans with ('q)... + rewrite A... Defined. Definition temp_hints (l: Location) (r r': Region): r <> r' -> option - (abstraction.AltHint conc_thermo.system in_region l r r'). + (abstraction.AltHint ap l r r'). Proof with auto. - intros. - destruct r. destruct r'. - destruct l. - unfold abstraction.AltHint, in_region, square_abstraction.in_region, - square_abstraction.square, in_osquare. - simpl. - unfold in_orange at 2 4. - unfold orange_right at 1. unfold orange_left at 2. - unfold TempInterval_bounds. - destruct (TempInterval_qbounds t). - destruct (TempInterval_qbounds t0). - destruct x. - destruct x0. - destruct o1. - destruct o4. - simpl. - destruct (Qeq_dec q q0). - constructor. - intros. - destruct H0. destruct H1. - destruct H2. destruct H3. - apply (@he (temp_flow Heat)) with (snd p) ('q)... - unfold temp_flow... - rewrite q1... - exact None. - exact None. - exact None. - exact None. - exact None. + intros l [ci ti] [ci' ti'] H. + destruct l; [idtac | exact None | exact None]. + unfold abstraction.AltHint, in_region, square_abstraction.in_region, + square_abstraction.square, in_osquare. + simpl abstract.in_region. + unfold square_abstraction.in_region, in_osquare. + simpl @fst. simpl @snd. + unfold in_orange at 2 4. + unfold orange_right at 1. unfold orange_left at 2. + unfold TempInterval_bounds. + destruct (TempInterval_qbounds ti) as [[ti_lo ti_hi] ti_le]. + destruct (TempInterval_qbounds ti') as [[ti'_lo ti'_hi] ti'_le]. + destruct ti_lo; [idtac | exact None]. + destruct ti'_hi; [idtac | exact None]. + simpl. + destruct (Qeq_dec q q0); [idtac | exact None]. + apply Some. + intros p [H0 [H2 H4]] t [H1 [H3 H5]]. + apply (strongly_increasing_inv_mild) with (temp_flow Heat (snd p))... + unfold temp_flow... + rewrite flow_zero. + apply CRle_trans with ('q)... + rewrite q1... Defined. Definition hints (l: Location) (r r': Region) (E: r <> r') := @@ -288,26 +277,27 @@ Definition hints (l: Location) (r r': Region) (E: r <> r') := (* The abstract system: *) -Definition system (eps: Qpos): abstract.System conc_thermo.system. -Proof with auto. - intro eps. - eapply (@abstraction.abstract_system _ _ _ (square_abstraction.NoDup_squareIntervals NoDup_clock_intervals NoDup_temp_intervals) conc_thermo.system in_region - in_region_wd _ - (fun x => @regions_cover_invariants (fst x) (snd x)) -(abstraction.dealt_hints in_region_wd hints) +Let invariant_dec := + square_abstraction.invariant_dec ClockInterval_bounds TempInterval_bounds _ _ invariant_squares_correct. + +Lemma reset_components p l l': reset l l' p = + (square_abstraction.apply_Reset (clock_reset l l') (fst p), + square_abstraction.apply_Reset (temp_reset l l') (snd p)). +Proof. reflexivity. Qed. + +Let disc_trans_dec eps := + square_abstraction.disc_trans + NoDup_clock_intervals NoDup_temp_intervals + clock_flow temp_flow _ initial_invariant reset invariant_wd NoDup_locations + absClockInterval absTempInterval + (invariant_dec eps) clock_reset temp_reset reset_components + absClockInterval_correct absTempInterval_correct (guard_dec eps) eps. + +Let cont_trans eps := abstraction.cont_trans + (@abstraction.dealt_hints _ ap hints) (square_abstraction.cont_trans_cond_dec - ClockInterval_bounds TempInterval_bounds clock_flow temp_flow - clock_flow_inv temp_flow_inv clock_rfis temp_rfis _ _ _ _ _ _ invariant_squares_correct _ _ eps) - (initial_dec eps) regions_cover_invariants). - Focus 2. - apply (square_abstraction.NoDup_disc_trans - NoDup_clock_intervals NoDup_temp_intervals - (square_abstraction.invariant_dec ClockInterval_bounds TempInterval_bounds _ _ invariant_squares_correct eps) - NoDup_locations - clock_reset temp_reset (guard_dec eps) eps). - apply (square_abstraction.respects_disc absClockInterval absTempInterval)... - unfold absClockInterval. intros. - destruct (s_absClockInterval (fst p))... destruct H... - unfold absTempInterval. intros. - destruct (s_absTempInterval (snd p))... -Defined. + clock_flow_inv temp_flow_inv clock_rfis temp_rfis + invariant_squares invariant_squares_correct eps). + +Definition system (eps: Qpos): abstract.System ap := + abstract.Build_System (initial_dec eps) (disc_trans_dec eps) (cont_trans eps). diff --git a/thermostat/safe.v b/thermostat/safe.v index c410ea9..30c0c5e 100644 --- a/thermostat/safe.v +++ b/thermostat/safe.v @@ -12,7 +12,7 @@ Set Implicit Arguments. Definition abs_sys := abs.system milli. -Definition vs := abstract_as_graph.vertices abs_sys. +Definition vs := abstract_as_graph.vertices abs.ap. Definition g := abstract_as_graph.g abs_sys. Definition graph := flat_map (@digraph.edges g) vs. @@ -25,7 +25,7 @@ Definition unsafe_abstract_states := Definition unsafe_abstracts_cover_unsafe_concretes: forall s, conc.state_unsafe s -> - forall r, abstract.abs abs_sys s r -> In r unsafe_abstract_states. + forall r, abstract.abs abs.ap s r -> In r unsafe_abstract_states. Proof with auto. intros [l [c t]] H [l' [ci ti]] [H0 [_ tin]]. subst. @@ -46,7 +46,7 @@ Theorem unsafe_correct: unsafe = false -> Safe. Proof with auto. unfold unsafe, Safe. intros srf [l [px py]] su. - apply (abstract_as_graph.states_unreachable (ahs:=abs_sys) conc.state_unsafe unsafe_abstract_states)... + apply (abstract_as_graph.states_unreachable abs_sys conc.state_unsafe unsafe_abstract_states)... apply unsafe_abstracts_cover_unsafe_concretes. Qed. diff --git a/util.v b/util.v index 5df5f5d..99b0082 100644 --- a/util.v +++ b/util.v @@ -188,3 +188,8 @@ Proof. destruct o. destruct x. reflexivity. intros. absurd P; auto. Qed. Program Definition weaken_decision (P: Prop) (d: decision P): overestimation P := d: bool. Next Obligation. destruct d; firstorder. Qed. + +Definition LazyProp (T: Prop): Prop := () -> T. +Definition force (T: Prop) (l: LazyProp T): T := l (). + +Hint Constructors unit.