Modulevortex-journal-0.1.0GHC2024

Vortex.Journal.Invariant

Place invariants: linear weights over tokens that every operation conserves. Checked once per net, over its operations, never per run: if every operation's post weighs what its pre does, every state the net reaches weighs what the initial marking does.

2 types
3 values

Packagevortex-journal-0.1.0
Exports5
LanguageGHC2024
LicenceMIT
SourceInvariant.hs

datadata Invariant tok

A named weighting of tokens.

Constructors

MkInvariant
- invariantName :: Text
- invariantWeight :: tok -> Integer

valueweigh :: Invariant tok -> Marking tok -> Integer

A marking's total weight.

datadata Breach op ans

An operation that does not conserve an invariant, with the weights of what it consumes and what it produces.

Constructors

MkBreach
- breachOp :: Answered op ans
- breachPre :: Integer
- breachPost :: Integer

Instances2Eq, Show

(Eq op, Eq ans) => Eq (Breach op ans)Defined in vortex-journal-0.1.0 · Vortex.Journal.Invariant
(Show op, Show ans) => Show (Breach op ans)Defined in vortex-journal-0.1.0 · Vortex.Journal.Invariant

valuecheckInvariant

:: Net op ans tok
-> [Answered op ans]
-> Invariant tok
-> [Breach op ans]

The operations, of those listed, that do not conserve the invariant (none, when it is one).

valuebound :: Net op ans tok -> Invariant tok -> tok -> Maybe Integer

What a conserved invariant with non-negative weights bounds a token's count by in every reachable state: the initial weight over the token's own weight. Nothing for a token of weight zero, which it does not bound.