Safe Haskell	Safe-Inferred
Language	Haskell2010

Modelling.PetriNet.Reach.Property

Description

originally from Autotool (https:/gitlab.imn.htwk-leipzig.deautotool/all0) based on revision: ad25a990816a162fdd13941ff889653f22d6ea0a based on file: collectionsrcPetri/Property.hs

Synopsis

data Property
- = Default
- | MaxNumPlaces Int
- | MaxNumTransitions Int
- | MaxEdgeMultiplicity Int
- | MaxInitialTokens Int
- | Capacity (Capacity ())
validates :: (Foldable f, Ord a, Ord b, OutputCapable m, Show a, Show b) => f Property -> Net a b -> LangM m
validate :: (Ord a, Ord t, OutputCapable m, Show a, Show t) => Property -> Net a t -> LangM m
guardBound :: (Ord a, OutputCapable m, Show a) => String -> a -> a -> LangM m
satisfiesAtAnyState :: (Ord s, Ord t, Show s, Show t) => (State s -> Bool) -> Net s t -> [t] -> Bool

Documentation

data Property Source #

Constructors

Default
MaxNumPlaces Int
MaxNumTransitions Int
MaxEdgeMultiplicity Int
MaxInitialTokens Int
Capacity (Capacity ())

Instances

Instances details

Generic Property Source #
Instance details Defined in Modelling.PetriNet.Reach.Property Associated Types type Rep Property :: Type -> Type # Methods from :: Property -> Rep Property x # to :: Rep Property x -> Property #
type Rep Property Source #
Instance details Defined in Modelling.PetriNet.Reach.Property type Rep Property = D1 ('MetaData "Property" "Modelling.PetriNet.Reach.Property" "modelling-tasks-0.0.0.1-5lkaY76HE6k79qLVIy6Ku2" 'False) ((C1 ('MetaCons "Default" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MaxNumPlaces" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "MaxNumTransitions" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)))) :+: (C1 ('MetaCons "MaxEdgeMultiplicity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: (C1 ('MetaCons "MaxInitialTokens" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :+: C1 ('MetaCons "Capacity" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Capacity ()))))))

validates :: (Foldable f, Ord a, Ord b, OutputCapable m, Show a, Show b) => f Property -> Net a b -> LangM m Source #

validate :: (Ord a, Ord t, OutputCapable m, Show a, Show t) => Property -> Net a t -> LangM m Source #

guardBound :: (Ord a, OutputCapable m, Show a) => String -> a -> a -> LangM m Source #

satisfiesAtAnyState :: (Ord s, Ord t, Show s, Show t) => (State s -> Bool) -> Net s t -> [t] -> Bool Source #

Checks if the given predicate p is satisfied after (partial) execution of the given sequence.