PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_complexity

A Framework for Certified Self-Stabilization
PADEC Coq Library


Global Imports

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

Local Imports

From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.
From Padec Require Import Ring_topology.
From Padec Require Import Dijkstra_algo.
From Padec Require Import Dijkstra_common.
From Padec Require Import Dijkstra_Z.
From Padec Require Import Dijkstra_sum_dist.
From Padec Require Import Self_Stabilization.
From Padec Require Import Steps.
From Padec Require Import NatUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import Count.
From Padec Require All_In.
From Padec Require FoldRight.
From Padec Require Import ListUtils.


Set Implicit Arguments.
Open Scope nat_scope.

Diskstra's first token ring algorithm

Complexity Bound

/contains:/ Proof of the complexity bound
/assumes:/ Parameter k>1; the network is a unidirectional rooted ring; N <= k
Case N >= 4
General case

Section Dijkstra_complexity.

  Context {Chans: Channels}
          {Net: Network}
          {RURN: Rooted_Unidirectional_Ring_Network Net}
          {DP: Dijkstra_parameters}.

  Notation Algo := Dijkstra_algo.
  Notation Root := (RURN_root (Net := Net)).
  Notation Ring := (URN_topo (Net := Net)).


  Notation N := (Ring_size Root).

  Hypothesis HNk: N <= k.

Proof for non-degenerated cases (N >= 4)

  Section Non_Degenerated.

    Hypothesis HN4: N >= 4.

Cost

The cost of a configuration:
    Definition cost (g: Env): nat := sum_dist g + (Z g) * N - 2.

sum_dist g + (Z g) * N < 3 implies a legitimate configuration
    Lemma cost_0_leg_state:
      forall g, Proper pequiv g -> Assume g ->
                sum_dist g + (Z g) * N < 3 -> Leg_state g.

Cost is bounded, using bounds for Z and sum_dist
    Lemma cost_bound:
      forall g, Assume g -> Proper pequiv g ->
                Z g <= N - 2 ->
                cost g <= Dijkstra_exact_bound N - 1.

Cost decreases
    Lemma cost_decreases:
      forall g, Assume g -> ~Leg_state g ->
                forall g', Step g' g -> cost g' < cost g.

    Lemma Dijkstra_exact_bound_g0: Dijkstra_exact_bound N > 0.

    Theorem Dijkstra_bound_non_degenerated_cases:
      Steps_complexity (Dijkstra_exact_bound N)
                       (fun e => Leg_state (s_hd e))
                       (fun e => Assume (s_hd e) /\ is_exec e).
  End Non_Degenerated.


End Dijkstra_complexity.

Unset Implicit Arguments.
Close Scope nat_scope.