CSPM.FiringRules.Verifier

A checker for the firing rules semantics of CSPM.

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

The Rule data type stores proof trees in a compressed form. These functions are also used to reconstruct an explicit representation of the transition.

Note : In our use-case for this module, it is an assertions that the proof tree generator only constructs valid proof trees, i.e. an invalid proof tree always means a bug in the proof tree generator. We use viewRule to reconstruct the transition and at the same time check that assertion. If one knows for sure that all proof trees are correct, it is possible to use a faster version of viewRule, which reconstructs the transition without checking the side conditions.

Documentation

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

This function reconstructs the transition that is actually proven by the proof tree. It returns 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)

Used for testing.

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

Used for testing.

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

Used for testing.