CSPM.FiringRules.Rules

This module defines data types for (CSP) proof trees. A proof tree shows that a particular transition is valid with respect to the firing rules semantics.

(For more info on the firing rule semantics see: The Theory and Practice of Concurrency A.W. Roscoe 1999.)

We use three separate data types: RuleTau stores a proof tree for a tau rule, RuleTick stores a proof tree for a tick rule and RuleEvent stores a proof tree for an event from Sigma.

There is a one-to-one correspondence between each constructor of the data types RuleTau, RuleTick, RuleEvent and one fireing rule.

Documentation

data Rule i

A sum-type for tau, tick and regular proof trees.

Constructors

TauRule (RuleTau i)

TickRule (RuleTick i)

EventRule (RuleEvent i)

Instances

(Eq (RuleEvent i), Eq (RuleTick i), Eq (RuleTau i)) => Eq (Rule i)

(Show (RuleEvent i), Show (RuleTick i), Show (RuleTau i)) => Show (Rule i)

Typeable (* -> *) Rule

isTauRule :: Rule i -> Bool

Is this a proof tree for a tau-transition ?

data RuleTau i

Representation of tau proof trees.

Constructors

Hidden (EventSet i) (RuleEvent i)

HideTau (EventSet i) (RuleTau i)

SeqTau (RuleTau i) (Process i)

SeqTick (RuleTick i) (Process i)

InternalChoiceL (Process i) (Process i)

InternalChoiceR (Process i) (Process i)

ChaosStop (EventSet i)

TimeoutOccurs (Process i) (Process i)

TimeoutTauR (RuleTau i) (Process i)

ExtChoiceTauL (RuleTau i) (Process i)

ExtChoiceTauR (Process i) (RuleTau i)

InterleaveTauL (RuleTau i) (Process i)

InterleaveTauR (Process i) (RuleTau i)

InterleaveTickL (RuleTick i) (Process i)

InterleaveTickR (Process i) (RuleTick i)

ShareTauL (EventSet i) (RuleTau i) (Process i)

ShareTauR (EventSet i) (Process i) (RuleTau i)

ShareTickL (EventSet i) (RuleTick i) (Process i)

ShareTickR (EventSet i) (Process i) (RuleTick i)

AParallelTauL (EventSet i) (EventSet i) (RuleTau i) (Process i)

AParallelTauR (EventSet i) (EventSet i) (Process i) (RuleTau i)

AParallelTickL (EventSet i) (EventSet i) (RuleTick i) (Process i)

AParallelTickR (EventSet i) (EventSet i) (Process i) (RuleTick i)

InterruptTauL (RuleTau i) (Process i)

InterruptTauR (Process i) (RuleTau i)

TauRepAParallel [Either (EventSet i, Process i) (EventSet i, RuleTau i)]

RenamingTau (RenamingRelation i) (RuleTau i)

LinkLinked (RenamingRelation i) (RuleEvent i) (RuleEvent i)

LinkTauL (RenamingRelation i) (RuleTau i) (Process i)

LinkTauR (RenamingRelation i) (Process i) (RuleTau i)

LinkTickL (RenamingRelation i) (RuleTick i) (Process i)

LinkTickR (RenamingRelation i) (Process i) (RuleTick i)

ExceptionTauL (EventSet i) (RuleTau i) (Process i)

ExceptionTauR (EventSet i) (Process i) (RuleTau i)

TraceSwitchOn (Process i)

Instances

(Eq (RuleEvent i), Eq (RuleTick i), Eq (Process i), Eq (EventSet i), Eq (RenamingRelation i)) => Eq (RuleTau i)

(Ord (RuleEvent i), Ord (RuleTick i), Ord (Process i), Ord (EventSet i), Ord (ExtProcess i), Ord (Prefix i), Ord (Event i), Ord (RenamingRelation i)) => Ord (RuleTau i)

(Show (RuleEvent i), Show (RuleTick i), Show (Process i), Show (EventSet i), Show (RenamingRelation i)) => Show (RuleTau i)

Arb i => Arbitrary (RuleTau i)

data RuleTick i

Representation of tick proof trees.

Constructors

SkipTick

HiddenTick (EventSet i) (RuleTick i)

InterruptTick (RuleTick i) (Process i)

TimeoutTick (RuleTick i) (Process i)

ShareOmega (EventSet i)

AParallelOmega (EventSet i) (EventSet i)

RepAParallelOmega [EventSet i]

InterleaveOmega

ExtChoiceTickL (RuleTick i) (Process i)

ExtChoiceTickR (Process i) (RuleTick i)

RenamingTick (RenamingRelation i) (RuleTick i)

LinkParallelTick (RenamingRelation i)

Instances

(Eq (Process i), Eq (EventSet i), Eq (Prefix i), Eq (ExtProcess i), Eq (RenamingRelation i)) => Eq (RuleTick i)

(Ord (Process i), Ord (EventSet i), Ord (Prefix i), Ord (ExtProcess i), Ord (RenamingRelation i)) => Ord (RuleTick i)

(Show (Process i), Show (EventSet i), Show (Prefix i), Show (ExtProcess i), Show (RenamingRelation i)) => Show (RuleTick i)

Arb i => Arbitrary (RuleTick i)

data RuleEvent i

Representation of regular proof trees.

Constructors

HPrefix (Event i) (Prefix i)

ExtChoiceL (RuleEvent i) (Process i)

ExtChoiceR (Process i) (RuleEvent i)

InterleaveL (RuleEvent i) (Process i)

InterleaveR (Process i) (RuleEvent i)

SeqNormal (RuleEvent i) (Process i)

NotHidden (EventSet i) (RuleEvent i)

NotShareL (EventSet i) (RuleEvent i) (Process i)

NotShareR (EventSet i) (Process i) (RuleEvent i)

Shared (EventSet i) (RuleEvent i) (RuleEvent i)

AParallelL (EventSet i) (EventSet i) (RuleEvent i) (Process i)

AParallelR (EventSet i) (EventSet i) (Process i) (RuleEvent i)

AParallelBoth (EventSet i) (EventSet i) (RuleEvent i) (RuleEvent i)

RepAParallelEvent [EventRepAPart i]

NoInterrupt (RuleEvent i) (Process i)

InterruptOccurs (Process i) (RuleEvent i)

TimeoutNo (RuleEvent i) (Process i)

Rename (RenamingRelation i) (Event i) (RuleEvent i)

RenameNotInDomain (RenamingRelation i) (RuleEvent i)

ChaosEvent (EventSet i) (Event i)

LinkEventL (RenamingRelation i) (RuleEvent i) (Process i)

LinkEventR (RenamingRelation i) (Process i) (RuleEvent i)

NoException (EventSet i) (RuleEvent i) (Process i)

ExceptionOccurs (EventSet i) (Process i) (RuleEvent i)

Instances

(Eq (Event i), Eq (Prefix i), Eq (Process i), Eq (ExtProcess i), Eq (EventSet i), Eq (RenamingRelation i)) => Eq (RuleEvent i)

(Ord (Event i), Ord (Prefix i), Ord (Process i), Ord (ExtProcess i), Ord (EventSet i), Ord (RenamingRelation i)) => Ord (RuleEvent i)

(Show (Event i), Show (Prefix i), Show (Process i), Show (ExtProcess i), Show (EventSet i), Show (RenamingRelation i)) => Show (RuleEvent i)

Arb i => Arbitrary (RuleEvent i)

type EventRepAPart i = Either (EventSet i, Process i) (EventSet i, RuleEvent i)