CSPM.FiringRules.Verifier

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.

Documentation

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

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 i

Like viewRule but just return the predecessor process.

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

Like viewRule but just return the event.

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

Like viewRule but just return the successor process.

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

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

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

Check a tau rule.

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

Check a tick rule.

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

Check a regular rule