-
Sébastien Bouchard authored
# Conflicts: # CaseStudies/Exploration/Definitions.v
ffbc0ddf
ExplorationDefs.v 3.20 KiB
Require Export Pactole.Setting.
Require Import Pactole.Util.Stream.
Set Implicit Arguments.
Section ExplorationDefs.
Context {Robots : Names} {Loc : Location}.
Context {Tframe Trobot Tinfo Tactive Tinactive: Type}.
Context {RC : robot_choice Trobot} {FC : frame_choice Tframe}.
Context {UC : update_choice Tactive} {IC : inactive_choice Tinactive}.
Context {St : State Tinfo} {Obs : Observation}.
Context {UpdFun : update_function Trobot Tframe Tactive}.
Context {InaFun : inactive_function Tinactive}.
(** ** Specification of exploration with stop *)
Definition is_visited (l : location) (c : configuration) : Prop :=
exists g, get_location (c (Good g)) == l.
(** Any node will eventually be visited. *)
Definition Will_be_visited (l : location) (e : execution) : Prop :=
eventually (instant (is_visited l)) e.
Definition simple_exploration (e : execution) :=
forall pt, Will_be_visited pt e.
Definition perpetual_exploration (e : execution) :=
Stream.forever simple_exploration e.
(** Eventually, all robots stop moving. *)
Definition Stall (e : execution) := hd e == (hd (tl e)).
Definition Stopped (e : execution) : Prop :=
forever Stall e.
Definition Will_stop (e : execution) : Prop :=
eventually Stopped e.
(** [ExplorationStop e] means that after a finite time, every node of the space has been
visited, and after that time, all robots will stay at the same place forever. *)
Definition ExplorationStop (e : execution) :=
simple_exploration e /\ Will_stop e.
Global Instance is_visited_compat :
Proper (equiv ==> equiv ==> iff) is_visited.
Proof using .
intros l1 l2 Hl c1 c2 Hc. unfold is_visited. split; intros [g H].
- exists g. rewrite <- Hl, <- Hc. exact H.
- exists g. rewrite Hl, Hc. exact H.
Qed.
Global Instance Will_be_visited_compat :
Proper (equiv ==> equiv ==> iff) Will_be_visited.
Proof using .
intros l1 l2 Hl e1 e2 He. unfold Will_be_visited. split; intros H.
- rewrite <- He, <- Hl. exact H.
- rewrite He, Hl. exact H.
Qed.
Global Instance simple_exploration_compat :
Proper (equiv ==> iff) simple_exploration.
Proof using .
intros e1 e2 He. unfold simple_exploration. now setoid_rewrite He.
Qed.
Global Instance perpetual_exploration_compat :
Proper (equiv ==> iff) perpetual_exploration.
Proof using . apply Stream.forever_compat, simple_exploration_compat. Qed.
Global Instance Stall_compat : Proper (equiv ==> iff) Stall.
Proof using .
intros e1 e2 He. unfold Stall. split; intros H.
- rewrite <- He. exact H.
- rewrite He. exact H.
Qed.
Global Instance Stopped_compat : Proper (equiv ==> iff) Stopped.
Proof using .
intros e1 e2 He. unfold Stopped. split; intros H.
- rewrite <- He. exact H.
- rewrite He. exact H.
Qed.
Global Instance Will_stop_compat : Proper (equiv ==> iff) Will_stop.
Proof using .
intros e1 e2 He. unfold Will_stop. split; intros H.
- rewrite <- He. exact H.
- rewrite He. exact H.
Qed.
Global Instance ExplorationStop_compat :
Proper (equiv ==> iff) ExplorationStop.
Proof using .
intros e1 e2 He. unfold ExplorationStop. split; intros [Hx Hs].
- split.
+ intros l. rewrite <- He. exact (Hx l).
+ rewrite <- He. exact Hs.
- split.
+ intros l. rewrite He. exact (Hx l).
+ rewrite He. exact Hs.
Qed.
End ExplorationDefs.