Coq Library
Tools

#### Global Imports

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

#### Local Imports

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)
This file adds nothing but gathers every important results, namely the results in Theorem 1. Meanwhile, it checks that no additionnal assumption has been introduced in the development.
Theorem 1:
• (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)).

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

(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).

(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).

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

(T.3) For , the bound of steps is also tight.
Theorem Tdot3:
N = 3 ->
exists e, Assume (s_hd e) /\ is_exec e /\
At_N_steps 3 (fun e => Leg_state (s_hd e)) e.

End Dijkstra_Global_Thm.

Unset Implicit Arguments.
Close Scope nat_scope.