Copyright	(c) Fontaine 2010 - 2011
License	BSD3
Maintainer	fontaine@cs.uni-duesseldorf.de
Stability	experimental
Portability	GHC-only
Safe Haskell	Safe
Language	Haskell2010

CSPM.FiringRules.Rules

Description

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.

Synopsis

Documentation

data Rule i Source #

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) Source #
Methods (==) :: Rule i -> Rule i -> Bool # (/=) :: Rule i -> Rule i -> Bool #
(Show (RuleEvent i), Show (RuleTick i), Show (RuleTau i)) => Show (Rule i) Source #
Methods showsPrec :: Int -> Rule i -> ShowS # show :: Rule i -> String # showList :: [Rule i] -> ShowS #

isTauRule :: Rule i -> Bool Source #

Is this a proof tree for a tau-transition ?

data RuleTau i Source #

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) Source #
Methods (==) :: RuleTau i -> RuleTau i -> Bool # (/=) :: RuleTau i -> RuleTau i -> Bool #
(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) Source #
Methods compare :: RuleTau i -> RuleTau i -> Ordering # (<) :: RuleTau i -> RuleTau i -> Bool # (<=) :: RuleTau i -> RuleTau i -> Bool # (>) :: RuleTau i -> RuleTau i -> Bool # (>=) :: RuleTau i -> RuleTau i -> Bool # max :: RuleTau i -> RuleTau i -> RuleTau i # min :: RuleTau i -> RuleTau i -> RuleTau i #
(Show (RuleEvent i), Show (RuleTick i), Show (Process i), Show (EventSet i), Show (RenamingRelation i)) => Show (RuleTau i) Source #
Methods showsPrec :: Int -> RuleTau i -> ShowS # show :: RuleTau i -> String # showList :: [RuleTau i] -> ShowS #

data RuleTick i Source #

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) Source #
Methods (==) :: RuleTick i -> RuleTick i -> Bool # (/=) :: RuleTick i -> RuleTick i -> Bool #
(Ord (Process i), Ord (EventSet i), Ord (Prefix i), Ord (ExtProcess i), Ord (RenamingRelation i)) => Ord (RuleTick i) Source #
Methods compare :: RuleTick i -> RuleTick i -> Ordering # (<) :: RuleTick i -> RuleTick i -> Bool # (<=) :: RuleTick i -> RuleTick i -> Bool # (>) :: RuleTick i -> RuleTick i -> Bool # (>=) :: RuleTick i -> RuleTick i -> Bool # max :: RuleTick i -> RuleTick i -> RuleTick i # min :: RuleTick i -> RuleTick i -> RuleTick i #
(Show (Process i), Show (EventSet i), Show (Prefix i), Show (ExtProcess i), Show (RenamingRelation i)) => Show (RuleTick i) Source #
Methods showsPrec :: Int -> RuleTick i -> ShowS # show :: RuleTick i -> String # showList :: [RuleTick i] -> ShowS #

data RuleEvent i Source #

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) Source #
Methods (==) :: RuleEvent i -> RuleEvent i -> Bool # (/=) :: RuleEvent i -> RuleEvent i -> Bool #
(Ord (Event i), Ord (Prefix i), Ord (Process i), Ord (ExtProcess i), Ord (EventSet i), Ord (RenamingRelation i)) => Ord (RuleEvent i) Source #
Methods compare :: RuleEvent i -> RuleEvent i -> Ordering # (<) :: RuleEvent i -> RuleEvent i -> Bool # (<=) :: RuleEvent i -> RuleEvent i -> Bool # (>) :: RuleEvent i -> RuleEvent i -> Bool # (>=) :: RuleEvent i -> RuleEvent i -> Bool # max :: RuleEvent i -> RuleEvent i -> RuleEvent i # min :: RuleEvent i -> RuleEvent i -> RuleEvent i #
(Show (Event i), Show (Prefix i), Show (Process i), Show (ExtProcess i), Show (EventSet i), Show (RenamingRelation i)) => Show (RuleEvent i) Source #
Methods showsPrec :: Int -> RuleEvent i -> ShowS # show :: RuleEvent i -> String # showList :: [RuleEvent i] -> ShowS #

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