Portability	GHC-only
Stability	experimental
Maintainer	fontaine@cs.uni-duesseldorf.de
Safe Haskell	Safe-Infered

CSPM.FiringRules.Verifier

Description

A checker for the firing rules semantics of CSPM.

viewRuleMaybe checks that a proof tree is valid with respect to the firing rules semantics of CSPM. It checks that the proof tree is syntactically valid and that all side conditions hold.

The Rule data type stores proof trees in a compressed form. viewRuleMaybe constructs an explicit representation of the transition.

viewRule calls viewRuleMaybe and throws an exception if the proof tree was not valid. The proof tree generators in this package only generate valid proof trees. viewRule is used to check that assertion.

Synopsis

Documentation

viewRule :: BL i => Rule i -> (Process i, TTE i, Process i)Source

This function constructs an explict representation of the transition from the proof tree of the transition. The transition as a triple (predecessor Process, Event, successor Process). If the proof tree is invalid it throws an exception.

viewProcBefore :: BL i => Rule i -> Process iSource

Like viewRule but just return the predecessor process.

viewEvent :: BL i => Rule i -> TTE iSource

Like viewRule but just return the event.

viewProcAfter :: BL i => Rule i -> Process iSource

Like viewRule but just return the successor process.

viewRuleMaybe :: BL i => Rule i -> Maybe (Process i, TTE i, Process i)Source

Like viewRule but returns Nothing in case of an invalid proof tree.

viewRuleTau :: forall i. BL i => RuleTau i -> Maybe (Process i, Process i)Source

Check a tau rule.

viewRuleTick :: BL i => RuleTick i -> Maybe (Process i)Source

Check a tick rule.

viewRuleEvent :: forall i. BL i => RuleEvent i -> Maybe (Process i, Event i, Process i)Source

Check a regular rule