PADEC - Coq Library

# Library Padec.Dijkstra.Dijkstra_Global_Thm

From Coq Require Import SetoidList.

From Coq Require Import SetoidClass.

From Coq Require Import Lia.

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 Ring_topology.

From Padec Require Import Fairness.

From Padec Require Import Self_Stabilization.

From Padec Require Import Dijkstra_algo.

From Padec Require Import Dijkstra_common.

From Padec Require Import Dijkstra_specifications.

From Padec Require Import Dijkstra_specifications_proved.

From Padec Require Import Dijkstra_complexity.

From Padec Require Import Dijkstra_complexity_degenerated.

From Padec Require Import Dijkstra_worst_case.

From Padec Require Import Dijkstra_worst_case_degenerated.

From Padec Require Import Steps.

Open Scope nat_scope.

Set Implicit Arguments.

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 Fairness.

From Padec Require Import Self_Stabilization.

From Padec Require Import Dijkstra_algo.

From Padec Require Import Dijkstra_common.

From Padec Require Import Dijkstra_specifications.

From Padec Require Import Dijkstra_specifications_proved.

From Padec Require Import Dijkstra_complexity.

From Padec Require Import Dijkstra_complexity_degenerated.

From Padec Require Import Dijkstra_worst_case.

From Padec Require Import Dijkstra_worst_case_degenerated.

From Padec Require Import Steps.

Open Scope nat_scope.

Set Implicit Arguments.

# Diskstra's first token ring algorithm

- Proof of self-stabilization and specification
- Proof of a complexity bound in steps
- Proof that this complexity bound is exact (by building a worst case prefix of execution)

- (B.G) Provided that , the stabilization time of Algorithm DTR is at most \DTCExact steps.
- (B.1-2) If or , the stabilization time is 0 step.
- (B.3) If , the stabilization time is at most 3
steps.
- (S) Algorithm \DTR is a self-stabilizing token circulation
in any unidirectional rooted ring of size such that
under the distributed unfair daemon.
- (T.G)] Provided that , this bound is
tight, {\em i.e.}, it can be reached. In other words,
for any ring of size at least 4, there exists an
execution whose stabilization time exactly matches the
bound.
- (T.3) For , the bound of steps is also tight.

Section Dijkstra_Global_Thm.

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 Env := (Env (Net := Net) (Algo := Dijkstra_algo)).

Existing Instance Dijkstra_RO_assumption.

Notation N := (Ring_size Root).

Hypothesis HNk: N <= k.

(B.G) Provided that , the stabilization
time of Algorithm DTR is at most \DTCExact steps.

Theorem BdotG:

4 <= N -> N <= k ->

Steps_complexity (Dijkstra_exact_bound N)

(fun e => Leg_state (s_hd e))

(fun e => Assume (s_hd e) /\ is_exec e).

4 <= N -> N <= k ->

Steps_complexity (Dijkstra_exact_bound N)

(fun e => Leg_state (s_hd e))

(fun e => Assume (s_hd e) /\ is_exec e).

(B.1-2) If or , the stabilization time is 0
step.

Theorem Bdot1minus2:

N = 1 \/ N = 2 ->

Steps_complexity 0

(fun e => Leg_state (s_hd e))

(fun e => Assume (s_hd e) /\ is_exec e).

N = 1 \/ N = 2 ->

Steps_complexity 0

(fun e => Leg_state (s_hd e))

(fun e => Assume (s_hd e) /\ is_exec e).

(B.3) If , the stabilization time is at most 3
steps.

Theorem Bdot3:

N = 3 ->

Steps_complexity 3

(fun e => Leg_state (s_hd e))

(fun e => Assume (s_hd e) /\ is_exec e).

N = 3 ->

Steps_complexity 3

(fun e => Leg_state (s_hd e))

(fun e => Assume (s_hd e) /\ is_exec e).

(S) Algorithm \DTR is a self-stabilizing token circulation
in any unidirectional rooted ring of size such that
under the distributed unfair daemon.

(T.G) Provided that , this bound is
tight, {\em i.e.}, it can be reached. In other words,
for any ring of size at least 4, there exists an
execution whose stabilization time exactly matches the
bound.

Theorem TdotG:

4 <= N -> N <= k ->

exists e, Assume (s_hd e) /\ is_exec e /\

At_N_steps (Dijkstra_exact_bound N)

(fun e => Leg_state (s_hd e)) e.

4 <= N -> N <= k ->

exists e, Assume (s_hd e) /\ is_exec e /\

At_N_steps (Dijkstra_exact_bound N)

(fun e => Leg_state (s_hd e)) e.

(T.3) For , the bound of steps is also tight.