PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_specifications

A Framework for Certified Self-Stabilization
PADEC Coq Library


Global Imports

From Coq Require Import SetoidClass.

Local Imports

From Padec Require Import Stream.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Exec.


Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Diskstra's first token ring algorithm

Dijkstra's Token Ring Specifications
/contains:/ Token Circulation Specification: A unique token always eventually passes through each node.
The specification is a property on an execution and contains

Section Token_Circulation_Spec.

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

  Definition Token_Circulation_Spec (e: Exec): Prop :=
    exists (Token: Env -> Node -> Prop),
      
      Always (fun e_ => forall n1 n2,
                  Token (s_hd e_) n1 ->
                  Token (s_hd e_) n2 -> n1 == n2) e
      /\
      
      forall (n: Node),
        Always (Eventually (fun e_ => Token (s_hd e_) n)) e.

End Token_Circulation_Spec.

Unset Implicit Arguments.
Close Scope nat_scope.
Close Scope signature_scope.