PADEC - Coq Library
Library Padec.Model.Composition
From Coq Require Import SetoidList.
From Coq Require Import Relations.
From Coq Require Import RelationPairs.
From Coq Require Import Bool.
From Coq Require Import Wellfounded.
From Coq Require Import SetoidClass.
From Coq Require Import Relations.
From Coq Require Import RelationPairs.
From Coq Require Import Bool.
From Coq Require Import Wellfounded.
From Coq Require Import SetoidClass.
From Padec Require Import SetoidUtil.
From Padec Require Import ListUtils.
From Padec Require Import OptionUtil.
From Padec Require Import WellfoundedUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Self_Stabilization.
From Padec Require Import Stream.
From Padec Require Import Simulation.
From Padec Require Import Exec.
From Padec Require Import Fairness.
Open Scope signature_scope.
Set Implicit Arguments.
Section Composition.
Context {Chans: Channels} {Net: Network}.
From Padec Require Import ListUtils.
From Padec Require Import OptionUtil.
From Padec Require Import WellfoundedUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Self_Stabilization.
From Padec Require Import Stream.
From Padec Require Import Simulation.
From Padec Require Import Exec.
From Padec Require Import Fairness.
Open Scope signature_scope.
Set Implicit Arguments.
Section Composition.
Context {Chans: Channels} {Net: Network}.
Variable (Algo1: Algorithm).
Notation S1 := (@State Chans Algo1).
Notation Env1:= (Env (Algo := Algo1)).
Notation Exec1 := (Exec (Algo:=Algo1)).
Variable Assumption1: Stable_Assumption (Algo := Algo1).
Existing Instance Assumption1.
Notation Assume1 := (Assume (Stable_Assumption := Assumption1)).
Notation Assume1_RO := (Assume_RO (Stable_Assumption := Assumption1)).
Instance Assume1_RO_compat: Proper fequiv Assume1_RO
:= (Assume_RO_compat (Stable_Assumption := Assumption1)).
Notation RO1 := (ROType (Stable_Assumption := Assumption1)).
Notation RO1_part := (getRO (Stable_Assumption := Assumption1)).
Instance RO1_Stable: Stable_Variable Algo1 RO1_part
:= (ROstable (Stable_Assumption := Assumption1)).
Instance RO1_part_compat: Proper fequiv RO1_part
:= (GetVar_compat (Stable_Variable := RO1_Stable)).
Instance RO1_Psetoid: PartialSetoid RO1
:= (VarType_setoid (Stable_Variable := RO1_Stable)).
Notation RO1_part_stable := (GetVar_stable (Stable_Variable := RO1_Stable)).
Notation S1 := (@State Chans Algo1).
Notation Env1:= (Env (Algo := Algo1)).
Notation Exec1 := (Exec (Algo:=Algo1)).
Variable Assumption1: Stable_Assumption (Algo := Algo1).
Existing Instance Assumption1.
Notation Assume1 := (Assume (Stable_Assumption := Assumption1)).
Notation Assume1_RO := (Assume_RO (Stable_Assumption := Assumption1)).
Instance Assume1_RO_compat: Proper fequiv Assume1_RO
:= (Assume_RO_compat (Stable_Assumption := Assumption1)).
Notation RO1 := (ROType (Stable_Assumption := Assumption1)).
Notation RO1_part := (getRO (Stable_Assumption := Assumption1)).
Instance RO1_Stable: Stable_Variable Algo1 RO1_part
:= (ROstable (Stable_Assumption := Assumption1)).
Instance RO1_part_compat: Proper fequiv RO1_part
:= (GetVar_compat (Stable_Variable := RO1_Stable)).
Instance RO1_Psetoid: PartialSetoid RO1
:= (VarType_setoid (Stable_Variable := RO1_Stable)).
Notation RO1_part_stable := (GetVar_stable (Stable_Variable := RO1_Stable)).
Variable (Algo2: Algorithm).
Notation S2 := (@State Chans Algo2).
Notation Env2:= (Env (Algo := Algo2)).
Notation Exec2 := (Exec (Algo:=Algo2)).
Variable Assumption2: Stable_Assumption (Algo := Algo2).
Existing Instance Assumption2.
Notation Assume2 := (Assume (Stable_Assumption := Assumption2)).
Notation Assume2_RO := (Assume_RO (Stable_Assumption := Assumption2)).
Instance Assume2_RO_compat: Proper fequiv Assume2_RO
:= (Assume_RO_compat (Stable_Assumption := Assumption2)).
Notation RO2 := (ROType (Stable_Assumption := Assumption2)).
Notation RO2_part := (getRO (Stable_Assumption := Assumption2)).
Instance RO2_Stable: Stable_Variable Algo2 RO2_part
:= (ROstable (Stable_Assumption := Assumption2)).
Instance RO2_part_compat: Proper fequiv RO2_part
:= (GetVar_compat (Stable_Variable := RO2_Stable)).
Instance RO2_Psetoid: PartialSetoid RO2
:= (VarType_setoid (Stable_Variable := RO2_Stable)).
Notation RO2_part_stable := (GetVar_stable (Stable_Variable := RO2_Stable)).
Notation S2 := (@State Chans Algo2).
Notation Env2:= (Env (Algo := Algo2)).
Notation Exec2 := (Exec (Algo:=Algo2)).
Variable Assumption2: Stable_Assumption (Algo := Algo2).
Existing Instance Assumption2.
Notation Assume2 := (Assume (Stable_Assumption := Assumption2)).
Notation Assume2_RO := (Assume_RO (Stable_Assumption := Assumption2)).
Instance Assume2_RO_compat: Proper fequiv Assume2_RO
:= (Assume_RO_compat (Stable_Assumption := Assumption2)).
Notation RO2 := (ROType (Stable_Assumption := Assumption2)).
Notation RO2_part := (getRO (Stable_Assumption := Assumption2)).
Instance RO2_Stable: Stable_Variable Algo2 RO2_part
:= (ROstable (Stable_Assumption := Assumption2)).
Instance RO2_part_compat: Proper fequiv RO2_part
:= (GetVar_compat (Stable_Variable := RO2_Stable)).
Instance RO2_Psetoid: PartialSetoid RO2
:= (VarType_setoid (Stable_Variable := RO2_Stable)).
Notation RO2_part_stable := (GetVar_stable (Stable_Variable := RO2_Stable)).
Algorithm 3 (Composite Algorithm)
- Algo3 is given the values of variables of Algo1 (i.e. in some
state of type S1) using function read1: S3 -> S1
- Algo3 can modify the values of variables of Algo1 (i.e. in some state of type S1) using function write1: S3 -> S1 -> S3 - same for Algo2, read2 and write2.
Class Composition_State: Type:=
{
S3: Type;
setoid: Setoid S3;
S3_dec: Decider (equiv (A:=S3));
read1: S3 -> S1;
write1: S3 -> S1 -> S3;
read2: S3 -> S2;
write2: S3 -> S2 -> S3;
read1_compat: Proper fequiv read1;
write1_compat: Proper fequiv write1;
read2_compat: Proper fequiv read2;
write2_compat: Proper fequiv write2;
Guarantees that write1 actually writes the S1 part of the
state, since the projection of the modified state on the
result allows to get back what was written. (same for S2)
stabRW1: forall (s1: S1) (s3: S3), read1 (write1 s3 s1) == s1;
stabRW2: forall (s2: S2) (s3: S3), read2 (write2 s3 s2) == s2;
stabRW2: forall (s2: S2) (s3: S3), read2 (write2 s3 s2) == s2;
Apart from the read-only part of S2, write2 cannot modified
the S1 part of the state. The idea behind this constraint
is that Algo2 cannot modify the (S2-writtable part of the)
data computed by Algo1. (Algo2 cannot either modify the
(S2-read-only part) because it is read-only).
stabRO12: forall (s2: S2) (s3: S3),
RO2_part s2 =~= RO2_part (read2 s3)
-> read1 (write2 s3 s2) == read1 s3
}.
Context `{CS: Composition_State}.
Existing Instance setoid.
Existing Instance read1_compat.
Existing Instance write1_compat.
Existing Instance read2_compat.
Existing Instance write2_compat.
RO2_part s2 =~= RO2_part (read2 s3)
-> read1 (write2 s3 s2) == read1 s3
}.
Context `{CS: Composition_State}.
Existing Instance setoid.
Existing Instance read1_compat.
Existing Instance write1_compat.
Existing Instance read2_compat.
Existing Instance write2_compat.
projection on S1 of a configuration
Notation lenv1 := (fun sn: Channel -> option S3 =>
(fun c => option_map (read1 (Composition_State:=CS)) (sn c))).
(fun c => option_map (read1 (Composition_State:=CS)) (sn c))).
projection on S2 of a configuration
Notation lenv2 := (fun sn: Channel -> option S3 =>
(fun c => option_map (read2 (Composition_State:=CS)) (sn c))).
Instance lenv1_compat: Proper fequiv lenv1.
Instance lenv2_compat: Proper fequiv lenv2.
(fun c => option_map (read2 (Composition_State:=CS)) (sn c))).
Instance lenv1_compat: Proper fequiv lenv1.
Instance lenv2_compat: Proper fequiv lenv2.
RUN function of Algo3
- the result of Algo1 on p, if Algo1 is enabled on p
- otherwise, the result of Algo2 on p otherwise.
Definition composition_run (s: S3) (sn: Channel -> option S3):
S3 :=
if State_dec (run (read1 s) (lenv1 sn)) (read1 s)
then
if State_dec (run (read2 s) (lenv2 sn)) (read2 s)
then s
else write2 s (run (read2 s) (lenv2 sn))
else write1 s (run (read1 s) (lenv1 sn)).
Instance composition_run_compat: Proper fequiv composition_run.
S3 :=
if State_dec (run (read1 s) (lenv1 sn)) (read1 s)
then
if State_dec (run (read2 s) (lenv2 sn)) (read2 s)
then s
else write2 s (run (read2 s) (lenv2 sn))
else write1 s (run (read1 s) (lenv1 sn)).
Instance composition_run_compat: Proper fequiv composition_run.
Instance Collateral_composition: Algorithm :=
{| State_dec := S3_dec; run_compat := composition_run_compat |}.
Notation Algo3 := Collateral_composition.
Notation Env3 := (Env (Algo := Algo3)).
Notation Exec3 := (Exec (Algo:=Algo3)).
{| State_dec := S3_dec; run_compat := composition_run_compat |}.
Notation Algo3 := Collateral_composition.
Notation Env3 := (Env (Algo := Algo3)).
Notation Exec3 := (Exec (Algo:=Algo3)).
The read-only part of Algo3 is made of the read-only variables of Algo1
Let RO3 := RO1.
Instance RO3_Psetoid: PartialSetoid RO3 := RO1_Psetoid.
Notation RO3_part := (fun s: S3 => RO1_part (read1 s)).
Instance RO3_part_compat: Proper fequiv RO3_part.
Lemma RO3_part_stable: forall s sn,
RO3_part (run s sn) =~= RO3_part s.
Instance RO3_Stable: Stable_Variable Algo3 RO3_part.
Instance RO3_Psetoid: PartialSetoid RO3 := RO1_Psetoid.
Notation RO3_part := (fun s: S3 => RO1_part (read1 s)).
Instance RO3_part_compat: Proper fequiv RO3_part.
Lemma RO3_part_stable: forall s sn,
RO3_part (run s sn) =~= RO3_part s.
Instance RO3_Stable: Stable_Variable Algo3 RO3_part.
The read-only Assumption for Algo3 is given by the read-only
assumption of Algo1
Definition Assume3_RO: (Node -> RO3) -> Prop :=
(fun r => Assume1_RO (fun n => (r n))).
Instance Assume3_RO_compat: Proper fequiv Assume3_RO.
Instance Assumption3: Stable_Assumption (Algo := Algo3).
Notation Assume3 := (Assume (Stable_Assumption := Assumption3)).
(fun r => Assume1_RO (fun n => (r n))).
Instance Assume3_RO_compat: Proper fequiv Assume3_RO.
Instance Assumption3: Stable_Assumption (Algo := Algo3).
Notation Assume3 := (Assume (Stable_Assumption := Assumption3)).
Definition envread1 (g: Env3): Env1 := fun n => read1 (g n).
Lemma envread1_compat: Proper fequiv envread1.
Lemma envread1_prop:
forall g1 g2 n, g1 =~= g2 ->
(local_env (envread1 g1) n)
=~=
fun c => option_map read1 (local_env g2 n c) .
Lemma Assume_31:
forall g, Proper pequiv g ->
(Assume3 g <-> Assume1 (envread1 g)).
Lemma envread1_compat: Proper fequiv envread1.
Lemma envread1_prop:
forall g1 g2 n, g1 =~= g2 ->
(local_env (envread1 g1) n)
=~=
fun c => option_map read1 (local_env g2 n c) .
Lemma Assume_31:
forall g, Proper pequiv g ->
(Assume3 g <-> Assume1 (envread1 g)).
Definition envread2 (g: Env3): Env2 := fun n => read2 (g n).
Lemma envread2_compat: Proper fequiv envread2.
Lemma envread2_prop:
forall g1 g2 n, g1 =~= g2 ->
(local_env (envread2 g1) n)
=~=
fun c => option_map read2 (local_env g2 n c) .
Lemma envread2_compat: Proper fequiv envread2.
Lemma envread2_prop:
forall g1 g2 n, g1 =~= g2 ->
(local_env (envread2 g1) n)
=~=
fun c => option_map read2 (local_env g2 n c) .
Lemma run1_rewrite:
forall g g': Env3,
g =~= g' ->
forall n n', n == n' ->
run (read1 (g n)) (lenv1 (local_env g n))
== RUN (envread1 g') n'.
Lemma run2_rewrite:
forall g g': Env3,
g =~= g' -> forall n n', n == n' ->
run (read2 (g n)) (lenv2 (local_env g n))
== RUN (envread2 g') n'.
Alternative definition for RUN3
Definition composition_RUN_alt_def (g: Env3) (n: Node): S3 :=
if enabled_b (envread1 g) n then
write1 (g n) (RUN (envread1 g) n)
else if enabled_b (envread2 g) n then
write2 (g n) (RUN (envread2 g) n)
else (g n).
Lemma composition_RUN_alt:
fequiv RUN composition_RUN_alt_def.
Lemma RUN_31_enabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = true ->
read1 (RUN g n) == (RUN (envread1 g) n).
Lemma RUN_31_disabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
read1 (RUN g n) == (envread1 g) n.
Lemma RUN_32_enabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
enabled_b (envread2 g) n = true ->
read2 (RUN g n) == (RUN (envread2 g) n).
Lemma RUN_32_disabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
enabled_b (envread2 g) n = false ->
read2 (RUN g n) == (envread2 g) n.
Lemma RUN_3_disabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
enabled_b (envread2 g) n = false ->
RUN g n == g n.
if enabled_b (envread1 g) n then
write1 (g n) (RUN (envread1 g) n)
else if enabled_b (envread2 g) n then
write2 (g n) (RUN (envread2 g) n)
else (g n).
Lemma composition_RUN_alt:
fequiv RUN composition_RUN_alt_def.
Lemma RUN_31_enabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = true ->
read1 (RUN g n) == (RUN (envread1 g) n).
Lemma RUN_31_disabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
read1 (RUN g n) == (envread1 g) n.
Lemma RUN_32_enabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
enabled_b (envread2 g) n = true ->
read2 (RUN g n) == (RUN (envread2 g) n).
Lemma RUN_32_disabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
enabled_b (envread2 g) n = false ->
read2 (RUN g n) == (envread2 g) n.
Lemma RUN_3_disabled:
forall (g: Env3) (n: Node),
Proper fequiv g ->
enabled_b (envread1 g) n = false ->
enabled_b (envread2 g) n = false ->
RUN g n == g n.
Lemma enabled_12_3:
forall g n, Proper pequiv g ->
(enabled_b g n = true <-> enabled_b (envread1 g) n = true
\/
enabled_b (envread2 g) n = true).
Lemma enabled_12_3_alt:
forall g n, Proper pequiv g ->
enabled_b g n = enabled_b (envread1 g) n
|| enabled_b (envread2 g) n.
Lemma enabled_13:
forall g3 n, Proper fequiv g3 ->
enabled_b (envread1 g3) n = true -> enabled_b g3 n = true.
Lemma enabled_23:
forall g3 n,
Proper fequiv g3 ->
enabled_b (envread2 g3) n = true ->
enabled_b g3 n = true.
Lemma enabled_32:
forall g3 n,
Proper fequiv g3 ->
enabled_b (envread1 g3) n = false ->
enabled_b g3 n = true ->
enabled_b (envread2 g3) n = true.
Lemma disabled_12_3:
forall g n, Proper pequiv g ->
enabled_b g n = false <-> enabled_b (envread1 g) n = false
/\
enabled_b (envread2 g) n = false.
Lemma Step_disabled1_unchanged1:
forall (g' g: Env3), Step g' g ->
forall n, enabled_b (envread1 g) n = false ->
read1 (g' n) == read1 (g n).
forall g n, Proper pequiv g ->
(enabled_b g n = true <-> enabled_b (envread1 g) n = true
\/
enabled_b (envread2 g) n = true).
Lemma enabled_12_3_alt:
forall g n, Proper pequiv g ->
enabled_b g n = enabled_b (envread1 g) n
|| enabled_b (envread2 g) n.
Lemma enabled_13:
forall g3 n, Proper fequiv g3 ->
enabled_b (envread1 g3) n = true -> enabled_b g3 n = true.
Lemma enabled_23:
forall g3 n,
Proper fequiv g3 ->
enabled_b (envread2 g3) n = true ->
enabled_b g3 n = true.
Lemma enabled_32:
forall g3 n,
Proper fequiv g3 ->
enabled_b (envread1 g3) n = false ->
enabled_b g3 n = true ->
enabled_b (envread2 g3) n = true.
Lemma disabled_12_3:
forall g n, Proper pequiv g ->
enabled_b g n = false <-> enabled_b (envread1 g) n = false
/\
enabled_b (envread2 g) n = false.
Lemma Step_disabled1_unchanged1:
forall (g' g: Env3), Step g' g ->
forall n, enabled_b (envread1 g) n = false ->
read1 (g' n) == read1 (g n).
Lemma has_moved_12_3_all:
forall g' g n,
Step g' g ->
has_moved_b g' g n = true <->
enabled_b (envread1 g) n = true /\
has_moved_b (envread1 g') (envread1 g) n = true
\/
enabled_b (envread1 g) n = false /\
has_moved_b (envread1 g') (envread1 g) n = false /\
enabled_b (envread2 g) n = true /\
has_moved_b (envread2 g') (envread2 g) n = true.
Lemma has_moved_12_3_true:
forall g' g n,
Step g' g ->
has_moved_b g' g n = true <->
has_moved_b (envread1 g') (envread1 g) n = true \/
has_moved_b (envread2 g') (envread2 g) n = true.
Lemma has_moved_12_3_true_alt:
forall g' g n, Step g' g ->
has_moved_b g' g n =
has_moved_b (envread1 g') (envread1 g) n
|| has_moved_b (envread2 g') (envread2 g) n.
Lemma has_moved_12_3_false:
forall g' g n, Step g' g ->
has_moved_b g' g n = false <->
has_moved_b (envread1 g') (envread1 g) n = false
/\ has_moved_b (envread2 g') (envread2 g) n = false.
Lemma has_moved_13:
forall g3' g3 n,
has_moved_b (envread1 g3') (envread1 g3) n = true ->
has_moved_b g3' g3 n = true.
Lemma has_moved_31:
forall g3' g3 n,
Step g3' g3 ->
enabled_b (envread1 g3) n = true ->
has_moved_b g3' g3 n = true ->
has_moved_b (envread1 g3') (envread1 g3) n = true.
Lemma has_moved_23:
forall g3' g3 n,
has_moved_b (envread2 g3') (envread2 g3) n = true ->
has_moved_b g3' g3 n = true.
Lemma has_moved_32:
forall g3' g3 n,
Step g3' g3 ->
enabled_b (envread1 g3) n = false ->
has_moved_b g3' g3 n = true ->
has_moved_b (envread2 g3') (envread2 g3) n = true.
forall g' g n,
Step g' g ->
has_moved_b g' g n = true <->
enabled_b (envread1 g) n = true /\
has_moved_b (envread1 g') (envread1 g) n = true
\/
enabled_b (envread1 g) n = false /\
has_moved_b (envread1 g') (envread1 g) n = false /\
enabled_b (envread2 g) n = true /\
has_moved_b (envread2 g') (envread2 g) n = true.
Lemma has_moved_12_3_true:
forall g' g n,
Step g' g ->
has_moved_b g' g n = true <->
has_moved_b (envread1 g') (envread1 g) n = true \/
has_moved_b (envread2 g') (envread2 g) n = true.
Lemma has_moved_12_3_true_alt:
forall g' g n, Step g' g ->
has_moved_b g' g n =
has_moved_b (envread1 g') (envread1 g) n
|| has_moved_b (envread2 g') (envread2 g) n.
Lemma has_moved_12_3_false:
forall g' g n, Step g' g ->
has_moved_b g' g n = false <->
has_moved_b (envread1 g') (envread1 g) n = false
/\ has_moved_b (envread2 g') (envread2 g) n = false.
Lemma has_moved_13:
forall g3' g3 n,
has_moved_b (envread1 g3') (envread1 g3) n = true ->
has_moved_b g3' g3 n = true.
Lemma has_moved_31:
forall g3' g3 n,
Step g3' g3 ->
enabled_b (envread1 g3) n = true ->
has_moved_b g3' g3 n = true ->
has_moved_b (envread1 g3') (envread1 g3) n = true.
Lemma has_moved_23:
forall g3' g3 n,
has_moved_b (envread2 g3') (envread2 g3) n = true ->
has_moved_b g3' g3 n = true.
Lemma has_moved_32:
forall g3' g3 n,
Step g3' g3 ->
enabled_b (envread1 g3) n = false ->
has_moved_b g3' g3 n = true ->
has_moved_b (envread2 g3') (envread2 g3) n = true.
CoFixpoint execread1 (e3: Exec3): Exec1 :=
match e3 with
| s_one g3 => s_one (envread1 g3)
| s_cons g3 e3' => s_cons (envread1 g3) (execread1 e3')
end.
Lemma execread1_unfold:
forall e3,
execread1 e3 =
match e3 with
| s_one g3 => s_one (envread1 g3)
| s_cons g3 e3' => s_cons (envread1 g3) (execread1 e3')
end.
Lemma execread1_fold_cons:
forall g3 e3, execread1 (s_cons g3 e3) =
(s_cons (envread1 g3) (execread1 e3)).
Lemma execread1_fold_one:
forall g3, execread1 (s_one g3) = (s_one (envread1 g3)).
Instance execread1_compat: Proper fequiv execread1.
Lemma s_hd_read1: forall e3,
envread1 (s_hd e3) = s_hd (execread1 e3).
match e3 with
| s_one g3 => s_one (envread1 g3)
| s_cons g3 e3' => s_cons (envread1 g3) (execread1 e3')
end.
Lemma execread1_unfold:
forall e3,
execread1 e3 =
match e3 with
| s_one g3 => s_one (envread1 g3)
| s_cons g3 e3' => s_cons (envread1 g3) (execread1 e3')
end.
Lemma execread1_fold_cons:
forall g3 e3, execread1 (s_cons g3 e3) =
(s_cons (envread1 g3) (execread1 e3)).
Lemma execread1_fold_one:
forall g3, execread1 (s_one g3) = (s_one (envread1 g3)).
Instance execread1_compat: Proper fequiv execread1.
Lemma s_hd_read1: forall e3,
envread1 (s_hd e3) = s_hd (execread1 e3).
CoFixpoint execread2 (e3: Exec3): Exec2 :=
match e3 with
| s_one g3 => s_one (envread2 g3)
| s_cons g3 e3' => s_cons (envread2 g3) (execread2 e3')
end.
Lemma execread2_unfold:
forall e3,
execread2 e3 =
match e3 with
| s_one g3 => s_one (envread2 g3)
| s_cons g3 e3' => s_cons (envread2 g3) (execread2 e3')
end.
Lemma execread2_fold_cons:
forall g3 e3, execread2 (s_cons g3 e3) =
(s_cons (envread2 g3) (execread2 e3)).
Lemma execread2_fold_one:
forall g3, execread2 (s_one g3) = (s_one (envread2 g3)).
Instance execread2_compat: Proper fequiv execread2.
Lemma s_hd_read2: forall e3,
envread2 (s_hd e3) = s_hd (execread2 e3).
match e3 with
| s_one g3 => s_one (envread2 g3)
| s_cons g3 e3' => s_cons (envread2 g3) (execread2 e3')
end.
Lemma execread2_unfold:
forall e3,
execread2 e3 =
match e3 with
| s_one g3 => s_one (envread2 g3)
| s_cons g3 e3' => s_cons (envread2 g3) (execread2 e3')
end.
Lemma execread2_fold_cons:
forall g3 e3, execread2 (s_cons g3 e3) =
(s_cons (envread2 g3) (execread2 e3)).
Lemma execread2_fold_one:
forall g3, execread2 (s_one g3) = (s_one (envread2 g3)).
Instance execread2_compat: Proper fequiv execread2.
Lemma s_hd_read2: forall e3,
envread2 (s_hd e3) = s_hd (execread2 e3).
Terminal Configurations:
Lemma terminal_31:
forall (g: Env3), terminal g -> terminal (envread1 g).
Lemma terminal_32:
forall (g: Env3), terminal g -> terminal (envread2 g).
Lemma terminal_12_3:
forall g, Proper fequiv g ->
terminal (envread1 g) /\ terminal (envread2 g) ->
terminal g.
forall (g: Env3), terminal g -> terminal (envread1 g).
Lemma terminal_32:
forall (g: Env3), terminal g -> terminal (envread2 g).
Lemma terminal_12_3:
forall g, Proper fequiv g ->
terminal (envread1 g) /\ terminal (envread2 g) ->
terminal g.
Once Algo1 has reached a terminal configuration, it remains in
the same terminal configuration
Lemma terminal1_continued':
forall g' g,
Step g' g -> terminal (envread1 g) -> envread1 g =~= envread1 g'.
Lemma terminal1_continued:
forall g' g,
Step g' g ->
terminal (envread1 g) -> terminal (envread1 g').
Lemma terminal1_continued'_bis_:
forall e3 g1,
is_exec e3 -> terminal (envread1 (s_hd e3)) ->
g1 =~= envread1 (s_hd e3) ->
Always (fun e => s_hd e =~= g1) (execread1 e3).
Lemma terminal1_continued'_bis:
forall e3,
is_exec e3 -> terminal (envread1 (s_hd e3)) ->
Always (fun e => s_hd e =~= envread1 (s_hd e3)) (execread1 e3).
Lemma terminal1_continued_bis:
forall e3,
is_exec e3 -> terminal (envread1 (s_hd e3)) ->
Always (fun e => terminal (envread1 (s_hd e))) e3.
Lemma terminal1_continued_bis'':
forall e3,
is_exec e3 ->
Eventually (fun e => terminal (envread1 (s_hd e))) e3 ->
Eventually (Always (fun e => terminal (envread1 (s_hd e)))) e3.
forall g' g,
Step g' g -> terminal (envread1 g) -> envread1 g =~= envread1 g'.
Lemma terminal1_continued:
forall g' g,
Step g' g ->
terminal (envread1 g) -> terminal (envread1 g').
Lemma terminal1_continued'_bis_:
forall e3 g1,
is_exec e3 -> terminal (envread1 (s_hd e3)) ->
g1 =~= envread1 (s_hd e3) ->
Always (fun e => s_hd e =~= g1) (execread1 e3).
Lemma terminal1_continued'_bis:
forall e3,
is_exec e3 -> terminal (envread1 (s_hd e3)) ->
Always (fun e => s_hd e =~= envread1 (s_hd e3)) (execread1 e3).
Lemma terminal1_continued_bis:
forall e3,
is_exec e3 -> terminal (envread1 (s_hd e3)) ->
Always (fun e => terminal (envread1 (s_hd e))) e3.
Lemma terminal1_continued_bis'':
forall e3,
is_exec e3 ->
Eventually (fun e => terminal (envread1 (s_hd e))) e3 ->
Eventually (Always (fun e => terminal (envread1 (s_hd e)))) e3.
Lemma EN_1_3: forall e3 n,
Proper fequiv (s_hd e3) ->
EN n (execread1 e3) ->
EN n e3.
Lemma EN_2_3: forall e3 n,
Proper fequiv (s_hd e3) ->
EN n (execread2 e3) ->
EN n e3.
Lemma ACT_1_3: forall g3 e3 n,
Step (s_hd e3) g3 ->
ACT n (execread1 (s_cons g3 e3)) ->
ACT n (s_cons g3 e3).
Lemma ACT_3_1:
forall g e n,
Step (s_hd e) g ->
EN n (execread1 (s_cons g e)) ->
ACT n (s_cons g e) ->
ACT n (execread1 (s_cons g e)).
Lemma NEUT_3_1':
forall g e n,
Step (s_hd e) g ->
EN n (execread1 (s_cons g e)) ->
NEUT n (s_cons g e) ->
NEUT n (execread1 (s_cons g e)).
Lemma NEUT_3_1:
forall e n,
is_exec e ->
EN n (execread1 e) ->
NEUT n e ->
NEUT n (execread1 e).
Lemma EN_AN_1_3:
forall e n,
is_exec e ->
EN n (execread1 e) -> AN n e ->
AN n (execread1 e).
Lemma E_AN_3_1:
forall e3 n,
is_exec e3 ->
EN n (execread1 e3) ->
Eventually (AN n) e3 ->
Eventually (AN n) (execread1 e3).
Lemma ACT_3_2:
forall e n, is_exec e ->
enabled_b (envread1 (s_hd e)) n = false ->
ACT n e ->
ACT n (execread2 e).
Lemma NEUT_3_2:
forall e n, is_exec e -> terminal (envread1 (s_hd e)) ->
NEUT n e ->
NEUT n (execread2 e).
Lemma term_EN_AN_3_2:
forall e n, is_exec e ->
terminal (envread1 (s_hd e)) ->
EN n (execread2 e) ->
AN n e ->
AN n (execread2 e).
Lemma E_AN_3_2:
forall e3 n,
is_exec e3 ->
terminal (envread1 (s_hd e3)) ->
EN n (execread2 e3) ->
Eventually (AN n) e3 ->
Eventually (AN n) (execread2 e3).
Once Algo1 has reached a terminal configuration, the
projection of an execution on Algo2 is actually an execution of Algo2.
Lemma Step_32:
forall g' g,
Step g' g ->
(forall n, enabled_b (envread1 g) n = false \/
has_moved_b g' g n = false) ->
Step (envread2 g') (envread2 g).
Lemma is_exec_3_2:
forall e3, is_exec e3 -> terminal (envread1 (s_hd e3)) ->
is_exec (execread2 e3).
Lemma Step_31:
forall g' g, Step g' g ->
forall n, enabled_b (envread1 g) n = true ->
has_moved_b g' g n = true ->
Step (envread1 g') (envread1 g).
forall g' g,
Step g' g ->
(forall n, enabled_b (envread1 g) n = false \/
has_moved_b g' g n = false) ->
Step (envread2 g') (envread2 g).
Lemma is_exec_3_2:
forall e3, is_exec e3 -> terminal (envread1 (s_hd e3)) ->
is_exec (execread2 e3).
Lemma Step_31:
forall g' g, Step g' g ->
forall n, enabled_b (envread1 g) n = true ->
has_moved_b g' g n = true ->
Step (envread1 g') (envread1 g).
Algo1 is silent, hence its spec can be reduced to a
predicate SPEC1 on Env1
Algo2 is self-stabilizing for its specification SPEC2,
under the daemon LS2, with legitimate states LS2
Variable (SPEC2: Exec2 -> Prop)
(LS2: Env2 -> Prop)
(DF2: Exec2 -> Prop)
(spec_ok2: spec_ok Assumption2 DF2 LS2 SPEC2).
(LS2: Env2 -> Prop)
(DF2: Exec2 -> Prop)
(spec_ok2: spec_ok Assumption2 DF2 LS2 SPEC2).
Assumption between 1 and 2: once Algo1 has stabilized
into SPEC1, Assume2 should hold.
Variable (SPEC1_Assume2:
forall (g: Env3),
Proper fequiv g -> Assume3 g -> SPEC1 (envread1 g) ->
Assume2 (envread2 g)).
forall (g: Env3),
Proper fequiv g -> Assume3 g -> SPEC1 (envread1 g) ->
Assume2 (envread2 g)).
Algo3: an execution meets the specification for Algo3, SPEC3,
if its projection on Algo2 meets SPEC2 and if it verifies SPEC1
on each of its configurations.
Definition Compo_SPEC SPEC_env1 SPEC2 :=
fun e => Always (fun ex => SPEC_env1 (envread1 (s_hd ex))) e /\
SPEC2 (execread2 e).
Notation SPEC3 := (Compo_SPEC SPEC1 SPEC2).
Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).
Theorem composition_spec_ok:
forall DF3: Exec3 -> Prop,
(forall e, is_exec e -> DF3 e ->
terminal (s_hd (execread1 e))->
DF2 (execread2 e)) ->
spec_ok Assumption3 DF3 LS3 SPEC3.
End Spec_OK.
fun e => Always (fun ex => SPEC_env1 (envread1 (s_hd ex))) e /\
SPEC2 (execread2 e).
Notation SPEC3 := (Compo_SPEC SPEC1 SPEC2).
Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).
Theorem composition_spec_ok:
forall DF3: Exec3 -> Prop,
(forall e, is_exec e -> DF3 e ->
terminal (s_hd (execread1 e))->
DF2 (execread2 e)) ->
spec_ok Assumption3 DF3 LS3 SPEC3.
End Spec_OK.
Algo1 is silent, hence its spec can be reduced to a predicate
SPEC1 on Env1
Assumption between 1 and 2: once Algo1 has stabilized into
SPEC1, Assume2 should hold.
Variable (SPEC1_Assume2:
forall (g: Env3),
Proper fequiv g -> Assume3 g -> SPEC1 (envread1 g) ->
Assume2 (envread2 g)).
forall (g: Env3),
Proper fequiv g -> Assume3 g -> SPEC1 (envread1 g) ->
Assume2 (envread2 g)).
Algo2 is silent:
Algo3
Notation SPEC3 := (fun g => SPEC1 (envread1 g) /\
SPEC2 (envread2 g)).
Theorem composition_P_correctness:
P_correctness Assumption3 SPEC3.
End Partial_Correctness.
SPEC2 (envread2 g)).
Theorem composition_P_correctness:
P_correctness Assumption3 SPEC3.
End Partial_Correctness.
Legitimate states for Algo1: terminal states Legitimate states for Algo2:
Variable (LS2: Env2 -> Prop) (LS2_compat: Proper pequiv LS2).
Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).
Notation LS3 := (fun g3 => terminal (envread1 g3) /\ LS2 (envread2 g3)).
Assumption between 1 and 2: once Algo1 has stabilized Assume2
should hold.
Variable (Term1_Assume2:
forall (g: Env3),
Proper fequiv g -> Assume3 g -> terminal (envread1 g) ->
Assume2 (envread2 g)).
forall (g: Env3),
Proper fequiv g -> Assume3 g -> terminal (envread1 g) ->
Assume2 (envread2 g)).
Daemon fairness
Variable (DF2: Exec2 -> Prop) (DF3: Exec3 -> Prop)
(hDF3: forall e, is_exec e -> DF3 e ->
terminal (s_hd (execread1 e))->
DF2 (execread2 e)).
Theorem composition_closure:
closure Assumption2 DF2 LS2 -> closure Assumption3 DF3 LS3.
End Closure.
(hDF3: forall e, is_exec e -> DF3 e ->
terminal (s_hd (execread1 e))->
DF2 (execread2 e)).
Theorem composition_closure:
closure Assumption2 DF2 LS2 -> closure Assumption3 DF3 LS3.
End Closure.
Termination:
- (A) One way of preventing this from happening, is to assume that
from any configuration of the first algorithm, the second one will
stabilize in a finite time. This will imply that, in a finite
time, any daemon avoiding to execute A1 steps will run out of
options and thus will be forced to make A1 progress. Such
hypothesis is sufficient to ensure the stabilization of an
algorithm.
- (B) That is not the only solution, one other is to change the execution model by adding a fairness assumption to the scheduler. For example, a weakly fair scheduler will have to eventually activate any rule that stays enabled for a sufficiently long time. This is what will make A1 progress in this solution.
Termination: Case A
Section A.
Variable (Hterm1: (termination (Algo := Algo1) Assumption1)).
Variable (Hterm2: forall (g: Env2),
Proper fequiv g ->
Acc (Step (Algo := Algo2)) g).
Lemma Hterm2_alt: well_founded (Step (Algo := Algo2)).
Variable (Hterm1: (termination (Algo := Algo1) Assumption1)).
Variable (Hterm2: forall (g: Env2),
Proper fequiv g ->
Acc (Step (Algo := Algo2)) g).
Lemma Hterm2_alt: well_founded (Step (Algo := Algo2)).
****
We show first termination for the lexicographic order:
this order is a relation on pairs (Env1, Env2) built by:
****
We show Acc for this order (see Lemma term_lexico_pairs_Acc):
- lp1: Step (Algo1) g1' g1 -> lexp (g1,_) (g1',_)
- lp2: eqE1 g1' g1 -> Step (Algo2) g2' g2
- > lexp (g1,g2) (g1',g2')
- the first order (on Algo1) is Acc (this is directly obtained from the assumption Hterm1)
- the second order (on Algo2) is well_founded
(this is obtained from Lemma Hterm2_alt)
- other properties about composition and transitivity:
- forall g' g2 g1: Env1, Step g' g1 -> eqE1 g1 g2 -> Step g' g2
(compatibility of Step)
- transitive eqE1
- forall g' g2 g1: Env1, Step g' g1 -> eqE1 g1 g2 -> Step g' g2
(compatibility of Step)
Lemma term_lexico_pairs:
forall g, Assume3 g -> Proper fequiv g ->
Acc (lexico_pairs fequiv (Step (Algo := Algo1))
(Step (Algo := Algo2)))
(envread1 g, envread2 g).
****
We then need to show that Step is included into this order
in some sense:
See Lemma incl_lexp.
We introduce a Boolean predicate step1_b
that allows to decide wether a step from Algo3 is to take
into account for Algo1 or for Algo2 (remember that within
a step, some nodes may have performed a step from Algo1
while others from Algo2).
The proof of Lemma incl_lexp is divided on two cases. For a
step of Algo3 between g and g', we split the proof into the case when
(step1_b g' g) is true and the case when it is false.
- inclusion Step (lexp @@ F)
- we fix F := fun g3 => (envread1 g3, envread2 g3)
- A step from Algo3 has to be considered for convergence
in Algo1, as far as some configuration of Algo1
evolves, hence as far as at least a node has actually
executed an action of Algo1. This is exactly what
step1_b expresses: it is true when, during a step of
Algo3, there exists a node which is enabled for some
action of Algo1 and actually moves.
- Any other step of Algo3 (ie when step1_b is false, ie no node executes an action of Algo1) is considered in the convergence of Algo2.
- In case (step1_b g' g) is true,
Lemma Step1_is_Step_Algo1 proves that for a step of Algo3
between g and g' (we note d3 the corresponding Diff),
there is a step of Algo1 between (envread1 g) and (envread1 g').
- In case (step1_b g' g) is false, we have to prove that
- eqE1 (envread1 g') (envread1 g)
which is shown by Lema Step_disabled1_unchanged1, and that
- there is a step of Algo2 between (envread2 g) and (envread2 g'). This is shown by Lemma Step2_is_Step_Algo2.
- eqE1 (envread1 g') (envread1 g)
which is shown by Lema Step_disabled1_unchanged1, and that
Definition step1_b (g' g: Env3): bool :=
existsb
(fun (n: Node) =>
andb (enabled_b (envread1 g) n)
(has_moved_b g' g n))
all_nodes.
Lemma step1_b_true:
forall g' g, Proper fequiv g -> Proper fequiv g' ->
(step1_b g' g = true <->
exists n, enabled_b (envread1 g) n = true /\
has_moved_b g' g n = true).
Lemma step1_b_false:
forall g' g, Proper fequiv g -> Proper fequiv g' ->
(step1_b g' g = false <->
forall n, enabled_b (envread1 g) n = false \/
has_moved_b g' g n = false).
Lemma Step1_is_Step_Algo1:
forall g' g, step1_b g' g = true -> Step g' g ->
Step (envread1 g') (envread1 g).
Lemma Step2_is_Step_Algo2:
forall g' g, step1_b g' g = false -> Step g' g ->
Step (envread2 g') (envread2 g).
Lemma incl_lexico_pairs:
inclusion (Step (Algo := Algo3))
(RelCompFun
(lexico_pairs fequiv (Step (Algo := Algo1))
(Step (Algo := Algo2)))
(fun (g: Env3) => (envread1 g, envread2 g))).
Theorem termination_A: termination Assumption3.
End A.
Algo1 is silent under weakly fair daemon
Algo2 converges to some legitimate states LS2, under weakly
faire daemon
Variable (LS2: Env2 -> Prop)
(LS2_compat: Proper pequiv LS2)
(Conv2: convergence Assumption2 weakly_fair LS2).
(LS2_compat: Proper pequiv LS2)
(Conv2: convergence Assumption2 weakly_fair LS2).
Assumption between 1 and 2: once Algo1 has stabilized, Assume2
should hold.
Variable (assume_32:
forall g3, Proper fequiv g3 -> Assume3 g3 ->
terminal (envread1 g3) ->
Assume2 (envread2 g3)).
forall g3, Proper fequiv g3 -> Assume3 g3 ->
terminal (envread1 g3) ->
Assume2 (envread2 g3)).
Legitimate States for Algo3
Lemma WF_exec_3_2:
forall (e3: Exec3),
is_exec e3 ->
terminal (envread1 (s_hd e3)) ->
weakly_fair e3 ->
weakly_fair (execread2 e3).
Section With_Squeeze.
Lemma move1_en_an_neq:
forall g3 e3 n,
Step (s_hd e3) g3 ->
enabled_b (envread1 g3) n = true ->
AN n (s_cons g3 e3) ->
~ (envread1 g3) =~= (envread1 (s_hd e3)).
Lemma move1_term_en_neq:
forall g3' g3 n,
Step g3' g3 ->
terminal g3' ->
enabled_b (envread1 g3) n = true ->
~(envread1 g3') =~= (envread1 g3).
Lemma execread1_all_compat:
forall e3, is_exec e3 -> Proper pequiv (execread1 e3).
Lemma non_terminal1_Skippable:
forall g3 e3, is_exec (s_cons g3 e3) ->
weakly_fair (s_cons g3 e3) ->
~ terminal (envread1 g3) ->
Skippable (envread1 g3)
(s_cons (envread1 g3) (execread1 e3)).
Lemma exec_can_collapse:
forall e3, is_exec e3 -> weakly_fair e3 ->
Squeezable (execread1 e3).
Lemma is_constant_terminal:
forall e3 g1, is_exec e3 -> weakly_fair e3 ->
is_constant g1 (execread1 e3) -> terminal g1.
Lemma Step_31_neq:
forall g3' g3,
Step g3' g3 ->
~ (envread1 g3') =~= (envread1 g3) ->
Step (envread1 g3') (envread1 g3).
Lemma suffix_13:
forall e1 e3, Proper pequiv e3 -> is_suffix (execread1 e3) e1 ->
exists e3', is_suffix e3 e3' /\ (execread1 e3') =~= e1.
Lemma is_exec_simu':
forall (e3: Exec3) (e1: Exec1),
is_exec e3 ->
Always (fun e =>
forall g1, is_constant g1 (execread1 e)
-> terminal g1) e3 ->
Simulation e1 (execread1 e3) ->
Always moves e1 -> is_exec e1.
Lemma is_exec_simu:
forall (e3: Exec3) (e1: Exec1),
is_exec e3 -> weakly_fair e3 ->
Simulation e1 (execread1 e3) -> Always moves e1 ->
is_exec e1.
Lemma collapse_is_exec:
forall e3 (ise: is_exec e3) (wf: weakly_fair e3),
is_exec (@Squeeze
_ _ Env_dec
_ (execread1_all_compat ise)
(exec_can_collapse ise wf)).
Lemma weakly_fair_monotonic:
Simulation_monotonic (A := Env1) weakly_fair.
Lemma weakly_fair_simu:
forall (e3: Exec3) (e1: Exec1),
is_exec e3 -> weakly_fair e3 ->
Simulation e1 (execread1 e3) ->
weakly_fair e1.
Lemma collapse_weakly_fair:
forall e3 (ise: is_exec e3) (wf: weakly_fair e3),
weakly_fair (@Squeeze
_ _ Env_dec _
(execread1_all_compat ise)
(exec_can_collapse ise wf)).
End With_Squeeze.
Lemma E_term1:
forall e3,
Assume3 (s_hd e3) -> is_exec e3 -> weakly_fair e3 ->
Eventually (fun e => terminal (envread1 (s_hd e))) e3.
Lemma assume_suffix:
forall e, Assume3 (s_hd e) -> is_exec e ->
forall e_suf, is_suffix e e_suf -> Assume3 (s_hd e_suf).
Theorem composition_convergence: convergence Assumption3 weakly_fair LS3.
End B.
Section Results.
Theorem Compo_B_Self_Stab (SPEC_env1: Env1 -> Prop) SPEC2:
(forall g, Proper fequiv g -> SPEC_env1 (envread1 g) ->
Assume2 (envread2 g)) ->
silence Assumption1 weakly_fair ->
self_stabilization Assumption1 weakly_fair (only_one SPEC_env1) ->
self_stabilization Assumption2 weakly_fair SPEC2 ->
self_stabilization Assumption3 weakly_fair (Compo_SPEC SPEC_env1 SPEC2).
Theorem Compo_Silent_Silent_B_Silent:
(forall g, Proper fequiv g ->
Assume3 g -> terminal (envread1 g) ->
Assume2 (envread2 g)) ->
silence Assumption1 weakly_fair ->
silence Assumption2 weakly_fair ->
silence Assumption3 weakly_fair.
End Results.
End Composition.
Close Scope signature_scope.
Unset Implicit Arguments.
forall (e3: Exec3),
is_exec e3 ->
terminal (envread1 (s_hd e3)) ->
weakly_fair e3 ->
weakly_fair (execread2 e3).
Section With_Squeeze.
Lemma move1_en_an_neq:
forall g3 e3 n,
Step (s_hd e3) g3 ->
enabled_b (envread1 g3) n = true ->
AN n (s_cons g3 e3) ->
~ (envread1 g3) =~= (envread1 (s_hd e3)).
Lemma move1_term_en_neq:
forall g3' g3 n,
Step g3' g3 ->
terminal g3' ->
enabled_b (envread1 g3) n = true ->
~(envread1 g3') =~= (envread1 g3).
Lemma execread1_all_compat:
forall e3, is_exec e3 -> Proper pequiv (execread1 e3).
Lemma non_terminal1_Skippable:
forall g3 e3, is_exec (s_cons g3 e3) ->
weakly_fair (s_cons g3 e3) ->
~ terminal (envread1 g3) ->
Skippable (envread1 g3)
(s_cons (envread1 g3) (execread1 e3)).
Lemma exec_can_collapse:
forall e3, is_exec e3 -> weakly_fair e3 ->
Squeezable (execread1 e3).
Lemma is_constant_terminal:
forall e3 g1, is_exec e3 -> weakly_fair e3 ->
is_constant g1 (execread1 e3) -> terminal g1.
Lemma Step_31_neq:
forall g3' g3,
Step g3' g3 ->
~ (envread1 g3') =~= (envread1 g3) ->
Step (envread1 g3') (envread1 g3).
Lemma suffix_13:
forall e1 e3, Proper pequiv e3 -> is_suffix (execread1 e3) e1 ->
exists e3', is_suffix e3 e3' /\ (execread1 e3') =~= e1.
Lemma is_exec_simu':
forall (e3: Exec3) (e1: Exec1),
is_exec e3 ->
Always (fun e =>
forall g1, is_constant g1 (execread1 e)
-> terminal g1) e3 ->
Simulation e1 (execread1 e3) ->
Always moves e1 -> is_exec e1.
Lemma is_exec_simu:
forall (e3: Exec3) (e1: Exec1),
is_exec e3 -> weakly_fair e3 ->
Simulation e1 (execread1 e3) -> Always moves e1 ->
is_exec e1.
Lemma collapse_is_exec:
forall e3 (ise: is_exec e3) (wf: weakly_fair e3),
is_exec (@Squeeze
_ _ Env_dec
_ (execread1_all_compat ise)
(exec_can_collapse ise wf)).
Lemma weakly_fair_monotonic:
Simulation_monotonic (A := Env1) weakly_fair.
Lemma weakly_fair_simu:
forall (e3: Exec3) (e1: Exec1),
is_exec e3 -> weakly_fair e3 ->
Simulation e1 (execread1 e3) ->
weakly_fair e1.
Lemma collapse_weakly_fair:
forall e3 (ise: is_exec e3) (wf: weakly_fair e3),
weakly_fair (@Squeeze
_ _ Env_dec _
(execread1_all_compat ise)
(exec_can_collapse ise wf)).
End With_Squeeze.
Lemma E_term1:
forall e3,
Assume3 (s_hd e3) -> is_exec e3 -> weakly_fair e3 ->
Eventually (fun e => terminal (envread1 (s_hd e))) e3.
Lemma assume_suffix:
forall e, Assume3 (s_hd e) -> is_exec e ->
forall e_suf, is_suffix e e_suf -> Assume3 (s_hd e_suf).
Theorem composition_convergence: convergence Assumption3 weakly_fair LS3.
End B.
Section Results.
Theorem Compo_B_Self_Stab (SPEC_env1: Env1 -> Prop) SPEC2:
(forall g, Proper fequiv g -> SPEC_env1 (envread1 g) ->
Assume2 (envread2 g)) ->
silence Assumption1 weakly_fair ->
self_stabilization Assumption1 weakly_fair (only_one SPEC_env1) ->
self_stabilization Assumption2 weakly_fair SPEC2 ->
self_stabilization Assumption3 weakly_fair (Compo_SPEC SPEC_env1 SPEC2).
Theorem Compo_Silent_Silent_B_Silent:
(forall g, Proper fequiv g ->
Assume3 g -> terminal (envread1 g) ->
Assume2 (envread2 g)) ->
silence Assumption1 weakly_fair ->
silence Assumption2 weakly_fair ->
silence Assumption3 weakly_fair.
End Results.
End Composition.
Close Scope signature_scope.
Unset Implicit Arguments.