{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
#if !MIN_VERSION_base(4,18,0)
{-# LANGUAGE DerivingStrategies #-}
#endif
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TupleSections #-}

{-|
originally from Autotool (https://gitlab.imn.htwk-leipzig.de/autotool/all0)
based on revision: ad25a990816a162fdd13941ff889653f22d6ea0a
based on file: collection/src/Petri/Reach.hs
-}
module Modelling.PetriNet.Reach.Reach (
  -- * Types
  ReachInstance(..),
  NetGoal(..),
  ReachConfig(..),
  NetGoalConfig(..),
  checkReachConfig,

  -- * Generation
  generateReach,

  -- * Task creation
  reachTask,
  verifyReach,

  -- * Evaluation
  reachEvaluation,
  reachSyntax,
  reachInitial,

  -- * Configuration
  defaultReachConfig,
  defaultReachInstance,

  -- * Utilities
  bimapReachInstance,
  bimapNetGoal,
  toShowReachInstance,
  toShowNetGoal,
  assertReachPoints,
  isNoLonger,
  rejectSpaceballsPattern,
  reportReachFor,
  transitionsValid,
  levelsWithAlternatives,
  provideSolutionsFeedback,
  validateDrawabilityAndSolutionFiltering,
) where

import qualified Control.Monad.Trans              as Monad (lift)
import qualified Data.Map                         as M (elems, empty, fromDistinctAscList, map, unionWith)
import qualified Data.Set                         as S (fromList, member, toList, union, empty)

import Autolib.Reader                   (Reader)
import Autolib.ToDoc                    (ToDoc)
import Data.List.NonEmpty                 (NonEmpty((:|)), fromList)

import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Data.Data                        (Data)
import Modelling.Auxiliary.Output (
  hoveringInformation,
  )
import Modelling.PetriNet.Reach.Draw    (drawToFile, isPetriDrawable)
import Modelling.PetriNet.Reach.Filter (
  FilterConfig (..),
  shouldDiscardSolutions,
  defaultFilterConfig,
  hasSpaceballsPrefix,
  noFiltering,
  )
import Modelling.PetriNet.Reach.Property (
  Property (Default),
  validate,
  )
import Modelling.PetriNet.Reach.Roll    (netLimitsFiltered, simpleConnectionGenerator)
import Modelling.PetriNet.Reach.Step    (executes, successors)
import Modelling.PetriNet.Reach.Type (
  ArrowDensityConstraints(..),
  Capacity (Unbounded),
  Net (start, transitions),
  Place (..),
  ShowPlace (ShowPlace),
  ShowTransition (ShowTransition),
  State,
  Transition (..),
  TransitionBehaviorConstraints (..),
  TransitionsList (TransitionsList),
  bimapNet,
  example,
  mapState,
  mark,
  noArrowDensityConstraints,
  )

import Control.Applicative              (Alternative, (<|>))
import Control.Functor.Trans            (FunctorTrans (lift))
import Control.Monad                    (guard, msum, replicateM, when, unless, (>=>))
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.Monad.Extra              (findM, whenJust)
import Control.Monad.Trans.Maybe        (MaybeT (MaybeT, runMaybeT))
import Modelling.PetriNet.Reach.ConfigValidation (
  checkBasicPetriConfig,
  checkFilterConfigWith,
  )
import Control.OutputCapable.Blocks (
  ArticleToUse (IndefiniteArticle),
  GenericOutputCapable (assertion, code, image, indent, refuse, paragraph, text),
  LangM,
  MinimumThreshold (MinimumThreshold),
  OutputCapable,
  Rated,
  collapsed,
  english,
  german,
  printSolutionAndAssertWithMinimum,
  translate,
  translations,
  yesNo,
  )
import Control.OutputCapable.Blocks.Generic (
  ($>>),
  ($>>=),
  )
import Control.Monad.Random             (mkStdGen)
import Control.Monad.Trans.Random       (RandT, evalRandT)
import System.Random.Shuffle            (shuffleM)
import System.Random.Internal           (StdGen)
import Data.Bifunctor                   (Bifunctor (second), bimap)
import Data.Either.Combinators          (whenRight)
import Data.Foldable                    (sequenceA_, traverse_)
import Data.GraphViz                    (GraphvizCommand (..))
import Data.List                        (singleton, transpose)
import Data.List.Extra                  (groupSort, nubSort)
import Data.Ratio                       ((%))
import Data.String.Interpolate          (i)
#if !MIN_VERSION_base(4,18,0)
import Data.Typeable                    (Typeable)
#endif
import GHC.Generics                     (Generic)

verifyReach :: (Ord a, Ord t, OutputCapable m, Show a, Show t)
  => ReachInstance a t
  -> LangM m
verifyReach :: forall a t (m :: * -> *).
(Ord a, Ord t, OutputCapable m, Show a, Show t) =>
ReachInstance a t -> LangM m
verifyReach ReachInstance a t
inst = do
  let n :: Net a t
n = NetGoal a t -> Net a t
forall s t. NetGoal s t -> Net s t
petriNet (ReachInstance a t -> NetGoal a t
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance a t
inst)
  Property -> Net a t -> LangM m
forall a t (m :: * -> *).
(Ord a, Ord t, OutputCapable m, Show a, Show t) =>
Property -> Net a t -> LangM m
validate Property
Default Net a t
n
  Property -> Net a t -> LangM m
forall a t (m :: * -> *).
(Ord a, Ord t, OutputCapable m, Show a, Show t) =>
Property -> Net a t -> LangM m
validate Property
Default (Net a t -> LangM m) -> Net a t -> LangM m
forall a b. (a -> b) -> a -> b
$ Net a t
n { start = goal (netGoal inst) }
  Bool -> LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> GenericLangM l m () -> GenericLangM l m ()
assertion (ReachInstance a t -> Bool
forall s t. ReachInstance s t -> Bool
showGoalNet ReachInstance a t
inst Bool -> Bool -> Bool
|| ReachInstance a t -> Bool
forall s t. ReachInstance s t -> Bool
showPlaceNames ReachInstance a t
inst) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
    String -> State (Map Language String) ()
english String
"At least one of goal net or place names must be shown."
    String -> State (Map Language String) ()
german String
"Mindestens eines von Zielnetz oder Plätze-Namen muss angezeigt werden."
  pure ()

reachTask
  :: (
    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
reachTask :: forall (m :: * -> *) s t.
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 Ord s, Ord t, OutputCapable m, Show s, Show t) =>
Bool -> String -> ReachInstance s t -> LangM m
reachTask Bool
showInputHelp String
path ReachInstance s t
inst = do
  if ReachInstance s t -> Bool
forall s t. ReachInstance s t -> Bool
showGoalNet ReachInstance s t
inst
    then String -> Either String String
forall a b. a -> Either a b
Left
    (String -> Either String String)
-> GenericLangM Language m String
-> GenericLangM Language m (Either String String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m String -> GenericLangM Language m String
forall (f :: * -> *) a.
Functor f =>
f a -> GenericLangM Language f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a.
(FunctorTrans t, Functor f) =>
f a -> t f a
lift (Net s t -> m String
drawFileWithSettings (Net s t
n { start = goal (netGoal inst) }))
    else Either String String
-> GenericLangM Language m (Either String String)
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ State s -> String
forall a. Show a => a -> String
show (State s -> String) -> State s -> String
forall a b. (a -> b) -> a -> b
$ NetGoal s t -> State s
forall s t. NetGoal s t -> State s
goal (ReachInstance s t -> NetGoal s t
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance s t
inst))
  GenericLangM Language m (Either String String)
-> (Either String String -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \Either String String
g ->
    m String -> GenericLangM Language m String
forall (f :: * -> *) a.
Functor f =>
f a -> GenericLangM Language f a
forall (t :: (* -> *) -> * -> *) (f :: * -> *) a.
(FunctorTrans t, Functor f) =>
f a -> t f a
lift (Net s t -> m String
drawFileWithSettings Net s t
n)
  GenericLangM Language m String
-> (String -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \String
img -> Bool
-> String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> GenericLangM Language m ()
forall (m :: * -> *).
OutputCapable m =>
Bool
-> String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> LangM m
reportReachFor
    Bool
showInputHelp
    String
img
    (ReachInstance s t -> Maybe Int
forall s t. ReachInstance s t -> Maybe Int
noLongerThan ReachInstance s t
inst)
    (ReachInstance s t -> Maybe Int
forall s t. ReachInstance s t -> Maybe Int
withLengthHint ReachInstance s t
inst)
    (ReachInstance s t -> Int
forall s t. ReachInstance s t -> Int
minLength ReachInstance s t
inst)
    (ReachInstance s t -> Bool
forall s t. ReachInstance s t -> Bool
withMinLengthHint ReachInstance s t
inst)
    (Either String String -> Maybe (Either String String)
forall a. a -> Maybe a
Just Either String String
g)
  where
    n :: Net s t
n = NetGoal s t -> Net s t
forall s t. NetGoal s t -> Net s t
petriNet (ReachInstance s t -> NetGoal s t
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance s t
inst)
    drawFileWithSettings :: Net s t -> m String
drawFileWithSettings = Bool -> String -> GraphvizCommand -> Net s t -> m String
forall s t (m :: * -> *).
(Ord s, Ord t, Show s, Show t, MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m) =>
Bool -> String -> GraphvizCommand -> Net s t -> m String
drawToFile (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ ReachInstance s t -> Bool
forall s t. ReachInstance s t -> Bool
showPlaceNames ReachInstance s t
inst) String
path (NetGoal s t -> GraphvizCommand
forall s t. NetGoal s t -> GraphvizCommand
drawUsing (ReachInstance s t -> NetGoal s t
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance s t
inst))

reportReachFor
  :: OutputCapable m
  => Bool
  -> FilePath
  -> Maybe Int
  -> Maybe Int
  -> Int
  -> Bool
  -> Maybe (Either FilePath String)
  -> LangM m
reportReachFor :: forall (m :: * -> *).
OutputCapable m =>
Bool
-> String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> LangM m
reportReachFor Bool
showInputHelp String
img Maybe Int
noLonger Maybe Int
lengthHint Int
minLength Bool
showMinLengthHint Maybe (Either String String)
maybeGoal = do
  LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
    String -> State (Map Language String) ()
english String
"For the Petri net"
    String -> State (Map Language String) ()
german String
"Gesucht ist für das Petrinetz"
  String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
image String
img
  LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ case Maybe (Either String String)
maybeGoal of
    Maybe (Either String String)
Nothing -> State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
      String -> State (Map Language String) ()
english String
"a transition sequence is sought which leads to a marking without successors (i.e., to a deadlock)."
      String -> State (Map Language String) ()
german String
"eine Transitionsfolge, die zu einer Markierung ohne Nachfolger (also zu einem Deadlock) führt."
    Just Either String String
g -> do
      State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
        String -> State (Map Language String) ()
english String
"a transition sequence is sought which leads to the following marking:"
        String -> State (Map Language String) ()
german String
"eine Transitionsfolge, durch welche die folgende Markierung erreicht wird:"
      LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ (String -> LangM m)
-> (String -> LangM m) -> Either String String -> LangM m
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
image String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text Either String String
g
      pure ()

  Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
showInputHelp (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ do
   LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
      String -> State (Map Language String) ()
english String
"State your answer as a sequence of the following kind:"
      String -> State (Map Language String) ()
german String
"Geben Sie Ihre Lösung als Auflistung der folgenden Art an:"
   let
      (Transition
t1, Transition
t2, Transition
t3) = (Int -> Transition
Transition Int
1, Int -> Transition
Transition Int
2, Int -> Transition
Transition Int
3)
      showT :: Transition -> String
showT = ShowTransition -> String
forall a. Show a => a -> String
show (ShowTransition -> String)
-> (Transition -> ShowTransition) -> Transition -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition -> ShowTransition
ShowTransition
      (String
st1, String
st2, String
st3) = (Transition -> String
showT Transition
t1, Transition -> String
showT Transition
t2, Transition -> String
showT Transition
t3)
   String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
code (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ TransitionsList -> String
forall a. Show a => a -> String
show (TransitionsList -> String) -> TransitionsList -> String
forall a b. (a -> b) -> a -> b
$ [Transition] -> TransitionsList
TransitionsList [Transition
t1, Transition
t2, Transition
t3]
   LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
    String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
      String
"Where giving these three steps means that after firing ",
      String
st1, String
", then ", String
st2, String
", and finally ", String
st3,
      String
" (in exactly this order), the sought marking is reached."
      ]
    String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
      String
"Wobei die Angabe dieser drei Schritte bedeuten soll, dass nach dem Schalten von ",
      String
st1, String
", danach ", String
st2, String
", und schließlich ", String
st3,
      String
" (in genau dieser Reihenfolge), die gesuchte Markierung erreicht wird."
      ]
   pure ()

  LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ case Maybe Int
noLonger of
    Maybe Int
Nothing ->
      State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
        String -> State (Map Language String) ()
english String
"Your answer can be arbitrarily short or long."
        String -> State (Map Language String) ()
german String
"Ihre Lösung kann beliebig kurz oder lang sein."

    Just Int
maxL ->
      let
        isExactMatch :: Bool
isExactMatch = Bool
showMinLengthHint Bool -> Bool -> Bool
&& Int
maxL Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
minLength
        (String
englishConstraint, String
germanConstraint) =
          if Bool
isExactMatch
          then (String
"have exactly", String
"muss genau")
          else (String
"not exceed", String
"darf maximal")
      in State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
        String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          String
"Your answer must ",
          String
englishConstraint, String
" ", Int -> String
forall a. Show a => a -> String
show Int
maxL, String
" steps."]
        String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
          String
"Ihre Lösung ", String
germanConstraint, String
" ", Int -> String
forall a. Show a => a -> String
show Int
maxL,
          String
"Schritte enthalten."]

  let maxStepsHint :: [LangM m]
maxStepsHint = case Maybe Int
lengthHint of
        Just Int
maxSteps | Bool
showMinLengthHint Bool -> Bool -> Bool
&& Int
maxSteps Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
minLength -> LangM m -> [LangM m]
forall a. a -> [a]
singleton (LangM m -> [LangM m]) -> LangM m -> [LangM m]
forall a b. (a -> b) -> a -> b
$ LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
          String -> State (Map Language String) ()
english [i|The shortest solutions have exactly #{maxSteps} steps.|]
          String -> State (Map Language String) ()
german [i|Die kürzesten Lösungen haben genau #{maxSteps} Schritte.|]
        Just Int
maxSteps -> LangM m -> [LangM m]
forall a. a -> [a]
singleton (LangM m -> [LangM m]) -> LangM m -> [LangM m]
forall a b. (a -> b) -> a -> b
$ LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
          String -> State (Map Language String) ()
english [i|There is a solution with not more than #{maxSteps} steps.|]
          String -> State (Map Language String) ()
german [i|Es gibt eine Lösung mit nicht mehr als #{maxSteps} Schritten.|]
        Maybe Int
Nothing -> []
      minStepsHint :: [LangM m]
minStepsHint = if Bool
showMinLengthHint Bool -> Bool -> Bool
&& Maybe Int
lengthHint Maybe Int -> Maybe Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Maybe Int
forall a. a -> Maybe a
Just Int
minLength
        then LangM m -> [LangM m]
forall a. a -> [a]
singleton (LangM m -> [LangM m]) -> LangM m -> [LangM m]
forall a b. (a -> b) -> a -> b
$ LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
          String -> State (Map Language String) ()
english [i|There is no solution with less than #{minLength} steps.|]
          String -> State (Map Language String) ()
german [i|Es gibt keine Lösung mit weniger als #{minLength} Schritten.|]
        else []
      hints :: [LangM m]
hints = [LangM m]
maxStepsHint [LangM m] -> [LangM m] -> [LangM m]
forall a. [a] -> [a] -> [a]
++ [LangM m]
minStepsHint
      titleText :: Map Language String
titleText = if [LangM m] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [LangM m]
hints Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
        then State (Map Language String) () -> Map Language String
forall l a. State (Map l a) () -> Map l a
translations (State (Map Language String) () -> Map Language String)
-> State (Map Language String) () -> Map Language String
forall a b. (a -> b) -> a -> b
$ do
          String -> State (Map Language String) ()
english String
"Hints on solution length"
          String -> State (Map Language String) ()
german String
"Hinweise zur Lösungslänge"
        else State (Map Language String) () -> Map Language String
forall l a. State (Map l a) () -> Map l a
translations (State (Map Language String) () -> Map Language String)
-> State (Map Language String) () -> Map Language String
forall a b. (a -> b) -> a -> b
$ do
          String -> State (Map Language String) ()
english String
"Hint on solution length"
          String -> State (Map Language String) ()
german String
"Hinweis zur Lösungslänge"
  Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([LangM m] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [LangM m]
hints) (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ Bool -> Map Language String -> LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> Map l String -> GenericLangM l m () -> GenericLangM l m ()
collapsed Bool
True Map Language String
titleText (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ [LangM m] -> LangM m
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Applicative f) =>
t (f a) -> f ()
sequenceA_ [LangM m]
hints
  Bool -> LangM m
forall (m :: * -> *). OutputCapable m => Bool -> LangM m
hoveringInformation Bool
True
  pure ()

reachInitial :: ReachInstance s Transition -> TransitionsList
reachInitial :: forall s. ReachInstance s Transition -> TransitionsList
reachInitial = [Transition] -> TransitionsList
TransitionsList ([Transition] -> TransitionsList)
-> (ReachInstance s Transition -> [Transition])
-> ReachInstance s Transition
-> TransitionsList
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Transition] -> [Transition]
forall a. [a] -> [a]
reverse ([Transition] -> [Transition])
-> (ReachInstance s Transition -> [Transition])
-> ReachInstance s Transition
-> [Transition]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Transition -> [Transition]
forall a. Set a -> [a]
S.toList (Set Transition -> [Transition])
-> (ReachInstance s Transition -> Set Transition)
-> ReachInstance s Transition
-> [Transition]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net s Transition -> Set Transition
forall s t. Net s t -> Set t
transitions (Net s Transition -> Set Transition)
-> (ReachInstance s Transition -> Net s Transition)
-> ReachInstance s Transition
-> Set Transition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NetGoal s Transition -> Net s Transition
forall s t. NetGoal s t -> Net s t
petriNet (NetGoal s Transition -> Net s Transition)
-> (ReachInstance s Transition -> NetGoal s Transition)
-> ReachInstance s Transition
-> Net s Transition
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReachInstance s Transition -> NetGoal s Transition
forall s t. ReachInstance s t -> NetGoal s t
netGoal

reachSyntax
  :: OutputCapable m
  => ReachInstance s Transition
  -> [Transition]
  -> LangM m
reachSyntax :: forall (m :: * -> *) s.
OutputCapable m =>
ReachInstance s Transition -> [Transition] -> LangM m
reachSyntax ReachInstance s Transition
inst [Transition]
ts =
  do Net s Transition -> [Transition] -> LangM m
forall (m :: * -> *) s.
OutputCapable m =>
Net s Transition -> [Transition] -> LangM m
transitionsValid (NetGoal s Transition -> Net s Transition
forall s t. NetGoal s t -> Net s t
petriNet (ReachInstance s Transition -> NetGoal s Transition
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance s Transition
inst)) [Transition]
ts
     Maybe Int -> [Transition] -> LangM m
forall (m :: * -> *) a.
OutputCapable m =>
Maybe Int -> [a] -> LangM m
isNoLonger (ReachInstance s Transition -> Maybe Int
forall s t. ReachInstance s t -> Maybe Int
noLongerThan ReachInstance s Transition
inst) [Transition]
ts
     Maybe Int -> [Transition] -> LangM m
forall t (m :: * -> *).
(Enum t, Eq t, OutputCapable m, Show t) =>
Maybe Int -> [t] -> LangM m
rejectSpaceballsPattern (ReachInstance s Transition -> Maybe Int
forall s t. ReachInstance s t -> Maybe Int
rejectSpaceballsLength ReachInstance s Transition
inst) [Transition]
ts
     pure ()

transitionsValid :: OutputCapable m => Net s Transition -> [Transition] -> LangM m
transitionsValid :: forall (m :: * -> *) s.
OutputCapable m =>
Net s Transition -> [Transition] -> LangM m
transitionsValid Net s Transition
n =
  (Transition -> GenericLangM Language m ())
-> [Transition] -> GenericLangM Language m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_ Transition -> GenericLangM Language m ()
forall {m :: * -> *}.
GenericOutputCapable Language m =>
Transition -> GenericLangM Language m ()
assertTransition ([Transition] -> GenericLangM Language m ())
-> ([Transition] -> [Transition])
-> [Transition]
-> GenericLangM Language m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Transition] -> [Transition]
forall a. Ord a => [a] -> [a]
nubSort
  where
    assertTransition :: Transition -> GenericLangM Language m ()
assertTransition Transition
t = Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> GenericLangM l m () -> GenericLangM l m ()
assertion (Transition -> Bool
isValidTransition Transition
t) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
      let t' :: String
t' = ShowTransition -> String
forall a. Show a => a -> String
show (ShowTransition -> String) -> ShowTransition -> String
forall a b. (a -> b) -> a -> b
$ Transition -> ShowTransition
ShowTransition Transition
t
      String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
t' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is a transition of the given Petri net?"
      String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
t' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ist eine Transition des gegebenen Petrinetzes?"
    isValidTransition :: Transition -> Bool
isValidTransition =  (Transition -> Set Transition -> Bool
forall a. Eq a => a -> Set a -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Net s Transition -> Set Transition
forall s t. Net s t -> Set t
transitions Net s Transition
n)

provideSolutionsFeedback
  :: Int
  -> Either (NonEmpty [Transition]) (NonEmpty [Transition])
  -> Maybe String
provideSolutionsFeedback :: Int
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
-> Maybe String
provideSolutionsFeedback Int
maxDisplayedSolutions Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList
  | Int
maxDisplayedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 = Maybe String
forall a. Maybe a
Nothing
  | Bool
otherwise = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ case Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList of
      Left ([Transition]
oneSolution :| []) ->
        TransitionsList -> String
forall a. Show a => a -> String
show ([Transition] -> TransitionsList
TransitionsList [Transition]
oneSolution) String -> String -> String
forall a. [a] -> [a] -> [a]
++
          if Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxDisplayedSolutions
            then String
"\n\n(This is the one shortest solution.)"
            else String
"\n\n(This is a shortest solution, but more may exist.)"
      Left ([Transition]
firstSolution :| [[Transition]]
restSolutions) ->
        let displayedSolutions :: [[Transition]]
displayedSolutions = [Transition]
firstSolution [Transition] -> [[Transition]] -> [[Transition]]
forall a. a -> [a] -> [a]
: [[Transition]]
restSolutions
            solutionsText :: String
solutionsText = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ([Transition] -> String) -> [[Transition]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (TransitionsList -> String
forall a. Show a => a -> String
show (TransitionsList -> String)
-> ([Transition] -> TransitionsList) -> [Transition] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Transition] -> TransitionsList
TransitionsList) [[Transition]]
displayedSolutions
        in String
solutionsText String -> String -> String
forall a. [a] -> [a] -> [a]
++
          if Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [[Transition]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Transition]]
restSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxDisplayedSolutions
            then String
"\n(These are all the shortest solutions.)"
            else String
"\n(These are shortest solutions, but more may exist.)"
      Right ([Transition]
theOnlySolution :| []) ->
        TransitionsList -> String
forall a. Show a => a -> String
show ([Transition] -> TransitionsList
TransitionsList [Transition]
theOnlySolution) String -> String -> String
forall a. [a] -> [a] -> [a]
++
          String
"\n\n(This is the only solution.)"
      Right ([Transition]
firstSolution :| [[Transition]]
restSolutions) ->
        let displayedSolutions :: [[Transition]]
displayedSolutions = [Transition]
firstSolution [Transition] -> [[Transition]] -> [[Transition]]
forall a. a -> [a] -> [a]
: Int -> [[Transition]] -> [[Transition]]
forall a. Int -> [a] -> [a]
take (Int
maxDisplayedSolutions Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [[Transition]]
restSolutions
            solutionsText :: String
solutionsText = [String] -> String
unlines ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ ([Transition] -> String) -> [[Transition]] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (TransitionsList -> String
forall a. Show a => a -> String
show (TransitionsList -> String)
-> ([Transition] -> TransitionsList) -> [Transition] -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Transition] -> TransitionsList
TransitionsList) [[Transition]]
displayedSolutions
        in String
solutionsText String -> String -> String
forall a. [a] -> [a] -> [a]
++
          if [[Transition]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[Transition]]
restSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
maxDisplayedSolutions
            then String
"\n(These are all the solutions.)"
            else String
"\n(These are solutions, but more exist.)"

reachEvaluation
  :: (
    Alternative m,
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    OutputCapable m
    )
  => FilePath
  -> ReachInstance Place Transition
  -> [Transition]
  -> Rated m
reachEvaluation :: forall (m :: * -> *).
(Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m,
 MonadThrow m, OutputCapable m) =>
String -> ReachInstance Place Transition -> [Transition] -> Rated m
reachEvaluation String
path ReachInstance Place Transition
reach [Transition]
ts =
  do GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
       String -> State (Map Language String) ()
english String
"Start marking:"
       String -> State (Map Language String) ()
german String
"Startmarkierung:"
     GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
indent (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ String -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> GenericLangM Language m ())
-> String -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State ShowPlace -> String
forall a. Show a => a -> String
show (Net ShowPlace ShowTransition -> State ShowPlace
forall s t. Net s t -> State s
start Net ShowPlace ShowTransition
n)
     pure ()
  GenericLangM Language m ()
-> GenericLangM Language m Rational
-> GenericLangM Language m Rational
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a -> GenericLangM l m b -> GenericLangM l m b
$>> String
-> GraphvizCommand
-> Net ShowPlace ShowTransition
-> [ShowTransition]
-> LangM' m (Either Int (State ShowPlace))
forall (m :: * -> *) s t.
(Alternative m, MonadCache m, MonadDiagrams m, MonadGraphviz m,
 MonadThrow m, Ord s, Ord t, OutputCapable m, Show s, Show t) =>
String
-> GraphvizCommand
-> Net s t
-> [t]
-> LangM' m (Either Int (State s))
executes String
path (NetGoal ShowPlace ShowTransition -> GraphvizCommand
forall s t. NetGoal s t -> GraphvizCommand
drawUsing (ReachInstance ShowPlace ShowTransition
-> NetGoal ShowPlace ShowTransition
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance ShowPlace ShowTransition
reachInstance)) Net ShowPlace ShowTransition
n ((Transition -> ShowTransition) -> [Transition] -> [ShowTransition]
forall a b. (a -> b) -> [a] -> [b]
map Transition -> ShowTransition
ShowTransition [Transition]
ts)
  LangM' m (Either Int (State ShowPlace))
-> (Either Int (State ShowPlace)
    -> GenericLangM Language m Rational)
-> GenericLangM Language m Rational
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \Either Int (State ShowPlace)
eitherOutcome -> Either Int (State ShowPlace)
-> (State ShowPlace -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (m :: * -> *) a b.
Applicative m =>
Either a b -> (b -> m ()) -> m ()
whenRight Either Int (State ShowPlace)
eitherOutcome (\State ShowPlace
outcome ->
    Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (m :: * -> *). OutputCapable m => Bool -> LangM m -> LangM m
yesNo (State ShowPlace
outcome State ShowPlace -> State ShowPlace -> Bool
forall a. Eq a => a -> a -> Bool
== NetGoal ShowPlace ShowTransition -> State ShowPlace
forall s t. NetGoal s t -> State s
goal (ReachInstance ShowPlace ShowTransition
-> NetGoal ShowPlace ShowTransition
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance ShowPlace ShowTransition
reachInstance)) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> State (Map Language String) ()
english String
"Reached target marking?"
      String -> State (Map Language String) ()
german String
"Zielmarkierung erreicht?"
    )
  GenericLangM Language m ()
-> GenericLangM Language m Rational
-> GenericLangM Language m Rational
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a -> GenericLangM l m b -> GenericLangM l m b
$>> Maybe String
-> (ReachInstance ShowPlace ShowTransition
    -> State ShowPlace -> Bool)
-> (ReachInstance ShowPlace ShowTransition -> Int)
-> ReachInstance ShowPlace ShowTransition
-> [Transition]
-> Either Int (State ShowPlace)
-> GenericLangM Language m Rational
forall (m :: * -> *) i a b.
OutputCapable m =>
Maybe String
-> (i -> a -> Bool)
-> (i -> Int)
-> i
-> [b]
-> Either Int a
-> Rated m
assertReachPoints
    Maybe String
aSolution
    (State ShowPlace -> State ShowPlace -> Bool
forall a. Eq a => a -> a -> Bool
(==) (State ShowPlace -> State ShowPlace -> Bool)
-> (ReachInstance ShowPlace ShowTransition -> State ShowPlace)
-> ReachInstance ShowPlace ShowTransition
-> State ShowPlace
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NetGoal ShowPlace ShowTransition -> State ShowPlace
forall s t. NetGoal s t -> State s
goal (NetGoal ShowPlace ShowTransition -> State ShowPlace)
-> (ReachInstance ShowPlace ShowTransition
    -> NetGoal ShowPlace ShowTransition)
-> ReachInstance ShowPlace ShowTransition
-> State ShowPlace
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ReachInstance ShowPlace ShowTransition
-> NetGoal ShowPlace ShowTransition
forall s t. ReachInstance s t -> NetGoal s t
netGoal)
    ReachInstance ShowPlace ShowTransition -> Int
forall s t. ReachInstance s t -> Int
minLength
    ReachInstance ShowPlace ShowTransition
reachInstance
    [Transition]
ts
    Either Int (State ShowPlace)
eitherOutcome
  where
    reachInstance :: ReachInstance ShowPlace ShowTransition
reachInstance = ReachInstance Place Transition
-> ReachInstance ShowPlace ShowTransition
toShowReachInstance ReachInstance Place Transition
reach
    n :: Net ShowPlace ShowTransition
n = NetGoal ShowPlace ShowTransition -> Net ShowPlace ShowTransition
forall s t. NetGoal s t -> Net s t
petriNet (ReachInstance ShowPlace ShowTransition
-> NetGoal ShowPlace ShowTransition
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance ShowPlace ShowTransition
reachInstance)
    aSolution :: Maybe String
aSolution = Int
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
-> Maybe String
provideSolutionsFeedback (ReachInstance Place Transition -> Int
forall s t. ReachInstance s t -> Int
maxDisplayedSolutions ReachInstance Place Transition
reach) (ReachInstance Place Transition
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
forall s t.
ReachInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
shortestSolutions ReachInstance Place Transition
reach)

{-|
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.
-}
levelsWithAlternatives :: Ord s => Net s t -> [[(State s, [[t]])]]
levelsWithAlternatives :: forall s t. Ord s => Net s t -> [[(State s, [[t]])]]
levelsWithAlternatives Net s t
n =
  let f :: Set (State s) -> [(State s, [[t]])] -> [[(State s, [[t]])]]
f Set (State s)
_    [] = []
      f Set (State s)
done [(State s, [[t]])]
xs =
        let done' :: Set (State s)
done' = Set (State s) -> Set (State s) -> Set (State s)
forall a. Ord a => Set a -> Set a -> Set a
S.union Set (State s)
done (Set (State s) -> Set (State s)) -> Set (State s) -> Set (State s)
forall a b. (a -> b) -> a -> b
$ [State s] -> Set (State s)
forall a. Ord a => [a] -> Set a
S.fromList ([State s] -> Set (State s)) -> [State s] -> Set (State s)
forall a b. (a -> b) -> a -> b
$ ((State s, [[t]]) -> State s) -> [(State s, [[t]])] -> [State s]
forall a b. (a -> b) -> [a] -> [b]
map (State s, [[t]]) -> State s
forall a b. (a, b) -> a
fst [(State s, [[t]])]
xs
            next :: [(State s, [[t]])]
next = ((State s, [[[t]]]) -> (State s, [[t]]))
-> [(State s, [[[t]]])] -> [(State s, [[t]])]
forall a b. (a -> b) -> [a] -> [b]
map (([[[t]]] -> [[t]]) -> (State s, [[[t]]]) -> (State s, [[t]])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second [[[t]]] -> [[t]]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) ([(State s, [[[t]]])] -> [(State s, [[t]])])
-> [(State s, [[[t]]])] -> [(State s, [[t]])]
forall a b. (a -> b) -> a -> b
$ [(State s, [[t]])] -> [(State s, [[[t]]])]
forall k v. Ord k => [(k, v)] -> [(k, [v])]
groupSort [ (State s
y, ([t] -> [t]) -> [[t]] -> [[t]]
forall a b. (a -> b) -> [a] -> [b]
map (t
tt -> [t] -> [t]
forall a. a -> [a] -> [a]
:) [[t]]
ps) |
                (State s
x,[[t]]
ps) <- [(State s, [[t]])]
xs,
                (t
t,State s
y) <- Net s t -> State s -> [(t, State s)]
forall s t. Ord s => Net s t -> State s -> [(t, State s)]
successors Net s t
n State s
x,
                Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ State s -> Set (State s) -> Bool
forall a. Ord a => a -> Set a -> Bool
S.member State s
y Set (State s)
done'
              ]
         in [(State s, [[t]])]
xs [(State s, [[t]])] -> [[(State s, [[t]])]] -> [[(State s, [[t]])]]
forall a. a -> [a] -> [a]
: Set (State s) -> [(State s, [[t]])] -> [[(State s, [[t]])]]
f Set (State s)
done' [(State s, [[t]])]
next
  in Set (State s) -> [(State s, [[t]])] -> [[(State s, [[t]])]]
f Set (State s)
forall a. Set a
S.empty [(Net s t -> State s
forall s t. Net s t -> State s
start Net s t
n, [[]])]

assertReachPoints
  :: OutputCapable m
  => Maybe String
  -> (i -> a -> Bool)
  -> (i -> Int)
  -> i
  -> [b]
  -> Either Int a
  -> Rated m
assertReachPoints :: forall (m :: * -> *) i a b.
OutputCapable m =>
Maybe String
-> (i -> a -> Bool)
-> (i -> Int)
-> i
-> [b]
-> Either Int a
-> Rated m
assertReachPoints Maybe String
aCorrectSolution i -> a -> Bool
p i -> Int
size i
inst [b]
ts Either Int a
eitherOutcome = do
  let points :: Rational
points = (Int -> Rational) -> (a -> Rational) -> Either Int a -> Rational
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
        Int -> Rational
forall {a}. Integral a => a -> Rational
partly
        (\a
x -> if i -> a -> Bool
p i
inst a
x then Rational
1 else Int -> Rational
forall {a}. Integral a => a -> Rational
partly (Int -> Rational) -> Int -> Rational
forall a b. (a -> b) -> a -> b
$ [b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
ts)
        Either Int a
eitherOutcome
  MinimumThreshold
-> Bool -> Maybe (ArticleToUse, String) -> Rational -> Rated m
forall (m :: * -> *).
OutputCapable m =>
MinimumThreshold
-> Bool -> Maybe (ArticleToUse, String) -> Rational -> Rated m
printSolutionAndAssertWithMinimum
    (Rational -> MinimumThreshold
MinimumThreshold (Rational -> MinimumThreshold) -> Rational -> MinimumThreshold
forall a b. (a -> b) -> a -> b
$ Integer
1 Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
3)
    Bool
False
    ((ArticleToUse
IndefiniteArticle,) (String -> (ArticleToUse, String))
-> Maybe String -> Maybe (ArticleToUse, String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
aCorrectSolution)
    Rational
points
  where
    partly :: a -> Rational
partly a
x = a -> Int -> Rational
forall {a} {a}. (Integral a, Integral a) => a -> a -> Rational
partiallyCorrect a
x (Int -> Rational) -> Int -> Rational
forall a b. (a -> b) -> a -> b
$ i -> Int
size i
inst
    partiallyCorrect :: a -> a -> Rational
partiallyCorrect a
x a
y = Rational -> Rational -> Rational
forall a. Ord a => a -> a -> a
min Rational
0.6 (Rational -> Rational) -> Rational -> Rational
forall a b. (a -> b) -> a -> b
$
      if a
y a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0
      then Rational
0
      else a -> Integer
forall a. Integral a => a -> Integer
toInteger a
x Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% a -> Integer
forall a. Integral a => a -> Integer
toInteger a
y

isNoLonger :: OutputCapable m => Maybe Int -> [a] -> LangM m
isNoLonger :: forall (m :: * -> *) a.
OutputCapable m =>
Maybe Int -> [a] -> LangM m
isNoLonger Maybe Int
maybeMaxLength [a]
ts =
  Maybe Int
-> (Int -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (m :: * -> *) a.
Applicative m =>
Maybe a -> (a -> m ()) -> m ()
whenJust Maybe Int
maybeMaxLength ((Int -> GenericLangM Language m ()) -> GenericLangM Language m ())
-> (Int -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ \Int
maxLength ->
    Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> GenericLangM l m () -> GenericLangM l m ()
assertion ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
ts Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
maxLength) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [
        String
"At most",
        Int -> String
forall a. Show a => a -> String
show Int
maxLength,
        String
"steps provided?"
        ]
      String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
unwords [
        String
"Höchstens",
        Int -> String
forall a. Show a => a -> String
show Int
maxLength,
        String
"Schritte angegeben?"
        ]

rejectSpaceballsPattern
  :: (Enum t, Eq t, OutputCapable m, Show t)
  => Maybe Int
  -> [t]
  -> LangM m
rejectSpaceballsPattern :: forall t (m :: * -> *).
(Enum t, Eq t, OutputCapable m, Show t) =>
Maybe Int -> [t] -> LangM m
rejectSpaceballsPattern Maybe Int
maybeRejectSpaceballsLength [t]
ts =
  Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Bool -> (Int -> Bool) -> Maybe Int -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Int -> [t] -> Bool
forall a. (Enum a, Eq a) => Int -> [a] -> Bool
`hasSpaceballsPrefix` [t]
ts) Maybe Int
maybeRejectSpaceballsLength) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
    let longestSpaceballsPrefix :: [t]
longestSpaceballsPrefix = [t] -> [t]
forall a. (Enum a, Eq a) => [a] -> [a]
findLongestSpaceballsPrefix [t]
ts
        prefixString :: String
prefixString = [t] -> String
forall a. Show a => a -> String
show [t]
longestSpaceballsPrefix
    GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
refuse (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
      String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
        String
"The solution (or its prefix) ",
        String
prefixString,
        String
" that you submitted might have made for a good PIN in the Spaceballs movie, but is not correct here."
        ]
      String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [
        String
"Die Lösung (oder ihr Präfix) ",
        String
prefixString,
        String
", die Sie eingereicht haben, wäre vielleicht eine gute PIN im Spaceballs-Film gewesen, ist hier aber nicht korrekt."
        ]

-- | Find the longest Spaceballs-like prefix in a sequence
-- A Spaceballs prefix is one where elements follow the pattern [x, x+1, x+2, ...]
findLongestSpaceballsPrefix :: (Enum a, Eq a) => [a] -> [a]
findLongestSpaceballsPrefix :: forall a. (Enum a, Eq a) => [a] -> [a]
findLongestSpaceballsPrefix [] = []
findLongestSpaceballsPrefix (a
x:[a]
xs) =
  a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: ((a, a) -> a) -> [(a, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> a
forall a b. (a, b) -> b
snd (((a, a) -> Bool) -> [(a, a)] -> [(a, a)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((a -> a -> Bool) -> (a, a) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)) ([a] -> [a] -> [(a, a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [a -> a
forall a. Enum a => a -> a
succ a
x ..] [a]
xs))

data ReachInstance s t = ReachInstance {
  forall s t. ReachInstance s t -> NetGoal s t
netGoal           :: NetGoal s t,
  forall s t. ReachInstance s t -> Int
minLength         :: Int,
  forall s t. ReachInstance s t -> Maybe Int
noLongerThan      :: Maybe Int,
  forall s t. ReachInstance s t -> Bool
showGoalNet       :: Bool,
  forall s t. ReachInstance s t -> Bool
showPlaceNames    :: Bool,
  forall s t. ReachInstance s t -> Int
maxDisplayedSolutions :: Int,
  -- | 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'.
  forall s t.
ReachInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
shortestSolutions :: Either (NonEmpty [t]) (NonEmpty [t]),
  forall s t. ReachInstance s t -> Maybe Int
withLengthHint    :: Maybe Int,
  forall s t. ReachInstance s t -> Bool
withMinLengthHint :: Bool,
  -- | 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.
  forall s t. ReachInstance s t -> Maybe Int
rejectSpaceballsLength :: Maybe Int
  }
  deriving ((forall x. ReachInstance s t -> Rep (ReachInstance s t) x)
-> (forall x. Rep (ReachInstance s t) x -> ReachInstance s t)
-> Generic (ReachInstance s t)
forall x. Rep (ReachInstance s t) x -> ReachInstance s t
forall x. ReachInstance s t -> Rep (ReachInstance s t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s t x. Rep (ReachInstance s t) x -> ReachInstance s t
forall s t x. ReachInstance s t -> Rep (ReachInstance s t) x
$cfrom :: forall s t x. ReachInstance s t -> Rep (ReachInstance s t) x
from :: forall x. ReachInstance s t -> Rep (ReachInstance s t) x
$cto :: forall s t x. Rep (ReachInstance s t) x -> ReachInstance s t
to :: forall x. Rep (ReachInstance s t) x -> ReachInstance s t
Generic, ReadPrec [ReachInstance s t]
ReadPrec (ReachInstance s t)
Int -> ReadS (ReachInstance s t)
ReadS [ReachInstance s t]
(Int -> ReadS (ReachInstance s t))
-> ReadS [ReachInstance s t]
-> ReadPrec (ReachInstance s t)
-> ReadPrec [ReachInstance s t]
-> Read (ReachInstance s t)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec [ReachInstance s t]
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec (ReachInstance s t)
forall s t.
(Read s, Read t, Ord s, Ord t) =>
Int -> ReadS (ReachInstance s t)
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadS [ReachInstance s t]
$creadsPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
Int -> ReadS (ReachInstance s t)
readsPrec :: Int -> ReadS (ReachInstance s t)
$creadList :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadS [ReachInstance s t]
readList :: ReadS [ReachInstance s t]
$creadPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec (ReachInstance s t)
readPrec :: ReadPrec (ReachInstance s t)
$creadListPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec [ReachInstance s t]
readListPrec :: ReadPrec [ReachInstance s t]
Read, Int -> ReachInstance s t -> String -> String
[ReachInstance s t] -> String -> String
ReachInstance s t -> String
(Int -> ReachInstance s t -> String -> String)
-> (ReachInstance s t -> String)
-> ([ReachInstance s t] -> String -> String)
-> Show (ReachInstance s t)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall s t.
(Show s, Show t) =>
Int -> ReachInstance s t -> String -> String
forall s t.
(Show s, Show t) =>
[ReachInstance s t] -> String -> String
forall s t. (Show s, Show t) => ReachInstance s t -> String
$cshowsPrec :: forall s t.
(Show s, Show t) =>
Int -> ReachInstance s t -> String -> String
showsPrec :: Int -> ReachInstance s t -> String -> String
$cshow :: forall s t. (Show s, Show t) => ReachInstance s t -> String
show :: ReachInstance s t -> String
$cshowList :: forall s t.
(Show s, Show t) =>
[ReachInstance s t] -> String -> String
showList :: [ReachInstance s t] -> String -> String
Show, Typeable (ReachInstance s t)
Typeable (ReachInstance s t) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> ReachInstance s t
 -> c (ReachInstance s t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (ReachInstance s t))
-> (ReachInstance s t -> Constr)
-> (ReachInstance s t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (ReachInstance s t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (ReachInstance s t)))
-> ((forall b. Data b => b -> b)
    -> ReachInstance s t -> ReachInstance s t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> ReachInstance s t -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> ReachInstance s t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> ReachInstance s t -> m (ReachInstance s t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ReachInstance s t -> m (ReachInstance s t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> ReachInstance s t -> m (ReachInstance s t))
-> Data (ReachInstance s t)
ReachInstance s t -> Constr
ReachInstance s t -> DataType
(forall b. Data b => b -> b)
-> ReachInstance s t -> ReachInstance s t
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> ReachInstance s t -> u
forall u. (forall d. Data d => d -> u) -> ReachInstance s t -> [u]
forall s t.
(Data s, Data t, Ord s, Ord t) =>
Typeable (ReachInstance s t)
forall s t.
(Data s, Data t, Ord s, Ord t) =>
ReachInstance s t -> Constr
forall s t.
(Data s, Data t, Ord s, Ord t) =>
ReachInstance s t -> DataType
forall s t.
(Data s, Data t, Ord s, Ord t) =>
(forall b. Data b => b -> b)
-> ReachInstance s t -> ReachInstance s t
forall s t u.
(Data s, Data t, Ord s, Ord t) =>
Int -> (forall d. Data d => d -> u) -> ReachInstance s t -> u
forall s t u.
(Data s, Data t, Ord s, Ord t) =>
(forall d. Data d => d -> u) -> ReachInstance s t -> [u]
forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r
forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r
forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, Monad m) =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReachInstance s t)
forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ReachInstance s t
-> c (ReachInstance s t)
forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ReachInstance s t))
forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ReachInstance s t))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReachInstance s t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ReachInstance s t
-> c (ReachInstance s t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ReachInstance s t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ReachInstance s t))
$cgfoldl :: forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ReachInstance s t
-> c (ReachInstance s t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> ReachInstance s t
-> c (ReachInstance s t)
$cgunfold :: forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReachInstance s t)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (ReachInstance s t)
$ctoConstr :: forall s t.
(Data s, Data t, Ord s, Ord t) =>
ReachInstance s t -> Constr
toConstr :: ReachInstance s t -> Constr
$cdataTypeOf :: forall s t.
(Data s, Data t, Ord s, Ord t) =>
ReachInstance s t -> DataType
dataTypeOf :: ReachInstance s t -> DataType
$cdataCast1 :: forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (ReachInstance s t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (ReachInstance s t))
$cdataCast2 :: forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ReachInstance s t))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (ReachInstance s t))
$cgmapT :: forall s t.
(Data s, Data t, Ord s, Ord t) =>
(forall b. Data b => b -> b)
-> ReachInstance s t -> ReachInstance s t
gmapT :: (forall b. Data b => b -> b)
-> ReachInstance s t -> ReachInstance s t
$cgmapQl :: forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> ReachInstance s t -> r
$cgmapQr :: forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(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
$cgmapQ :: forall s t u.
(Data s, Data t, Ord s, Ord t) =>
(forall d. Data d => d -> u) -> ReachInstance s t -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> ReachInstance s t -> [u]
$cgmapQi :: forall s t u.
(Data s, Data t, Ord s, Ord t) =>
Int -> (forall d. Data d => d -> u) -> ReachInstance s t -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> ReachInstance s t -> u
$cgmapM :: forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, Monad m) =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
$cgmapMp :: forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
$cgmapMo :: forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> ReachInstance s t -> m (ReachInstance s t)
Data, Parser [ReachInstance s t]
Parser (ReachInstance s t)
Int -> Parser (ReachInstance s t)
Parser (ReachInstance s t)
-> (Int -> Parser (ReachInstance s t))
-> Parser (ReachInstance s t)
-> (Int -> Parser (ReachInstance s t))
-> Parser [ReachInstance s t]
-> Reader (ReachInstance s t)
forall a.
Parser a
-> (Int -> Parser a)
-> Parser a
-> (Int -> Parser a)
-> Parser [a]
-> Reader a
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser [ReachInstance s t]
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (ReachInstance s t)
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (ReachInstance s t)
$catomic_reader :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (ReachInstance s t)
atomic_reader :: Parser (ReachInstance s t)
$catomic_readerPrec :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (ReachInstance s t)
atomic_readerPrec :: Int -> Parser (ReachInstance s t)
$creader :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (ReachInstance s t)
reader :: Parser (ReachInstance s t)
$creaderPrec :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (ReachInstance s t)
readerPrec :: Int -> Parser (ReachInstance s t)
$creaderList :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser [ReachInstance s t]
readerList :: Parser [ReachInstance s t]
Reader, Int -> ReachInstance s t -> Doc
[ReachInstance s t] -> Doc
(Int -> ReachInstance s t -> Doc)
-> ([ReachInstance s t] -> Doc) -> ToDoc (ReachInstance s t)
forall a. (Int -> a -> Doc) -> ([a] -> Doc) -> ToDoc a
forall s t. (ToDoc s, ToDoc t) => Int -> ReachInstance s t -> Doc
forall s t. (ToDoc s, ToDoc t) => [ReachInstance s t] -> Doc
$ctoDocPrec :: forall s t. (ToDoc s, ToDoc t) => Int -> ReachInstance s t -> Doc
toDocPrec :: Int -> ReachInstance s t -> Doc
$ctoDocList :: forall s t. (ToDoc s, ToDoc t) => [ReachInstance s t] -> Doc
toDocList :: [ReachInstance s t] -> Doc
ToDoc)
#if !MIN_VERSION_base(4,18,0)
  deriving Typeable
#endif

data NetGoal s t = NetGoal {
  forall s t. NetGoal s t -> GraphvizCommand
drawUsing         :: GraphvizCommand,
  forall s t. NetGoal s t -> Net s t
petriNet          :: Net s t,
  forall s t. NetGoal s t -> State s
goal              :: State s
  }
  deriving ((forall x. NetGoal s t -> Rep (NetGoal s t) x)
-> (forall x. Rep (NetGoal s t) x -> NetGoal s t)
-> Generic (NetGoal s t)
forall x. Rep (NetGoal s t) x -> NetGoal s t
forall x. NetGoal s t -> Rep (NetGoal s t) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s t x. Rep (NetGoal s t) x -> NetGoal s t
forall s t x. NetGoal s t -> Rep (NetGoal s t) x
$cfrom :: forall s t x. NetGoal s t -> Rep (NetGoal s t) x
from :: forall x. NetGoal s t -> Rep (NetGoal s t) x
$cto :: forall s t x. Rep (NetGoal s t) x -> NetGoal s t
to :: forall x. Rep (NetGoal s t) x -> NetGoal s t
Generic, ReadPrec [NetGoal s t]
ReadPrec (NetGoal s t)
Int -> ReadS (NetGoal s t)
ReadS [NetGoal s t]
(Int -> ReadS (NetGoal s t))
-> ReadS [NetGoal s t]
-> ReadPrec (NetGoal s t)
-> ReadPrec [NetGoal s t]
-> Read (NetGoal s t)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec [NetGoal s t]
forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec (NetGoal s t)
forall s t.
(Read s, Read t, Ord s, Ord t) =>
Int -> ReadS (NetGoal s t)
forall s t. (Read s, Read t, Ord s, Ord t) => ReadS [NetGoal s t]
$creadsPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
Int -> ReadS (NetGoal s t)
readsPrec :: Int -> ReadS (NetGoal s t)
$creadList :: forall s t. (Read s, Read t, Ord s, Ord t) => ReadS [NetGoal s t]
readList :: ReadS [NetGoal s t]
$creadPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec (NetGoal s t)
readPrec :: ReadPrec (NetGoal s t)
$creadListPrec :: forall s t.
(Read s, Read t, Ord s, Ord t) =>
ReadPrec [NetGoal s t]
readListPrec :: ReadPrec [NetGoal s t]
Read, Int -> NetGoal s t -> String -> String
[NetGoal s t] -> String -> String
NetGoal s t -> String
(Int -> NetGoal s t -> String -> String)
-> (NetGoal s t -> String)
-> ([NetGoal s t] -> String -> String)
-> Show (NetGoal s t)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall s t.
(Show s, Show t) =>
Int -> NetGoal s t -> String -> String
forall s t. (Show s, Show t) => [NetGoal s t] -> String -> String
forall s t. (Show s, Show t) => NetGoal s t -> String
$cshowsPrec :: forall s t.
(Show s, Show t) =>
Int -> NetGoal s t -> String -> String
showsPrec :: Int -> NetGoal s t -> String -> String
$cshow :: forall s t. (Show s, Show t) => NetGoal s t -> String
show :: NetGoal s t -> String
$cshowList :: forall s t. (Show s, Show t) => [NetGoal s t] -> String -> String
showList :: [NetGoal s t] -> String -> String
Show, Typeable (NetGoal s t)
Typeable (NetGoal s t) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> NetGoal s t -> c (NetGoal s t))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (NetGoal s t))
-> (NetGoal s t -> Constr)
-> (NetGoal s t -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (NetGoal s t)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (NetGoal s t)))
-> ((forall b. Data b => b -> b) -> NetGoal s t -> NetGoal s t)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r)
-> (forall u. (forall d. Data d => d -> u) -> NetGoal s t -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> NetGoal s t -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t))
-> Data (NetGoal s t)
NetGoal s t -> Constr
NetGoal s t -> DataType
(forall b. Data b => b -> b) -> NetGoal s t -> NetGoal s t
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> NetGoal s t -> u
forall u. (forall d. Data d => d -> u) -> NetGoal s t -> [u]
forall s t.
(Data s, Data t, Ord s, Ord t) =>
Typeable (NetGoal s t)
forall s t. (Data s, Data t, Ord s, Ord t) => NetGoal s t -> Constr
forall s t.
(Data s, Data t, Ord s, Ord t) =>
NetGoal s t -> DataType
forall s t.
(Data s, Data t, Ord s, Ord t) =>
(forall b. Data b => b -> b) -> NetGoal s t -> NetGoal s t
forall s t u.
(Data s, Data t, Ord s, Ord t) =>
Int -> (forall d. Data d => d -> u) -> NetGoal s t -> u
forall s t u.
(Data s, Data t, Ord s, Ord t) =>
(forall d. Data d => d -> u) -> NetGoal s t -> [u]
forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r
forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r
forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, Monad m) =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NetGoal s t)
forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NetGoal s t -> c (NetGoal s t)
forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (NetGoal s t))
forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NetGoal s t))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NetGoal s t)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NetGoal s t -> c (NetGoal s t)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (NetGoal s t))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NetGoal s t))
$cgfoldl :: forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NetGoal s t -> c (NetGoal s t)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> NetGoal s t -> c (NetGoal s t)
$cgunfold :: forall s t (c :: * -> *).
(Data s, Data t, Ord s, Ord t) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NetGoal s t)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (NetGoal s t)
$ctoConstr :: forall s t. (Data s, Data t, Ord s, Ord t) => NetGoal s t -> Constr
toConstr :: NetGoal s t -> Constr
$cdataTypeOf :: forall s t.
(Data s, Data t, Ord s, Ord t) =>
NetGoal s t -> DataType
dataTypeOf :: NetGoal s t -> DataType
$cdataCast1 :: forall s t (t :: * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (NetGoal s t))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (NetGoal s t))
$cdataCast2 :: forall s t (t :: * -> * -> *) (c :: * -> *).
(Data s, Data t, Ord s, Ord t, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NetGoal s t))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (NetGoal s t))
$cgmapT :: forall s t.
(Data s, Data t, Ord s, Ord t) =>
(forall b. Data b => b -> b) -> NetGoal s t -> NetGoal s t
gmapT :: (forall b. Data b => b -> b) -> NetGoal s t -> NetGoal s t
$cgmapQl :: forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> NetGoal s t -> r
$cgmapQr :: forall s t r r'.
(Data s, Data t, Ord s, Ord t) =>
(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
$cgmapQ :: forall s t u.
(Data s, Data t, Ord s, Ord t) =>
(forall d. Data d => d -> u) -> NetGoal s t -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> NetGoal s t -> [u]
$cgmapQi :: forall s t u.
(Data s, Data t, Ord s, Ord t) =>
Int -> (forall d. Data d => d -> u) -> NetGoal s t -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> NetGoal s t -> u
$cgmapM :: forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, Monad m) =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
$cgmapMp :: forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
$cgmapMo :: forall s t (m :: * -> *).
(Data s, Data t, Ord s, Ord t, MonadPlus m) =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> NetGoal s t -> m (NetGoal s t)
Data, Parser [NetGoal s t]
Parser (NetGoal s t)
Int -> Parser (NetGoal s t)
Parser (NetGoal s t)
-> (Int -> Parser (NetGoal s t))
-> Parser (NetGoal s t)
-> (Int -> Parser (NetGoal s t))
-> Parser [NetGoal s t]
-> Reader (NetGoal s t)
forall a.
Parser a
-> (Int -> Parser a)
-> Parser a
-> (Int -> Parser a)
-> Parser [a]
-> Reader a
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser [NetGoal s t]
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (NetGoal s t)
forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (NetGoal s t)
$catomic_reader :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (NetGoal s t)
atomic_reader :: Parser (NetGoal s t)
$catomic_readerPrec :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (NetGoal s t)
atomic_readerPrec :: Int -> Parser (NetGoal s t)
$creader :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser (NetGoal s t)
reader :: Parser (NetGoal s t)
$creaderPrec :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Int -> Parser (NetGoal s t)
readerPrec :: Int -> Parser (NetGoal s t)
$creaderList :: forall s t.
(Ord s, Ord t, Reader s, Reader t) =>
Parser [NetGoal s t]
readerList :: Parser [NetGoal s t]
Reader, Int -> NetGoal s t -> Doc
[NetGoal s t] -> Doc
(Int -> NetGoal s t -> Doc)
-> ([NetGoal s t] -> Doc) -> ToDoc (NetGoal s t)
forall a. (Int -> a -> Doc) -> ([a] -> Doc) -> ToDoc a
forall s t. (ToDoc s, ToDoc t) => Int -> NetGoal s t -> Doc
forall s t. (ToDoc s, ToDoc t) => [NetGoal s t] -> Doc
$ctoDocPrec :: forall s t. (ToDoc s, ToDoc t) => Int -> NetGoal s t -> Doc
toDocPrec :: Int -> NetGoal s t -> Doc
$ctoDocList :: forall s t. (ToDoc s, ToDoc t) => [NetGoal s t] -> Doc
toDocList :: [NetGoal s t] -> Doc
ToDoc)
#if !MIN_VERSION_base(4,18,0)
  deriving Typeable
#endif

bimapReachInstance
  :: (Ord a, Ord b)
  => (s -> a)
  -> (t -> b)
  -> ReachInstance s t
  -> ReachInstance a b
bimapReachInstance :: forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> ReachInstance s t -> ReachInstance a b
bimapReachInstance s -> a
f t -> b
g ReachInstance {Bool
Int
Maybe Int
Either (NonEmpty [t]) (NonEmpty [t])
NetGoal s t
netGoal :: forall s t. ReachInstance s t -> NetGoal s t
showGoalNet :: forall s t. ReachInstance s t -> Bool
showPlaceNames :: forall s t. ReachInstance s t -> Bool
noLongerThan :: forall s t. ReachInstance s t -> Maybe Int
withLengthHint :: forall s t. ReachInstance s t -> Maybe Int
minLength :: forall s t. ReachInstance s t -> Int
withMinLengthHint :: forall s t. ReachInstance s t -> Bool
rejectSpaceballsLength :: forall s t. ReachInstance s t -> Maybe Int
maxDisplayedSolutions :: forall s t. ReachInstance s t -> Int
shortestSolutions :: forall s t.
ReachInstance s t -> Either (NonEmpty [t]) (NonEmpty [t])
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
..} = ReachInstance {
    netGoal :: NetGoal a b
netGoal           = (s -> a) -> (t -> b) -> NetGoal s t -> NetGoal a b
forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> NetGoal s t -> NetGoal a b
bimapNetGoal s -> a
f t -> b
g NetGoal s t
netGoal,
    minLength :: Int
minLength         = Int
minLength,
    noLongerThan :: Maybe Int
noLongerThan      = Maybe Int
noLongerThan,
    showGoalNet :: Bool
showGoalNet       = Bool
showGoalNet,
    showPlaceNames :: Bool
showPlaceNames    = Bool
showPlaceNames,
    maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
maxDisplayedSolutions,
    shortestSolutions :: Either (NonEmpty [b]) (NonEmpty [b])
shortestSolutions = (NonEmpty [t] -> NonEmpty [b])
-> (NonEmpty [t] -> NonEmpty [b])
-> Either (NonEmpty [t]) (NonEmpty [t])
-> Either (NonEmpty [b]) (NonEmpty [b])
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap (([t] -> [b]) -> NonEmpty [t] -> NonEmpty [b]
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t -> b) -> [t] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map t -> b
g)) (([t] -> [b]) -> NonEmpty [t] -> NonEmpty [b]
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((t -> b) -> [t] -> [b]
forall a b. (a -> b) -> [a] -> [b]
map t -> b
g)) Either (NonEmpty [t]) (NonEmpty [t])
shortestSolutions,
    withLengthHint :: Maybe Int
withLengthHint    = Maybe Int
withLengthHint,
    withMinLengthHint :: Bool
withMinLengthHint = Bool
withMinLengthHint,
    rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = Maybe Int
rejectSpaceballsLength
    }

bimapNetGoal
  :: (Ord a, Ord b)
  => (s -> a)
  -> (t -> b)
  -> NetGoal s t
  -> NetGoal a b
bimapNetGoal :: forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> NetGoal s t -> NetGoal a b
bimapNetGoal s -> a
f t -> b
g NetGoal {GraphvizCommand
Net s t
State s
petriNet :: forall s t. NetGoal s t -> Net s t
goal :: forall s t. NetGoal s t -> State s
drawUsing :: forall s t. NetGoal s t -> GraphvizCommand
drawUsing :: GraphvizCommand
petriNet :: Net s t
goal :: State s
..} = NetGoal {
    drawUsing :: GraphvizCommand
drawUsing = GraphvizCommand
drawUsing,
    goal :: State a
goal      = (s -> a) -> State s -> State a
forall b a. Ord b => (a -> b) -> State a -> State b
mapState s -> a
f State s
goal,
    petriNet :: Net a b
petriNet  = (s -> a) -> (t -> b) -> Net s t -> Net a b
forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> Net s t -> Net a b
bimapNet s -> a
f t -> b
g Net s t
petriNet
    }

toShowReachInstance
  :: ReachInstance Place Transition
  -> ReachInstance ShowPlace ShowTransition
toShowReachInstance :: ReachInstance Place Transition
-> ReachInstance ShowPlace ShowTransition
toShowReachInstance = (Place -> ShowPlace)
-> (Transition -> ShowTransition)
-> ReachInstance Place Transition
-> ReachInstance ShowPlace ShowTransition
forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> ReachInstance s t -> ReachInstance a b
bimapReachInstance Place -> ShowPlace
ShowPlace Transition -> ShowTransition
ShowTransition

toShowNetGoal
  :: NetGoal Place Transition
  -> NetGoal ShowPlace ShowTransition
toShowNetGoal :: NetGoal Place Transition -> NetGoal ShowPlace ShowTransition
toShowNetGoal = (Place -> ShowPlace)
-> (Transition -> ShowTransition)
-> NetGoal Place Transition
-> NetGoal ShowPlace ShowTransition
forall a b s t.
(Ord a, Ord b) =>
(s -> a) -> (t -> b) -> NetGoal s t -> NetGoal a b
bimapNetGoal Place -> ShowPlace
ShowPlace Transition -> ShowTransition
ShowTransition

data ReachConfig = ReachConfig {
  ReachConfig -> NetGoalConfig
netGoalConfig       :: NetGoalConfig,
  ReachConfig -> Int
maxPrintedSolutions :: Int,
  ReachConfig -> Maybe Int
rejectLongerThan    :: Maybe Int,
  ReachConfig -> Bool
showLengthHint      :: Bool,
  ReachConfig -> Bool
showMinLengthHint   :: Bool,
  ReachConfig -> Bool
showTargetNet       :: Bool,
  ReachConfig -> Bool
showPlaceNamesInNet :: Bool,
  ReachConfig -> FilterConfig
filterConfig        :: FilterConfig
  }
  deriving ((forall x. ReachConfig -> Rep ReachConfig x)
-> (forall x. Rep ReachConfig x -> ReachConfig)
-> Generic ReachConfig
forall x. Rep ReachConfig x -> ReachConfig
forall x. ReachConfig -> Rep ReachConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ReachConfig -> Rep ReachConfig x
from :: forall x. ReachConfig -> Rep ReachConfig x
$cto :: forall x. Rep ReachConfig x -> ReachConfig
to :: forall x. Rep ReachConfig x -> ReachConfig
Generic, ReadPrec [ReachConfig]
ReadPrec ReachConfig
Int -> ReadS ReachConfig
ReadS [ReachConfig]
(Int -> ReadS ReachConfig)
-> ReadS [ReachConfig]
-> ReadPrec ReachConfig
-> ReadPrec [ReachConfig]
-> Read ReachConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS ReachConfig
readsPrec :: Int -> ReadS ReachConfig
$creadList :: ReadS [ReachConfig]
readList :: ReadS [ReachConfig]
$creadPrec :: ReadPrec ReachConfig
readPrec :: ReadPrec ReachConfig
$creadListPrec :: ReadPrec [ReachConfig]
readListPrec :: ReadPrec [ReachConfig]
Read, Int -> ReachConfig -> String -> String
[ReachConfig] -> String -> String
ReachConfig -> String
(Int -> ReachConfig -> String -> String)
-> (ReachConfig -> String)
-> ([ReachConfig] -> String -> String)
-> Show ReachConfig
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> ReachConfig -> String -> String
showsPrec :: Int -> ReachConfig -> String -> String
$cshow :: ReachConfig -> String
show :: ReachConfig -> String
$cshowList :: [ReachConfig] -> String -> String
showList :: [ReachConfig] -> String -> String
Show)
#if !MIN_VERSION_base(4,18,0)
  deriving Typeable
#endif

data NetGoalConfig = NetGoalConfig {
  NetGoalConfig -> Int
numPlaces :: Int,
  NetGoalConfig -> Int
numTransitions :: Int,
  NetGoalConfig -> Capacity Place
capacity :: Capacity Place,
  -- | Graph layout commands to choose from (randomly selected during generation)
  NetGoalConfig -> [GraphvizCommand]
graphLayouts :: [GraphvizCommand],
  NetGoalConfig -> Int
maxTransitionLength :: Int,
  NetGoalConfig -> Int
minTransitionLength :: Int,
  -- | Maximum number of places where token counts may differ between start and goal state.
  -- Must be in the range @1..numPlaces@.
  NetGoalConfig -> Int
maxPlacesChanged    :: Int,
  NetGoalConfig -> TransitionBehaviorConstraints
transitionBehaviorConstraints :: TransitionBehaviorConstraints,
  NetGoalConfig -> ArrowDensityConstraints
arrowDensityConstraints :: ArrowDensityConstraints
  }
  deriving ((forall x. NetGoalConfig -> Rep NetGoalConfig x)
-> (forall x. Rep NetGoalConfig x -> NetGoalConfig)
-> Generic NetGoalConfig
forall x. Rep NetGoalConfig x -> NetGoalConfig
forall x. NetGoalConfig -> Rep NetGoalConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. NetGoalConfig -> Rep NetGoalConfig x
from :: forall x. NetGoalConfig -> Rep NetGoalConfig x
$cto :: forall x. Rep NetGoalConfig x -> NetGoalConfig
to :: forall x. Rep NetGoalConfig x -> NetGoalConfig
Generic, ReadPrec [NetGoalConfig]
ReadPrec NetGoalConfig
Int -> ReadS NetGoalConfig
ReadS [NetGoalConfig]
(Int -> ReadS NetGoalConfig)
-> ReadS [NetGoalConfig]
-> ReadPrec NetGoalConfig
-> ReadPrec [NetGoalConfig]
-> Read NetGoalConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS NetGoalConfig
readsPrec :: Int -> ReadS NetGoalConfig
$creadList :: ReadS [NetGoalConfig]
readList :: ReadS [NetGoalConfig]
$creadPrec :: ReadPrec NetGoalConfig
readPrec :: ReadPrec NetGoalConfig
$creadListPrec :: ReadPrec [NetGoalConfig]
readListPrec :: ReadPrec [NetGoalConfig]
Read, Int -> NetGoalConfig -> String -> String
[NetGoalConfig] -> String -> String
NetGoalConfig -> String
(Int -> NetGoalConfig -> String -> String)
-> (NetGoalConfig -> String)
-> ([NetGoalConfig] -> String -> String)
-> Show NetGoalConfig
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> NetGoalConfig -> String -> String
showsPrec :: Int -> NetGoalConfig -> String -> String
$cshow :: NetGoalConfig -> String
show :: NetGoalConfig -> String
$cshowList :: [NetGoalConfig] -> String -> String
showList :: [NetGoalConfig] -> String -> String
Show)
#if !MIN_VERSION_base(4,18,0)
  deriving Typeable
#endif

defaultReachConfig :: ReachConfig
defaultReachConfig :: ReachConfig
defaultReachConfig = ReachConfig {
  netGoalConfig :: NetGoalConfig
netGoalConfig = NetGoalConfig {
    numPlaces :: Int
numPlaces           = Int
6,
    numTransitions :: Int
numTransitions      = Int
6,
    capacity :: Capacity Place
Modelling.PetriNet.Reach.Reach.capacity = Capacity Place
forall s. Capacity s
Unbounded,
    graphLayouts :: [GraphvizCommand]
graphLayouts = [GraphvizCommand
Dot, GraphvizCommand
Neato, GraphvizCommand
TwoPi, GraphvizCommand
Circo, GraphvizCommand
Fdp, GraphvizCommand
Sfdp, GraphvizCommand
Osage, GraphvizCommand
Patchwork],
    maxTransitionLength :: Int
maxTransitionLength = Int
6,
    minTransitionLength :: Int
minTransitionLength = Int
6,
    maxPlacesChanged :: Int
maxPlacesChanged    = Int
3,
    transitionBehaviorConstraints :: TransitionBehaviorConstraints
transitionBehaviorConstraints = TransitionBehaviorConstraints {
      allowedTokenChanges :: Maybe Ordering
allowedTokenChanges = Maybe Ordering
forall a. Maybe a
Nothing,
      areNonPreserving :: Maybe Int
areNonPreserving = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
2
      },
    arrowDensityConstraints :: ArrowDensityConstraints
arrowDensityConstraints = ArrowDensityConstraints
noArrowDensityConstraints {
      incomingArrowsPerTransition = (0, Just 3),
      outgoingArrowsPerTransition = (0, Just 3),
      incomingArrowsPerPlace = (0, Just 2),
      outgoingArrowsPerPlace = (0, Just 2)
      }
    },
  maxPrintedSolutions :: Int
maxPrintedSolutions = Int
1,
  rejectLongerThan :: Maybe Int
rejectLongerThan    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
6,
  showLengthHint :: Bool
showLengthHint      = Bool
False,
  showMinLengthHint :: Bool
showMinLengthHint   = Bool
True,
  showTargetNet :: Bool
showTargetNet       = Bool
True,
  showPlaceNamesInNet :: Bool
showPlaceNamesInNet = Bool
False,
  filterConfig :: FilterConfig
filterConfig        = FilterConfig
defaultFilterConfig { forbiddenCycleLengths = [], requireCycleLengthsAny = [3], transitionCoverageRequirement = 1 % 2 }
  }

defaultReachInstance :: ReachInstance Place Transition
defaultReachInstance :: ReachInstance Place Transition
defaultReachInstance = ReachInstance {
  netGoal :: NetGoal Place Transition
netGoal = NetGoal {
    drawUsing :: GraphvizCommand
drawUsing         = GraphvizCommand
Circo,
    petriNet :: Net Place Transition
petriNet          = (Net Place Transition, State Place) -> Net Place Transition
forall a b. (a, b) -> a
fst (Net Place Transition, State Place)
example,
    goal :: State Place
goal              = (Net Place Transition, State Place) -> State Place
forall a b. (a, b) -> b
snd (Net Place Transition, State Place)
example
    },
  minLength :: Int
minLength         = Int
12,
  noLongerThan :: Maybe Int
noLongerThan      = Maybe Int
forall a. Maybe a
Nothing,
  showGoalNet :: Bool
showGoalNet       = Bool
True,
  showPlaceNames :: Bool
showPlaceNames    = Bool
False,
  maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
0,
  shortestSolutions :: Either (NonEmpty [Transition]) (NonEmpty [Transition])
shortestSolutions = NonEmpty [Transition]
-> Either (NonEmpty [Transition]) (NonEmpty [Transition])
forall a b. a -> Either a b
Left ([] [Transition] -> [[Transition]] -> NonEmpty [Transition]
forall a. a -> [a] -> NonEmpty a
:| []), -- TO DO: add a solution
  withLengthHint :: Maybe Int
withLengthHint    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
12,
  withMinLengthHint :: Bool
withMinLengthHint = Bool
False,
  rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = Maybe Int
forall a. Maybe a
Nothing
}

findNetGoalWithSolutions
  :: forall m. (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => FilterConfig
  -> Int
  -> NetGoalConfig
  -> RandT StdGen m (Maybe (NetGoal Place Transition, Either (NonEmpty [Transition]) (NonEmpty [Transition])))
findNetGoalWithSolutions :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
FilterConfig
-> Int
-> NetGoalConfig
-> RandT
     StdGen
     m
     (Maybe
        (NetGoal Place Transition,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
findNetGoalWithSolutions FilterConfig
filterConfig Int
maxPrintedSolutions NetGoalConfig {Int
[GraphvizCommand]
ArrowDensityConstraints
TransitionBehaviorConstraints
Capacity Place
numPlaces :: NetGoalConfig -> Int
numTransitions :: NetGoalConfig -> Int
capacity :: NetGoalConfig -> Capacity Place
graphLayouts :: NetGoalConfig -> [GraphvizCommand]
maxTransitionLength :: NetGoalConfig -> Int
minTransitionLength :: NetGoalConfig -> Int
maxPlacesChanged :: NetGoalConfig -> Int
transitionBehaviorConstraints :: NetGoalConfig -> TransitionBehaviorConstraints
arrowDensityConstraints :: NetGoalConfig -> ArrowDensityConstraints
numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
graphLayouts :: [GraphvizCommand]
maxTransitionLength :: Int
minTransitionLength :: Int
maxPlacesChanged :: Int
transitionBehaviorConstraints :: TransitionBehaviorConstraints
arrowDensityConstraints :: ArrowDensityConstraints
..} =
  let ps :: [Place]
ps = [Int -> Place
Place Int
1 .. Int -> Place
Place Int
numPlaces]
      try :: RandT StdGen m [[(Int, MaybeT (RandT StdGen m) (NetGoal Place Transition, Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
      try :: RandT
  StdGen
  m
  [[(Int,
     MaybeT
       (RandT StdGen m)
       (NetGoal Place Transition,
        Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
try = do
        let generateNet :: RandT StdGen m (Net Place Transition)
generateNet =
              RandT StdGen m (Net Place Transition)
-> (Net Place Transition -> RandT StdGen m (Net Place Transition))
-> Maybe (Net Place Transition)
-> RandT StdGen m (Net Place Transition)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RandT StdGen m (Net Place Transition)
generateNet Net Place Transition -> RandT StdGen m (Net Place Transition)
forall a. a -> RandT StdGen m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Net Place Transition)
 -> RandT StdGen m (Net Place Transition))
-> RandT StdGen m (Maybe (Net Place Transition))
-> RandT StdGen m (Net Place Transition)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (RandT StdGen m [Place]
 -> RandT StdGen m [Place]
 -> Transition
 -> RandT StdGen m (Connection Place Transition))
-> ArrowDensityConstraints
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> TransitionBehaviorConstraints
-> RandT StdGen m (Maybe (Net Place Transition))
forall (m :: * -> *) s t.
(MonadRandom m, Ord s, Ord t) =>
(m [s] -> m [s] -> t -> m (Connection s t))
-> ArrowDensityConstraints
-> Int
-> [s]
-> [t]
-> Capacity s
-> TransitionBehaviorConstraints
-> m (Maybe (Net s t))
netLimitsFiltered RandT StdGen m [Place]
-> RandT StdGen m [Place]
-> Transition
-> RandT StdGen m (Connection Place Transition)
forall (m :: * -> *) s t.
Monad m =>
m [s] -> m [s] -> t -> m (Connection s t)
simpleConnectionGenerator
                ArrowDensityConstraints
arrowDensityConstraints
                Int
numPlaces
                [Place]
ps
                [Transition]
ts
                Capacity Place
capacity
                TransitionBehaviorConstraints
transitionBehaviorConstraints
        Net Place Transition
n <- RandT StdGen m (Net Place Transition)
generateNet
        return $ do
         [(State Place, [[Transition]])]
zs <-
            Int
-> [[(State Place, [[Transition]])]]
-> [[(State Place, [[Transition]])]]
forall a. Int -> [a] -> [a]
take (Int
maxTransitionLength Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
minTransitionLength Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
            ([[(State Place, [[Transition]])]]
 -> [[(State Place, [[Transition]])]])
-> [[(State Place, [[Transition]])]]
-> [[(State Place, [[Transition]])]]
forall a b. (a -> b) -> a -> b
$ Int
-> [[(State Place, [[Transition]])]]
-> [[(State Place, [[Transition]])]]
forall a. Int -> [a] -> [a]
drop Int
minTransitionLength
            ([[(State Place, [[Transition]])]]
 -> [[(State Place, [[Transition]])]])
-> [[(State Place, [[Transition]])]]
-> [[(State Place, [[Transition]])]]
forall a b. (a -> b) -> a -> b
$ Net Place Transition -> [[(State Place, [[Transition]])]]
forall s t. Ord s => Net s t -> [[(State s, [[t]])]]
levelsWithAlternatives Net Place Transition
n
         return $ do
          (State Place
z', [[Transition]]
transitionSequences) <- [(State Place, [[Transition]])]
zs
          let d :: Int
d = [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int]
placeDifferences
              placeDifferences :: [Int]
placeDifferences = do
                Place
p <- [Place]
ps
                let diff :: Int
diff = State Place -> Place -> Int
forall s. Ord s => State s -> s -> Int
mark (Net Place Transition -> State Place
forall s t. Net s t -> State s
start Net Place Transition
n) Place
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- State Place -> Place -> Int
forall s. Ord s => State s -> s -> Int
mark State Place
z' Place
p
                Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
diff Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
0)
                return (Int -> Int
forall a. Num a => a -> a
abs Int
diff)
              allShortestSolutions :: [[Transition]]
allShortestSolutions = ([Transition] -> [Transition]) -> [[Transition]] -> [[Transition]]
forall a b. (a -> b) -> [a] -> [b]
map [Transition] -> [Transition]
forall a. [a] -> [a]
reverse [[Transition]]
transitionSequences
          Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Int
maxPlacesChanged Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
numPlaces Bool -> Bool -> Bool
|| Int
maxPlacesChanged Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [Int] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Int]
placeDifferences)
          return (Int
d, do
            (GraphvizCommand
cmd, Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList) <- Net Place Transition
-> [GraphvizCommand]
-> [[Transition]]
-> FilterConfig
-> Int
-> Int
-> MaybeT
     (RandT StdGen m)
     (GraphvizCommand,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall t (m :: * -> *) 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]))
validateDrawabilityAndSolutionFiltering
              Net Place Transition
n [GraphvizCommand]
graphLayouts [[Transition]]
allShortestSolutions FilterConfig
filterConfig Int
numTransitions Int
maxPrintedSolutions
            let netGoal :: NetGoal Place Transition
netGoal = NetGoal {
                  drawUsing :: GraphvizCommand
drawUsing   = GraphvizCommand
cmd,
                  goal :: State Place
goal        = State Place
z',
                  petriNet :: Net Place Transition
petriNet    = Net Place Transition
n
                }
            (NetGoal Place Transition,
 Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> MaybeT
     (RandT StdGen m)
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall a. a -> MaybeT (RandT StdGen m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NetGoal Place Transition
netGoal, Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList))
  in do
        [[[(Int,
    MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
groupedByLevel <- [[[(Int,
    MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
-> [[[(Int,
       MaybeT
         (RandT StdGen m)
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
forall a. [a] -> [a]
reverse ([[[(Int,
     MaybeT
       (RandT StdGen m)
       (NetGoal Place Transition,
        Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
 -> [[[(Int,
        MaybeT
          (RandT StdGen m)
          (NetGoal Place Transition,
           Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]])
-> ([[[(Int,
        MaybeT
          (RandT StdGen m)
          (NetGoal Place Transition,
           Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
    -> [[[(Int,
           MaybeT
             (RandT StdGen m)
             (NetGoal Place Transition,
              Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]])
-> [[[(Int,
       MaybeT
         (RandT StdGen m)
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
-> [[[(Int,
       MaybeT
         (RandT StdGen m)
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[[(Int,
    MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
-> [[[(Int,
       MaybeT
         (RandT StdGen m)
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
forall a. [[a]] -> [[a]]
transpose ([[[(Int,
     MaybeT
       (RandT StdGen m)
       (NetGoal Place Transition,
        Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
 -> [[[(Int,
        MaybeT
          (RandT StdGen m)
          (NetGoal Place Transition,
           Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]])
-> RandT
     StdGen
     m
     [[[(Int,
         MaybeT
           (RandT StdGen m)
           (NetGoal Place Transition,
            Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
-> RandT
     StdGen
     m
     [[[(Int,
         MaybeT
           (RandT StdGen m)
           (NetGoal Place Transition,
            Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> RandT
     StdGen
     m
     [[(Int,
        MaybeT
          (RandT StdGen m)
          (NetGoal Place Transition,
           Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
-> RandT
     StdGen
     m
     [[[(Int,
         MaybeT
           (RandT StdGen m)
           (NetGoal Place Transition,
            Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
forall (m :: * -> *) a. Applicative m => Int -> m a -> m [a]
replicateM Int
1000 RandT
  StdGen
  m
  [[(Int,
     MaybeT
       (RandT StdGen m)
       (NetGoal Place Transition,
        Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
try
        let choosePerDistance :: [[(Int, MaybeT (RandT StdGen m) a)]] -> [MaybeT (RandT StdGen m) a]
            choosePerDistance :: forall a.
[[(Int, MaybeT (RandT StdGen m) a)]] -> [MaybeT (RandT StdGen m) a]
choosePerDistance = Map Int (MaybeT (RandT StdGen m) a) -> [MaybeT (RandT StdGen m) a]
forall k a. Map k a -> [a]
M.elems (Map Int (MaybeT (RandT StdGen m) a)
 -> [MaybeT (RandT StdGen m) a])
-> ([[(Int, MaybeT (RandT StdGen m) a)]]
    -> Map Int (MaybeT (RandT StdGen m) a))
-> [[(Int, MaybeT (RandT StdGen m) a)]]
-> [MaybeT (RandT StdGen m) a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(Int, MaybeT (RandT StdGen m) a)]
 -> Map Int (MaybeT (RandT StdGen m) a)
 -> Map Int (MaybeT (RandT StdGen m) a))
-> Map Int (MaybeT (RandT StdGen m) a)
-> [[(Int, MaybeT (RandT StdGen m) a)]]
-> Map Int (MaybeT (RandT StdGen m) a)
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((MaybeT (RandT StdGen m) a
 -> MaybeT (RandT StdGen m) a -> MaybeT (RandT StdGen m) a)
-> Map Int (MaybeT (RandT StdGen m) a)
-> Map Int (MaybeT (RandT StdGen m) a)
-> Map Int (MaybeT (RandT StdGen m) a)
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith MaybeT (RandT StdGen m) a
-> MaybeT (RandT StdGen m) a -> MaybeT (RandT StdGen m) a
forall a.
MaybeT (RandT StdGen m) a
-> MaybeT (RandT StdGen m) a -> MaybeT (RandT StdGen m) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Map Int (MaybeT (RandT StdGen m) a)
 -> Map Int (MaybeT (RandT StdGen m) a)
 -> Map Int (MaybeT (RandT StdGen m) a))
-> ([(Int, MaybeT (RandT StdGen m) a)]
    -> Map Int (MaybeT (RandT StdGen m) a))
-> [(Int, MaybeT (RandT StdGen m) a)]
-> Map Int (MaybeT (RandT StdGen m) a)
-> Map Int (MaybeT (RandT StdGen m) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([MaybeT (RandT StdGen m) a] -> MaybeT (RandT StdGen m) a)
-> Map Int [MaybeT (RandT StdGen m) a]
-> Map Int (MaybeT (RandT StdGen m) a)
forall a b k. (a -> b) -> Map k a -> Map k b
M.map ([MaybeT (RandT StdGen m) a]
-> MaybeT (RandT StdGen m) [MaybeT (RandT StdGen m) a]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM ([MaybeT (RandT StdGen m) a]
 -> MaybeT (RandT StdGen m) [MaybeT (RandT StdGen m) a])
-> ([MaybeT (RandT StdGen m) a] -> MaybeT (RandT StdGen m) a)
-> [MaybeT (RandT StdGen m) a]
-> MaybeT (RandT StdGen m) a
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> [MaybeT (RandT StdGen m) a] -> MaybeT (RandT StdGen m) a
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum) (Map Int [MaybeT (RandT StdGen m) a]
 -> Map Int (MaybeT (RandT StdGen m) a))
-> ([(Int, MaybeT (RandT StdGen m) a)]
    -> Map Int [MaybeT (RandT StdGen m) a])
-> [(Int, MaybeT (RandT StdGen m) a)]
-> Map Int (MaybeT (RandT StdGen m) a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, [MaybeT (RandT StdGen m) a])]
-> Map Int [MaybeT (RandT StdGen m) a]
forall k a. [(k, a)] -> Map k a
M.fromDistinctAscList ([(Int, [MaybeT (RandT StdGen m) a])]
 -> Map Int [MaybeT (RandT StdGen m) a])
-> ([(Int, MaybeT (RandT StdGen m) a)]
    -> [(Int, [MaybeT (RandT StdGen m) a])])
-> [(Int, MaybeT (RandT StdGen m) a)]
-> Map Int [MaybeT (RandT StdGen m) a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Int, MaybeT (RandT StdGen m) a)]
-> [(Int, [MaybeT (RandT StdGen m) a])]
forall k v. Ord k => [(k, v)] -> [(k, [v])]
groupSort) Map Int (MaybeT (RandT StdGen m) a)
forall k a. Map k a
M.empty
        MaybeT
  (RandT StdGen m)
  (NetGoal Place Transition,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     StdGen
     m
     (Maybe
        (NetGoal Place Transition,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT ([MaybeT
   (RandT StdGen m)
   (NetGoal Place Transition,
    Either (NonEmpty [Transition]) (NonEmpty [Transition]))]
-> MaybeT
     (RandT StdGen m)
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum (([[(Int,
    MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
 -> MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> [[[(Int,
       MaybeT
         (RandT StdGen m)
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
-> [MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition]))]
forall a b. (a -> b) -> [a] -> [b]
map ([MaybeT
   (RandT StdGen m)
   (NetGoal Place Transition,
    Either (NonEmpty [Transition]) (NonEmpty [Transition]))]
-> MaybeT
     (RandT StdGen m)
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, MonadPlus m) =>
t (m a) -> m a
msum ([MaybeT
    (RandT StdGen m)
    (NetGoal Place Transition,
     Either (NonEmpty [Transition]) (NonEmpty [Transition]))]
 -> MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> ([[(Int,
       MaybeT
         (RandT StdGen m)
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
    -> [MaybeT
          (RandT StdGen m)
          (NetGoal Place Transition,
           Either (NonEmpty [Transition]) (NonEmpty [Transition]))])
-> [[(Int,
      MaybeT
        (RandT StdGen m)
        (NetGoal Place Transition,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
-> MaybeT
     (RandT StdGen m)
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[(Int,
   MaybeT
     (RandT StdGen m)
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]
-> [MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition]))]
choosePerDistance) [[[(Int,
    MaybeT
      (RandT StdGen m)
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))]]]
groupedByLevel))
  where
    ts :: [Transition]
ts = [Int -> Transition
Transition Int
1 .. Int -> Transition
Transition Int
numTransitions]

-- | Validate drawability and solution filter criteria, then prepare solutions for output
validateDrawabilityAndSolutionFiltering
  :: (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]))
validateDrawabilityAndSolutionFiltering :: forall t (m :: * -> *) 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]))
validateDrawabilityAndSolutionFiltering Net p t
petri [GraphvizCommand]
drawCommands [[t]]
allShortestSolutions FilterConfig
filterConfig Int
numTransitions Int
maxPrintedSolutions = do
  Bool -> MaybeT (RandT StdGen m) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ FilterConfig -> Int -> [[t]] -> Bool
forall a. (Enum a, Ord a) => FilterConfig -> Int -> [[a]] -> Bool
shouldDiscardSolutions FilterConfig
filterConfig Int
numTransitions [[t]]
allShortestSolutions)
  [GraphvizCommand]
shuffledCommands <- [GraphvizCommand] -> MaybeT (RandT StdGen m) [GraphvizCommand]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [GraphvizCommand]
drawCommands
  GraphvizCommand
cmd <- RandT StdGen m (Maybe GraphvizCommand)
-> MaybeT (RandT StdGen m) GraphvizCommand
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (RandT StdGen m (Maybe GraphvizCommand)
 -> MaybeT (RandT StdGen m) GraphvizCommand)
-> RandT StdGen m (Maybe GraphvizCommand)
-> MaybeT (RandT StdGen m) GraphvizCommand
forall a b. (a -> b) -> a -> b
$ (GraphvizCommand -> RandT StdGen m Bool)
-> [GraphvizCommand] -> RandT StdGen m (Maybe GraphvizCommand)
forall (m :: * -> *) a.
Monad m =>
(a -> m Bool) -> [a] -> m (Maybe a)
findM (m Bool -> RandT StdGen m Bool
forall (m :: * -> *) a. Monad m => m a -> RandT StdGen m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
Monad.lift (m Bool -> RandT StdGen m Bool)
-> (GraphvizCommand -> m Bool)
-> GraphvizCommand
-> RandT StdGen m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Net p t -> GraphvizCommand -> m Bool
forall (m :: * -> *) s t.
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, Ord s, Ord t,
 Show s, Show t) =>
Net s t -> GraphvizCommand -> m Bool
isPetriDrawable Net p t
petri) [GraphvizCommand]
shuffledCommands
  Either (NonEmpty [t]) (NonEmpty [t])
solutionsList <-
    if FilterConfig
filterConfig FilterConfig -> FilterConfig -> Bool
forall a. Eq a => a -> a -> Bool
== FilterConfig
noFiltering
      then Either (NonEmpty [t]) (NonEmpty [t])
-> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t]))
forall a. a -> MaybeT (RandT StdGen m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (NonEmpty [t]) (NonEmpty [t])
 -> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t])))
-> Either (NonEmpty [t]) (NonEmpty [t])
-> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t]))
forall a b. (a -> b) -> a -> b
$ NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t])
forall a b. a -> Either a b
Left (NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t]))
-> NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t])
forall a b. (a -> b) -> a -> b
$ [[t]] -> NonEmpty [t]
forall a. HasCallStack => [a] -> NonEmpty a
fromList (Int -> [[t]] -> [[t]]
forall a. Int -> [a] -> [a]
take (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
1 Int
maxPrintedSolutions) [[t]]
allShortestSolutions)
      else if Int
maxPrintedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= [[t]] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[t]]
allShortestSolutions
        then Either (NonEmpty [t]) (NonEmpty [t])
-> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t]))
forall a. a -> MaybeT (RandT StdGen m) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either (NonEmpty [t]) (NonEmpty [t])
 -> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t])))
-> Either (NonEmpty [t]) (NonEmpty [t])
-> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t]))
forall a b. (a -> b) -> a -> b
$ NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t])
forall a b. b -> Either a b
Right (NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t]))
-> NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t])
forall a b. (a -> b) -> a -> b
$ [[t]] -> NonEmpty [t]
forall a. HasCallStack => [a] -> NonEmpty a
fromList [[t]]
allShortestSolutions
        else NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t])
forall a b. b -> Either a b
Right (NonEmpty [t] -> Either (NonEmpty [t]) (NonEmpty [t]))
-> ([[t]] -> NonEmpty [t])
-> [[t]]
-> Either (NonEmpty [t]) (NonEmpty [t])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[t]] -> NonEmpty [t]
forall a. HasCallStack => [a] -> NonEmpty a
fromList ([[t]] -> Either (NonEmpty [t]) (NonEmpty [t]))
-> MaybeT (RandT StdGen m) [[t]]
-> MaybeT (RandT StdGen m) (Either (NonEmpty [t]) (NonEmpty [t]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [[t]] -> MaybeT (RandT StdGen m) [[t]]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [[t]]
allShortestSolutions
  pure (GraphvizCommand
cmd, Either (NonEmpty [t]) (NonEmpty [t])
solutionsList)

-- | Generate NetGoal with filtering for trivial solutions
generateNetGoal
  :: forall m. (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => FilterConfig
  -> Int
  -> NetGoalConfig
  -> Int
  -> m (NetGoal Place Transition, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
generateNetGoal :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
FilterConfig
-> Int
-> NetGoalConfig
-> Int
-> m (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
generateNetGoal FilterConfig
filterConfig Int
maxPrintedSolutions NetGoalConfig
netGoalConfig Int
seed =
  RandT
  StdGen
  m
  (NetGoal Place Transition,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> StdGen
-> m (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *) g a. Monad m => RandT g m a -> g -> m a
evalRandT RandT
  StdGen
  m
  (NetGoal Place Transition,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
generate (StdGen
 -> m (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> StdGen
-> m (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall a b. (a -> b) -> a -> b
$ Int -> StdGen
mkStdGen Int
seed
  where
    generate
      :: RandT StdGen m (NetGoal Place Transition, Either (NonEmpty [Transition]) (NonEmpty [Transition]))
    generate :: RandT
  StdGen
  m
  (NetGoal Place Transition,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
generate =
      RandT
  StdGen
  m
  (NetGoal Place Transition,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> ((NetGoal Place Transition,
     Either (NonEmpty [Transition]) (NonEmpty [Transition]))
    -> RandT
         StdGen
         m
         (NetGoal Place Transition,
          Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> Maybe
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     StdGen
     m
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RandT
  StdGen
  m
  (NetGoal Place Transition,
   Either (NonEmpty [Transition]) (NonEmpty [Transition]))
generate (NetGoal Place Transition,
 Either (NonEmpty [Transition]) (NonEmpty [Transition]))
-> RandT
     StdGen
     m
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall a. a -> RandT StdGen m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe
   (NetGoal Place Transition,
    Either (NonEmpty [Transition]) (NonEmpty [Transition]))
 -> RandT
      StdGen
      m
      (NetGoal Place Transition,
       Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> RandT
     StdGen
     m
     (Maybe
        (NetGoal Place Transition,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
-> RandT
     StdGen
     m
     (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< FilterConfig
-> Int
-> NetGoalConfig
-> RandT
     StdGen
     m
     (Maybe
        (NetGoal Place Transition,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
FilterConfig
-> Int
-> NetGoalConfig
-> RandT
     StdGen
     m
     (Maybe
        (NetGoal Place Transition,
         Either (NonEmpty [Transition]) (NonEmpty [Transition])))
findNetGoalWithSolutions FilterConfig
filterConfig Int
maxPrintedSolutions NetGoalConfig
netGoalConfig

checkReachConfig :: ReachConfig -> Maybe String
checkReachConfig :: ReachConfig -> Maybe String
checkReachConfig ReachConfig {Bool
Int
Maybe Int
FilterConfig
NetGoalConfig
netGoalConfig :: ReachConfig -> NetGoalConfig
maxPrintedSolutions :: ReachConfig -> Int
rejectLongerThan :: ReachConfig -> Maybe Int
showLengthHint :: ReachConfig -> Bool
showMinLengthHint :: ReachConfig -> Bool
showTargetNet :: ReachConfig -> Bool
showPlaceNamesInNet :: ReachConfig -> Bool
filterConfig :: ReachConfig -> FilterConfig
netGoalConfig :: NetGoalConfig
maxPrintedSolutions :: Int
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showTargetNet :: Bool
showPlaceNamesInNet :: Bool
filterConfig :: FilterConfig
..} =
  Int
-> Int
-> Capacity Place
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> TransitionBehaviorConstraints
-> ArrowDensityConstraints
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
checkBasicPetriConfig
    (NetGoalConfig -> Int
numPlaces NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> Int
numTransitions NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> Capacity Place
capacity NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> Int
minTransitionLength NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> Int
maxTransitionLength NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> TransitionBehaviorConstraints
transitionBehaviorConstraints NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> ArrowDensityConstraints
arrowDensityConstraints NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> [GraphvizCommand]
graphLayouts NetGoalConfig
netGoalConfig)
    Maybe Int
rejectLongerThan
    Bool
showLengthHint
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  (let maxPlacesDiff :: Int
maxPlacesDiff = NetGoalConfig -> Int
maxPlacesChanged NetGoalConfig
netGoalConfig
   in if Int
maxPlacesDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1
        then String -> Maybe String
forall a. a -> Maybe a
Just String
"maxPlacesChanged must be at least 1"
        else if Int
maxPlacesDiff Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> NetGoalConfig -> Int
numPlaces NetGoalConfig
netGoalConfig
             then String -> Maybe String
forall a. a -> Maybe a
Just String
"maxPlacesChanged cannot be greater than numPlaces"
             else Maybe String
forall a. Maybe a
Nothing)
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  Maybe Int -> Int -> Int -> FilterConfig -> Maybe String
checkFilterConfigWith
    Maybe Int
rejectLongerThan
    (NetGoalConfig -> Int
minTransitionLength NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> Int
numTransitions NetGoalConfig
netGoalConfig)
    FilterConfig
filterConfig
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  (if Int
maxPrintedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
0
    then String -> Maybe String
forall a. a -> Maybe a
Just String
"maxPrintedSolutions must be non-negative"
    else case FilterConfig -> Maybe Int
solutionSetLimit FilterConfig
filterConfig of
      Just Int
maxSolutions | Int
maxPrintedSolutions Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
maxSolutions ->
        String -> Maybe String
forall a. a -> Maybe a
Just String
"maxPrintedSolutions cannot be greater than solutionSetLimit"
      Maybe Int
_ -> Maybe String
forall a. Maybe a
Nothing)
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
  if Bool
showTargetNet Bool -> Bool -> Bool
|| Bool
showPlaceNamesInNet
      then Maybe String
forall a. Maybe a
Nothing
      else String -> Maybe String
forall a. a -> Maybe a
Just String
"At least one of showTargetNet or showPlaceNamesInNet must be True"

generateReach
  :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => ReachConfig
  -> Int
  -> m (ReachInstance Place Transition)
generateReach :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
ReachConfig -> Int -> m (ReachInstance Place Transition)
generateReach ReachConfig {Bool
Int
Maybe Int
FilterConfig
NetGoalConfig
netGoalConfig :: ReachConfig -> NetGoalConfig
maxPrintedSolutions :: ReachConfig -> Int
rejectLongerThan :: ReachConfig -> Maybe Int
showLengthHint :: ReachConfig -> Bool
showMinLengthHint :: ReachConfig -> Bool
showTargetNet :: ReachConfig -> Bool
showPlaceNamesInNet :: ReachConfig -> Bool
filterConfig :: ReachConfig -> FilterConfig
netGoalConfig :: NetGoalConfig
maxPrintedSolutions :: Int
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showTargetNet :: Bool
showPlaceNamesInNet :: Bool
filterConfig :: FilterConfig
..} Int
seed = do
  (NetGoal Place Transition
netGoal, Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList) <- FilterConfig
-> Int
-> NetGoalConfig
-> Int
-> m (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
FilterConfig
-> Int
-> NetGoalConfig
-> Int
-> m (NetGoal Place Transition,
      Either (NonEmpty [Transition]) (NonEmpty [Transition]))
generateNetGoal FilterConfig
filterConfig Int
maxPrintedSolutions NetGoalConfig
netGoalConfig Int
seed
  ReachInstance Place Transition
-> m (ReachInstance Place Transition)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ReachInstance Place Transition
 -> m (ReachInstance Place Transition))
-> ReachInstance Place Transition
-> m (ReachInstance Place Transition)
forall a b. (a -> b) -> a -> b
$ ReachInstance {
    netGoal :: NetGoal Place Transition
netGoal           = NetGoal Place Transition
netGoal,
    minLength :: Int
minLength         = NetGoalConfig -> Int
minTransitionLength NetGoalConfig
netGoalConfig,
    noLongerThan :: Maybe Int
noLongerThan      = Maybe Int
rejectLongerThan,
    showGoalNet :: Bool
showGoalNet       = Bool
showTargetNet,
    showPlaceNames :: Bool
showPlaceNames    = Bool
showPlaceNamesInNet,
    shortestSolutions :: Either (NonEmpty [Transition]) (NonEmpty [Transition])
shortestSolutions = Either (NonEmpty [Transition]) (NonEmpty [Transition])
solutionsList,
    maxDisplayedSolutions :: Int
maxDisplayedSolutions = Int
maxPrintedSolutions,
    withLengthHint :: Maybe Int
withLengthHint    =
      if Bool
showLengthHint then Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ NetGoalConfig -> Int
maxTransitionLength NetGoalConfig
netGoalConfig else Maybe Int
forall a. Maybe a
Nothing,
    withMinLengthHint :: Bool
withMinLengthHint = Bool
showMinLengthHint,
    rejectSpaceballsLength :: Maybe Int
rejectSpaceballsLength = FilterConfig -> Maybe Int
spaceballsPrefixThreshold FilterConfig
filterConfig
    }