Safe Haskell	Safe-Inferred
Language	Haskell2010

Modelling.PetriNet.Reach.Reach

Description

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

Documentation

verifyReach :: (Ord a, Ord t, OutputCapable m, Show a, Show t) => ReachInstance a t -> LangM m Source #

reachTask :: (MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m, Ord s, Ord t, OutputCapable m, Show s, Show t) => FilePath -> ReachInstance s t -> LangM m Source #

reportReachFor :: OutputCapable m => FilePath -> Maybe Int -> Maybe Int -> Int -> Bool -> Maybe (Either FilePath String) -> LangM m Source #

reachInitial :: ReachInstance s Transition -> TransitionsList Source #

reachSyntax :: OutputCapable m => ReachInstance s Transition -> [Transition] -> LangM m Source #

transitionsValid :: OutputCapable m => Net s Transition -> [Transition] -> LangM m Source #

reachEvaluation :: (Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m, OutputCapable m) => FilePath -> ReachInstance Place Transition -> [Transition] -> Rated m Source #

netGoalSolution :: Ord s => NetGoal s t -> [t] Source #

reachSolution :: Ord s => ReachInstance s t -> [t] Source #

assertReachPoints :: OutputCapable m => Maybe String -> (i -> a -> Bool) -> (i -> Int) -> i -> [b] -> Either Int a -> Rated m Source #

isNoLonger :: OutputCapable m => Maybe Int -> [a] -> LangM m Source #

data ReachInstance s t Source #

Constructors

ReachInstance
Fields netGoal :: NetGoal s t minLength :: Int noLongerThan :: Maybe Int showGoalNet :: Bool showPlaceNames :: Bool showSolution :: Bool withLengthHint :: Maybe Int withMinLengthHint :: Bool

Instances

Instances details

(Data s, Data t, Ord s, Ord t) => Data (ReachInstance s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ReachInstance s t -> c (ReachInstance s t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (ReachInstance s t) # toConstr :: ReachInstance s t -> Constr # dataTypeOf :: ReachInstance s t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (ReachInstance s t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (ReachInstance s t)) # gmapT :: (forall b. Data b => b -> b) -> ReachInstance s t -> ReachInstance s t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r # gmapQ :: (forall d. Data d => d -> u) -> ReachInstance s t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ReachInstance s t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ReachInstance s t -> m (ReachInstance s t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ReachInstance s t -> m (ReachInstance s t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ReachInstance s t -> m (ReachInstance s t) #
Generic (ReachInstance s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Associated Types type Rep (ReachInstance s t) :: Type -> Type # Methods from :: ReachInstance s t -> Rep (ReachInstance s t) x # to :: Rep (ReachInstance s t) x -> ReachInstance s t #
(Read s, Read t, Ord s, Ord t) => Read (ReachInstance s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods readsPrec :: Int -> ReadS (ReachInstance s t) # readList :: ReadS [ReachInstance s t] # readPrec :: ReadPrec (ReachInstance s t) # readListPrec :: ReadPrec [ReachInstance s t] #
(Show s, Show t) => Show (ReachInstance s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods showsPrec :: Int -> ReachInstance s t -> ShowS # show :: ReachInstance s t -> String # showList :: [ReachInstance s t] -> ShowS #
type Rep (ReachInstance s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach type Rep (ReachInstance s t) = D1 ('MetaData "ReachInstance" "Modelling.PetriNet.Reach.Reach" "modelling-tasks-0.0.0.1-5lkaY76HE6k79qLVIy6Ku2" 'False) (C1 ('MetaCons "ReachInstance" 'PrefixI 'True) (((S1 ('MetaSel ('Just "netGoal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (NetGoal s t)) :: S1 ('MetaSel ('Just "minLength") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "noLongerThan") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :: S1 ('MetaSel ('Just "showGoalNet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool))) :: ((S1 ('MetaSel ('Just "showPlaceNames") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "showSolution") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "withLengthHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)) :*: S1 ('MetaSel ('Just "withMinLengthHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data NetGoal s t Source #

Constructors

NetGoal
Fields drawUsing :: GraphvizCommand petriNet :: Net s t goal :: State s

Instances

Instances details

(Data s, Data t, Ord s, Ord t) => Data (NetGoal s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> NetGoal s t -> c (NetGoal s t) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (NetGoal s t) # toConstr :: NetGoal s t -> Constr # dataTypeOf :: NetGoal s t -> DataType # dataCast1 :: Typeable t0 => (forall d. Data d => c (t0 d)) -> Maybe (c (NetGoal s t)) # dataCast2 :: Typeable t0 => (forall d e. (Data d, Data e) => c (t0 d e)) -> Maybe (c (NetGoal s t)) # gmapT :: (forall b. Data b => b -> b) -> NetGoal s t -> NetGoal s t # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r # gmapQ :: (forall d. Data d => d -> u) -> NetGoal s t -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> NetGoal s t -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t) #
Generic (NetGoal s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Associated Types type Rep (NetGoal s t) :: Type -> Type # Methods from :: NetGoal s t -> Rep (NetGoal s t) x # to :: Rep (NetGoal s t) x -> NetGoal s t #
(Read s, Read t, Ord s, Ord t) => Read (NetGoal s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods readsPrec :: Int -> ReadS (NetGoal s t) # readList :: ReadS [NetGoal s t] # readPrec :: ReadPrec (NetGoal s t) # readListPrec :: ReadPrec [NetGoal s t] #
(Show s, Show t) => Show (NetGoal s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods showsPrec :: Int -> NetGoal s t -> ShowS # show :: NetGoal s t -> String # showList :: [NetGoal s t] -> ShowS #
type Rep (NetGoal s t) Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach type Rep (NetGoal s t) = D1 ('MetaData "NetGoal" "Modelling.PetriNet.Reach.Reach" "modelling-tasks-0.0.0.1-5lkaY76HE6k79qLVIy6Ku2" 'False) (C1 ('MetaCons "NetGoal" 'PrefixI 'True) (S1 ('MetaSel ('Just "drawUsing") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 GraphvizCommand) :: (S1 ('MetaSel ('Just "petriNet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Net s t)) :: S1 ('MetaSel ('Just "goal") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (State s)))))

bimapReachInstance :: (Ord a, Ord b) => (s -> a) -> (t -> b) -> ReachInstance s t -> ReachInstance a b Source #

bimapNetGoal :: (Ord a, Ord b) => (s -> a) -> (t -> b) -> NetGoal s t -> NetGoal a b Source #

toShowReachInstance :: ReachInstance Place Transition -> ReachInstance ShowPlace ShowTransition Source #

toShowNetGoal :: NetGoal Place Transition -> NetGoal ShowPlace ShowTransition Source #

data ReachConfig Source #

Constructors

ReachConfig
Fields netGoalConfig :: NetGoalConfig printSolution :: Bool rejectLongerThan :: Maybe Int showLengthHint :: Bool showMinLengthHint :: Bool showTargetNet :: Bool showPlaceNamesInNet :: Bool

Instances

Instances details

Generic ReachConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Associated Types type Rep ReachConfig :: Type -> Type # Methods from :: ReachConfig -> Rep ReachConfig x # to :: Rep ReachConfig x -> ReachConfig #
Read ReachConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods readsPrec :: Int -> ReadS ReachConfig # readList :: ReadS [ReachConfig] # readPrec :: ReadPrec ReachConfig # readListPrec :: ReadPrec [ReachConfig] #
Show ReachConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods showsPrec :: Int -> ReachConfig -> ShowS # show :: ReachConfig -> String # showList :: [ReachConfig] -> ShowS #
type Rep ReachConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach type Rep ReachConfig = D1 ('MetaData "ReachConfig" "Modelling.PetriNet.Reach.Reach" "modelling-tasks-0.0.0.1-5lkaY76HE6k79qLVIy6Ku2" 'False) (C1 ('MetaCons "ReachConfig" 'PrefixI 'True) ((S1 ('MetaSel ('Just "netGoalConfig") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NetGoalConfig) :: (S1 ('MetaSel ('Just "printSolution") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "rejectLongerThan") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Int)))) :: ((S1 ('MetaSel ('Just "showLengthHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "showMinLengthHint") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :: (S1 ('MetaSel ('Just "showTargetNet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :: S1 ('MetaSel ('Just "showPlaceNamesInNet") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

data NetGoalConfig Source #

Constructors

NetGoalConfig
Fields numPlaces :: Int numTransitions :: Int capacity :: Capacity Place drawCommands :: [GraphvizCommand] maxTransitionLength :: Int minTransitionLength :: Int postconditionsRange :: (Int, Maybe Int) preconditionsRange :: (Int, Maybe Int)

Instances

Instances details

Generic NetGoalConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Associated Types type Rep NetGoalConfig :: Type -> Type # Methods from :: NetGoalConfig -> Rep NetGoalConfig x # to :: Rep NetGoalConfig x -> NetGoalConfig #
Read NetGoalConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods readsPrec :: Int -> ReadS NetGoalConfig # readList :: ReadS [NetGoalConfig] # readPrec :: ReadPrec NetGoalConfig # readListPrec :: ReadPrec [NetGoalConfig] #
Show NetGoalConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach Methods showsPrec :: Int -> NetGoalConfig -> ShowS # show :: NetGoalConfig -> String # showList :: [NetGoalConfig] -> ShowS #
type Rep NetGoalConfig Source #
Instance details Defined in Modelling.PetriNet.Reach.Reach type Rep NetGoalConfig = D1 ('MetaData "NetGoalConfig" "Modelling.PetriNet.Reach.Reach" "modelling-tasks-0.0.0.1-5lkaY76HE6k79qLVIy6Ku2" 'False) (C1 ('MetaCons "NetGoalConfig" 'PrefixI 'True) (((S1 ('MetaSel ('Just "numPlaces") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "numTransitions") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "capacity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Capacity Place)) :: S1 ('MetaSel ('Just "drawCommands") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [GraphvizCommand]))) :: ((S1 ('MetaSel ('Just "maxTransitionLength") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :: S1 ('MetaSel ('Just "minTransitionLength") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :: (S1 ('MetaSel ('Just "postconditionsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Maybe Int)) :*: S1 ('MetaSel ('Just "preconditionsRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Int, Maybe Int))))))

defaultReachConfig :: ReachConfig Source #

defaultReachInstance :: ReachInstance Place Transition Source #

generateNetGoal :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m) => NetGoalConfig -> Int -> m (NetGoal Place Transition) Source #

checkReachConfig :: ReachConfig -> Maybe String Source #

generateReach :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m) => ReachConfig -> Int -> m (ReachInstance Place Transition) Source #