{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# Language DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# Language QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE DeriveDataTypeable #-}

module Modelling.PetriNet.MatchToMath (
  GraphToMathInstance,
  Math,
  MathConfig (..),
  MatchInstance (..),
  MathToGraphInstance,
  addPartNames,
  checkGraphToMathConfig,
  checkMathConfig,
  defaultGraphToMathInstance,
  defaultMathConfig,
  defaultMathToGraphInstance,
  graphToMath,
  graphToMathEvaluation,
  graphToMathSyntax,
  graphToMathTask,
  matchSolution,
  mathToGraph,
  mathToGraphEvaluation,
  mathToGraphSyntax,
  mathToGraphTask,
  petriNetRnd,
  )  where

import qualified Data.Map                         as M (
  empty,
  filter,
  foldrWithKey,
  keys,
  partition,
  )

import Capabilities.Alloy               (MonadAlloy, getInstances)
import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.Auxiliary.Common       (Object (oName), findFittingRandomElements)
import Modelling.Auxiliary.Output       (
  hoveringInformation,
  extra,
  )
import Modelling.PetriNet.Alloy (
  compAdvConstraints,
  compBasicConstraints,
  compChange,
  moduleHelpers,
  modulePetriAdditions,
  modulePetriConcepts,
  modulePetriConstraints,
  modulePetriSignature,
  petriScopeBitWidth,
  petriScopeMaxSeq,
  signatures,
  taskInstance,
  )
import Modelling.PetriNet.Diagram       (cacheNet, isNetDrawable)
import Modelling.PetriNet.LaTeX         (toPetriMath)
import Modelling.PetriNet.Parser (
  parseChange,
  parseRenamedNet,
  )
import Modelling.PetriNet.Types (
  AdvConfig,
  AlloyConfig,
  BasicConfig (..),
  Change,
  ChangeConfig (..),
  Drawable,
  DrawSettings (..),
  GraphConfig (..),
  Net (..),
  PetriLike (..),
  PetriMath (..),
  PetriNode (..),
  SimpleNode (..),
  SimplePetriLike,
  allDrawSettings,
  checkBasicConfig,
  checkChangeConfig,
  checkGraphLayouts,
  defaultAdvConfig,
  defaultAlloyConfig,
  defaultBasicConfig,
  defaultChangeConfig,
  defaultGraphConfig,
  isPlaceNode,
  mapChange,
  shuffleNames,
  )

import Control.Applicative              (Alternative ((<|>)))
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.OutputCapable.Blocks       (
  ArticleToUse (DefiniteArticle),
  GenericOutputCapable (..),
  LangM,
  Language,
  OutputCapable,
  ($=<<),
  english,
  german,
  singleChoice,
  translate,
  translations,
  )
import Control.Monad.Extra              (findM)
import Control.Monad.Random             (
  MonadRandom,
  RandT,
  RandomGen,
  StdGen,
  evalRandT,
  mkStdGen,
  )
import Control.Monad.Trans              (lift)
import Data.Bifoldable                  (Bifoldable (bifoldMap))
import Data.Bifunctor                   (Bifunctor (bimap, second))
import Data.Bitraversable               (Bitraversable (bitraverse), bimapM)
import Data.Data                        (Data, Typeable)
import Data.GraphViz                    (GraphvizCommand (Circo, Dot, Fdp, Sfdp))
import Data.Map                         (Map, fromList, mapWithKey, toList)
import Data.String.Interpolate          (i)
import GHC.Generics                     (Generic)
import Image.LaTeX.Render               (Formula)
import Language.Alloy.Call (
  AlloyInstance,
  )
import System.Random.Shuffle            (shuffleM)

type Math = PetriMath Formula

type GraphToMathInstance = MatchInstance (Drawable (SimplePetriLike String)) Math
type MathToGraphInstance = MatchInstance Math (Drawable (SimplePetriLike String))

{-# DEPRECATED addPartNames "the whole type class NamedParts will be removed" #-}
class NamedParts n where
  addPartNames :: n a -> n (String, a)

instance NamedParts PetriMath where
  addPartNames :: forall a. PetriMath a -> PetriMath (String, a)
addPartNames PetriMath a
pm = PetriMath {
    $sel:netMath:PetriMath :: (String, a)
netMath            = (String
"net", PetriMath a -> a
forall a. PetriMath a -> a
netMath PetriMath a
pm),
    $sel:placesMath:PetriMath :: (String, a)
placesMath         = (String
"places", PetriMath a -> a
forall a. PetriMath a -> a
placesMath PetriMath a
pm),
    $sel:transitionsMath:PetriMath :: (String, a)
transitionsMath    = (String
"transitions", PetriMath a -> a
forall a. PetriMath a -> a
transitionsMath PetriMath a
pm),
    $sel:tokenChangeMath:PetriMath :: [((String, a), (String, a))]
tokenChangeMath    =
        [((String
"in" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n, a
x), (String
"out" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
n, a
y))
        | (Integer
n, (a
x, a
y)) <- [Integer] -> [(a, a)] -> [(Integer, (a, a))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Integer
1 :: Integer ..] ([(a, a)] -> [(Integer, (a, a))])
-> [(a, a)] -> [(Integer, (a, a))]
forall a b. (a -> b) -> a -> b
$ PetriMath a -> [(a, a)]
forall a. PetriMath a -> [(a, a)]
tokenChangeMath PetriMath a
pm],
    $sel:initialMarkingMath:PetriMath :: (String, a)
initialMarkingMath = (String
"marking", PetriMath a -> a
forall a. PetriMath a -> a
initialMarkingMath PetriMath a
pm),
    $sel:placeOrderMath:PetriMath :: Maybe (String, a)
placeOrderMath     = (String
"order",) (a -> (String, a)) -> Maybe a -> Maybe (String, a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> PetriMath a -> Maybe a
forall a. PetriMath a -> Maybe a
placeOrderMath PetriMath a
pm
    }

data MathConfig = MathConfig {
  MathConfig -> BasicConfig
basicConfig :: BasicConfig,
  MathConfig -> AdvConfig
advConfig :: AdvConfig,
  MathConfig -> ChangeConfig
changeConfig :: ChangeConfig,
  MathConfig -> Int
generatedWrongInstances :: Int,
  MathConfig -> GraphConfig
graphConfig :: GraphConfig,
  MathConfig -> Bool
printSolution :: Bool,
  MathConfig -> Bool
useDifferentGraphLayouts :: Bool,
  MathConfig -> Int
wrongInstances :: Int,
  MathConfig -> AlloyConfig
alloyConfig :: AlloyConfig,
  MathConfig -> Maybe (Map Language String)
extraText :: Maybe (Map Language String)
  } deriving ((forall x. MathConfig -> Rep MathConfig x)
-> (forall x. Rep MathConfig x -> MathConfig) -> Generic MathConfig
forall x. Rep MathConfig x -> MathConfig
forall x. MathConfig -> Rep MathConfig x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. MathConfig -> Rep MathConfig x
from :: forall x. MathConfig -> Rep MathConfig x
$cto :: forall x. Rep MathConfig x -> MathConfig
to :: forall x. Rep MathConfig x -> MathConfig
Generic, ReadPrec [MathConfig]
ReadPrec MathConfig
Int -> ReadS MathConfig
ReadS [MathConfig]
(Int -> ReadS MathConfig)
-> ReadS [MathConfig]
-> ReadPrec MathConfig
-> ReadPrec [MathConfig]
-> Read MathConfig
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS MathConfig
readsPrec :: Int -> ReadS MathConfig
$creadList :: ReadS [MathConfig]
readList :: ReadS [MathConfig]
$creadPrec :: ReadPrec MathConfig
readPrec :: ReadPrec MathConfig
$creadListPrec :: ReadPrec [MathConfig]
readListPrec :: ReadPrec [MathConfig]
Read, Int -> MathConfig -> String -> String
[MathConfig] -> String -> String
MathConfig -> String
(Int -> MathConfig -> String -> String)
-> (MathConfig -> String)
-> ([MathConfig] -> String -> String)
-> Show MathConfig
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> MathConfig -> String -> String
showsPrec :: Int -> MathConfig -> String -> String
$cshow :: MathConfig -> String
show :: MathConfig -> String
$cshowList :: [MathConfig] -> String -> String
showList :: [MathConfig] -> String -> String
Show)

defaultMathConfig :: MathConfig
defaultMathConfig :: MathConfig
defaultMathConfig = MathConfig {
  $sel:basicConfig:MathConfig :: BasicConfig
basicConfig = BasicConfig
defaultBasicConfig,
  $sel:advConfig:MathConfig :: AdvConfig
advConfig = AdvConfig
defaultAdvConfig,
  $sel:changeConfig:MathConfig :: ChangeConfig
changeConfig = ChangeConfig
defaultChangeConfig {
    $sel:tokenChangeOverall:ChangeConfig :: Int
tokenChangeOverall = Int
0,
    $sel:maxTokenChangePerPlace:ChangeConfig :: Int
maxTokenChangePerPlace = Int
0
    },
  $sel:generatedWrongInstances:MathConfig :: Int
generatedWrongInstances = Int
50,
  $sel:graphConfig:MathConfig :: GraphConfig
graphConfig = GraphConfig
defaultGraphConfig,
  $sel:printSolution:MathConfig :: Bool
printSolution = Bool
False,
  $sel:useDifferentGraphLayouts:MathConfig :: Bool
useDifferentGraphLayouts = Bool
False,
  $sel:wrongInstances:MathConfig :: Int
wrongInstances = Int
3,
  $sel:alloyConfig:MathConfig :: AlloyConfig
alloyConfig = AlloyConfig
defaultAlloyConfig,
  $sel:extraText:MathConfig :: Maybe (Map Language String)
extraText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

data MatchInstance a b = MatchInstance {
  forall a b. MatchInstance a b -> a
from :: a,
  forall a b. MatchInstance a b -> Bool
showSolution :: Bool,
  forall a b. MatchInstance a b -> Map Int (Bool, b)
to :: Map Int (Bool, b),
  forall a b. MatchInstance a b -> Maybe (Map Language String)
addText :: Maybe (Map Language String)
  }
  deriving (Typeable (MatchInstance a b)
Typeable (MatchInstance a b)
-> (forall (c :: * -> *).
    (forall d b. Data d => c (d -> b) -> d -> c b)
    -> (forall g. g -> c g)
    -> MatchInstance a b
    -> c (MatchInstance a b))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (MatchInstance a b))
-> (MatchInstance a b -> Constr)
-> (MatchInstance a b -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (MatchInstance a b)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c (MatchInstance a b)))
-> ((forall b. Data b => b -> b)
    -> MatchInstance a b -> MatchInstance a b)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> MatchInstance a b -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> MatchInstance a b -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> MatchInstance a b -> m (MatchInstance a b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> MatchInstance a b -> m (MatchInstance a b))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> MatchInstance a b -> m (MatchInstance a b))
-> Data (MatchInstance a b)
MatchInstance a b -> Constr
MatchInstance a b -> DataType
(forall b. Data b => b -> b)
-> MatchInstance a b -> MatchInstance a b
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) -> MatchInstance a b -> u
forall u. (forall d. Data d => d -> u) -> MatchInstance a b -> [u]
forall {a} {b}. (Data b, Data a) => Typeable (MatchInstance a b)
forall a b. (Data b, Data a) => MatchInstance a b -> Constr
forall a b. (Data b, Data a) => MatchInstance a b -> DataType
forall a b.
(Data b, Data a) =>
(forall b. Data b => b -> b)
-> MatchInstance a b -> MatchInstance a b
forall a b u.
(Data b, Data a) =>
Int -> (forall d. Data d => d -> u) -> MatchInstance a b -> u
forall a b u.
(Data b, Data a) =>
(forall d. Data d => d -> u) -> MatchInstance a b -> [u]
forall a b r r'.
(Data b, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
forall a b r r'.
(Data b, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
forall a b (m :: * -> *).
(Data b, Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
forall a b (m :: * -> *).
(Data b, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
forall a b (c :: * -> *).
(Data b, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (MatchInstance a b)
forall a b (c :: * -> *).
(Data b, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MatchInstance a b
-> c (MatchInstance a b)
forall a b (t :: * -> *) (c :: * -> *).
(Data b, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (MatchInstance a b))
forall a b (t :: * -> * -> *) (c :: * -> *).
(Data b, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (MatchInstance a b))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (MatchInstance a b)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MatchInstance a b
-> c (MatchInstance a b)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (MatchInstance a b))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (MatchInstance a b))
$cgfoldl :: forall a b (c :: * -> *).
(Data b, Data a) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MatchInstance a b
-> c (MatchInstance a b)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> MatchInstance a b
-> c (MatchInstance a b)
$cgunfold :: forall a b (c :: * -> *).
(Data b, Data a) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (MatchInstance a b)
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (MatchInstance a b)
$ctoConstr :: forall a b. (Data b, Data a) => MatchInstance a b -> Constr
toConstr :: MatchInstance a b -> Constr
$cdataTypeOf :: forall a b. (Data b, Data a) => MatchInstance a b -> DataType
dataTypeOf :: MatchInstance a b -> DataType
$cdataCast1 :: forall a b (t :: * -> *) (c :: * -> *).
(Data b, Data a, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (MatchInstance a b))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (MatchInstance a b))
$cdataCast2 :: forall a b (t :: * -> * -> *) (c :: * -> *).
(Data b, Data a, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (MatchInstance a b))
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c (MatchInstance a b))
$cgmapT :: forall a b.
(Data b, Data a) =>
(forall b. Data b => b -> b)
-> MatchInstance a b -> MatchInstance a b
gmapT :: (forall b. Data b => b -> b)
-> MatchInstance a b -> MatchInstance a b
$cgmapQl :: forall a b r r'.
(Data b, Data a) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
$cgmapQr :: forall a b r r'.
(Data b, Data a) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> MatchInstance a b -> r
$cgmapQ :: forall a b u.
(Data b, Data a) =>
(forall d. Data d => d -> u) -> MatchInstance a b -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> MatchInstance a b -> [u]
$cgmapQi :: forall a b u.
(Data b, Data a) =>
Int -> (forall d. Data d => d -> u) -> MatchInstance a b -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> MatchInstance a b -> u
$cgmapM :: forall a b (m :: * -> *).
(Data b, Data a, Monad m) =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
$cgmapMp :: forall a b (m :: * -> *).
(Data b, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
$cgmapMo :: forall a b (m :: * -> *).
(Data b, Data a, MonadPlus m) =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> MatchInstance a b -> m (MatchInstance a b)
Data, (forall a b. (a -> b) -> MatchInstance a a -> MatchInstance a b)
-> (forall a b. a -> MatchInstance a b -> MatchInstance a a)
-> Functor (MatchInstance a)
forall a b. a -> MatchInstance a b -> MatchInstance a a
forall a b. (a -> b) -> MatchInstance a a -> MatchInstance a b
forall a a b. a -> MatchInstance a b -> MatchInstance a a
forall a a b. (a -> b) -> MatchInstance a a -> MatchInstance a b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall a a b. (a -> b) -> MatchInstance a a -> MatchInstance a b
fmap :: forall a b. (a -> b) -> MatchInstance a a -> MatchInstance a b
$c<$ :: forall a a b. a -> MatchInstance a b -> MatchInstance a a
<$ :: forall a b. a -> MatchInstance a b -> MatchInstance a a
Functor, (forall x. MatchInstance a b -> Rep (MatchInstance a b) x)
-> (forall x. Rep (MatchInstance a b) x -> MatchInstance a b)
-> Generic (MatchInstance a b)
forall x. Rep (MatchInstance a b) x -> MatchInstance a b
forall x. MatchInstance a b -> Rep (MatchInstance a b) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a b x. Rep (MatchInstance a b) x -> MatchInstance a b
forall a b x. MatchInstance a b -> Rep (MatchInstance a b) x
$cfrom :: forall a b x. MatchInstance a b -> Rep (MatchInstance a b) x
from :: forall x. MatchInstance a b -> Rep (MatchInstance a b) x
$cto :: forall a b x. Rep (MatchInstance a b) x -> MatchInstance a b
to :: forall x. Rep (MatchInstance a b) x -> MatchInstance a b
Generic, ReadPrec [MatchInstance a b]
ReadPrec (MatchInstance a b)
Int -> ReadS (MatchInstance a b)
ReadS [MatchInstance a b]
(Int -> ReadS (MatchInstance a b))
-> ReadS [MatchInstance a b]
-> ReadPrec (MatchInstance a b)
-> ReadPrec [MatchInstance a b]
-> Read (MatchInstance a b)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall a b. (Read a, Read b) => ReadPrec [MatchInstance a b]
forall a b. (Read a, Read b) => ReadPrec (MatchInstance a b)
forall a b. (Read a, Read b) => Int -> ReadS (MatchInstance a b)
forall a b. (Read a, Read b) => ReadS [MatchInstance a b]
$creadsPrec :: forall a b. (Read a, Read b) => Int -> ReadS (MatchInstance a b)
readsPrec :: Int -> ReadS (MatchInstance a b)
$creadList :: forall a b. (Read a, Read b) => ReadS [MatchInstance a b]
readList :: ReadS [MatchInstance a b]
$creadPrec :: forall a b. (Read a, Read b) => ReadPrec (MatchInstance a b)
readPrec :: ReadPrec (MatchInstance a b)
$creadListPrec :: forall a b. (Read a, Read b) => ReadPrec [MatchInstance a b]
readListPrec :: ReadPrec [MatchInstance a b]
Read, Int -> MatchInstance a b -> String -> String
[MatchInstance a b] -> String -> String
MatchInstance a b -> String
(Int -> MatchInstance a b -> String -> String)
-> (MatchInstance a b -> String)
-> ([MatchInstance a b] -> String -> String)
-> Show (MatchInstance a b)
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
forall a b.
(Show a, Show b) =>
Int -> MatchInstance a b -> String -> String
forall a b.
(Show a, Show b) =>
[MatchInstance a b] -> String -> String
forall a b. (Show a, Show b) => MatchInstance a b -> String
$cshowsPrec :: forall a b.
(Show a, Show b) =>
Int -> MatchInstance a b -> String -> String
showsPrec :: Int -> MatchInstance a b -> String -> String
$cshow :: forall a b. (Show a, Show b) => MatchInstance a b -> String
show :: MatchInstance a b -> String
$cshowList :: forall a b.
(Show a, Show b) =>
[MatchInstance a b] -> String -> String
showList :: [MatchInstance a b] -> String -> String
Show)

instance Bifoldable MatchInstance where
  bifoldMap :: forall m a b.
Monoid m =>
(a -> m) -> (b -> m) -> MatchInstance a b -> m
bifoldMap a -> m
f b -> m
g m :: MatchInstance a b
m@MatchInstance {} = a -> m
f (MatchInstance a b -> a
forall a b. MatchInstance a b -> a
from MatchInstance a b
m) m -> m -> m
forall a. Monoid a => a -> a -> a
`mappend` ((Bool, b) -> m) -> Map Int (Bool, b) -> m
forall m a. Monoid m => (a -> m) -> Map Int a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (b -> m
g (b -> m) -> ((Bool, b) -> b) -> (Bool, b) -> m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, b) -> b
forall a b. (a, b) -> b
snd) (MatchInstance a b -> Map Int (Bool, b)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to MatchInstance a b
m)

instance Bifunctor MatchInstance where
  bimap :: forall a b c d.
(a -> b) -> (c -> d) -> MatchInstance a c -> MatchInstance b d
bimap a -> b
f c -> d
g m :: MatchInstance a c
m@MatchInstance {} = MatchInstance a c
m {
    $sel:from:MatchInstance :: b
from = a -> b
f (a -> b) -> a -> b
forall a b. (a -> b) -> a -> b
$ MatchInstance a c -> a
forall a b. MatchInstance a b -> a
from MatchInstance a c
m,
    $sel:to:MatchInstance :: Map Int (Bool, d)
to   = (c -> d) -> (Bool, c) -> (Bool, d)
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 c -> d
g ((Bool, c) -> (Bool, d)) -> Map Int (Bool, c) -> Map Int (Bool, d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> MatchInstance a c -> Map Int (Bool, c)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to MatchInstance a c
m,
    $sel:addText:MatchInstance :: Maybe (Map Language String)
addText = MatchInstance a c -> Maybe (Map Language String)
forall a b. MatchInstance a b -> Maybe (Map Language String)
addText MatchInstance a c
m
    }

instance Bitraversable MatchInstance where
  bitraverse :: forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c)
-> (b -> f d) -> MatchInstance a b -> f (MatchInstance c d)
bitraverse a -> f c
f b -> f d
g m :: MatchInstance a b
m@MatchInstance {} = c
-> Bool
-> Map Int (Bool, d)
-> Maybe (Map Language String)
-> MatchInstance c d
forall a b.
a
-> Bool
-> Map Int (Bool, b)
-> Maybe (Map Language String)
-> MatchInstance a b
MatchInstance
    (c
 -> Bool
 -> Map Int (Bool, d)
 -> Maybe (Map Language String)
 -> MatchInstance c d)
-> f c
-> f (Bool
      -> Map Int (Bool, d)
      -> Maybe (Map Language String)
      -> MatchInstance c d)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> f c
f (MatchInstance a b -> a
forall a b. MatchInstance a b -> a
from MatchInstance a b
m)
    f (Bool
   -> Map Int (Bool, d)
   -> Maybe (Map Language String)
   -> MatchInstance c d)
-> f Bool
-> f (Map Int (Bool, d)
      -> Maybe (Map Language String) -> MatchInstance c d)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Bool -> f Bool
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MatchInstance a b -> Bool
forall a b. MatchInstance a b -> Bool
showSolution MatchInstance a b
m)
    f (Map Int (Bool, d)
   -> Maybe (Map Language String) -> MatchInstance c d)
-> f (Map Int (Bool, d))
-> f (Maybe (Map Language String) -> MatchInstance c d)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Bool, b) -> f (Bool, d))
-> Map Int (Bool, b) -> f (Map Int (Bool, d))
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> Map Int a -> f (Map Int b)
traverse ((b -> f d) -> (Bool, b) -> f (Bool, d)
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> (Bool, a) -> f (Bool, b)
traverse b -> f d
g) (MatchInstance a b -> Map Int (Bool, b)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to MatchInstance a b
m)
    f (Maybe (Map Language String) -> MatchInstance c d)
-> f (Maybe (Map Language String)) -> f (MatchInstance c d)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe (Map Language String) -> f (Maybe (Map Language String))
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MatchInstance a b -> Maybe (Map Language String)
forall a b. MatchInstance a b -> Maybe (Map Language String)
addText MatchInstance a b
m)

evalWithStdGen
  :: Monad m
  => Int
  -> RandT StdGen m a
  -> m a
evalWithStdGen :: forall (m :: * -> *) a. Monad m => Int -> RandT StdGen m a -> m a
evalWithStdGen = (RandT StdGen m a -> StdGen -> m a)
-> StdGen -> RandT StdGen m a -> m a
forall a b c. (a -> b -> c) -> b -> a -> c
flip RandT StdGen m a -> StdGen -> m a
forall (m :: * -> *) g a. Monad m => RandT g m a -> g -> m a
evalRandT (StdGen -> RandT StdGen m a -> m a)
-> (Int -> StdGen) -> Int -> RandT StdGen m a -> m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> StdGen
mkStdGen

writeDia
  :: (
    Data (n String),
    Data (p n String),
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Net p n,
    Typeable n,
    Typeable p
    )
  => FilePath
  -> MatchInstance (Drawable (p n String)) b
  -> m (MatchInstance FilePath b)
writeDia :: forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *) b.
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
String
-> MatchInstance (Drawable (p n String)) b
-> m (MatchInstance String b)
writeDia String
path = (Drawable (p n String) -> m String)
-> (b -> m b)
-> MatchInstance (Drawable (p n String)) b
-> m (MatchInstance String b)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM (\(p n String
n, DrawSettings
ds) -> DrawSettings -> String -> p n String -> m String
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
DrawSettings -> String -> p n String -> m String
writeGraph DrawSettings
ds String
path p n String
n) b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure

writeDias
  :: (
    Data (n String),
    Data (p n String),
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Net p n,
    Typeable n,
    Typeable p
    )
  => FilePath
  -> MatchInstance a (Drawable (p n String))
  -> m (MatchInstance a FilePath)
writeDias :: forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *) a.
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
String
-> MatchInstance a (Drawable (p n String))
-> m (MatchInstance a String)
writeDias String
path MatchInstance a (Drawable (p n String))
inst =
  let inst' :: MatchInstance a (String, Drawable (p n String))
inst' = MatchInstance a (Drawable (p n String))
inst {
        $sel:from:MatchInstance :: a
from = MatchInstance a (Drawable (p n String)) -> a
forall a b. MatchInstance a b -> a
from MatchInstance a (Drawable (p n String))
inst,
        $sel:to:MatchInstance :: Map Int (Bool, (String, Drawable (p n String)))
to   = (Int
 -> (Bool, Drawable (p n String))
 -> (Bool, (String, Drawable (p n String))))
-> Map Int (Bool, Drawable (p n String))
-> Map Int (Bool, (String, Drawable (p n String)))
forall k a b. (k -> a -> b) -> Map k a -> Map k b
mapWithKey (\Int
k -> (Drawable (p n String) -> (String, Drawable (p n String)))
-> (Bool, Drawable (p n String))
-> (Bool, (String, Drawable (p n String)))
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 -> String
forall a. Show a => a -> String
show Int
k,)) (Map Int (Bool, Drawable (p n String))
 -> Map Int (Bool, (String, Drawable (p n String))))
-> Map Int (Bool, Drawable (p n String))
-> Map Int (Bool, (String, Drawable (p n String)))
forall a b. (a -> b) -> a -> b
$ MatchInstance a (Drawable (p n String))
-> Map Int (Bool, Drawable (p n String))
forall a b. MatchInstance a b -> Map Int (Bool, b)
to MatchInstance a (Drawable (p n String))
inst
        }
  in (a -> m a)
-> ((String, Drawable (p n String)) -> m String)
-> MatchInstance a (String, Drawable (p n String))
-> m (MatchInstance a String)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bimapM a -> m a
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (\(String
_, (p n String
n, DrawSettings
d)) -> DrawSettings -> String -> p n String -> m String
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
DrawSettings -> String -> p n String -> m String
writeGraph DrawSettings
d String
path p n String
n) MatchInstance a (String, Drawable (p n String))
inst'

writeGraph
  :: (
    Data (n String),
    Data (p n String),
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Net p n,
    Typeable n,
    Typeable p
    )
  => DrawSettings
  -> FilePath
  -> p n String
  -> m FilePath
writeGraph :: forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
DrawSettings -> String -> p n String -> m String
writeGraph DrawSettings
drawSettings String
path p n String
pl =
  String -> p n String -> DrawSettings -> m String
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
String -> p n String -> DrawSettings -> m String
cacheNet
    String
path
    p n String
pl
    DrawSettings
drawSettings

graphToMath
  :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n)
  => MathConfig
  -> Int
  -> Int
  -> m (MatchInstance (Drawable (p n String)) Math)
graphToMath :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n) =>
MathConfig
-> Int -> Int -> m (MatchInstance (Drawable (p n String)) Math)
graphToMath config :: MathConfig
config@MathConfig {Bool
Int
Maybe (Map Language String)
AlloyConfig
BasicConfig
GraphConfig
ChangeConfig
AdvConfig
$sel:basicConfig:MathConfig :: MathConfig -> BasicConfig
$sel:advConfig:MathConfig :: MathConfig -> AdvConfig
$sel:changeConfig:MathConfig :: MathConfig -> ChangeConfig
$sel:generatedWrongInstances:MathConfig :: MathConfig -> Int
$sel:graphConfig:MathConfig :: MathConfig -> GraphConfig
$sel:printSolution:MathConfig :: MathConfig -> Bool
$sel:useDifferentGraphLayouts:MathConfig :: MathConfig -> Bool
$sel:wrongInstances:MathConfig :: MathConfig -> Int
$sel:alloyConfig:MathConfig :: MathConfig -> AlloyConfig
$sel:extraText:MathConfig :: MathConfig -> Maybe (Map Language String)
basicConfig :: BasicConfig
advConfig :: AdvConfig
changeConfig :: ChangeConfig
generatedWrongInstances :: Int
graphConfig :: GraphConfig
printSolution :: Bool
useDifferentGraphLayouts :: Bool
wrongInstances :: Int
alloyConfig :: AlloyConfig
extraText :: Maybe (Map Language String)
..} Int
segment Int
seed = Int
-> RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
-> m (MatchInstance (Drawable (p n String)) Math)
forall (m :: * -> *) a. Monad m => Int -> RandT StdGen m a -> m a
evalWithStdGen Int
seed RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
getInstance
  where
    getInstance :: RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
getInstance = do
      [DrawSettings]
allShuffled <- [DrawSettings] -> RandT StdGen m [DrawSettings]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM ([DrawSettings] -> RandT StdGen m [DrawSettings])
-> [DrawSettings] -> RandT StdGen m [DrawSettings]
forall a b. (a -> b) -> a -> b
$ GraphConfig -> [DrawSettings]
allDrawSettings GraphConfig
graphConfig
      (p n String
petri, Math
m, [(p n String, Change)]
changes) <- MathConfig
-> Int -> RandT StdGen m (p n String, Math, [(p n String, Change)])
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n, RandomGen g) =>
MathConfig
-> Int -> RandT g m (p n String, Math, [(p n String, Change)])
matchToMath MathConfig
config Int
segment
      let maths :: [Math]
maths = ((p n String, Change) -> Math) -> [(p n String, Change)] -> [Math]
forall a b. (a -> b) -> [a] -> [b]
map (p n String -> Math
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
p n String -> Math
toPetriMath (p n String -> Math)
-> ((p n String, Change) -> p n String)
-> (p n String, Change)
-> Math
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (p n String, Change) -> p n String
forall a b. (a, b) -> a
fst) [(p n String, Change)]
changes
      Maybe DrawSettings
maybeDrawSettings <- (DrawSettings -> RandT StdGen m Bool)
-> [DrawSettings] -> RandT StdGen m (Maybe DrawSettings)
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
lift (m Bool -> RandT StdGen m Bool)
-> (DrawSettings -> m Bool) -> DrawSettings -> RandT StdGen m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p n String -> DrawSettings -> m Bool
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n) =>
p n String -> DrawSettings -> m Bool
isNetDrawable p n String
petri) [DrawSettings]
allShuffled
      RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
-> (DrawSettings
    -> RandT StdGen m (MatchInstance (Drawable (p n String)) Math))
-> Maybe DrawSettings
-> RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
        RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
getInstance
        (\DrawSettings
d -> MathConfig
-> Drawable (p n String)
-> Math
-> [Math]
-> RandT StdGen m (MatchInstance (Drawable (p n String)) Math)
forall (m :: * -> *) a b.
MonadRandom m =>
MathConfig -> a -> b -> [b] -> m (MatchInstance a b)
matchMathInstance MathConfig
config (p n String
petri, DrawSettings
d) Math
m [Math]
maths)
        Maybe DrawSettings
maybeDrawSettings

mathToGraph
  :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n)
  => MathConfig
  -> Int
  -> Int
  -> m (MatchInstance Math (Drawable (p n String)))
mathToGraph :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n) =>
MathConfig
-> Int -> Int -> m (MatchInstance Math (Drawable (p n String)))
mathToGraph config :: MathConfig
config@MathConfig {Bool
Int
Maybe (Map Language String)
AlloyConfig
BasicConfig
GraphConfig
ChangeConfig
AdvConfig
$sel:basicConfig:MathConfig :: MathConfig -> BasicConfig
$sel:advConfig:MathConfig :: MathConfig -> AdvConfig
$sel:changeConfig:MathConfig :: MathConfig -> ChangeConfig
$sel:generatedWrongInstances:MathConfig :: MathConfig -> Int
$sel:graphConfig:MathConfig :: MathConfig -> GraphConfig
$sel:printSolution:MathConfig :: MathConfig -> Bool
$sel:useDifferentGraphLayouts:MathConfig :: MathConfig -> Bool
$sel:wrongInstances:MathConfig :: MathConfig -> Int
$sel:alloyConfig:MathConfig :: MathConfig -> AlloyConfig
$sel:extraText:MathConfig :: MathConfig -> Maybe (Map Language String)
basicConfig :: BasicConfig
advConfig :: AdvConfig
changeConfig :: ChangeConfig
generatedWrongInstances :: Int
graphConfig :: GraphConfig
printSolution :: Bool
useDifferentGraphLayouts :: Bool
wrongInstances :: Int
alloyConfig :: AlloyConfig
extraText :: Maybe (Map Language String)
..} Int
segment Int
seed = Int
-> RandT StdGen m (MatchInstance Math (Drawable (p n String)))
-> m (MatchInstance Math (Drawable (p n String)))
forall (m :: * -> *) a. Monad m => Int -> RandT StdGen m a -> m a
evalWithStdGen Int
seed RandT StdGen m (MatchInstance Math (Drawable (p n String)))
getInstance
  where
    getInstance :: RandT StdGen m (MatchInstance Math (Drawable (p n String)))
getInstance = do
      (p n String
petri, Math
math, [(p n String, Change)]
changes) <- MathConfig
-> Int -> RandT StdGen m (p n String, Math, [(p n String, Change)])
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n, RandomGen g) =>
MathConfig
-> Int -> RandT g m (p n String, Math, [(p n String, Change)])
matchToMath MathConfig
config Int
segment
      let petriNets :: [p n String]
petriNets = ((p n String, Change) -> p n String)
-> [(p n String, Change)] -> [p n String]
forall a b. (a -> b) -> [a] -> [b]
map (p n String, Change) -> p n String
forall a b. (a, b) -> a
fst [(p n String, Change)]
changes
          allPetriNets :: [p n String]
allPetriNets = p n String
petri p n String -> [p n String] -> [p n String]
forall a. a -> [a] -> [a]
: [p n String]
petriNets
          predicates :: [DrawSettings -> RandT StdGen m Bool]
predicates = (p n String -> DrawSettings -> RandT StdGen m Bool)
-> [p n String] -> [DrawSettings -> RandT StdGen m Bool]
forall a b. (a -> b) -> [a] -> [b]
map (\p n String
x -> 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
lift (m Bool -> RandT StdGen m Bool)
-> (DrawSettings -> m Bool) -> DrawSettings -> RandT StdGen m Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. p n String -> DrawSettings -> m Bool
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n) =>
p n String -> DrawSettings -> m Bool
isNetDrawable p n String
x) [p n String]
allPetriNets
          availableLayouts :: [DrawSettings]
availableLayouts = GraphConfig -> [DrawSettings]
allDrawSettings GraphConfig
graphConfig
      Maybe [DrawSettings]
maybeDrawSettings <- Bool
-> [DrawSettings]
-> [DrawSettings -> RandT StdGen m Bool]
-> RandT StdGen m (Maybe [DrawSettings])
forall (m :: * -> *) a.
MonadRandom m =>
Bool -> [a] -> [a -> m Bool] -> m (Maybe [a])
findFittingRandomElements Bool
useDifferentGraphLayouts [DrawSettings]
availableLayouts [DrawSettings -> RandT StdGen m Bool]
predicates
      case Maybe [DrawSettings]
maybeDrawSettings of
        Just (DrawSettings
d : [DrawSettings]
ds) ->
          MathConfig
-> Math
-> Drawable (p n String)
-> [Drawable (p n String)]
-> RandT StdGen m (MatchInstance Math (Drawable (p n String)))
forall (m :: * -> *) a b.
MonadRandom m =>
MathConfig -> a -> b -> [b] -> m (MatchInstance a b)
matchMathInstance MathConfig
config Math
math (p n String
petri, DrawSettings
d) ([Drawable (p n String)]
 -> RandT StdGen m (MatchInstance Math (Drawable (p n String))))
-> [Drawable (p n String)]
-> RandT StdGen m (MatchInstance Math (Drawable (p n String)))
forall a b. (a -> b) -> a -> b
$ [p n String] -> [DrawSettings] -> [Drawable (p n String)]
forall a b. [a] -> [b] -> [(a, b)]
zip [p n String]
petriNets [DrawSettings]
ds
        Just [] -> String
-> RandT StdGen m (MatchInstance Math (Drawable (p n String)))
forall a. HasCallStack => String -> a
error String
"impossible"
        Maybe [DrawSettings]
Nothing -> RandT StdGen m (MatchInstance Math (Drawable (p n String)))
getInstance

matchMathInstance
  :: MonadRandom m
  => MathConfig
  -> a
  -> b
  -> [b]
  -> m (MatchInstance a b)
matchMathInstance :: forall (m :: * -> *) a b.
MonadRandom m =>
MathConfig -> a -> b -> [b] -> m (MatchInstance a b)
matchMathInstance MathConfig
c a
x b
y [b]
ys = do
  [(Bool, b)]
ys' <- [(Bool, b)] -> m [(Bool, b)]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM ([(Bool, b)] -> m [(Bool, b)]) -> [(Bool, b)] -> m [(Bool, b)]
forall a b. (a -> b) -> a -> b
$ (Bool
True, b
y) (Bool, b) -> [(Bool, b)] -> [(Bool, b)]
forall a. a -> [a] -> [a]
: (b -> (Bool, b)) -> [b] -> [(Bool, b)]
forall a b. (a -> b) -> [a] -> [b]
map (Bool
False,) [b]
ys
  return $ MatchInstance {
    $sel:from:MatchInstance :: a
from = a
x,
    $sel:showSolution:MatchInstance :: Bool
showSolution = MathConfig -> Bool
printSolution MathConfig
c,
    $sel:to:MatchInstance :: Map Int (Bool, b)
to = [(Int, (Bool, b))] -> Map Int (Bool, b)
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(Int, (Bool, b))] -> Map Int (Bool, b))
-> [(Int, (Bool, b))] -> Map Int (Bool, b)
forall a b. (a -> b) -> a -> b
$ [Int] -> [(Bool, b)] -> [(Int, (Bool, b))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] [(Bool, b)]
ys',
    $sel:addText:MatchInstance :: Maybe (Map Language String)
addText = MathConfig -> Maybe (Map Language String)
extraText MathConfig
c
    }

matchToMath
  :: (
    MonadAlloy m,
    MonadCatch m,
    MonadDiagrams m,
    MonadGraphviz m,
    Net p n,
    RandomGen g
    )
  => MathConfig
  -> Int
  -> RandT g m (p n String, Math, [(p n String, Change)])
matchToMath :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n, RandomGen g) =>
MathConfig
-> Int -> RandT g m (p n String, Math, [(p n String, Change)])
matchToMath MathConfig
config Int
segment = do
  (String
f, p n String
net, Math
math) <- MathConfig -> Int -> RandT g m (String, p n String, Math)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
MathConfig -> Int -> RandT g m (String, p n String, Math)
netMathInstance MathConfig
config Int
segment
  [AlloyInstance]
fList <- Maybe Integer -> Maybe Int -> String -> RandT g m [AlloyInstance]
forall (m :: * -> *).
MonadAlloy m =>
Maybe Integer -> Maybe Int -> String -> m [AlloyInstance]
getInstances
    (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Int -> Integer
forall a. Integral a => a -> Integer
toInteger (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ MathConfig -> Int
generatedWrongInstances MathConfig
config)
    Maybe Int
forall a. Maybe a
Nothing
    String
f
  [AlloyInstance]
fList' <- Int -> [AlloyInstance] -> [AlloyInstance]
forall a. Int -> [a] -> [a]
take (MathConfig -> Int
wrongInstances MathConfig
config) ([AlloyInstance] -> [AlloyInstance])
-> RandT g m [AlloyInstance] -> RandT g m [AlloyInstance]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [AlloyInstance] -> RandT g m [AlloyInstance]
forall (m :: * -> *) a. MonadRandom m => [a] -> m [a]
shuffleM [AlloyInstance]
fList
  if MathConfig -> Int
wrongInstances MathConfig
config Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [AlloyInstance] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AlloyInstance]
fList'
    then do
    [(AlloyInstance, Change)]
alloyChanges <- (AlloyInstance -> RandT g m (AlloyInstance, Change))
-> [AlloyInstance] -> RandT g m [(AlloyInstance, Change)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM AlloyInstance -> RandT g m (AlloyInstance, Change)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (AlloyInstance, Change)
addChange [AlloyInstance]
fList'
    [(p n String, Change)]
changes <- (AlloyInstance -> RandT g m (p n String))
-> (AlloyInstance, Change) -> RandT g m (p n String, Change)
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (a, c) -> m (b, c)
firstM AlloyInstance -> RandT g m (p n String)
parse ((AlloyInstance, Change) -> RandT g m (p n String, Change))
-> [(AlloyInstance, Change)] -> RandT g m [(p n String, Change)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
`mapM` [(AlloyInstance, Change)]
alloyChanges
    let changes' :: [(p n String, Change)]
changes' = ([p n String] -> [Change] -> [(p n String, Change)])
-> ([p n String], [Change]) -> [(p n String, Change)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [p n String] -> [Change] -> [(p n String, Change)]
forall a b. [a] -> [b] -> [(a, b)]
zip (([p n String], [Change]) -> [(p n String, Change)])
-> ([p n String], [Change]) -> [(p n String, Change)]
forall a b. (a -> b) -> a -> b
$ [(p n String, Change)] -> ([p n String], [Change])
forall a b. [(a, b)] -> ([a], [b])
unzip [(p n String, Change)]
changes
    (p n String, Math, [(p n String, Change)])
-> RandT g m (p n String, Math, [(p n String, Change)])
forall a. a -> RandT g m a
forall (f :: * -> *) a. Applicative f => a -> f a
return (p n String
net, Math
math, [(p n String, Change)]
changes')
    else MathConfig
-> Int -> RandT g m (p n String, Math, [(p n String, Change)])
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n, RandomGen g) =>
MathConfig
-> Int -> RandT g m (p n String, Math, [(p n String, Change)])
matchToMath MathConfig
config Int
segment
  where
    parse :: AlloyInstance -> RandT g m (p n String)
parse = String -> String -> AlloyInstance -> RandT g m (p n String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadThrow m, Net p n) =>
String -> String -> AlloyInstance -> m (p n String)
parseRenamedNet String
"flow" String
"tokens"

firstM :: Monad m => (a -> m b) -> (a, c) -> m (b, c)
firstM :: forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (a, c) -> m (b, c)
firstM a -> m b
f (a
p, c
c) = (,c
c) (b -> (b, c)) -> m b -> m (b, c)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> m b
f a
p

netMathInstance
  :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g)
  => MathConfig
  -> Int
  -> RandT g m (String, p n String, Math)
netMathInstance :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
MathConfig -> Int -> RandT g m (String, p n String, Math)
netMathInstance MathConfig
config = (MathConfig
 -> AlloyInstance -> RandT g m (String, p n String, Math))
-> (MathConfig -> String)
-> MathConfig
-> (MathConfig -> AlloyConfig)
-> MathConfig
-> Int
-> RandT g m (String, p n String, Math)
forall (m :: * -> *) g f a config.
(MonadThrow m, RandomGen g, MonadAlloy m) =>
(f -> AlloyInstance -> RandT g m a)
-> (config -> String)
-> f
-> (config -> AlloyConfig)
-> config
-> Int
-> RandT g m a
taskInstance
  MathConfig -> AlloyInstance -> RandT g m (String, p n String, Math)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
MathConfig -> AlloyInstance -> RandT g m (String, p n String, Math)
mathInstance
  (\MathConfig
c -> BasicConfig -> AdvConfig -> String
petriNetRnd (MathConfig -> BasicConfig
basicConfig MathConfig
c) (MathConfig -> AdvConfig
advConfig MathConfig
c))
  MathConfig
config
  (\MathConfig
c -> MathConfig -> AlloyConfig
alloyConfig (MathConfig
c :: MathConfig))
  MathConfig
config

mathInstance
  :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g)
  => MathConfig
  -> AlloyInstance
  -> RandT g m (String, p n String, Math)
mathInstance :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
MathConfig -> AlloyInstance -> RandT g m (String, p n String, Math)
mathInstance MathConfig
config AlloyInstance
inst = do
  p n String
petriLike <- String -> String -> AlloyInstance -> RandT g m (p n String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadThrow m, Net p n) =>
String -> String -> AlloyInstance -> m (p n String)
parseRenamedNet String
"flow" String
"tokens" AlloyInstance
inst
  p n String
petriLike' <- (p n String, Bimap String String) -> p n String
forall a b. (a, b) -> a
fst ((p n String, Bimap String String) -> p n String)
-> RandT g m (p n String, Bimap String String)
-> RandT g m (p n String)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> p n String -> RandT g m (p n String, Bimap String String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) a g.
(MonadThrow m, Net p n, Ord a, RandomGen g) =>
p n a -> RandT g m (p n a, Bimap a a)
shuffleNames p n String
petriLike
  let math :: Math
math = p n String -> Math
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
p n String -> Math
toPetriMath p n String
petriLike'
  let f :: String
f = p n String -> MathConfig -> String
forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
p n String -> MathConfig -> String
renderFalse p n String
petriLike' MathConfig
config
  (String, p n String, Math) -> RandT g m (String, p n String, Math)
forall a. a -> RandT g m a
forall (f :: * -> *) a. Applicative f => a -> f a
return (String
f, p n String
petriLike', Math
math)

graphToMathTask
  :: (MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m, OutputCapable m)
  => FilePath
  -> GraphToMathInstance
  -> LangM m
graphToMathTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
String -> GraphToMathInstance -> LangM m
graphToMathTask String
path GraphToMathInstance
task = 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
"Consider the following graphical representation of a Petri net:"
    String -> State (Map Language String) ()
german String
"Betrachten Sie folgende grafische Darstellung eines Petrinetzes:"
  String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
image (String -> LangM m) -> m String -> LangM m
forall (m :: * -> *) a l b.
Monad m =>
(a -> GenericLangM l m b) -> m a -> GenericLangM l m b
$=<< MatchInstance String Math -> String
forall a b. MatchInstance a b -> a
from (MatchInstance String Math -> String)
-> m (MatchInstance String Math) -> m String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> GraphToMathInstance -> m (MatchInstance String Math)
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *) b.
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
String
-> MatchInstance (Drawable (p n String)) b
-> m (MatchInstance String b)
writeDia String
path GraphToMathInstance
task
  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
"Which of the following mathematical representations denotes this Petri net?"
    String -> State (Map Language String) ()
german String
"Welche der folgenden mathematischen Repräsentationen formalisiert dieses Petrinetz?"
  (Int -> LangM m) -> [(Int, LangM m)] -> LangM m
forall a. (a -> LangM m) -> [(a, LangM m)] -> LangM m
forall l (m :: * -> *) a.
GenericOutputCapable l m =>
(a -> GenericLangM l m ())
-> [(a, GenericLangM l m ())] -> GenericLangM l m ()
enumerateM
    (String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
text (String -> LangM m) -> (Int -> String) -> Int -> LangM m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
". ") (String -> String) -> (Int -> String) -> Int -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> String
forall a. Show a => a -> String
show)
    ([(Int, LangM m)] -> LangM m) -> [(Int, LangM m)] -> LangM m
forall a b. (a -> b) -> a -> b
$ ((Int, (Bool, Math)) -> (Int, LangM m))
-> [(Int, (Bool, Math))] -> [(Int, LangM m)]
forall a b. (a -> b) -> [a] -> [b]
map (((Bool, Math) -> LangM m) -> (Int, (Bool, Math)) -> (Int, LangM m)
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 ((String -> LangM m) -> Math -> LangM m
forall (m :: * -> *) a.
OutputCapable m =>
(a -> LangM m) -> PetriMath a -> LangM m
mathToOutput String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
latex (Math -> LangM m)
-> ((Bool, Math) -> Math) -> (Bool, Math) -> LangM m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool, Math) -> Math
forall a b. (a, b) -> b
snd)) ([(Int, (Bool, Math))] -> [(Int, LangM m)])
-> [(Int, (Bool, Math))] -> [(Int, LangM m)]
forall a b. (a -> b) -> a -> b
$ Map Int (Bool, Math) -> [(Int, (Bool, Math))]
forall k a. Map k a -> [(k, a)]
toList (GraphToMathInstance -> Map Int (Bool, Math)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to GraphToMathInstance
task)
  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|Please state your answer by giving the number of the matching representation only.|]
    String -> State (Map Language String) ()
german [i|Geben Sie Ihre Antwort durch Angabe der Nummer der passenden Repräsentation an.|]
  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
$ 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 [i|Stating |]
      String -> State (Map Language String) ()
german [i|Die Angabe von |]
    String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
code String
"1"
    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| as answer would indicate that representation 1 matches the given graphical representation (and the other mathematical representations don't).|]
      String -> State (Map Language String) ()
german [i| als Antwort würde bedeuten, dass Repräsentation 1 zur gegebenen grafischen Darstellung passt (und die anderen mathematischen Repräsentationen nicht).|]
    pure ()
  LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph LangM m
forall (m :: * -> *). OutputCapable m => LangM m
hoveringInformation
  Maybe (Map Language String) -> LangM m
forall (m :: * -> *).
OutputCapable m =>
Maybe (Map Language String) -> LangM m
extra (Maybe (Map Language String) -> LangM m)
-> Maybe (Map Language String) -> LangM m
forall a b. (a -> b) -> a -> b
$ GraphToMathInstance -> Maybe (Map Language String)
forall a b. MatchInstance a b -> Maybe (Map Language String)
addText GraphToMathInstance
task
  pure ()

mathToOutput :: OutputCapable m => (a -> LangM m) -> PetriMath a -> LangM m
mathToOutput :: forall (m :: * -> *) a.
OutputCapable m =>
(a -> LangM m) -> PetriMath a -> LangM m
mathToOutput a -> LangM m
f PetriMath a
pm = 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
$ do
  a -> LangM m
f (a -> LangM m) -> a -> LangM m
forall a b. (a -> b) -> a -> b
$ PetriMath a -> a
forall a. PetriMath a -> a
netMath PetriMath a
pm
  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
", where "
    String -> State (Map Language String) ()
german String
", mit "
  a -> LangM m
f (a -> LangM m) -> a -> LangM m
forall a b. (a -> b) -> a -> b
$ PetriMath a -> a
forall a. PetriMath a -> a
placesMath PetriMath a
pm
  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
" and "
    String -> State (Map Language String) ()
german String
" und "
  a -> LangM m
f (a -> LangM m) -> a -> LangM m
forall a b. (a -> b) -> a -> b
$ PetriMath a -> a
forall a. PetriMath a -> a
transitionsMath PetriMath a
pm
  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
", as well as"
    String -> State (Map Language String) ()
german String
", sowie"
  case PetriMath a -> Maybe a
forall a. PetriMath a -> Maybe a
placeOrderMath PetriMath a
pm of
    Maybe a
Nothing -> () -> LangM m
forall a. a -> GenericLangM Language m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just a
o  -> 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
" using the place ordering "
        String -> State (Map Language String) ()
german String
" mit der Stellenreihenfolge "
      a -> LangM m
f a
o
      pure ()
  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
$ String -> State (Map Language String) ()
english String
":"
  [LangM m] -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
[GenericLangM l m ()] -> GenericLangM l m ()
itemizeM ([LangM m] -> LangM m) -> [LangM m] -> LangM m
forall a b. (a -> b) -> a -> b
$ ((a, a) -> LangM m) -> [(a, a)] -> [LangM m]
forall a b. (a -> b) -> [a] -> [b]
map (a -> LangM m
f (a -> LangM m) -> ((a, a) -> a) -> (a, a) -> LangM m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a) -> a
forall a b. (a, b) -> a
fst) ([(a, a)] -> [LangM m]) -> [(a, a)] -> [LangM m]
forall a b. (a -> b) -> a -> b
$ PetriMath a -> [(a, a)]
forall a. PetriMath a -> [(a, a)]
tokenChangeMath PetriMath a
pm
  [LangM m] -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
[GenericLangM l m ()] -> GenericLangM l m ()
itemizeM ([LangM m] -> LangM m) -> [LangM m] -> LangM m
forall a b. (a -> b) -> a -> b
$ ((a, a) -> LangM m) -> [(a, a)] -> [LangM m]
forall a b. (a -> b) -> [a] -> [b]
map (a -> LangM m
f (a -> LangM m) -> ((a, a) -> a) -> (a, a) -> LangM m
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a, a) -> a
forall a b. (a, b) -> b
snd) ([(a, a)] -> [LangM m]) -> [(a, a)] -> [LangM m]
forall a b. (a -> b) -> a -> b
$ PetriMath a -> [(a, a)]
forall a. PetriMath a -> [(a, a)]
tokenChangeMath PetriMath a
pm
  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
"Moreover, "
    String -> State (Map Language String) ()
german String
"und "
  a -> LangM m
f (a -> LangM m) -> a -> LangM m
forall a b. (a -> b) -> a -> b
$ PetriMath a -> a
forall a. PetriMath a -> a
initialMarkingMath PetriMath a
pm
  pure ()

mathToGraphTask
  :: (MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m, OutputCapable m)
  => FilePath
  -> MathToGraphInstance
  -> LangM m
mathToGraphTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
String -> MathToGraphInstance -> LangM m
mathToGraphTask String
path MathToGraphInstance
task = 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
"Consider the following mathematical representation of a Petri net:"
    String -> State (Map Language String) ()
german String
"Betrachten Sie folgende mathematische Repräsentation eines Petrinetzes:"
  (String -> LangM m) -> Math -> LangM m
forall (m :: * -> *) a.
OutputCapable m =>
(a -> LangM m) -> PetriMath a -> LangM m
mathToOutput String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
latex (Math -> LangM m) -> Math -> LangM m
forall a b. (a -> b) -> a -> b
$ MathToGraphInstance -> Math
forall a b. MatchInstance a b -> a
from MathToGraphInstance
task
  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
"Which of the following diagrams represents this Petri net?"
    String -> State (Map Language String) ()
german String
"Welches der folgenden Diagramme stellt dieses Petrinetz dar?"
  (Int -> String)
-> ((Bool, String) -> String) -> Map Int (Bool, String) -> LangM m
forall k a. (k -> String) -> (a -> String) -> Map k a -> LangM m
forall l (m :: * -> *) k a.
GenericOutputCapable l m =>
(k -> String) -> (a -> String) -> Map k a -> GenericLangM l m ()
images Int -> String
forall a. Show a => a -> String
show (Bool, String) -> String
forall a b. (a, b) -> b
snd (Map Int (Bool, String) -> LangM m)
-> m (Map Int (Bool, String)) -> LangM m
forall (m :: * -> *) a l b.
Monad m =>
(a -> GenericLangM l m b) -> m a -> GenericLangM l m b
$=<< MatchInstance Math String -> Map Int (Bool, String)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to (MatchInstance Math String -> Map Int (Bool, String))
-> m (MatchInstance Math String) -> m (Map Int (Bool, String))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> String -> MathToGraphInstance -> m (MatchInstance Math String)
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *) a.
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, Typeable n, Typeable p) =>
String
-> MatchInstance a (Drawable (p n String))
-> m (MatchInstance a String)
writeDias String
path MathToGraphInstance
task
  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|Please state your answer by giving the number of the matching diagram only.|]
    String -> State (Map Language String) ()
german [i|Geben Sie Ihre Antwort durch Angabe der Nummer des passenden Diagramms an.|]
  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
$ 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 [i|Stating |]
      String -> State (Map Language String) ()
german [i|Die Angabe von |]
    String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
code String
"1"
    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| as answer would indicate that diagram 1 matches the given mathematical representation (and the other diagrams don't).|]
      String -> State (Map Language String) ()
german [i| als Antwort würde bedeuten, dass Diagramm 1 zur gegebenen mathematischen Repräsentation passt (und die anderen Diagramme nicht).|]
    pure ()
  LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph LangM m
forall (m :: * -> *). OutputCapable m => LangM m
hoveringInformation
  Maybe (Map Language String) -> LangM m
forall (m :: * -> *).
OutputCapable m =>
Maybe (Map Language String) -> LangM m
extra (Maybe (Map Language String) -> LangM m)
-> Maybe (Map Language String) -> LangM m
forall a b. (a -> b) -> a -> b
$ MathToGraphInstance -> Maybe (Map Language String)
forall a b. MatchInstance a b -> Maybe (Map Language String)
addText MathToGraphInstance
task
  pure ()

graphToMathSyntax
  :: OutputCapable m
  => GraphToMathInstance
  -> Int
  -> LangM m
graphToMathSyntax :: forall (m :: * -> *).
OutputCapable m =>
GraphToMathInstance -> Int -> LangM m
graphToMathSyntax GraphToMathInstance
task Int
x =
  Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> GenericLangM l m () -> GenericLangM l m ()
assertion (Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Map Int (Bool, Math) -> Int
forall a. Map Int a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (GraphToMathInstance -> Map Int (Bool, Math)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to GraphToMathInstance
task)) (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
"The indicated mathematical representation is part of the task?"
    String -> State (Map Language String) ()
german String
"Die angegebene mathematische Repräsentation ist Bestandteil der Aufgabenstellung?"

graphToMathEvaluation
  :: OutputCapable m
  => GraphToMathInstance
  -> Int
  -> LangM m
graphToMathEvaluation :: forall (m :: * -> *).
OutputCapable m =>
GraphToMathInstance -> Int -> LangM m
graphToMathEvaluation = do
  let what :: Map Language String
what = 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
"mathematical representation"
        String -> State (Map Language String) ()
german String
"mathematische Repräsentation"
  Map Language String -> GraphToMathInstance -> Int -> LangM m
forall (m :: * -> *) a b.
OutputCapable m =>
Map Language String -> MatchInstance a b -> Int -> LangM m
evaluation Map Language String
what

matchSolution :: MatchInstance a b -> Int
matchSolution :: forall a b. MatchInstance a b -> Int
matchSolution = [Int] -> Int
forall a. HasCallStack => [a] -> a
head ([Int] -> Int)
-> (MatchInstance a b -> [Int]) -> MatchInstance a b -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Int (Bool, b) -> [Int]
forall k a. Map k a -> [k]
M.keys (Map Int (Bool, b) -> [Int])
-> (MatchInstance a b -> Map Int (Bool, b))
-> MatchInstance a b
-> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Bool, b) -> Bool) -> Map Int (Bool, b) -> Map Int (Bool, b)
forall a k. (a -> Bool) -> Map k a -> Map k a
M.filter (Bool, b) -> Bool
forall a b. (a, b) -> a
fst (Map Int (Bool, b) -> Map Int (Bool, b))
-> (MatchInstance a b -> Map Int (Bool, b))
-> MatchInstance a b
-> Map Int (Bool, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MatchInstance a b -> Map Int (Bool, b)
forall a b. MatchInstance a b -> Map Int (Bool, b)
to

mathToGraphSyntax
  :: OutputCapable m
  => MathToGraphInstance
  -> Int
  -> LangM m
mathToGraphSyntax :: forall (m :: * -> *).
OutputCapable m =>
MathToGraphInstance -> Int -> LangM m
mathToGraphSyntax MathToGraphInstance
task Int
x =
  Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
Bool -> GenericLangM l m () -> GenericLangM l m ()
assertion (Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
x Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Map Int (Bool, Drawable (PetriLike SimpleNode String)) -> Int
forall a. Map Int a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (MathToGraphInstance
-> Map Int (Bool, Drawable (PetriLike SimpleNode String))
forall a b. MatchInstance a b -> Map Int (Bool, b)
to MathToGraphInstance
task)) (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
"The indicated graphical representation is part of the task?"
    String -> State (Map Language String) ()
german String
"Die angegebene grafische Repräsentation ist Bestandteil der Aufgabenstellung?"

mathToGraphEvaluation
  :: OutputCapable m
  => MathToGraphInstance
  -> Int
  -> LangM m
mathToGraphEvaluation :: forall (m :: * -> *).
OutputCapable m =>
MathToGraphInstance -> Int -> LangM m
mathToGraphEvaluation = do
  let what :: Map Language String
what = 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
"graphical representation"
        String -> State (Map Language String) ()
german String
"grafische Darstellung"
  Map Language String -> MathToGraphInstance -> Int -> LangM m
forall (m :: * -> *) a b.
OutputCapable m =>
Map Language String -> MatchInstance a b -> Int -> LangM m
evaluation Map Language String
what

evaluation
  :: OutputCapable m
  => Map Language String
  -> MatchInstance a b
  -> Int
  -> LangM m
evaluation :: forall (m :: * -> *) a b.
OutputCapable m =>
Map Language String -> MatchInstance a b -> Int -> LangM m
evaluation Map Language String
what MatchInstance a b
task = do
  let solution :: Int
solution = MatchInstance a b -> Int
forall a b. MatchInstance a b -> Int
matchSolution MatchInstance a b
task
      maybeSolution :: Maybe String
maybeSolution =
        if MatchInstance a b -> Bool
forall a b. MatchInstance a b -> Bool
showSolution MatchInstance a b
task
        then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
solution
        else Maybe String
forall a. Maybe a
Nothing
  ArticleToUse
-> Map Language String -> Maybe String -> Int -> Int -> LangM m
forall (m :: * -> *) a.
(OutputCapable m, Eq a) =>
ArticleToUse
-> Map Language String -> Maybe String -> a -> a -> LangM m
singleChoice ArticleToUse
DefiniteArticle Map Language String
what Maybe String
maybeSolution Int
solution

checkGraphToMathConfig :: MathConfig -> Maybe String
checkGraphToMathConfig :: MathConfig -> Maybe String
checkGraphToMathConfig c :: MathConfig
c@MathConfig {
  Bool
$sel:useDifferentGraphLayouts:MathConfig :: MathConfig -> Bool
useDifferentGraphLayouts :: Bool
useDifferentGraphLayouts
  }
  | Bool
useDifferentGraphLayouts
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"Setting useDifferentGraphLayouts to True is not supported for this task type."
  | Bool
otherwise
  = MathConfig -> Maybe String
checkMathConfig MathConfig
c

checkMathConfig :: MathConfig -> Maybe String
checkMathConfig :: MathConfig -> Maybe String
checkMathConfig c :: MathConfig
c@MathConfig {
  BasicConfig
$sel:basicConfig:MathConfig :: MathConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  ChangeConfig
$sel:changeConfig:MathConfig :: MathConfig -> ChangeConfig
changeConfig :: ChangeConfig
changeConfig,
  GraphConfig
$sel:graphConfig:MathConfig :: MathConfig -> GraphConfig
graphConfig :: GraphConfig
graphConfig,
  Bool
$sel:useDifferentGraphLayouts:MathConfig :: MathConfig -> Bool
useDifferentGraphLayouts :: Bool
useDifferentGraphLayouts,
  Int
$sel:wrongInstances:MathConfig :: MathConfig -> Int
wrongInstances :: Int
wrongInstances
  } = BasicConfig -> Maybe String
checkBasicConfig BasicConfig
basicConfig
  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
<|> GraphConfig -> Maybe String
prohibitHideNames GraphConfig
graphConfig
  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
<|> BasicConfig -> ChangeConfig -> Maybe String
checkChangeConfig BasicConfig
basicConfig ChangeConfig
changeConfig
  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
<|> MathConfig -> Maybe String
checkConfig MathConfig
c
  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
<|> Bool -> Int -> GraphConfig -> Maybe String
checkGraphLayouts Bool
useDifferentGraphLayouts Int
wrongInstances GraphConfig
graphConfig

prohibitHideNames :: GraphConfig -> Maybe String
prohibitHideNames :: GraphConfig -> Maybe String
prohibitHideNames GraphConfig
gc
  | GraphConfig -> Bool
hidePlaceNames GraphConfig
gc
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"Place names are required for this task type"
  | GraphConfig -> Bool
hideTransitionNames GraphConfig
gc
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"Transition names are required for this task type"
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing

checkConfig :: MathConfig -> Maybe String
checkConfig :: MathConfig -> Maybe String
checkConfig MathConfig {
  Int
$sel:generatedWrongInstances:MathConfig :: MathConfig -> Int
generatedWrongInstances :: Int
generatedWrongInstances,
  Int
$sel:wrongInstances:MathConfig :: MathConfig -> Int
wrongInstances :: Int
wrongInstances
  }
  | Int
wrongInstances Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"There has to be at least one wrongInstance"
  | Int
generatedWrongInstances Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
wrongInstances
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"generatedWrongInstances must not be lower than wrongInstances"
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing

addChange :: MonadThrow m => AlloyInstance -> m (AlloyInstance, Change)
addChange :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (AlloyInstance, Change)
addChange AlloyInstance
alloy = do
  PetriChange Object
change <- AlloyInstance -> m (PetriChange Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (PetriChange Object)
parseChange AlloyInstance
alloy
  return (AlloyInstance
alloy, (Object -> String) -> PetriChange Object -> Change
forall b a. Ord b => (a -> b) -> PetriChange a -> PetriChange b
mapChange Object -> String
oName PetriChange Object
change)

petriNetRnd :: BasicConfig -> AdvConfig -> String
petriNetRnd :: BasicConfig -> AdvConfig -> String
petriNetRnd basicC :: BasicConfig
basicC@BasicConfig{Int
places :: Int
$sel:places:BasicConfig :: BasicConfig -> Int
places,Int
transitions :: Int
$sel:transitions:BasicConfig :: BasicConfig -> Int
transitions} AdvConfig
advConfig = [i|module PetriNetRnd

#{modulePetriSignature}
#{modulePetriAdditions}
#{moduleHelpers}
#{modulePetriConcepts}
#{modulePetriConstraints}
#{signatures "added" places transitions}

fact{
  no givenPlaces
  no givenTransitions
}

pred showNets[#{activated} : set Transitions] {
  \#Places = #{places}
  \#Transitions = #{transitions}
  #{compBasicConstraints activated basicC}
  #{compAdvConstraints advConfig}
}
run showNets for exactly #{petriScopeMaxSeq basicC} Nodes, #{petriScopeBitWidth basicC} Int
|]
  where
    activated :: String
activated = String
"activatedTrans"

renderFalse :: Net p n => p n String -> MathConfig -> String
renderFalse :: forall (p :: (* -> *) -> * -> *) (n :: * -> *).
Net p n =>
p n String -> MathConfig -> String
renderFalse
  p n String
net
  MathConfig {BasicConfig
$sel:basicConfig:MathConfig :: MathConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig, AdvConfig
$sel:advConfig:MathConfig :: MathConfig -> AdvConfig
advConfig :: AdvConfig
advConfig, ChangeConfig
$sel:changeConfig:MathConfig :: MathConfig -> ChangeConfig
changeConfig :: ChangeConfig
changeConfig} = [i|module FalseNet

#{modulePetriSignature}
#{moduleHelpers}
#{modulePetriConcepts}
#{modulePetriConstraints}

#{places}
#{transitions}

fact{
#{initialMark}
#{defaultFlow}
}

pred showFalseNets[#{activated} : set Transitions]{
  #{compBasicConstraints activated basicConfig}
  #{compAdvConstraints advConfig}
  #{compChange changeConfig}
}

run showFalseNets for exactly #{petriScopeMaxSeq basicConfig} Nodes, #{petriScopeBitWidth basicConfig} Int
|]
  where
    allNodes :: Map String (n String)
allNodes    = p n String -> Map String (n String)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
nodes p n String
net
    (Map String (n String)
ps, Map String (n String)
ts)    = (n String -> Bool)
-> Map String (n String)
-> (Map String (n String), Map String (n String))
forall a k. (a -> Bool) -> Map k a -> (Map k a, Map k a)
M.partition n String -> Bool
forall a. n a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isPlaceNode Map String (n String)
allNodes
    activated :: String
activated   = String
"activatedTrans"
    places :: String
places      = [String] -> String
unlines [String -> String -> String
extendLine String
p String
"givenPlaces" | String
p <- Map String (n String) -> [String]
forall k a. Map k a -> [k]
M.keys Map String (n String)
ps]
    transitions :: String
transitions = [String] -> String
unlines [String -> String -> String
extendLine String
t String
"givenTransitions" | String
t <- Map String (n String) -> [String]
forall k a. Map k a -> [k]
M.keys Map String (n String)
ts]
    initialMark :: String
initialMark = (String -> Int -> String -> String)
-> String -> Map String Int -> String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey (\String
k -> String -> String -> String
forall a. [a] -> [a] -> [a]
(++) (String -> String -> String)
-> (Int -> String) -> Int -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Int -> String
tokenLine String
k) String
"" (Map String Int -> String) -> Map String Int -> String
forall a b. (a -> b) -> a -> b
$ n String -> Int
forall a. n a -> Int
forall (n :: * -> *) a. PetriNode n => n a -> Int
initialTokens (n String -> Int) -> Map String (n String) -> Map String Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map String (n String)
ps
    defaultFlow :: String
defaultFlow = (String -> n String -> String -> String)
-> String -> Map String (n String) -> String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey (\String
k n String
_ -> (String -> String
printFlow String
k String -> String -> String
forall a. [a] -> [a] -> [a]
++)) String
"" Map String (n String)
allNodes
    printFlow :: String -> String
    printFlow :: String -> String
printFlow String
x = (String -> n String -> String -> String)
-> String -> Map String (n String) -> String
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
M.foldrWithKey
      (\String
y n String
_ -> String -> String -> String
forall a. [a] -> [a] -> [a]
(++) (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> Maybe Int -> String
flowLine String
x String
y (Maybe Int -> String) -> Maybe Int -> String
forall a b. (a -> b) -> a -> b
$ String -> String -> p n String -> Maybe Int
forall a. Ord a => a -> a -> p n a -> Maybe Int
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> a -> p n a -> Maybe Int
flow String
x String
y p n String
net)
      String
""
      Map String (n String)
allNodes
    extendLine :: String -> String -> String
    extendLine :: String -> String -> String
extendLine String
n String
k = [i|one sig #{n} extends #{k}{}
|]
    tokenLine :: String -> Int -> String
    tokenLine :: String -> Int -> String
tokenLine String
k Int
l = [i|  #{k}.defaultTokens = #{l}
|]
    flowLine :: String -> String -> Maybe Int -> String
    flowLine :: String -> String -> Maybe Int -> String
flowLine String
from String
to Maybe Int
Nothing  = [i|  no #{from}.defaultFlow[#{to}]
|]
    flowLine String
from String
to (Just Int
f) = [i|  #{from}.defaultFlow[#{to}] = #{f}
|]

defaultGraphToMathInstance :: GraphToMathInstance
defaultGraphToMathInstance :: GraphToMathInstance
defaultGraphToMathInstance = MatchInstance {
  $sel:from:MatchInstance :: Drawable (PetriLike SimpleNode String)
from = (
    PetriLike {
      $sel:allNodes:PetriLike :: Map String (SimpleNode String)
allNodes = [(String, SimpleNode String)] -> Map String (SimpleNode String)
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
        (String
"s1",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
2, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t3",Int
1)]}),
        (String
"s2",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
0, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t1",Int
1),(String
"t2",Int
1)]}),
        (String
"s3",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
        (String
"s4",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
0, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
        (String
"t1",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s3",Int
1)]}),
        (String
"t2",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s4",Int
1)]}),
        (String
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s3",Int
1)]})
        ]
      },
    DrawSettings {
      $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
True,
      $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
      $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
True,
      $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
      $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Sfdp
      }
    ),
  $sel:showSolution:MatchInstance :: Bool
showSolution = Bool
False,
  $sel:to:MatchInstance :: Map Int (Bool, Math)
to = [(Int, (Bool, Math))] -> Map Int (Bool, Math)
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
    (Int
1,(Bool
False,PetriMath {
      $sel:netMath:PetriMath :: String
netMath = String
"N = \\left(S, T, \\vphantom{()}^{\\bullet}(), ()^{\\bullet}, m_0\\right)",
      $sel:placesMath:PetriMath :: String
placesMath = String
"S = \\left\\{s_{1},s_{2},s_{3},s_{4}\\right\\}",
      $sel:transitionsMath:PetriMath :: String
transitionsMath = String
"T = \\left\\{t_{1},t_{2},t_{3}\\right\\}",
      $sel:tokenChangeMath:PetriMath :: [(String, String)]
tokenChangeMath = [
        (String
"^{\\bullet}t_{1} = \\left(0,1,0,0\\right)",String
"t_{1}^{\\bullet} = \\left(0,0,1,0\\right)"),
        (String
"^{\\bullet}t_{2} = \\left(0,1,0,0\\right)",String
"t_{2}^{\\bullet} = \\left(1,0,0,1\\right)"),
        (String
"^{\\bullet}t_{3} = \\left(1,0,0,0\\right)",String
"t_{3}^{\\bullet} = \\left(0,0,1,1\\right)")
        ],
      $sel:initialMarkingMath:PetriMath :: String
initialMarkingMath = String
"m_0 = \\left(2,0,1,0\\right)",
      $sel:placeOrderMath:PetriMath :: Maybe String
placeOrderMath = String -> Maybe String
forall a. a -> Maybe a
Just String
"\\left(s_{1},s_{2},s_{3},s_{4}\\right)"
      })),
    (Int
2,(Bool
False,PetriMath {
      $sel:netMath:PetriMath :: String
netMath = String
"N = \\left(S, T, \\vphantom{()}^{\\bullet}(), ()^{\\bullet}, m_0\\right)",
      $sel:placesMath:PetriMath :: String
placesMath = String
"S = \\left\\{s_{1},s_{2},s_{3},s_{4}\\right\\}",
      $sel:transitionsMath:PetriMath :: String
transitionsMath = String
"T = \\left\\{t_{1},t_{2},t_{3}\\right\\}",
      $sel:tokenChangeMath:PetriMath :: [(String, String)]
tokenChangeMath = [
        (String
"^{\\bullet}t_{1} = \\left(0,1,0,0\\right)",String
"t_{1}^{\\bullet} = \\left(1,0,1,0\\right)"),
        (String
"^{\\bullet}t_{2} = \\left(0,1,0,0\\right)",String
"t_{2}^{\\bullet} = \\left(0,0,0,1\\right)"),
        (String
"^{\\bullet}t_{3} = \\left(1,0,0,0\\right)",String
"t_{3}^{\\bullet} = \\left(0,0,1,1\\right)")
        ],
      $sel:initialMarkingMath:PetriMath :: String
initialMarkingMath = String
"m_0 = \\left(2,0,1,0\\right)",
      $sel:placeOrderMath:PetriMath :: Maybe String
placeOrderMath = String -> Maybe String
forall a. a -> Maybe a
Just String
"\\left(s_{1},s_{2},s_{3},s_{4}\\right)"
      })),
    (Int
3,(Bool
False,PetriMath {
      $sel:netMath:PetriMath :: String
netMath = String
"N = \\left(S, T, \\vphantom{()}^{\\bullet}(), ()^{\\bullet}, m_0\\right)",
      $sel:placesMath:PetriMath :: String
placesMath = String
"S = \\left\\{s_{1},s_{2},s_{3},s_{4}\\right\\}",
      $sel:transitionsMath:PetriMath :: String
transitionsMath = String
"T = \\left\\{t_{1},t_{2},t_{3}\\right\\}",
      $sel:tokenChangeMath:PetriMath :: [(String, String)]
tokenChangeMath = [
        (String
"^{\\bullet}t_{1} = \\left(0,1,0,0\\right)",String
"t_{1}^{\\bullet} = \\left(1,0,0,0\\right)"),
        (String
"^{\\bullet}t_{2} = \\left(0,1,0,0\\right)",String
"t_{2}^{\\bullet} = \\left(0,0,0,1\\right)"),
        (String
"^{\\bullet}t_{3} = \\left(1,0,0,0\\right)",String
"t_{3}^{\\bullet} = \\left(0,0,1,0\\right)")
        ],
      $sel:initialMarkingMath:PetriMath :: String
initialMarkingMath = String
"m_0 = \\left(2,0,1,0\\right)",
      $sel:placeOrderMath:PetriMath :: Maybe String
placeOrderMath = String -> Maybe String
forall a. a -> Maybe a
Just String
"\\left(s_{1},s_{2},s_{3},s_{4}\\right)"
      })),
    (Int
4,(Bool
True,PetriMath {
      $sel:netMath:PetriMath :: String
netMath = String
"N = \\left(S, T, \\vphantom{()}^{\\bullet}(), ()^{\\bullet}, m_0\\right)",
      $sel:placesMath:PetriMath :: String
placesMath = String
"S = \\left\\{s_{1},s_{2},s_{3},s_{4}\\right\\}",
      $sel:transitionsMath:PetriMath :: String
transitionsMath = String
"T = \\left\\{t_{1},t_{2},t_{3}\\right\\}",
      $sel:tokenChangeMath:PetriMath :: [(String, String)]
tokenChangeMath = [
        (String
"^{\\bullet}t_{1} = \\left(0,1,0,0\\right)",String
"t_{1}^{\\bullet} = \\left(0,0,1,0\\right)"),
        (String
"^{\\bullet}t_{2} = \\left(0,1,0,0\\right)",String
"t_{2}^{\\bullet} = \\left(0,0,0,1\\right)"),
        (String
"^{\\bullet}t_{3} = \\left(1,0,0,0\\right)",String
"t_{3}^{\\bullet} = \\left(0,0,1,0\\right)")
        ],
      $sel:initialMarkingMath:PetriMath :: String
initialMarkingMath = String
"m_0 = \\left(2,0,1,0\\right)",
      $sel:placeOrderMath:PetriMath :: Maybe String
placeOrderMath = String -> Maybe String
forall a. a -> Maybe a
Just String
"\\left(s_{1},s_{2},s_{3},s_{4}\\right)"
      }))
    ],
    $sel:addText:MatchInstance :: Maybe (Map Language String)
addText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

defaultMathToGraphInstance :: MathToGraphInstance
defaultMathToGraphInstance :: MathToGraphInstance
defaultMathToGraphInstance = MatchInstance {
  $sel:from:MatchInstance :: Math
from = PetriMath {
    $sel:netMath:PetriMath :: String
netMath = String
"N = \\left(S, T, \\vphantom{()}^{\\bullet}(), ()^{\\bullet}, m_0\\right)",
    $sel:placesMath:PetriMath :: String
placesMath = String
"S = \\left\\{s_{1},s_{2},s_{3},s_{4}\\right\\}",
    $sel:transitionsMath:PetriMath :: String
transitionsMath = String
"T = \\left\\{t_{1},t_{2},t_{3}\\right\\}",
    $sel:tokenChangeMath:PetriMath :: [(String, String)]
tokenChangeMath = [
      (String
"^{\\bullet}t_{1} = \\left(0,0,1,0\\right)",String
"t_{1}^{\\bullet} = \\left(1,0,0,0\\right)"),
      (String
"^{\\bullet}t_{2} = \\left(0,0,0,1\\right)",String
"t_{2}^{\\bullet} = \\left(0,1,0,0\\right)"),
      (String
"^{\\bullet}t_{3} = \\left(0,0,1,0\\right)",String
"t_{3}^{\\bullet} = \\left(0,0,0,1\\right)")
      ],
    $sel:initialMarkingMath:PetriMath :: String
initialMarkingMath = String
"m_0 = \\left(1,1,0,1\\right)",
    $sel:placeOrderMath:PetriMath :: Maybe String
placeOrderMath = String -> Maybe String
forall a. a -> Maybe a
Just String
"\\left(s_{1},s_{2},s_{3},s_{4}\\right)"
    },
  $sel:showSolution:MatchInstance :: Bool
showSolution = Bool
False,
  $sel:to:MatchInstance :: Map Int (Bool, Drawable (PetriLike SimpleNode String))
to = [(Int, (Bool, Drawable (PetriLike SimpleNode String)))]
-> Map Int (Bool, Drawable (PetriLike SimpleNode String))
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
    (Int
1,(Bool
True,(
      PetriLike {
        $sel:allNodes:PetriLike :: Map String (SimpleNode String)
allNodes = [(String, SimpleNode String)] -> Map String (SimpleNode String)
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
          (String
"s1",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s2",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s3",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
0, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t1",Int
1),(String
"t3",Int
1)]}),
          (String
"s4",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t2",Int
1)]}),
          (String
"t1",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s1",Int
1)]}),
          (String
"t2",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s2",Int
1)]}),
          (String
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s4",Int
1)]})
          ]
        },
      DrawSettings {
        $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
True,
        $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
        $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
True,
        $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
        $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Dot
        }
      ))),
    (Int
2,(Bool
False,(
      PetriLike {
        $sel:allNodes:PetriLike :: Map String (SimpleNode String)
allNodes = [(String, SimpleNode String)] -> Map String (SimpleNode String)
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
          (String
"s1",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s2",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s3",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
0, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t1",Int
2),(String
"t3",Int
2)]}),
          (String
"s4",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t2",Int
1)]}),
          (String
"t1",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s1",Int
1)]}),
          (String
"t2",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s2",Int
1)]}),
          (String
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s4",Int
1)]})
          ]
        },
      DrawSettings {
        $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
True,
        $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
        $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
True,
        $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
        $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Sfdp
        }
      ))),
    (Int
3,(Bool
False,(
      PetriLike {
        $sel:allNodes:PetriLike :: Map String (SimpleNode String)
allNodes = [(String, SimpleNode String)] -> Map String (SimpleNode String)
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
          (String
"s1",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s2",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s3",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
0, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t1",Int
1),(String
"t3",Int
1)]}),
          (String
"s4",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t2",Int
1)]}),
          (String
"t1",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s1",Int
2),(String
"s2",Int
1)]}),
          (String
"t2",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s2",Int
1)]}),
          (String
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s4",Int
1)]})
          ]
        },
      DrawSettings {
        $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
True,
        $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
        $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
True,
        $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
        $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Circo}
      ))),
    (Int
4,(Bool
False,(
      PetriLike {
        $sel:allNodes:PetriLike :: Map String (SimpleNode String)
allNodes = [(String, SimpleNode String)] -> Map String (SimpleNode String)
forall k a. Ord k => [(k, a)] -> Map k a
fromList [
          (String
"s1",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s2",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty}),
          (String
"s3",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
0, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t1",Int
2),(String
"t3",Int
1)]}),
          (String
"s4",SimplePlace {$sel:initial:SimplePlace :: Int
initial = Int
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"t2",Int
1)]}),
          (String
"t1",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s1",Int
2)]}),
          (String
"t2",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s2",Int
1)]}),
          (String
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
fromList [(String
"s4",Int
1)]})
          ]
        },
      DrawSettings {
        $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
True,
        $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
        $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
True,
        $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
        $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Fdp
        }
      )))
    ],
    $sel:addText:MatchInstance :: Maybe (Map Language String)
addText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }