PADEC - Coq Library

Library Padec.KDomSet.KDomSet_specification

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Import

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import ZArith.

Local Import

From Padec Require Import SetoidUtil.
From Padec Require Import RelationA.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Graph_Diameter.
From Padec Require Import Tree_topology_ALT.

Open Scope Z_scope.
Set Implicit Arguments.

Specification for a k-hop-dominating set algorithm

Section KDomSet_Specification.

Problem Definition

Let assume an algorithm and a positive number k

  Context {Chans: Channels}
          {Net: Network}
          {Algo: Algorithm}.

The parameter K itself (from K-Dominating-Set)

  Class KDomSet_parameters := {
                               k: Z;
                               k_pos: k > 0
                             }.
  Context {KDP: KDomSet_parameters}.

Graph, specified as a relation by the network Net

  Notation R_Sym_Net :=
    (fun n n' => exists c , is_channel n c n' \/
                           is_channel n' c n).

Some configuration of the system (made of the network and the algorithm) contains a k-hop-dominating set

if one can express a predicate on nodes: kDominator which identifies nodes to be in some k-hop-dominating set.

Precisely, for every node, it should be linked to a node in the k-hop-dominating set thanks to a path whose length is smaller than k.

Predicates which holds when the node is identified as in the k-hop-dominating set in the current configuration.

  Variable (kDominator: Env -> Node -> Prop).

  Definition kDOM (env: Env): Prop :=
    forall (p: Node),
    exists (d: Node ),
      kDominator env d /\
      ( p == d \/
        exists path , is_path R_Sym_Net d path p /\
                     (Z_of_nat (S (length path)) <= k)%Z ).

End KDomSet_Specification.

Close Scope Z_scope.
Unset Implicit Arguments.