PADEC - Coq Library

Library Padec.Model.Rounds_Steps_inductive_def

A Framework for Certified Self-Stabilization
PADEC Coq Library

June 2016

Global Imports

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

Local Imports

From Padec Require Import ZUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Stream.
From Padec Require Import Stream_Length.
From Padec Require Import Exec.
From Padec Require Import Rounds_inductive_def.
From Padec Require Import Steps.
From Padec Require Import BoolSet.
From Padec Require Import Self_Stabilization.

Open Scope signature_scope.
Set Implicit Arguments.

Synchronous Daemon:

number of steps = number of rounds

Section Synchronous.

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

  Notation NSet := (BoolSet (A := Node)).
  Notation eqNSet := (eqBoolSet (eqA := (equiv (A := Node)))).
  Notation leNSet := (leBoolSet (eqA := (equiv (A := Node)))).

  Lemma synchronous_rounds_steps:
    forall (P: Exec -> Prop) (P_dec: Weak_Dec pequiv P)
           (e: Exec) (pe: Proper pequiv e) (he: Eventually P e),
      synchronous_exec e -> is_exec e ->
      count_steps P_dec pe he = count_rounds P_dec pe he.

End Synchronous.

Sequential Algorithm:

at most one enabled node per configuration hence, number of steps = number of rounds

Section Sequential.

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

  Notation NSet := (BoolSet (A := Node)).
  Notation eqNSet := (eqBoolSet (eqA := (equiv (A := Node)))).
  Notation leNSet := (leBoolSet (eqA := (equiv (A := Node)))).

  Hypothesis progress_ACT:
    forall e, is_exec e -> (exists n , EN_b n e = true ) -> (exists p , ACT_b p e = true ).

  Lemma sequential_rounds_steps:
    forall (P: Exec -> Prop) (P_dec: Weak_Dec pequiv P)
           (e: Exec) (pe: Proper pequiv e) (he: Eventually P e),
      sequential_exec e -> is_exec e ->
      count_steps P_dec pe he = count_rounds P_dec pe he.

End Sequential.

Close Scope signature_scope.
Unset Implicit Arguments.