Safe Haskell	None
Language	Haskell2010

Modelling.PetriNet.Reach.Reach

Contents

Types
Generation
Task creation
Evaluation
Configuration
Utilities

Description

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

Synopsis

data ReachInstance s t = ReachInstance {
- netGoal :: NetGoal s t
- minLength :: Int
- noLongerThan :: Maybe Int
- showGoalNet :: Bool
- showPlaceNames :: Bool
- maxDisplayedSolutions :: Int
- shortestSolutions :: Either (NonEmpty [t]) (NonEmpty [t])
- withLengthHint :: Maybe Int
- withMinLengthHint :: Bool
- rejectSpaceballsLength :: Maybe Int
}
data NetGoal s t = NetGoal {
- drawUsing :: GraphvizCommand
- petriNet :: Net s t
- goal :: State s
}
data ReachConfig = ReachConfig {
- netGoalConfig :: NetGoalConfig
- maxPrintedSolutions :: Int
- rejectLongerThan :: Maybe Int
- showLengthHint :: Bool
- showMinLengthHint :: Bool
- showTargetNet :: Bool
- showPlaceNamesInNet :: Bool
- filterConfig :: FilterConfig
}
data NetGoalConfig = NetGoalConfig {
- numPlaces :: Int
- numTransitions :: Int
- capacity :: Capacity Place
- graphLayouts :: [GraphvizCommand]
- maxTransitionLength :: Int
- minTransitionLength :: Int
- maxPlacesChanged :: Int
- transitionBehaviorConstraints :: TransitionBehaviorConstraints
- arrowDensityConstraints :: ArrowDensityConstraints
}
checkReachConfig :: ReachConfig -> Maybe String
generateReach :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m) => ReachConfig -> Int -> m (ReachInstance Place Transition)
reachTask :: forall (m :: Type -> Type) s t. (MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m, Ord s, Ord t, OutputCapable m, Show s, Show t) => Bool -> FilePath -> ReachInstance s t -> LangM m
verifyReach :: forall a t (m :: Type -> Type). (Ord a, Ord t, OutputCapable m, Show a, Show t) => ReachInstance a t -> LangM m
reachEvaluation :: forall (m :: Type -> Type). (Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m, OutputCapable m) => FilePath -> ReachInstance Place Transition -> [Transition] -> Rated m
reachSyntax :: forall (m :: Type -> Type) s. OutputCapable m => ReachInstance s Transition -> [Transition] -> LangM m
reachInitial :: ReachInstance s Transition -> TransitionsList
defaultReachConfig :: ReachConfig
defaultReachInstance :: ReachInstance Place Transition
bimapReachInstance :: (Ord a, Ord b) => (s -> a) -> (t -> b) -> ReachInstance s t -> ReachInstance a b
bimapNetGoal :: (Ord a, Ord b) => (s -> a) -> (t -> b) -> NetGoal s t -> NetGoal a b
toShowReachInstance :: ReachInstance Place Transition -> ReachInstance ShowPlace ShowTransition
toShowNetGoal :: NetGoal Place Transition -> NetGoal ShowPlace ShowTransition
assertReachPoints :: forall (m :: Type -> Type) i a b. OutputCapable m => Maybe String -> (i -> a -> Bool) -> (i -> Int) -> i -> [b] -> Either Int a -> Rated m
isNoLonger :: forall (m :: Type -> Type) a. OutputCapable m => Maybe Int -> [a] -> LangM m
rejectSpaceballsPattern :: forall t (m :: Type -> Type). (Enum t, Eq t, OutputCapable m, Show t) => Maybe Int -> [t] -> LangM m
reportReachFor :: forall (m :: Type -> Type). OutputCapable m => Bool -> FilePath -> Maybe Int -> Maybe Int -> Int -> Bool -> Maybe (Either FilePath String) -> LangM m
transitionsValid :: forall (m :: Type -> Type) s. OutputCapable m => Net s Transition -> [Transition] -> LangM m
levelsWithAlternatives :: Ord s => Net s t -> [[(State s, [[t]])]]
provideSolutionsFeedback :: Int -> Either (NonEmpty [Transition]) (NonEmpty [Transition]) -> Maybe String
validateDrawabilityAndSolutionFiltering :: forall t (m :: Type -> Type) p. (Enum t, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Ord p, Ord t, Show p, Show t) => Net p t -> [GraphvizCommand] -> [[t]] -> FilterConfig -> Int -> Int -> MaybeT (RandT StdGen m) (GraphvizCommand, Either (NonEmpty [t]) (NonEmpty [t]))

Types

data ReachInstance s t Source #

Constructors

ReachInstance

Fields

netGoal :: NetGoal s t
minLength :: Int
noLongerThan :: Maybe Int
showGoalNet :: Bool
showPlaceNames :: Bool
maxDisplayedSolutions :: Int
shortestSolutions :: Either (NonEmpty [t]) (NonEmpty [t])
Solutions to the reach task. Left contains (some) shortest solutions when no filtering is applied. Right contains all solutions when filtering is applied. Note: Left may not contain all shortest solutions, only up to maxDisplayedSolutions.
withLengthHint :: Maybe Int
withMinLengthHint :: Bool
rejectSpaceballsLength :: Maybe Int
Minimum length of Spaceballs PIN pattern to reject during syntax checking. If set to Just n, sequences starting with n or more consecutive transitions (e.g., [t1, t2, t3, t4]) will be rejected.

Instances

Instances details

(Ord s, Ord t, Reader s, Reader t) => Reader (ReachInstance s t) Source #

Instance details

Defined in Modelling.PetriNet.Reach.Reach

Methods

atomic_reader :: Parser (ReachInstance s t)

atomic_readerPrec :: Int -> Parser (ReachInstance s t)

reader :: Parser (ReachInstance s t)

readerPrec :: Int -> Parser (ReachInstance s t)

readerList :: Parser [ReachInstance s t]

(ToDoc s, ToDoc t) => ToDoc (ReachInstance s t) Source #

Instance details

Defined in Modelling.PetriNet.Reach.Reach

Methods

toDocPrec :: Int -> ReachInstance s t -> Doc

toDocList :: [ReachInstance s t] -> Doc

(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)

Instance details

Defined in Modelling.PetriNet.Reach.Reach

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

data NetGoal s t Source #

Constructors

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

Instances

Instances details

(Ord s, Ord t, Reader s, Reader t) => Reader (NetGoal s t) Source #

Instance details

Defined in Modelling.PetriNet.Reach.Reach

Methods

atomic_reader :: Parser (NetGoal s t)

atomic_readerPrec :: Int -> Parser (NetGoal s t)

reader :: Parser (NetGoal s t)

readerPrec :: Int -> Parser (NetGoal s t)

readerList :: Parser [NetGoal s t]

(ToDoc s, ToDoc t) => ToDoc (NetGoal s t) Source #

Instance details

Defined in Modelling.PetriNet.Reach.Reach

Methods

toDocPrec :: Int -> NetGoal s t -> Doc

toDocList :: [NetGoal s t] -> Doc

(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)

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-2KiclaEArwR4yz1IHg8eKf" '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)))))

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-2KiclaEArwR4yz1IHg8eKf" '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)))))

data ReachConfig Source #

Constructors

ReachConfig
Fields netGoalConfig :: NetGoalConfig maxPrintedSolutions :: Int rejectLongerThan :: Maybe Int showLengthHint :: Bool showMinLengthHint :: Bool showTargetNet :: Bool showPlaceNamesInNet :: Bool filterConfig :: FilterConfig

Instances

Instances details

Generic ReachConfig Source #

Instance details

Defined in Modelling.PetriNet.Reach.Reach

Associated Types

type Rep ReachConfig

Instance details

Defined in Modelling.PetriNet.Reach.Reach

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

data NetGoalConfig Source #

Constructors

NetGoalConfig

Fields

numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
graphLayouts :: [GraphvizCommand]
Graph layout commands to choose from (randomly selected during generation)
maxTransitionLength :: Int
minTransitionLength :: Int
maxPlacesChanged :: Int
Maximum number of places where token counts may differ between start and goal state. Must be in the range 1..numPlaces.
transitionBehaviorConstraints :: TransitionBehaviorConstraints
arrowDensityConstraints :: ArrowDensityConstraints

Instances

Instances details

Generic NetGoalConfig Source #

Instance details

Defined in Modelling.PetriNet.Reach.Reach

Associated Types

type Rep NetGoalConfig

Instance details

Defined in Modelling.PetriNet.Reach.Reach

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

checkReachConfig :: ReachConfig -> Maybe String Source #

Generation

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

Task creation

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

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

Evaluation

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

reachSyntax :: forall (m :: Type -> Type) s. OutputCapable m => ReachInstance s Transition -> [Transition] -> LangM m Source #

reachInitial :: ReachInstance s Transition -> TransitionsList Source #

Configuration

defaultReachConfig :: ReachConfig Source #

defaultReachInstance :: ReachInstance Place Transition Source #

Utilities

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 #

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

isNoLonger :: forall (m :: Type -> Type) a. OutputCapable m => Maybe Int -> [a] -> LangM m Source #

rejectSpaceballsPattern :: forall t (m :: Type -> Type). (Enum t, Eq t, OutputCapable m, Show t) => Maybe Int -> [t] -> LangM m Source #

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

transitionsValid :: forall (m :: Type -> Type) s. OutputCapable m => Net s Transition -> [Transition] -> LangM m Source #

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

Find all shortest paths to all reachable markings segmented by the length of paths starting with 0.

Each returned trace for a state is in reversed order.

provideSolutionsFeedback :: Int -> Either (NonEmpty [Transition]) (NonEmpty [Transition]) -> Maybe String Source #

validateDrawabilityAndSolutionFiltering Source #

Arguments

:: forall t (m :: Type -> Type) p. (Enum t, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Ord p, Ord t, Show p, Show t)
=> Net p t	Petri net to validate for drawability and from which the solutions were derived.
-> [GraphvizCommand]	List of Graphviz commands (drawing backends) to try for rendering the net. A random order is used.
-> [[t]]	All shortest solutions found, represented as sequences of transitions.
-> FilterConfig	Configuration describing how to filter or discard solutions before output.
-> Int	Total number of transitions in the Petri net, used in filtering decisions.
-> Int	Maximum number of solutions meant to be displayed to students.
-> MaybeT (RandT StdGen m) (GraphvizCommand, Either (NonEmpty [t]) (NonEmpty [t]))

Validate drawability and solution filter criteria, then prepare solutions for output