PADEC - Coq Library

Library Padec.KClustering.KClustering_def_termination

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

From Coq Require Import SetoidClass.
From Coq Require Import SetoidList.
From Coq Require Import ZArith.
From Coq Require Import Bool.
From Coq Require Import Union.
From Coq Require Import Relations.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import KClustering_algo.
From Padec Require Import KClustering_specification.
From Padec Require Import Spanning_Tree.
From Padec Require Import P_Q_Termination.

Open Scope signature_scope.
Open Scope Z_scope.
Set Implicit Arguments.

roadmap

1) show termination for each king of safe steps:

Step_decreasing Alpha_SafeStep alpha_potential all_nodes.
Step_decreasing Pcl_SafeStep pcl_potential all_nodes.
Step_decreasing Head_SafeStep hd_pot all_nodes.

2) use union_lex_wf3

Section KClustering_DEF_termination.

Channel and network

  Context {Chans: Channels} {Net: Symmetric_Network}
          {KCP: KClustering_parameters} {KCT: KC_algo_tools}.

  Variable (root: Node).
  Notation Env := (Env (Algo := KC_algo)).

Safe configurations and safe steps:

configurations with spanning tree assumed

  Section SafeEnv.

    Definition Pspanning_tree (g: Env): Prop :=
      Proper pequiv g /\ spanning_tree root (Par_part g)
      /\ Symmetric_Network_assumption
           Net (fun n => KCpeers (g n)) (fun n => KCreverse (g n)).

    Global Instance Pspanning_tree_compat: Proper fequiv Pspanning_tree.

safe configurations are stable

    Lemma KCpeers_Stable:
      forall g g', Step g' g ->
                   (SetoidClass.equiv ==>
                                      equivlistA (A:=Channel) SetoidClass.equiv )
                      (fun n => KCpeers (g' n ))
                                                    (fun n => KCpeers (g n )).

    Lemma KCreverse_Stable:
      forall g g',
        Step g' g ->
        forall n1 n2 c1 c2,
          n1 == n2 -> c1 == c2 ->
          InA (SetoidClass.equiv (A:=Channel)) c1 (KCpeers (g n1))
          -> KCreverse (g' n2) c2 == KCreverse (g n1) c1.

    Lemma spanning_tree_stable:
      forall (g: Env) (g': Env),
        Pspanning_tree g -> Step g' g -> Pspanning_tree g'.

  End SafeEnv.

  Notation getEnv := proj1_sig.

Alpha Steps: a safe step in which at least one node has

executed an alpha action. Note that other nodes may also have executed other kind of actions (parCl and Head actions).

  Section Alpha_SafeSteps.

    Definition alpha_enabled_bb (g: Env) (n: Node): bool :=
      alpha_enabled_b (g n) (local_env g n).

    Global Instance alpha_enabled_bb_compat: Proper fequiv alpha_enabled_bb.

Steps restricted to the ones such that: at least one node in the step executes an alpha action

    Definition QTrans_alpha (sg' sg: sig Pspanning_tree): Prop :=
      exists (p: Node ), alpha_enabled_bb (getEnv sg) p = true /\
                        has_moved_b (getEnv sg') (getEnv sg) p = true.

Boolean version of QTrans_alpha

    Definition alpha_step_b (g' g: Env): bool :=
      existsb
        (fun (n: Node) =>
           andb (alpha_enabled_bb g n) (has_moved_b g' g n))
        all_nodes.

Equivalence between both definitions

    Lemma QTrans_alpha_alt:
      forall sg' sg, QTrans_alpha sg' sg <->
                     alpha_step_b (getEnv sg') (getEnv sg) = true.

Alpha Safe Steps

    Definition Alpha_Safe :=
      (fun sg' sg: sig Pspanning_tree =>
         alpha_step_b (getEnv sg') (getEnv sg) = true).
    Definition Alpha_SafeStep := safeQStep Alpha_Safe.

  End Alpha_SafeSteps.

Parent Cluster Steps: No node has executed an alpha action,

at least one has executed a parCl action. Note that other nodes may also have executed a head action.

  Section Pcl_SafeSteps.

    Definition pcl_enabled_bb (g: Env) (n: Node): bool :=
      parCl_enabled_b (g n) (local_env g n).

    Global Instance pcl_enabled_bb_compat: Proper fequiv pcl_enabled_bb.

Steps restricted to the ones such that:

not an alpha safe step (i.e., no node executes an alpha action)
at least node executes a parCl action

    Definition QTrans_pcl (sg' sg: sig Pspanning_tree): Prop :=
      ~ QTrans_alpha sg' sg /\
      exists (p: Node ), pcl_enabled_bb (getEnv sg) p = true /\
                        has_moved_b (getEnv sg') (getEnv sg) p = true.

Boolean version of QTrans_pcl

    Definition pcl_step_b (g' g: Env): bool :=
      andb
        (forallb
           (fun n: Node => orb (negb (alpha_enabled_bb g n))
                               (negb (has_moved_b g' g n)))
           all_nodes)
        (existsb
           (fun (n: Node) =>
              andb (pcl_enabled_bb g n) (has_moved_b g' g n))
           all_nodes).

Equivalence between both definitions

    Lemma QTrans_pcl_alt:
      forall sg' sg, QTrans_pcl sg' sg <->
                     pcl_step_b (getEnv sg') (getEnv sg) = true.

Pcl Safe Step

    Definition Pcl_Safe :=
      (fun sg' sg: sig Pspanning_tree =>
         pcl_step_b (getEnv sg') (getEnv sg) = true).
    Definition Pcl_SafeStep := safeQStep Pcl_Safe.

  End Pcl_SafeSteps.

Head Cluster Steps: No node has executed either an alpha

action or an parCl action. At least one has executed a head action.

  Section Head_SafeSteps.

    Definition hd_enabled_bb (g: Env) (n: Node): bool :=
      (hd_enabled_b (g n) (local_env g n)).

    Global Instance hd_enabled_bb_compat: Proper fequiv hd_enabled_bb.

Steps that are neither alpha safe steps nor Plc safe steps. i.e., no node executes an alpha action nor a pcl action.

Definition QTrans_hd (sg' sg: sig Pspanning_tree): Prop :=
~ QTrans_alpha sg' sg /\ ~ QTrans_pcl sg' sg.

Boolean version of QTrans_hd

    Definition hd_step_b (g' g: Env): bool :=
      (forallb
         (fun n: Node =>
            orb (negb (orb (alpha_enabled_bb g n)
                           (pcl_enabled_bb g n)))
                (negb (has_moved_b g' g n)))
         all_nodes).

Equivalence between both definitions

    Lemma QTrans_hd_alt:
      forall sg' sg, QTrans_hd sg' sg <->
                     hd_step_b (getEnv sg') (getEnv sg) = true.

Head safe step

    Definition Head_Safe :=
      (fun sg' sg: sig Pspanning_tree =>
         hd_step_b (getEnv sg') (getEnv sg) = true).
    Definition Head_SafeStep := safeQStep Head_Safe.

  End Head_SafeSteps.

Safe Steps as union of Alpha, Cluster Parent, Cluster Head

Steps: the relation SafeStep is exactly the union of relations Alpha_SafeStep, Pcl_SafeStep and Head_SafeStep.

  Section Split_SafeStep.

    Lemma Trans_union:
      relation_equivalence
        (safeStep (safe := Pspanning_tree))
        (safeQStep (safe := Pspanning_tree)
                   (union Alpha_Safe
                          (union Pcl_Safe Head_Safe))).

  End Split_SafeStep.

End KClustering_DEF_termination.

Close Scope Z_scope.
Close Scope signature_scope.
Unset Implicit Arguments.