CSPM.FiringRules.Rules

This modules defines data types for (CSP) proof trees. A proof trees show 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 for tau rules, tick rules and regular rules.

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

A list of the implemented firing rules (as pdf) is available via the package maintainer or the web page.

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)

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)

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 (i.e. non-tau and non-tick transitions)

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)