Skip to content
Snippets Groups Projects
Commit fab40648 authored by Lionel Rieg's avatar Lionel Rieg
Browse files

Small changes in the definitions for exploration

parent e8e95920
No related branches found
No related tags found
No related merge requests found
...@@ -99,9 +99,15 @@ Global Instance UpdFun : update_function direction (Z * bool) unit := { ...@@ -99,9 +99,15 @@ Global Instance UpdFun : update_function direction (Z * bool) unit := {
Definition is_visited (pt : location) (config : configuration) := Definition is_visited (pt : location) (config : configuration) :=
exists g, config (Good g) == pt. exists g, config (Good g) == pt.
Definition Will_be_visited (pt : location) (e : execution) : Prop := Definition Will_be_visited (pt : location) (e : execution) :=
Stream.eventually (Stream.instant (is_visited pt)) e. Stream.eventually (Stream.instant (is_visited pt)) 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. *) (** Eventually, all robots stop moving. *)
Definition Stall (e : execution) := Stream.hd e == (Stream.hd (Stream.tl e)). Definition Stall (e : execution) := Stream.hd e == (Stream.hd (Stream.tl e)).
...@@ -111,19 +117,18 @@ Definition Stopped (e : execution) : Prop := ...@@ -111,19 +117,18 @@ Definition Stopped (e : execution) : Prop :=
Definition Will_stop (e : execution) : Prop := Definition Will_stop (e : execution) : Prop :=
Stream.eventually Stopped e. Stream.eventually Stopped e.
(** [Exploration_with_stop r d config] means that executing [r] against demon [d] from (** [Exploration_with_stop e] means that execution [e] indeed solves exploration with stop:
configuration [config] indeed solves exploration with stop: after a finite time, every after a finite time, every node of the space has been visited and all robots will stay
node of the space has been visited and all robots will stay at the same place forever. *) at the same place forever. *)
Definition ExplorationWithStop (r : robogram) (d : demon) (config : configuration) := Definition ExplorationWithStop (e : execution) :=
(forall l, Will_be_visited l (execute r d config)) simple_exploration e /\ Will_stop e.
/\ Will_stop (execute r d config).
(** [FullSolExplorationWithStop r d] means that the robogram [r] solves exploration with stop (** [FullSolExplorationWithStop r d] means that the robogram [r] solves exploration with stop
agains demon [d] regardless of the starting configuration. agains demon [d] regardless of the starting configuration.
This is actually impossible when the number of robots is less than the size of the ring. *) This is actually impossible when the number of robots is less than the size of the ring. *)
Definition FullSolExplorationWithStop (r : robogram) (d : demon) := Definition FullSolExplorationWithStop (r : robogram) (d : demon) :=
forall config, ExplorationWithStop r d config. forall config, ExplorationWithStop (execute r d config).
(** Acceptable starting configurations contain no tower, (** Acceptable starting configurations contain no tower,
that is, all robots are at different locations. *) that is, all robots are at different locations. *)
...@@ -133,7 +138,7 @@ Definition Valid_starting_config config : Prop := ...@@ -133,7 +138,7 @@ Definition Valid_starting_config config : Prop :=
Definition Explore_and_Stop (r : robogram) := Definition Explore_and_Stop (r : robogram) :=
forall d config, Fair d -> Valid_starting_config config -> forall d config, Fair d -> Valid_starting_config config ->
ExplorationWithStop r d config. ExplorationWithStop (execute r d config).
(** Compatibility properties *) (** Compatibility properties *)
Global Instance is_visited_compat : Proper (equiv ==> equiv ==> iff) is_visited. Global Instance is_visited_compat : Proper (equiv ==> equiv ==> iff) is_visited.
...@@ -149,6 +154,12 @@ Proof using . ...@@ -149,6 +154,12 @@ Proof using .
intros ? ? ?. now apply Stream.eventually_compat, Stream.instant_compat, is_visited_compat. intros ? ? ?. now apply Stream.eventually_compat, Stream.instant_compat, is_visited_compat.
Qed. 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. Global Instance Stall_compat : Proper (equiv ==> iff) Stall.
Proof using . Proof using .
intros e1 e2 He. split; intros Hs; unfold Stall in *; intros e1 e2 He. split; intros Hs; unfold Stall in *;
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment