PADEC - Coq Library

Library Padec.BFS.BFS_specification_proved_bis

*Certified Round Complexity of Self-Stabilizing Algorithms*

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Lia.

From Padec Require Import SetoidUtil.
From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Fairness.
From Padec Require Import Self_Stabilization.
From Padec Require Import BFS_algo_bis.
From Padec Require Import BFS_common_bis.
From Padec Require Import BFS_specification.
From Padec Require Import BFS_correctness_bis.
From Padec Require Import BFS_rounds_bis.
From Padec Require Import Rounds.

Open Scope nat_scope.
Set Implicit Arguments.

BFS: Proof of self-stabilization and specification

/contains:/ Proof that the algorithm is self-stabilizing wrt BFS construction (the algorithm is silent).

/assumes:/ G = (V, E) connected, rooted (r), semi-anonymous, Weakly fair daemon

Section BFS_spec_proved.

  Context {Chans: Channels}
          {Net: Network}
          {Graph_assumption: BFS_Assume}
          {Graph_network_assumption: Graph_Network_matching}.

  Existing Instance G_compat.

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

  Existing Instance BFS_RO_assumption.

reached Obtained from round complexity

  Theorem BFS_self_stab_prop:
    self_stabilization
      BFS_RO_assumption weakly_fair
      (only_one (BFS_Spanning_Tree_spec Root Par_Rel)).

End BFS_spec_proved.

Unset Implicit Arguments.
Close Scope nat_scope.