{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# 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 where

import qualified Control.Monad.Trans              as Monad (lift)
import qualified Data.Set                         as S (toList)

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.Property (
  Property (Default),
  validate,
  )
import Modelling.PetriNet.Reach.Roll    (netLimits)
import Modelling.PetriNet.Reach.Step    (executes, levels, levels')
import Modelling.PetriNet.Reach.Type (
  Capacity (Unbounded),
  Net (start, transitions),
  Place (..),
  ShowPlace (ShowPlace),
  ShowTransition (ShowTransition),
  State,
  Transition (..),
  TransitionsList (TransitionsList),
  bimapNet,
  example,
  hasIsolatedNodes,
  mapState,
  mark,
  )

import Control.Applicative              (Alternative, (<|>))
import Control.Functor.Trans            (FunctorTrans (lift))
import Control.Monad                    (forM, guard, when)
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.Monad.Extra              (findM, maybeM, whenJust)
import Modelling.PetriNet.Reach.ConfigValidation (
  checkBasicPetriConfig,
  )
import Control.OutputCapable.Blocks (
  ArticleToUse (IndefiniteArticle),
  GenericOutputCapable (assertion, code, image, indent, paragraph, text),
  LangM,
  MinimumThreshold (MinimumThreshold),
  OutputCapable,
  Rated,
  english,
  german,
  printSolutionAndAssertMinimum,
  translate,
  yesNo,
  )
import Control.OutputCapable.Blocks.Generic (
  ($>>),
  ($>>=),
  )
import Control.Monad.Random             (mkStdGen)
import Control.Monad.Trans.Random       (evalRandT)
import Data.Bifunctor                   (Bifunctor (second))
import Data.Either.Combinators          (whenRight)
import Data.Foldable                    (traverse_)
import Data.GraphViz                    (GraphvizCommand (..))
import Data.List                        (minimumBy)
import Data.List.Extra                  (nubSort)
import Data.Maybe                       (fromMaybe)
import Data.Ord                         (comparing)
import Data.Ratio                       ((%))
import Data.String.Interpolate          (i)
import Data.Typeable                    (Typeable)
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 :: State a
start = NetGoal a t -> State a
forall s t. NetGoal s t -> State s
goal (ReachInstance a t -> NetGoal a t
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance a t
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
    )
  => 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) =>
String -> ReachInstance s t -> LangM m
reachTask 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 :: State s
start = 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) }))
    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 -> String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> GenericLangM Language m ()
forall (m :: * -> *).
OutputCapable m =>
String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> LangM m
reportReachFor
    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
  => FilePath
  -> Maybe Int
  -> Maybe Int
  -> Int
  -> Bool
  -> Maybe (Either FilePath String)
  -> LangM m
reportReachFor :: forall (m :: * -> *).
OutputCapable m =>
String
-> Maybe Int
-> Maybe Int
-> Int
-> Bool
-> Maybe (Either String String)
-> LangM m
reportReachFor 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 ()
  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
"State your answer as an (arbitrarily short or long) sequence of the following kind:"
      String -> State (Map Language String) ()
german String
"Geben Sie Ihre Lösung als (beliebig kurze oder lange) Auflistung der folgenden Art an:"
    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
"has exactly", String
"genau")
          else (String
"does not exceed", String
"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
"State your solution as a sequence of the following kind that ",
          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
"Geben Sie Ihre Lösung als ", String
germanConstraint, String
" ", Int -> String
forall a. Show a => a -> String
show Int
maxL,
          String
"-schrittige 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."
      ]
  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 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|Hint: The shortest solutions have exactly #{maxSteps} steps.|]
      String -> State (Map Language String) ()
german [i|Hinweis: Die kürzesten Lösungen haben genau #{maxSteps} Schritte.|]
    Just Int
maxSteps -> 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|Hint: There is a solution with not more than #{maxSteps} steps.|]
      String -> State (Map Language String) ()
german [i|Hinweis: Es gibt eine Lösung mit nicht mehr als #{maxSteps} Schritten.|]
    Maybe Int
Nothing -> () -> LangM m
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  Bool -> LangM m -> LangM m
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (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) (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|Hint: There is no solution with less than #{minLength} steps.|]
    String -> State (Map Language String) ()
german [i|Hinweis: Es gibt keine Lösung mit weniger als #{minLength} Schritten.|]
  LangM m
forall (m :: * -> *). OutputCapable m => LangM m
hoveringInformation
  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
     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)

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
      | ReachInstance Place Transition -> Bool
forall s t. ReachInstance s t -> Bool
showSolution ReachInstance Place Transition
reach = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
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] -> TransitionsList)
-> [Transition] -> TransitionsList
forall a b. (a -> b) -> a -> b
$ ReachInstance Place Transition -> [Transition]
forall s t. Ord s => ReachInstance s t -> [t]
reachSolution ReachInstance Place Transition
reach
      | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

netGoalSolution :: Ord s => NetGoal s t -> [t]
netGoalSolution :: forall s t. Ord s => NetGoal s t -> [t]
netGoalSolution NetGoal s t
netGoal = [t] -> [t]
forall a. [a] -> [a]
reverse ([t] -> [t]) -> [t] -> [t]
forall a b. (a -> b) -> a -> b
$ (State s, [t]) -> [t]
forall a b. (a, b) -> b
snd ((State s, [t]) -> [t]) -> (State s, [t]) -> [t]
forall a b. (a -> b) -> a -> b
$ [(State s, [t])] -> (State s, [t])
forall a. HasCallStack => [a] -> a
head ([(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])])
-> [[(State s, [t])]] -> [(State s, [t])]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
  (((State s, [t]) -> Bool) -> [(State s, [t])] -> [(State s, [t])]
forall a. (a -> Bool) -> [a] -> [a]
filter (((State s, [t]) -> Bool) -> [(State s, [t])] -> [(State s, [t])])
-> ((State s, [t]) -> Bool) -> [(State s, [t])] -> [(State s, [t])]
forall a b. (a -> b) -> a -> b
$ (State s -> State s -> Bool
forall a. Eq a => a -> a -> Bool
== NetGoal s t -> State s
forall s t. NetGoal s t -> State s
goal NetGoal s t
netGoal) (State s -> Bool)
-> ((State s, [t]) -> State s) -> (State s, [t]) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State s, [t]) -> State s
forall a b. (a, b) -> a
fst)
  ([[(State s, [t])]] -> [(State s, [t])])
-> [[(State s, [t])]] -> [(State s, [t])]
forall a b. (a -> b) -> a -> b
$ Net s t -> [[(State s, [t])]]
forall s t. Ord s => Net s t -> [[(State s, [t])]]
levels' (Net s t -> [[(State s, [t])]]) -> Net s t -> [[(State s, [t])]]
forall a b. (a -> b) -> a -> b
$ NetGoal s t -> Net s t
forall s t. NetGoal s t -> Net s t
petriNet NetGoal s t
netGoal

reachSolution :: Ord s => ReachInstance s t -> [t]
reachSolution :: forall s t. Ord s => ReachInstance s t -> [t]
reachSolution ReachInstance s t
inst = NetGoal s t -> [t]
forall s t. Ord s => NetGoal s t -> [t]
netGoalSolution (ReachInstance s t -> NetGoal s t
forall s t. ReachInstance s t -> NetGoal s t
netGoal ReachInstance s t
inst)

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
-> ArticleToUse -> Maybe String -> Rational -> Rated m
forall (m :: * -> *).
OutputCapable m =>
MinimumThreshold
-> ArticleToUse -> Maybe String -> Rational -> Rated m
printSolutionAndAssertMinimum
    (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)
    ArticleToUse
IndefiniteArticle
    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?"
        ]

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 -> Bool
showSolution      :: Bool,
  forall s t. ReachInstance s t -> Maybe Int
withLengthHint    :: Maybe Int,
  forall s t. ReachInstance s t -> Bool
withMinLengthHint :: Bool
  } 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, 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)

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

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
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
showSolution :: forall s t. ReachInstance s t -> Bool
netGoal :: NetGoal s t
minLength :: Int
noLongerThan :: Maybe Int
showGoalNet :: Bool
showPlaceNames :: Bool
showSolution :: Bool
withLengthHint :: Maybe Int
withMinLengthHint :: Bool
..} = 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,
    showSolution :: Bool
showSolution      = Bool
showSolution,
    withLengthHint :: Maybe Int
withLengthHint    = Maybe Int
withLengthHint,
    withMinLengthHint :: Bool
withMinLengthHint = Bool
withMinLengthHint
    }

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 -> Bool
printSolution       :: Bool,
  ReachConfig -> Maybe Int
rejectLongerThan    :: Maybe Int,
  ReachConfig -> Bool
showLengthHint      :: Bool,
  ReachConfig -> Bool
showMinLengthHint   :: Bool,
  ReachConfig -> Bool
showTargetNet       :: Bool,
  ReachConfig -> Bool
showPlaceNamesInNet :: Bool
  }
  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, Typeable)

data NetGoalConfig = NetGoalConfig {
  NetGoalConfig -> Int
numPlaces :: Int,
  NetGoalConfig -> Int
numTransitions :: Int,
  NetGoalConfig -> Capacity Place
capacity :: Capacity Place,
  NetGoalConfig -> [GraphvizCommand]
drawCommands        :: [GraphvizCommand],
  NetGoalConfig -> Int
maxTransitionLength :: Int,
  NetGoalConfig -> Int
minTransitionLength :: Int,
  NetGoalConfig -> (Int, Maybe Int)
postconditionsRange :: (Int, Maybe Int),
  NetGoalConfig -> (Int, Maybe Int)
preconditionsRange  :: (Int, Maybe Int)
  }
  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, Typeable)

defaultReachConfig :: ReachConfig
defaultReachConfig :: ReachConfig
defaultReachConfig = ReachConfig {
  netGoalConfig :: NetGoalConfig
netGoalConfig = NetGoalConfig {
    numPlaces :: Int
numPlaces           = Int
4,
    numTransitions :: Int
numTransitions      = Int
4,
    capacity :: Capacity Place
Modelling.PetriNet.Reach.Reach.capacity = Capacity Place
forall s. Capacity s
Unbounded,
    drawCommands :: [GraphvizCommand]
drawCommands        = [GraphvizCommand
Dot, GraphvizCommand
Neato, GraphvizCommand
TwoPi, GraphvizCommand
Circo, GraphvizCommand
Fdp, GraphvizCommand
Sfdp, GraphvizCommand
Osage, GraphvizCommand
Patchwork],
    maxTransitionLength :: Int
maxTransitionLength = Int
8,
    minTransitionLength :: Int
minTransitionLength = Int
6,
    postconditionsRange :: (Int, Maybe Int)
postconditionsRange = (Int
0, Maybe Int
forall a. Maybe a
Nothing),
    preconditionsRange :: (Int, Maybe Int)
preconditionsRange  = (Int
0, Maybe Int
forall a. Maybe a
Nothing)
    },
  printSolution :: Bool
printSolution       = Bool
False,
  rejectLongerThan :: Maybe Int
rejectLongerThan    = Maybe Int
forall a. Maybe a
Nothing,
  showLengthHint :: Bool
showLengthHint      = Bool
True,
  showMinLengthHint :: Bool
showMinLengthHint   = Bool
True,
  showTargetNet :: Bool
showTargetNet       = Bool
True,
  showPlaceNamesInNet :: Bool
showPlaceNamesInNet = Bool
False
  }

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,
  showSolution :: Bool
showSolution      = Bool
False,
  withLengthHint :: Maybe Int
withLengthHint    = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
12,
  withMinLengthHint :: Bool
withMinLengthHint = Bool
False
}

generateNetGoal
  :: (MonadCatch m, MonadDiagrams m, MonadGraphviz m)
  => NetGoalConfig
  -> Int
  -> m (NetGoal Place Transition)
generateNetGoal :: forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
NetGoalConfig -> Int -> m (NetGoal Place Transition)
generateNetGoal NetGoalConfig {Int
[GraphvizCommand]
(Int, Maybe Int)
Capacity Place
numPlaces :: NetGoalConfig -> Int
numTransitions :: NetGoalConfig -> Int
capacity :: NetGoalConfig -> Capacity Place
drawCommands :: NetGoalConfig -> [GraphvizCommand]
maxTransitionLength :: NetGoalConfig -> Int
minTransitionLength :: NetGoalConfig -> Int
postconditionsRange :: NetGoalConfig -> (Int, Maybe Int)
preconditionsRange :: NetGoalConfig -> (Int, Maybe Int)
numPlaces :: Int
numTransitions :: Int
capacity :: Capacity Place
drawCommands :: [GraphvizCommand]
maxTransitionLength :: Int
minTransitionLength :: Int
postconditionsRange :: (Int, Maybe Int)
preconditionsRange :: (Int, Maybe Int)
..} Int
seed = do
  let ps :: [Place]
ps = [Int -> Place
Place Int
1 .. Int -> Place
Place Int
numPlaces]
      tries :: RandT
  StdGen m [[((Int, Int), (Net Place Transition, State Place))]]
tries = [Int]
-> (Int
    -> RandT
         StdGen m [((Int, Int), (Net Place Transition, State Place))])
-> RandT
     StdGen m [[((Int, Int), (Net Place Transition, State Place))]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Int
1 :: Int .. Int
1000] ((Int
  -> RandT
       StdGen m [((Int, Int), (Net Place Transition, State Place))])
 -> RandT
      StdGen m [[((Int, Int), (Net Place Transition, State Place))]])
-> (Int
    -> RandT
         StdGen m [((Int, Int), (Net Place Transition, State Place))])
-> RandT
     StdGen m [[((Int, Int), (Net Place Transition, State Place))]]
forall a b. (a -> b) -> a -> b
$ RandT StdGen m [((Int, Int), (Net Place Transition, State Place))]
-> Int
-> RandT
     StdGen m [((Int, Int), (Net Place Transition, State Place))]
forall a b. a -> b -> a
const (RandT StdGen m [((Int, Int), (Net Place Transition, State Place))]
 -> Int
 -> RandT
      StdGen m [((Int, Int), (Net Place Transition, State Place))])
-> RandT
     StdGen m [((Int, Int), (Net Place Transition, State Place))]
-> Int
-> RandT
     StdGen m [((Int, Int), (Net Place Transition, State Place))]
forall a b. (a -> b) -> a -> b
$ do
        Net Place Transition
n <- Int
-> Int
-> Int
-> Int
-> [Place]
-> [Transition]
-> Capacity Place
-> RandT StdGen m (Net Place Transition)
forall (m :: * -> *) s t.
(MonadRandom m, Ord s, Ord t) =>
Int -> Int -> Int -> Int -> [s] -> [t] -> Capacity s -> m (Net s t)
netLimits Int
vLow Int
vHigh Int
nLow Int
nHigh
            [Place]
ps
            [Transition]
ts
            Capacity Place
capacity
        return $ do
          -- Filter out nets with isolated nodes
          Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Net Place Transition -> Bool
forall s t. (Ord s, Ord t) => Net s t -> Bool
hasIsolatedNodes Net Place Transition
n
          (Int
l,[State Place]
zs) <-
            Int -> [(Int, [State Place])] -> [(Int, [State Place])]
forall a. Int -> [a] -> [a]
take (Int
maxTransitionLength Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ([(Int, [State Place])] -> [(Int, [State Place])])
-> [(Int, [State Place])] -> [(Int, [State Place])]
forall a b. (a -> b) -> a -> b
$ [Int] -> [[State Place]] -> [(Int, [State Place])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 :: Int ..] ([[State Place]] -> [(Int, [State Place])])
-> [[State Place]] -> [(Int, [State Place])]
forall a b. (a -> b) -> a -> b
$ Net Place Transition -> [[State Place]]
forall s t. Ord s => Net s t -> [[State s]]
levels Net Place Transition
n
          State Place
z' <- [State Place]
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] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ do
                Place
p <- [Place]
ps
                return $ Int -> Int
forall a. Num a => a -> a
abs (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)
          return ((Int -> Int
forall a. Num a => a -> a
negate Int
l, Int
d), (Net Place Transition
n, State Place
z'))
      out :: RandT
  StdGen m ((Net Place Transition, State Place), GraphvizCommand)
out = do
        [[((Int, Int), (Net Place Transition, State Place))]]
xs <- RandT
  StdGen m [[((Int, Int), (Net Place Transition, State Place))]]
tries
        let ((Int
l, Int
_), (Net Place Transition, State Place)
pn) = (((Int, Int), (Net Place Transition, State Place))
 -> ((Int, Int), (Net Place Transition, State Place)) -> Ordering)
-> [((Int, Int), (Net Place Transition, State Place))]
-> ((Int, Int), (Net Place Transition, State Place))
forall (t :: * -> *) a.
Foldable t =>
(a -> a -> Ordering) -> t a -> a
minimumBy ((((Int, Int), (Net Place Transition, State Place)) -> (Int, Int))
-> ((Int, Int), (Net Place Transition, State Place))
-> ((Int, Int), (Net Place Transition, State Place))
-> Ordering
forall a b. Ord a => (b -> a) -> b -> b -> Ordering
comparing ((Int, Int), (Net Place Transition, State Place)) -> (Int, Int)
forall a b. (a, b) -> a
fst) ([((Int, Int), (Net Place Transition, State Place))]
 -> ((Int, Int), (Net Place Transition, State Place)))
-> [((Int, Int), (Net Place Transition, State Place))]
-> ((Int, Int), (Net Place Transition, State Place))
forall a b. (a -> b) -> a -> b
$ [[((Int, Int), (Net Place Transition, State Place))]]
-> [((Int, Int), (Net Place Transition, State Place))]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[((Int, Int), (Net Place Transition, State Place))]]
xs
        if Int -> Int
forall a. Num a => a -> a
negate Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
minTransitionLength
          then do
            RandT
  StdGen m ((Net Place Transition, State Place), GraphvizCommand)
-> (GraphvizCommand
    -> RandT
         StdGen m ((Net Place Transition, State Place), GraphvizCommand))
-> RandT StdGen m (Maybe GraphvizCommand)
-> RandT
     StdGen m ((Net Place Transition, State Place), GraphvizCommand)
forall (m :: * -> *) b a.
Monad m =>
m b -> (a -> m b) -> m (Maybe a) -> m b
maybeM RandT
  StdGen m ((Net Place Transition, State Place), GraphvizCommand)
out (((Net Place Transition, State Place), GraphvizCommand)
-> RandT
     StdGen m ((Net Place Transition, State Place), GraphvizCommand)
forall a. a -> RandT StdGen m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (((Net Place Transition, State Place), GraphvizCommand)
 -> RandT
      StdGen m ((Net Place Transition, State Place), GraphvizCommand))
-> (GraphvizCommand
    -> ((Net Place Transition, State Place), GraphvizCommand))
-> GraphvizCommand
-> RandT
     StdGen m ((Net Place Transition, State Place), GraphvizCommand)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Net Place Transition, State Place)
pn,))
            (RandT StdGen m (Maybe GraphvizCommand)
 -> RandT
      StdGen m ((Net Place Transition, State Place), GraphvizCommand))
-> RandT StdGen m (Maybe GraphvizCommand)
-> RandT
     StdGen m ((Net Place Transition, State Place), 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 Place Transition -> 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 Place Transition, State Place) -> Net Place Transition
forall a b. (a, b) -> a
fst (Net Place Transition, State Place)
pn)) [GraphvizCommand]
drawCommands
          else RandT
  StdGen m ((Net Place Transition, State Place), GraphvizCommand)
out

  ((Net Place Transition
petri, State Place
state), GraphvizCommand
cmd) <- RandT
  StdGen m ((Net Place Transition, State Place), GraphvizCommand)
-> m ((Net Place Transition, State Place), GraphvizCommand)
forall {m :: * -> *} {a}. Monad m => RandT StdGen m a -> m a
eval RandT
  StdGen m ((Net Place Transition, State Place), GraphvizCommand)
out

  NetGoal Place Transition -> m (NetGoal Place Transition)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NetGoal Place Transition -> m (NetGoal Place Transition))
-> NetGoal Place Transition -> m (NetGoal Place Transition)
forall a b. (a -> b) -> a -> b
$ NetGoal {
    drawUsing :: GraphvizCommand
drawUsing   = GraphvizCommand
cmd,
    goal :: State Place
goal        = State Place
state,
    petriNet :: Net Place Transition
petriNet    = Net Place Transition
petri
    }

  where
    fixMaximum :: (a, Maybe Int) -> (a, Int)
fixMaximum = (Maybe Int -> Int) -> (a, Maybe Int) -> (a, Int)
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 (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
numPlaces (Int -> Int) -> (Maybe Int -> Int) -> Maybe Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
forall a. Bounded a => a
maxBound)
    (Int
vLow, Int
vHigh) = (Int, Maybe Int) -> (Int, Int)
forall {a}. (a, Maybe Int) -> (a, Int)
fixMaximum (Int, Maybe Int)
preconditionsRange
    (Int
nLow, Int
nHigh) = (Int, Maybe Int) -> (Int, Int)
forall {a}. (a, Maybe Int) -> (a, Int)
fixMaximum (Int, Maybe Int)
postconditionsRange
    ts :: [Transition]
ts = [Int -> Transition
Transition Int
1 .. Int -> Transition
Transition Int
numTransitions]
    eval :: RandT StdGen m a -> m a
eval RandT StdGen m a
f = RandT StdGen m a -> StdGen -> m a
forall (m :: * -> *) g a. Monad m => RandT g m a -> g -> m a
evalRandT RandT StdGen m a
f (StdGen -> m a) -> StdGen -> m a
forall a b. (a -> b) -> a -> b
$ Int -> StdGen
mkStdGen Int
seed

checkReachConfig :: ReachConfig -> Maybe String
checkReachConfig :: ReachConfig -> Maybe String
checkReachConfig ReachConfig {Bool
Maybe Int
NetGoalConfig
netGoalConfig :: ReachConfig -> NetGoalConfig
printSolution :: ReachConfig -> Bool
rejectLongerThan :: ReachConfig -> Maybe Int
showLengthHint :: ReachConfig -> Bool
showMinLengthHint :: ReachConfig -> Bool
showTargetNet :: ReachConfig -> Bool
showPlaceNamesInNet :: ReachConfig -> Bool
netGoalConfig :: NetGoalConfig
printSolution :: Bool
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showTargetNet :: Bool
showPlaceNamesInNet :: Bool
..} =
  Int
-> Int
-> Capacity Place
-> Int
-> Int
-> (Int, Maybe Int)
-> (Int, Maybe Int)
-> [GraphvizCommand]
-> Maybe Int
-> Bool
-> Maybe String
forall s.
Int
-> Int
-> Capacity s
-> Int
-> Int
-> (Int, Maybe Int)
-> (Int, Maybe Int)
-> [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 -> (Int, Maybe Int)
preconditionsRange NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> (Int, Maybe Int)
postconditionsRange NetGoalConfig
netGoalConfig)
    (NetGoalConfig -> [GraphvizCommand]
drawCommands 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
<|> 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
Maybe Int
NetGoalConfig
netGoalConfig :: ReachConfig -> NetGoalConfig
printSolution :: ReachConfig -> Bool
rejectLongerThan :: ReachConfig -> Maybe Int
showLengthHint :: ReachConfig -> Bool
showMinLengthHint :: ReachConfig -> Bool
showTargetNet :: ReachConfig -> Bool
showPlaceNamesInNet :: ReachConfig -> Bool
netGoalConfig :: NetGoalConfig
printSolution :: Bool
rejectLongerThan :: Maybe Int
showLengthHint :: Bool
showMinLengthHint :: Bool
showTargetNet :: Bool
showPlaceNamesInNet :: Bool
..} Int
seed = do
  NetGoal Place Transition
netGoal <- NetGoalConfig -> Int -> m (NetGoal Place Transition)
forall (m :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m) =>
NetGoalConfig -> Int -> m (NetGoal Place Transition)
generateNetGoal NetGoalConfig
netGoalConfig Int
seed
  pure $ 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,
    showSolution :: Bool
showSolution      = Bool
printSolution,
    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
    }