PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.KDomSet.KDomSet_specification_proved_tree_topology

A Framework for Certified Self-Stabilization
PADEC Coq Library

Global Import

From Coq Require Import Omega.
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import Count.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Tree_topology.
From Padec Require Import KDomSet_specification_tree_topology.
From Padec Require Import KDomSet_algo_tree_topology.
From Padec Require Import KDomSet_correctness_tree_topology.
From Padec Require Import KDomSet_termination_tree_topology.
From Padec Require Import KDomSet_count_tree_topology.

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

Definition of the algorithm and proof

Section KDomSet_Specification_Proved.

Channel and Network definitions
  Context {Chans: Channels}
          {Net: Network}
          {DTN: Down_Tree_Network Net}
          {KDP: KDomSet_parameters}.
  Let k_pos := k_pos.

  Notation Tree := (DTN_topo (Net := Net)).
  Context {SPAN: is_spanning _ Tree}.

  Notation Algo := KDom_algo.
  Notation Env := (Env (Net := Net) (Algo := KDom_algo)).


  Section Silent_Self_Stabilization.

    Theorem kdom_silent_self_stabilization:
      silence KDom_RO_assumption unfair_daemon /\
      self_stabilization KDom_RO_assumption unfair_daemon (only_one (kDOM kDominator_ (k := k))).

  End Silent_Self_Stabilization.

  Section Counting.

    Definition Dominators (g: Env) := { n: Node | kDominator_ g n }.

    Theorem counting:
      forall (g: Env),
        Assume g -> terminal g ->
        exists N D: nat,
          Num_Card Same Node N /\ Num_Card Same (Dominators g) D /\
          (N - 1 >= S (Z.to_nat k) * (D - 1))%nat.

  End Counting.

End KDomSet_Specification_Proved.

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