PADEC - Coq Library
Library Padec.MessagePassing.FairnessMP
From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.
From Coq Require Import Streams.
From Coq Require Import SetoidClass.
From Coq Require Import Bool.
From Coq Require Import Streams.
From Padec Require Import WellfoundedUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import AlgorithmMP.
From Padec Require Import RelModelMP.
From Padec Require Import ExecMP.
Open Scope signature_scope.
Set Implicit Arguments.
Section Fairness.
Context {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork} {Algo: MPAlgorithm}.
From Padec Require Import SetoidUtil.
From Padec Require Import AlgorithmMP.
From Padec Require Import RelModelMP.
From Padec Require Import ExecMP.
Open Scope signature_scope.
Set Implicit Arguments.
Section Fairness.
Context {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork} {Algo: MPAlgorithm}.
Definition unfair_daemon (e: Exec): Prop := True.
End Fairness.
Close Scope signature_scope.
Unset Implicit Arguments.
End Fairness.
Close Scope signature_scope.
Unset Implicit Arguments.