CSPM-FiringRules- Firing rules semantic of CSPM

Safe HaskellSafe-Inferred



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.



data Rule i Source

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


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


Typeable1 Rule 
(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) 
ExceptionTauL (EventSet i) (RuleTau i) (Process i) 
ExceptionTauR (EventSet i) (Process i) (RuleTau i) 
TraceSwitchOn (Process i) 


data RuleEvent i Source

Representation of regular proof trees.