{-# LANGUAGE ApplicativeDo #-}
{-# Language DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# Language QuasiQuotes #-}
{-# LANGUAGE RecordWildCards #-}

module Modelling.PetriNet.Concurrency (
  checkFindConcurrencyConfig,
  checkPickConcurrencyConfig,
  defaultFindConcurrencyInstance,
  defaultPickConcurrencyInstance,
  findConcurrency,
  findConcurrencyEvaluation,
  findConcurrencyGenerate,
  findConcurrencySolution,
  findConcurrencySyntax,
  findConcurrencyTask,
  parseConcurrency,
  petriNetFindConcur,
  petriNetPickConcur,
  pickConcurrency,
  pickConcurrencyGenerate,
  pickConcurrencyTask,
  simpleFindConcurrencyTask,
  simplePickConcurrencyTask,
  ) where

import qualified Modelling.PetriNet.Find          as Find (FindInstance (..), showSolution)
import qualified Modelling.PetriNet.Pick          as Pick (PickInstance (..))
import qualified Modelling.PetriNet.Types         as Find (
  FindConcurrencyConfig (..),
  )
import qualified Modelling.PetriNet.Types         as Pick (
  PickConcurrencyConfig (..),
  )

import qualified Data.Map                         as M (
  empty,
  fromList,
  )

import Capabilities.Alloy               (MonadAlloy)
import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.Auxiliary.Common (
  Object,
  parseWith,
  )
import Modelling.Auxiliary.Output (
  hoveringInformation,
  extra,
  )
import Modelling.PetriNet.Alloy (
  compAdvConstraints,
  compBasicConstraints,
  compChange,
  defaultConstraints,
  moduleHelpers,
  modulePetriAdditions,
  modulePetriConcepts,
  modulePetriConstraints,
  modulePetriSignature,
  petriScopeBitWidth,
  petriScopeMaxSeq,
  signatures,
  skolemVariable,
  taskInstance,
  unscopedSingleSig,
  )
import Modelling.PetriNet.Diagram (
  cacheNet,
  isNetDrawable,
  )
import Modelling.PetriNet.Find (
  FindInstance (..),
  checkConfigForFind,
  findInitial,
  findTaskInstance,
  toFindEvaluation,
  toFindSyntax,
  )
import Modelling.PetriNet.Parser        (
  asSingleton,
  )
import Modelling.PetriNet.Pick (
  PickInstance (..),
  checkConfigForPick,
  pickGenerate,
  pickTaskInstance,
  renderPick,
  wrong,
  wrongInstances,
  )
import Modelling.PetriNet.Reach.Type (
  Transition (Transition),
  parseTransitionPrec,
  )
import Modelling.PetriNet.Types         (
  AdvConfig (..),
  BasicConfig (..),
  ChangeConfig,
  Concurrent (Concurrent),
  DrawSettings (..),
  FindConcurrencyConfig (..),
  Net (..),
  PetriLike (PetriLike, allNodes),
  PickConcurrencyConfig (..),
  SimpleNode (..),
  SimplePetriNet,
  allDrawSettings,
  transitionPairShow,
  )

import Control.Applicative              (Alternative ((<|>)))
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.Monad.Extra              (findM)
import Control.OutputCapable.Blocks (
  ArticleToUse (DefiniteArticle),
  GenericOutputCapable (..),
  LangM',
  LangM,
  OutputCapable,
  Rated,
  ($=<<),
  english,
  german,
  printSolutionAndAssert,
  translate,
  translations,
  unLangM,
  )
import Control.Monad.Random (
  RandT,
  RandomGen,
  evalRandT,
  mkStdGen,
  )
import Control.Monad.Trans              (MonadTrans (lift))
import Data.Bifunctor                   (Bifunctor (bimap))
import Data.Data                        (Data, Typeable)
import Data.Either                      (isLeft)
import Data.GraphViz.Commands           (GraphvizCommand (Circo, Fdp))
import Data.String.Interpolate          (i, iii)
import Language.Alloy.Call (
  AlloyInstance,
  )
import System.Random.Shuffle            (shuffleM)

simpleFindConcurrencyTask
  :: (
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    OutputCapable m
    )
  => FilePath
  -> FindInstance SimplePetriNet (Concurrent Transition)
  -> LangM m
simpleFindConcurrencyTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
String
-> FindInstance SimplePetriNet (Concurrent Transition) -> LangM m
simpleFindConcurrencyTask = String
-> FindInstance SimplePetriNet (Concurrent Transition) -> LangM m
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, OutputCapable m,
 Typeable n, Typeable p) =>
String
-> FindInstance (p n String) (Concurrent Transition) -> LangM m
findConcurrencyTask

findConcurrencyTask
  :: (
    Data (n String),
    Data (p n String),
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Net p n,
    OutputCapable m,
    Typeable n,
    Typeable p
    )
  => FilePath
  -> FindInstance (p n String) (Concurrent Transition)
  -> LangM m
findConcurrencyTask :: forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, OutputCapable m,
 Typeable n, Typeable p) =>
String
-> FindInstance (p n String) (Concurrent Transition) -> LangM m
findConcurrencyTask String
path FindInstance (p n String) (Concurrent Transition)
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 Petri net:"
    String -> State (Map Language String) ()
german String
"Betrachten Sie folgendes Petrinetz:"
  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
$=<< 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 (FindInstance (p n String) (Concurrent Transition) -> p n String
forall n a. FindInstance n a -> n
net FindInstance (p n String) (Concurrent Transition)
task) (FindInstance (p n String) (Concurrent Transition) -> DrawSettings
forall n a. FindInstance n a -> DrawSettings
drawFindWith FindInstance (p n String) (Concurrent Transition)
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 [iii|
      Which pair of transitions is concurrently activated
      under the initial marking?
      |]
    String -> State (Map Language String) ()
german [iii|
      Welches Paar von Transitionen ist unter der Startmarkierung
      nebenläufig aktiviert?
      |]
  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 [iii|
        State your answer by giving a pair
        of concurrently activated transitions.
        #{" "}|]
      String -> State (Map Language String) ()
german [iii|
        Geben Sie Ihre Antwort durch Angabe eines Paars
        von nebenläufig aktivierten Transitionen an.
        #{" "}|]
    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 |]
    let ts :: (ShowTransition, ShowTransition)
ts = (Transition, Transition) -> (ShowTransition, ShowTransition)
transitionPairShow (Transition, Transition)
findInitial
    String -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
String -> GenericLangM l m ()
code (String -> LangM m) -> String -> LangM m
forall a b. (a -> b) -> a -> b
$ (ShowTransition, ShowTransition) -> String
forall a. Show a => a -> String
show (ShowTransition, ShowTransition)
ts
    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
      let (String
t1, String
t2) = (ShowTransition -> String)
-> (ShowTransition -> String)
-> (ShowTransition, ShowTransition)
-> (String, String)
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap ShowTransition -> String
forall a. Show a => a -> String
show ShowTransition -> String
forall a. Show a => a -> String
show (ShowTransition, ShowTransition)
ts
      String -> State (Map Language String) ()
english [iii|
        #{" "}as answer would indicate that transitions #{t1} and #{t2}
        are concurrently activated under the initial marking.
        #{" "}|]
      String -> State (Map Language String) ()
german [iii|
        #{" "}als Antwort würde bedeuten, dass Transitionen #{t1} und #{t2}
        unter der Startmarkierung nebenläufig aktiviert sind.
        #{" "}|]
    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
"The order of transitions within the pair does not matter here."
      String -> State (Map Language String) ()
german [iii|
        Die Reihenfolge der Transitionen innerhalb
        des Paars spielt hierbei keine Rolle.
        |]
    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
$ FindInstance (p n String) (Concurrent Transition)
-> Maybe (Map Language String)
forall n a. FindInstance n a -> Maybe (Map Language String)
Find.addText FindInstance (p n String) (Concurrent Transition)
task
  pure ()

findConcurrencySyntax
  :: OutputCapable m
  => FindInstance net (Concurrent Transition)
  -> (Transition, Transition)
  -> LangM' m ()
findConcurrencySyntax :: forall (m :: * -> *) net.
OutputCapable m =>
FindInstance net (Concurrent Transition)
-> (Transition, Transition) -> LangM' m ()
findConcurrencySyntax = Bool -> Int -> (Transition, Transition) -> LangM' m ()
forall (m :: * -> *).
OutputCapable m =>
Bool -> Int -> (Transition, Transition) -> LangM' m ()
toFindSyntax Bool
False (Int -> (Transition, Transition) -> LangM' m ())
-> (FindInstance net (Concurrent Transition) -> Int)
-> FindInstance net (Concurrent Transition)
-> (Transition, Transition)
-> LangM' m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindInstance net (Concurrent Transition) -> Int
forall n a. FindInstance n a -> Int
numberOfTransitions

findConcurrencyEvaluation
  :: (Monad m, OutputCapable m)
  => FindInstance net (Concurrent Transition)
  -> (Transition, Transition)
  -> Rated m
findConcurrencyEvaluation :: forall (m :: * -> *) net.
(Monad m, OutputCapable m) =>
FindInstance net (Concurrent Transition)
-> (Transition, Transition) -> Rated m
findConcurrencyEvaluation FindInstance net (Concurrent Transition)
task (Transition, Transition)
x = 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
"are concurrently activated"
        String -> State (Map Language String) ()
german String
"sind nebenläufig aktiviert"
  (Maybe String -> Rational -> Rated m)
-> (Maybe String, Rational) -> Rated m
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (ArticleToUse -> Maybe String -> Rational -> Rated m
forall (m :: * -> *).
OutputCapable m =>
ArticleToUse -> Maybe String -> Rational -> Rated m
printSolutionAndAssert ArticleToUse
DefiniteArticle)
    ((Maybe String, Rational) -> Rated m)
-> m (Maybe String, Rational) -> Rated m
forall (m :: * -> *) a l b.
Monad m =>
(a -> GenericLangM l m b) -> m a -> GenericLangM l m b
$=<< GenericLangM Language m (Maybe String, Rational)
-> m (Maybe String, Rational)
forall l (m :: * -> *) a. GenericLangM l m a -> m a
unLangM (GenericLangM Language m (Maybe String, Rational)
 -> m (Maybe String, Rational))
-> GenericLangM Language m (Maybe String, Rational)
-> m (Maybe String, Rational)
forall a b. (a -> b) -> a -> b
$ Map Language String
-> Bool
-> (Transition, Transition)
-> (Transition, Transition)
-> GenericLangM Language m (Maybe String, Rational)
forall a (m :: * -> *).
(Num a, OutputCapable m) =>
Map Language String
-> Bool
-> (Transition, Transition)
-> (Transition, Transition)
-> LangM' m (Maybe String, a)
toFindEvaluation Map Language String
what Bool
withSol (Transition, Transition)
concur (Transition, Transition)
x
  where
    concur :: (Transition, Transition)
concur = FindInstance net (Concurrent Transition)
-> (Transition, Transition)
forall net a. FindInstance net (Concurrent a) -> (a, a)
findConcurrencySolution FindInstance net (Concurrent Transition)
task
    withSol :: Bool
withSol = FindInstance net (Concurrent Transition) -> Bool
forall n a. FindInstance n a -> Bool
Find.showSolution FindInstance net (Concurrent Transition)
task

findConcurrencySolution :: FindInstance net (Concurrent a) -> (a, a)
findConcurrencySolution :: forall net a. FindInstance net (Concurrent a) -> (a, a)
findConcurrencySolution FindInstance net (Concurrent a)
task = (a, a)
concur
  where
    Concurrent (a, a)
concur = FindInstance net (Concurrent a) -> Concurrent a
forall n a. FindInstance n a -> a
toFind FindInstance net (Concurrent a)
task

simplePickConcurrencyTask
  :: (MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    OutputCapable m
    )
  => FilePath
  -> PickInstance SimplePetriNet
  -> LangM m
simplePickConcurrencyTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
String -> PickInstance SimplePetriNet -> LangM m
simplePickConcurrencyTask = String -> PickInstance SimplePetriNet -> LangM m
forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, OutputCapable m,
 Typeable n, Typeable p) =>
String -> PickInstance (p n String) -> LangM m
pickConcurrencyTask

pickConcurrencyTask
  :: (
    Data (n String),
    Data (p n String),
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    Net p n,
    OutputCapable m,
    Typeable n,
    Typeable p
    )
  => FilePath
  -> PickInstance (p n String)
  -> LangM m
pickConcurrencyTask :: forall (n :: * -> *) (p :: (* -> *) -> * -> *) (m :: * -> *).
(Data (n String), Data (p n String), MonadCache m, MonadDiagrams m,
 MonadGraphviz m, MonadThrow m, Net p n, OutputCapable m,
 Typeable n, Typeable p) =>
String -> PickInstance (p n String) -> LangM m
pickConcurrencyTask String
path PickInstance (p n String)
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 [iii|
      Which of the following Petri nets has exactly
      one pair of transitions that are concurrently activated
      under the initial marking?
      |]
    String -> State (Map Language String) ()
german [iii|
      Welches dieser Petrinetze hat genau ein Paar von Transitionen,
      die unter der Startmarkierung nebenläufig aktiviert sind?
      |]
  (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
$=<< String -> PickInstance (p n String) -> m (Map Int (Bool, 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 -> PickInstance (p n String) -> m (Map Int (Bool, String))
renderPick String
path PickInstance (p n String)
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 [iii|
      State your answer by giving the number of the Petri net
      having these concurrently activated transitions.
      #{" "}|]
    String -> State (Map Language String) ()
german [iii|
      Geben Sie Ihre Antwort durch Angabe der Nummer des Petrinetzes an,
      das diese nebenläufig aktivierten Transitionen hat.
      #{" "}|]
  let plural :: Bool
plural = PickInstance (p n String) -> Int
forall n. PickInstance n -> Int
wrongInstances PickInstance (p n String)
task Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1
  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 [iii|
        #{" "}as answer would indicate that Petri net 1 has
        exactly two transitions that are concurrently activated
        under the initial marking (and the other Petri
        #{if plural then "nets don't" else "net doesn't"}).
        |]
      String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ [iii|
        #{" "}als Antwort würde bedeuten, dass Petrinetz 1
        genau zwei unter der Startmarkierung
        nebenläufig aktivierte Transitionen hat (und
        #{" "}
        |]
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
plural
            then String
"die anderen Petrinetze nicht"
            else String
"das andere Petrinetz nicht")
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")."
    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
$ PickInstance (p n String) -> Maybe (Map Language String)
forall n. PickInstance n -> Maybe (Map Language String)
Pick.addText PickInstance (p n String)
task
  pure ()

findConcurrencyGenerate
  :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n)
  => FindConcurrencyConfig
  -> Int
  -> Int
  -> m (FindInstance (p n String) (Concurrent Transition))
findConcurrencyGenerate :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n) =>
FindConcurrencyConfig
-> Int
-> Int
-> m (FindInstance (p n String) (Concurrent Transition))
findConcurrencyGenerate FindConcurrencyConfig
config Int
segment = RandT StdGen m (FindInstance (p n String) (Concurrent Transition))
-> StdGen -> m (FindInstance (p n String) (Concurrent Transition))
forall (m :: * -> *) g a. Monad m => RandT g m a -> g -> m a
evalRandT RandT StdGen m (FindInstance (p n String) (Concurrent Transition))
getInstance (StdGen -> m (FindInstance (p n String) (Concurrent Transition)))
-> (Int -> StdGen)
-> Int
-> m (FindInstance (p n String) (Concurrent Transition))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> StdGen
mkStdGen
  where
    getInstance :: RandT StdGen m (FindInstance (p n String) (Concurrent Transition))
getInstance = do
      (p n String, Concurrent String)
petriConcurrency <- FindConcurrencyConfig
-> Int -> RandT StdGen m (p n String, Concurrent String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
FindConcurrencyConfig
-> Int -> RandT g m (p n String, Concurrent String)
findConcurrency FindConcurrencyConfig
config Int
segment
      [DrawSettings]
ds <- [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 -> [DrawSettings]) -> GraphConfig -> [DrawSettings]
forall a b. (a -> b) -> a -> b
$ FindConcurrencyConfig -> GraphConfig
Find.graphConfig FindConcurrencyConfig
config
      Maybe DrawSettings
d <- (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, Concurrent String) -> p n String
forall a b. (a, b) -> a
fst (p n String, Concurrent String)
petriConcurrency)) [DrawSettings]
ds
      RandT StdGen m (FindInstance (p n String) (Concurrent Transition))
-> (DrawSettings
    -> RandT
         StdGen m (FindInstance (p n String) (Concurrent Transition)))
-> Maybe DrawSettings
-> RandT
     StdGen m (FindInstance (p n String) (Concurrent Transition))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RandT StdGen m (FindInstance (p n String) (Concurrent Transition))
getInstance ((p n String
 -> Concurrent String
 -> DrawSettings
 -> RandT
      StdGen m (FindInstance (p n String) (Concurrent Transition)))
-> (p n String, Concurrent String)
-> DrawSettings
-> RandT
     StdGen m (FindInstance (p n String) (Concurrent Transition))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry p n String
-> Concurrent String
-> DrawSettings
-> RandT
     StdGen m (FindInstance (p n String) (Concurrent Transition))
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {t :: * -> *} {n}.
(MonadTrans t, Traversable t, MonadThrow m, Functor (t m)) =>
n
-> t String -> DrawSettings -> t m (FindInstance n (t Transition))
toInstance (p n String, Concurrent String)
petriConcurrency) Maybe DrawSettings
d
    toInstance :: n
-> t String -> DrawSettings -> t m (FindInstance n (t Transition))
toInstance n
petri t String
concurrency DrawSettings
drawSettings = do
      t Transition
c' <- m (t Transition) -> t m (t Transition)
forall (m :: * -> *) a. Monad m => m a -> t m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (t Transition) -> t m (t Transition))
-> m (t Transition) -> t m (t Transition)
forall a b. (a -> b) -> a -> b
$ (String -> m Transition) -> t String -> m (t Transition)
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) -> t a -> f (t b)
traverse
         ((Int -> Parser Transition) -> String -> m Transition
forall (m :: * -> *) a.
MonadThrow m =>
(Int -> Parser a) -> String -> m a
parseWith Int -> Parser Transition
parseTransitionPrec)
         t String
concurrency
      return $ FindInstance {
        $sel:drawFindWith:FindInstance :: DrawSettings
drawFindWith = DrawSettings
drawSettings,
        $sel:toFind:FindInstance :: t Transition
toFind = t Transition
c',
        $sel:net:FindInstance :: n
net = n
petri,
        $sel:numberOfPlaces:FindInstance :: Int
numberOfPlaces = BasicConfig -> Int
places BasicConfig
bc,
        $sel:numberOfTransitions:FindInstance :: Int
numberOfTransitions = BasicConfig -> Int
transitions BasicConfig
bc,
        $sel:showSolution:FindInstance :: Bool
showSolution = FindConcurrencyConfig -> Bool
Find.printSolution FindConcurrencyConfig
config,
        $sel:addText:FindInstance :: Maybe (Map Language String)
addText = FindConcurrencyConfig -> Maybe (Map Language String)
Find.extraText FindConcurrencyConfig
config
        }
    bc :: BasicConfig
bc = FindConcurrencyConfig -> BasicConfig
Find.basicConfig FindConcurrencyConfig
config

findConcurrency
  :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g)
  => FindConcurrencyConfig
  -> Int
  -> RandT g m (p n String, Concurrent String)
findConcurrency :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
FindConcurrencyConfig
-> Int -> RandT g m (p n String, Concurrent String)
findConcurrency = ((AlloyInstance -> m (Concurrent Object))
 -> AlloyInstance -> RandT g m (p n String, Concurrent String))
-> (FindConcurrencyConfig -> String)
-> (AlloyInstance -> m (Concurrent Object))
-> (FindConcurrencyConfig -> AlloyConfig)
-> FindConcurrencyConfig
-> Int
-> RandT g m (p n String, Concurrent String)
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
  (AlloyInstance -> m (Concurrent Object))
-> AlloyInstance -> RandT g m (p n String, Concurrent String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g
       (t :: * -> *).
(MonadThrow m, Net p n, RandomGen g, Traversable t) =>
(AlloyInstance -> m (t Object))
-> AlloyInstance -> RandT g m (p n String, t String)
findTaskInstance
  FindConcurrencyConfig -> String
petriNetFindConcur
  AlloyInstance -> m (Concurrent Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (Concurrent Object)
parseConcurrency
  FindConcurrencyConfig -> AlloyConfig
Find.alloyConfig

pickConcurrencyGenerate
  :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n)
  => PickConcurrencyConfig
  -> Int
  -> Int
  -> m (PickInstance (p n String))
pickConcurrencyGenerate :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n) =>
PickConcurrencyConfig
-> Int -> Int -> m (PickInstance (p n String))
pickConcurrencyGenerate = (PickConcurrencyConfig
 -> Int -> RandT StdGen m [(p n String, Maybe (Concurrent String))])
-> (PickConcurrencyConfig -> GraphConfig)
-> (PickConcurrencyConfig -> Bool)
-> (PickConcurrencyConfig -> Bool)
-> (PickConcurrencyConfig -> Maybe (Map Language String))
-> PickConcurrencyConfig
-> Int
-> Int
-> m (PickInstance (p n String))
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) c a.
(MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n) =>
(c -> Int -> RandT StdGen m [(p n String, Maybe a)])
-> (c -> GraphConfig)
-> (c -> Bool)
-> (c -> Bool)
-> (c -> Maybe (Map Language String))
-> c
-> Int
-> Int
-> m (PickInstance (p n String))
pickGenerate PickConcurrencyConfig
-> Int -> RandT StdGen m [(p n String, Maybe (Concurrent String))]
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
PickConcurrencyConfig
-> Int -> RandT g m [(p n String, Maybe (Concurrent String))]
pickConcurrency PickConcurrencyConfig -> GraphConfig
gc PickConcurrencyConfig -> Bool
ud PickConcurrencyConfig -> Bool
ws PickConcurrencyConfig -> Maybe (Map Language String)
et
  where
    gc :: PickConcurrencyConfig -> GraphConfig
gc = PickConcurrencyConfig -> GraphConfig
Pick.graphConfig
    ud :: PickConcurrencyConfig -> Bool
ud = PickConcurrencyConfig -> Bool
Pick.useDifferentGraphLayouts
    ws :: PickConcurrencyConfig -> Bool
ws = PickConcurrencyConfig -> Bool
Pick.printSolution
    et :: PickConcurrencyConfig -> Maybe (Map Language String)
et = PickConcurrencyConfig -> Maybe (Map Language String)
Pick.extraText


pickConcurrency
  :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g)
  => PickConcurrencyConfig
  -> Int
  -> RandT
    g
    m
    [(p n String, Maybe (Concurrent String))]
pickConcurrency :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
PickConcurrencyConfig
-> Int -> RandT g m [(p n String, Maybe (Concurrent String))]
pickConcurrency = ((AlloyInstance -> RandT g m (Concurrent Object))
 -> AlloyInstance
 -> RandT g m [(p n String, Maybe (Concurrent String))])
-> (PickConcurrencyConfig -> String)
-> (AlloyInstance -> RandT g m (Concurrent Object))
-> (PickConcurrencyConfig -> AlloyConfig)
-> PickConcurrencyConfig
-> Int
-> RandT g m [(p n String, Maybe (Concurrent String))]
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
  (AlloyInstance -> RandT g m (Concurrent Object))
-> AlloyInstance
-> RandT g m [(p n String, Maybe (Concurrent String))]
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *)
       (t :: * -> *).
(MonadThrow m, Net p n, Traversable t) =>
(AlloyInstance -> m (t Object))
-> AlloyInstance -> m [(p n String, Maybe (t String))]
pickTaskInstance
  PickConcurrencyConfig -> String
petriNetPickConcur
  AlloyInstance -> RandT g m (Concurrent Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (Concurrent Object)
parseConcurrency
  PickConcurrencyConfig -> AlloyConfig
Pick.alloyConfig


petriNetFindConcur :: FindConcurrencyConfig -> String
petriNetFindConcur :: FindConcurrencyConfig -> String
petriNetFindConcur FindConcurrencyConfig{
  BasicConfig
$sel:basicConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  AdvConfig
advConfig :: AdvConfig
$sel:advConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> AdvConfig
advConfig,
  ChangeConfig
changeConfig :: ChangeConfig
$sel:changeConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> ChangeConfig
changeConfig
  } = BasicConfig -> ChangeConfig -> Either Bool AdvConfig -> String
petriNetConcurrencyAlloy BasicConfig
basicConfig ChangeConfig
changeConfig (Either Bool AdvConfig -> String)
-> Either Bool AdvConfig -> String
forall a b. (a -> b) -> a -> b
$ AdvConfig -> Either Bool AdvConfig
forall a b. b -> Either a b
Right AdvConfig
advConfig

petriNetPickConcur :: PickConcurrencyConfig -> String
petriNetPickConcur :: PickConcurrencyConfig -> String
petriNetPickConcur PickConcurrencyConfig{
  BasicConfig
basicConfig :: BasicConfig
$sel:basicConfig:PickConcurrencyConfig :: PickConcurrencyConfig -> BasicConfig
basicConfig,
  ChangeConfig
changeConfig :: ChangeConfig
$sel:changeConfig:PickConcurrencyConfig :: PickConcurrencyConfig -> ChangeConfig
changeConfig,
  Bool
prohibitSourceTransitions :: Bool
$sel:prohibitSourceTransitions:PickConcurrencyConfig :: PickConcurrencyConfig -> Bool
prohibitSourceTransitions
  } =
  BasicConfig -> ChangeConfig -> Either Bool AdvConfig -> String
petriNetConcurrencyAlloy
    BasicConfig
basicConfig
    ChangeConfig
changeConfig
    (Bool -> Either Bool AdvConfig
forall a b. a -> Either a b
Left Bool
prohibitSourceTransitions)

{-|
Generate code for PetriNet concurrency tasks
-}
petriNetConcurrencyAlloy
  :: BasicConfig
  -> ChangeConfig
  -> Either Bool AdvConfig
  -- ^ Right for find task; Left for pick task (and the Bool in there says whether source transitions should be prohibited)
  -> String
petriNetConcurrencyAlloy :: BasicConfig -> ChangeConfig -> Either Bool AdvConfig -> String
petriNetConcurrencyAlloy BasicConfig
basicC ChangeConfig
changeC Either Bool AdvConfig
specific
  = [i|module PetriNetConcur

#{modulePetriSignature}
#{either (const sigs) (const modulePetriAdditions) specific}
#{moduleHelpers}
#{modulePetriConcepts}
#{modulePetriConstraints}

pred #{concurrencyPredicateName}[#{defaultActiveTrans}#{activated} : set Transitions, #{t1}, #{t2} : Transitions] {
  \#Places = #{places basicC}
  \#Transitions = #{transitions basicC}
  #{compBasicConstraints activated basicC}
  #{compChange changeC}
  #{sourceTransitionConstraints}
  no disj x,y : givenTransitions | concurrentDefault[x + y]
  disj[#{t1}, #{t2}] and concurrent[#{t1} + #{t2}]
  all disj u,v : Transitions |
    concurrent[u + v] implies #{t1} + #{t2} = u + v
  #{compConstraints}
}

run #{concurrencyPredicateName} for exactly #{petriScopeMaxSeq basicC} Nodes, #{petriScopeBitWidth basicC} Int
|]
  where
    activated :: String
activated        = String
"activatedTrans"
    activatedDefault :: String
activatedDefault = String
"defaultActiveTrans"
    compConstraints :: String
compConstraints = (Bool -> String)
-> (AdvConfig -> String) -> Either Bool AdvConfig -> String
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
      (String -> Bool -> String
forall a b. a -> b -> a
const (String -> Bool -> String) -> String -> Bool -> String
forall a b. (a -> b) -> a -> b
$ String -> BasicConfig -> String
defaultConstraints String
activatedDefault BasicConfig
basicC)
      AdvConfig -> String
compAdvConstraints
      Either Bool AdvConfig
specific
    sourceTransitionConstraints :: String
sourceTransitionConstraints
      | Left Bool
True <- Either Bool AdvConfig
specific = [i|
  no t : givenTransitions | no givenPlaces.flow[t]
  no t : Transitions | sourceTransitions[t]|]
      | Bool
otherwise = String
""
    defaultActiveTrans :: String
defaultActiveTrans
      | Either Bool AdvConfig -> Bool
forall a b. Either a b -> Bool
isLeft Either Bool AdvConfig
specific    = [i|#{activatedDefault} : set givenTransitions,|]
      | Bool
otherwise          = String
""
    sigs :: String
sigs = String -> Int -> Int -> String
signatures String
"given" (BasicConfig -> Int
places BasicConfig
basicC) (BasicConfig -> Int
transitions BasicConfig
basicC)
    t1 :: String
t1 = String
transition1
    t2 :: String
t2 = String
transition2

concurrencyPredicateName :: String
concurrencyPredicateName :: String
concurrencyPredicateName = String
"showConcurrency"

concurrencyTransition1 :: String
concurrencyTransition1 :: String
concurrencyTransition1 = String -> String -> String
skolemVariable String
concurrencyPredicateName String
transition1

concurrencyTransition2 :: String
concurrencyTransition2 :: String
concurrencyTransition2 = String -> String -> String
skolemVariable String
concurrencyPredicateName String
transition2

transition1 :: String
transition1 :: String
transition1 = String
"transition1"

transition2 :: String
transition2 :: String
transition2 = String
"transition2"

{-|
Parses the concurrency Skolem variables for singleton of transitions and returns
both as tuple.
It throws an error instead if unexpected behaviour occurs.
-}
parseConcurrency :: MonadThrow m => AlloyInstance -> m (Concurrent Object)
parseConcurrency :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (Concurrent Object)
parseConcurrency AlloyInstance
inst = do
  Set Object
t1 <- AlloyInstance -> String -> String -> m (Set Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> String -> String -> m (Set Object)
unscopedSingleSig AlloyInstance
inst String
concurrencyTransition1 String
""
  Set Object
t2 <- AlloyInstance -> String -> String -> m (Set Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> String -> String -> m (Set Object)
unscopedSingleSig AlloyInstance
inst String
concurrencyTransition2 String
""
  (Object, Object) -> Concurrent Object
forall a. (a, a) -> Concurrent a
Concurrent ((Object, Object) -> Concurrent Object)
-> m (Object, Object) -> m (Concurrent Object)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((,) (Object -> Object -> (Object, Object))
-> m Object -> m (Object -> (Object, Object))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Set Object -> m Object
forall (m :: * -> *) b. MonadThrow m => Set b -> m b
asSingleton Set Object
t1 m (Object -> (Object, Object)) -> m Object -> m (Object, Object)
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Set Object -> m Object
forall (m :: * -> *) b. MonadThrow m => Set b -> m b
asSingleton Set Object
t2)

checkFindConcurrencyConfig :: FindConcurrencyConfig -> Maybe String
checkFindConcurrencyConfig :: FindConcurrencyConfig -> Maybe String
checkFindConcurrencyConfig FindConcurrencyConfig {
  AdvConfig
$sel:advConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> AdvConfig
advConfig :: AdvConfig
advConfig,
  BasicConfig
$sel:basicConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  ChangeConfig
$sel:changeConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> ChangeConfig
changeConfig :: ChangeConfig
changeConfig,
  GraphConfig
$sel:graphConfig:FindConcurrencyConfig :: FindConcurrencyConfig -> GraphConfig
graphConfig :: GraphConfig
graphConfig
  }
  = BasicConfig -> ChangeConfig -> GraphConfig -> Maybe String
checkConfigForFind BasicConfig
basicConfig ChangeConfig
changeConfig 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 -> AdvConfig -> Maybe String
forall {a}.
InterpSink (IsCustomSink a) a =>
BasicConfig -> AdvConfig -> Maybe a
additionalCheck BasicConfig
basicConfig AdvConfig
advConfig
  where
    additionalCheck :: BasicConfig -> AdvConfig -> Maybe a
additionalCheck BasicConfig {Int
Maybe Bool
(Int, Int)
$sel:places:BasicConfig :: BasicConfig -> Int
$sel:transitions:BasicConfig :: BasicConfig -> Int
places :: Int
transitions :: Int
atLeastActive :: Int
flowOverall :: (Int, Int)
maxTokensPerPlace :: Int
maxFlowPerEdge :: Int
tokensOverall :: (Int, Int)
isConnected :: Maybe Bool
$sel:atLeastActive:BasicConfig :: BasicConfig -> Int
$sel:flowOverall:BasicConfig :: BasicConfig -> (Int, Int)
$sel:maxTokensPerPlace:BasicConfig :: BasicConfig -> Int
$sel:maxFlowPerEdge:BasicConfig :: BasicConfig -> Int
$sel:tokensOverall:BasicConfig :: BasicConfig -> (Int, Int)
$sel:isConnected:BasicConfig :: BasicConfig -> Maybe Bool
..} AdvConfig {Maybe Bool
presenceOfSelfLoops :: Maybe Bool
presenceOfSinkTransitions :: Maybe Bool
presenceOfSourceTransitions :: Maybe Bool
$sel:presenceOfSelfLoops:AdvConfig :: AdvConfig -> Maybe Bool
$sel:presenceOfSinkTransitions:AdvConfig :: AdvConfig -> Maybe Bool
$sel:presenceOfSourceTransitions:AdvConfig :: AdvConfig -> Maybe Bool
..}
      | Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= Maybe Bool
presenceOfSourceTransitions, Int
atLeastActive Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2
      = a -> Maybe a
forall a. a -> Maybe a
Just [iii|
        When 'atLeastActive' is greater than 2
        'presenceOfSourceTransitions' has to be 'Just False'
        |]
      | Bool
otherwise
      = Maybe a
forall a. Maybe a
Nothing

checkPickConcurrencyConfig :: PickConcurrencyConfig -> Maybe String
checkPickConcurrencyConfig :: PickConcurrencyConfig -> Maybe String
checkPickConcurrencyConfig PickConcurrencyConfig {
  BasicConfig
$sel:basicConfig:PickConcurrencyConfig :: PickConcurrencyConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  ChangeConfig
$sel:changeConfig:PickConcurrencyConfig :: PickConcurrencyConfig -> ChangeConfig
changeConfig :: ChangeConfig
changeConfig,
  GraphConfig
$sel:graphConfig:PickConcurrencyConfig :: PickConcurrencyConfig -> GraphConfig
graphConfig :: GraphConfig
graphConfig,
  Bool
$sel:useDifferentGraphLayouts:PickConcurrencyConfig :: PickConcurrencyConfig -> Bool
useDifferentGraphLayouts :: Bool
useDifferentGraphLayouts
  }
  = Bool
-> Int
-> BasicConfig
-> ChangeConfig
-> GraphConfig
-> Maybe String
checkConfigForPick
    Bool
useDifferentGraphLayouts
    Int
wrong
    BasicConfig
basicConfig
    ChangeConfig
changeConfig
    GraphConfig
graphConfig

defaultPickConcurrencyInstance :: PickInstance SimplePetriNet
defaultPickConcurrencyInstance :: PickInstance SimplePetriNet
defaultPickConcurrencyInstance = PickInstance {
  $sel:nets:PickInstance :: Map Int (Bool, Drawable SimplePetriNet)
nets = [(Int, (Bool, Drawable SimplePetriNet))]
-> Map Int (Bool, Drawable SimplePetriNet)
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [
    (Int
1,(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
M.fromList [
          (String
"s1",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
M.fromList [(String
"t1",Int
2),(String
"t2",Int
1),(String
"t3",Int
1)]}),
          (String
"s2",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
"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
M.fromList [(String
"t1",Int
1)]}),
          (String
"s4",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
"t1",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(String
"s1",Int
1),(String
"s4",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
M.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
M.fromList [(String
"s2",Int
1),(String
"s3",Int
1)]})
          ]
        },
      DrawSettings {
        $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
False,
        $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
        $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
False,
        $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
        $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Fdp
        }
      ))),
    (Int
2,(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
M.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
M.fromList [(String
"t1",Int
2),(String
"t2",Int
1),(String
"t3",Int
1)]}),
          (String
"s2",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
"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
M.fromList [(String
"t1",Int
1)]}),
          (String
"s4",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
M.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
M.fromList [(String
"s1",Int
1),(String
"s4",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
M.fromList [(String
"s1",Int
1),(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
M.fromList [(String
"s2",Int
1),(String
"s3",Int
1)]})
          ]
        },
      DrawSettings {
        $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
False,
        $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
        $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
False,
        $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
        $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Fdp
        }
      )))
    ],
  $sel:showSolution:PickInstance :: Bool
showSolution = Bool
False,
  $sel:addText:PickInstance :: Maybe (Map Language String)
addText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }

defaultFindConcurrencyInstance :: FindInstance SimplePetriNet (Concurrent Transition)
defaultFindConcurrencyInstance :: FindInstance SimplePetriNet (Concurrent Transition)
defaultFindConcurrencyInstance = FindInstance {
  $sel:drawFindWith:FindInstance :: DrawSettings
drawFindWith = DrawSettings {
    $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
False,
    $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
    },
  $sel:toFind:FindInstance :: Concurrent Transition
toFind = (Transition, Transition) -> Concurrent Transition
forall a. (a, a) -> Concurrent a
Concurrent (Int -> Transition
Transition Int
1,Int -> Transition
Transition Int
3),
  $sel:net:FindInstance :: SimplePetriNet
net = 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
M.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
M.fromList [(String
"t1",Int
1),(String
"t2",Int
2),(String
"t3",Int
1)]}),
      (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
1, $sel:flowOut:SimplePlace :: Map String Int
flowOut = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(String
"t3",Int
1)]}),
      (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
M.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
M.fromList [(String
"s2",Int
1),(String
"s4",Int
2)]}),
      (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
M.fromList [(String
"s2",Int
2)]})
      ]
    },
  $sel:numberOfPlaces:FindInstance :: Int
numberOfPlaces = Int
4,
  $sel:numberOfTransitions:FindInstance :: Int
numberOfTransitions = Int
3,
  $sel:showSolution:FindInstance :: Bool
showSolution = Bool
False,
  $sel:addText:FindInstance :: Maybe (Map Language String)
addText = Maybe (Map Language String)
forall a. Maybe a
Nothing
  }