Skip to content
Snippets Groups Projects
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.