CSPM-FiringRules- Firing rules semantic of CSPM




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.



data Rule i Source

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


TauRule (RuleTau i) 
TickRule (RuleTick i) 
EventRule (RuleEvent i) 


(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 -> BoolSource

Is this a proof tree for a tau-transition

data RuleTau i Source

Representation of tau proof trees.


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) 


data RuleEvent i Source

Representation of regular proof trees (i.e. non-tau and non-tick transitions)