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.

Synopsis

data Invariant
value weigh
data Breach
value checkInvariant
value bound

Packagevortex-journal-0.1.0
Exports5
LanguageGHC2024
LicenceMIT
SourceInvariant.hs

datadata Invariant tok

Source#

A named weighting of tokens.

Constructors

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

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

Source#

A marking's total weight.

datadata Breach op ans

Source#

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]

Source#

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

Source#

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.