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.
Rule data type stores proof trees in a compressed form.
These functions are also used to reconstruct an explicit representation of the transition.
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.
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
which reconstructs the transition without checking the side conditions.
- viewRule :: BL i => Rule i -> (Process i, TTE i, Process i)
- viewProcBefore :: BL i => Rule i -> Process i
- viewEvent :: BL i => Rule i -> TTE i
- viewProcAfter :: BL i => Rule i -> Process i
- viewRuleMaybe :: BL i => Rule i -> Maybe (Process i, TTE i, Process i)
- viewRuleTau :: forall i. BL i => RuleTau i -> Maybe (Process i, Process i)
- viewRuleTick :: BL i => RuleTick i -> Maybe (Process i)
- viewRuleEvent :: forall i. BL i => RuleEvent i -> Maybe (Process i, Event i, Process i)
viewRule but just return the predecessor process.
viewRule but just return the successor process.