{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE LambdaCase #-}

module Modelling.PetriNet.Conflict (
  ConflictPlaces,
  checkConflictConfig,
  checkFindConflictConfig,
  checkPickConflictConfig,
  conflictPlacesShow,
  defaultFindConflictInstance,
  defaultPickConflictInstance,
  findConflict,
  findConflictEvaluation,
  findConflictGenerate,
  findConflictPlacesEvaluation,
  findConflictPlacesSolution,
  findConflictSyntax,
  findConflictTask,
  parseConflict,
  petriNetFindConflict,
  petriNetPickConflict,
  pickConflict,
  pickConflictGenerate,
  pickConflictTask,
  simpleFindConflictTask,
  simplePickConflictTask,
  ) 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 (
  FindConflictConfig (..),
  )
import qualified Modelling.PetriNet.Types         as Pick (
  PickConflictConfig (..),
  )

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

import Capabilities.Alloy               (MonadAlloy)
import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.Auxiliary.Common (
  Object,
  parseWith,
  upperFirst,
  )
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,
  lToFind,
  toFindEvaluation,
  toFindSyntax,
  )
import Modelling.PetriNet.Parser        (
  asSingleton,
  )
import Modelling.PetriNet.Pick (
  PickInstance (..),
  checkConfigForPick,
  pickGenerate,
  pickTaskInstance,
  renderPick,
  wrong,
  wrongInstances,
  )
import Modelling.PetriNet.Reach.Type (
  Place (Place),
  ShowPlace (ShowPlace),
  ShowTransition (ShowTransition),
  Transition (Transition),
  parsePlacePrec,
  parseTransitionPrec,
  )
import Modelling.PetriNet.Types         (
  AdvConfig,
  BasicConfig (..),
  ChangeConfig,
  Conflict,
  ConflictConfig (..),
  DrawSettings (..),
  FindConflictConfig (..),
  Net,
  PetriConflict (Conflict, conflictPlaces, conflictTrans),
  PetriConflict' (PetriConflict', toPetriConflict),
  PetriLike (PetriLike, allNodes),
  PickConflictConfig (..),
  SimpleNode (..),
  SimplePetriNet,
  allDrawSettings,
  lConflictPlaces,
  transitionPairShow,
  )

import Control.Applicative              (Alternative, (<|>))
import Control.Lens                     ((.~), over)
import Control.Monad                    (unless)
import Control.Monad.Catch              (MonadCatch, MonadThrow)
import Control.Monad.Extra              (findM)
import Control.OutputCapable.Blocks (
  ArticleToUse (DefiniteArticle),
  GenericOutputCapable (..),
  LangM',
  LangM,
  OutputCapable,
  Rated,
  ($=<<),
  continueOrAbort,
  english,
  german,
  printSolutionAndAssert,
  recoverFrom,
  translate,
  translations,
  )
import Control.OutputCapable.Blocks.Generic (
  ($>>=),
  )
import Control.Monad.Random (
  RandT,
  RandomGen,
  evalRandT,
  mkStdGen
  )
import Control.Monad.Trans              (MonadTrans (lift))
import Data.Bifunctor                   (Bifunctor (bimap))
import Data.Bitraversable               (Bitraversable (bitraverse))
import Data.Bool                        (bool)
import Data.Data                        (Data, Typeable)
import Data.Either                      (isLeft)
import Data.Function                    ((&))
import Data.Foldable                    (for_)
import Data.GraphViz.Commands           (GraphvizCommand (Circo, Fdp))
import Data.List                        (partition, sort)
import Data.List.Extra                  (nubSort)
import Data.Ratio                       ((%))
import Data.String.Interpolate          (i, iii)
import Language.Alloy.Call (
  AlloyInstance
  )
import System.Random.Shuffle            (shuffleM)

simpleFindConflictTask
  :: (
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    OutputCapable m
    )
  => FilePath
  -> FindInstance SimplePetriNet Conflict
  -> LangM m
simpleFindConflictTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
String -> FindInstance SimplePetriNet Conflict -> LangM m
simpleFindConflictTask = String -> FindInstance SimplePetriNet Conflict -> 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) Conflict -> LangM m
findConflictTask

findConflictTask
  :: (
    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) Conflict
  -> LangM m
findConflictTask :: 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) Conflict -> LangM m
findConflictTask String
path FindInstance (p n String) Conflict
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) Conflict -> p n String
forall n a. FindInstance n a -> n
net FindInstance (p n String) Conflict
task) (FindInstance (p n String) Conflict -> DrawSettings
forall n a. FindInstance n a -> DrawSettings
drawFindWith FindInstance (p n String) Conflict
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 pair of transitions is in conflict under the initial marking?"
    String -> State (Map Language String) ()
german String
"Welches Paar von Transitionen steht unter der Startmarkierung in Konflikt?"
  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 String
"State your answer by giving a pair of conflicting transitions. "
      String -> State (Map Language String) ()
german String
"Geben Sie Ihre Antwort durch Angabe eines Paars von in Konflikt stehenden 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 [i| as answer would indicate that transitions #{t1} and #{t2} are in conflict under the initial marking. |]
      String -> State (Map Language String) ()
german [i| als Antwort würde bedeuten, dass Transitionen #{t1} und #{t2} unter der Startmarkierung in Konflikt stehen. |]
    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 String
"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) Conflict -> Maybe (Map Language String)
forall n a. FindInstance n a -> Maybe (Map Language String)
Find.addText FindInstance (p n String) Conflict
task
  pure ()

findConflictSyntax
  :: OutputCapable m
  => FindInstance net Conflict
  -> (Transition, Transition)
  -> LangM' m ()
findConflictSyntax :: forall (m :: * -> *) net.
OutputCapable m =>
FindInstance net Conflict
-> (Transition, Transition) -> LangM' m ()
findConflictSyntax = 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 Conflict -> Int)
-> FindInstance net Conflict
-> (Transition, Transition)
-> LangM' m ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindInstance net Conflict -> Int
forall n a. FindInstance n a -> Int
numberOfTransitions

findConflictEvaluation
  :: (Alternative m, Monad m, OutputCapable m)
  => FindInstance net Conflict
  -> (Transition, Transition)
  -> Rated m
findConflictEvaluation :: forall (m :: * -> *) net.
(Alternative m, Monad m, OutputCapable m) =>
FindInstance net Conflict -> (Transition, Transition) -> Rated m
findConflictEvaluation FindInstance net Conflict
task (Transition, Transition)
x = FindInstance net Conflict -> ConflictPlaces -> Rated m
forall (m :: * -> *) n.
(Alternative m, Monad m, OutputCapable m) =>
FindInstance n Conflict -> ConflictPlaces -> Rated m
findConflictPlacesEvaluation
  (FindInstance net Conflict
task FindInstance net Conflict
-> (FindInstance net Conflict -> FindInstance net Conflict)
-> FindInstance net Conflict
forall a b. a -> (a -> b) -> b
& (Conflict -> Identity Conflict)
-> FindInstance net Conflict
-> Identity (FindInstance net Conflict)
forall n a1 a2 (f :: * -> *).
Functor f =>
(a1 -> f a2) -> FindInstance n a1 -> f (FindInstance n a2)
lToFind ((Conflict -> Identity Conflict)
 -> FindInstance net Conflict
 -> Identity (FindInstance net Conflict))
-> (([Place] -> Identity [Place]) -> Conflict -> Identity Conflict)
-> ([Place] -> Identity [Place])
-> FindInstance net Conflict
-> Identity (FindInstance net Conflict)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Place] -> Identity [Place]) -> Conflict -> Identity Conflict
forall p1 t p2 (f :: * -> *).
Functor f =>
([p1] -> f [p2]) -> PetriConflict p1 t -> f (PetriConflict p2 t)
lConflictPlaces (([Place] -> Identity [Place])
 -> FindInstance net Conflict
 -> Identity (FindInstance net Conflict))
-> [Place]
-> FindInstance net Conflict
-> FindInstance net Conflict
forall s t a b. ASetter s t a b -> b -> s -> t
.~ [])
  ((Transition, Transition)
x, [])

type ConflictPlaces = ((Transition, Transition), [Place])

findConflictSolution :: FindInstance net (PetriConflict p t) -> (t, t)
findConflictSolution :: forall net p t. FindInstance net (PetriConflict p t) -> (t, t)
findConflictSolution = PetriConflict p t -> (t, t)
forall p t. PetriConflict p t -> (t, t)
conflictTrans (PetriConflict p t -> (t, t))
-> (FindInstance net (PetriConflict p t) -> PetriConflict p t)
-> FindInstance net (PetriConflict p t)
-> (t, t)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FindInstance net (PetriConflict p t) -> PetriConflict p t
forall n a. FindInstance n a -> a
toFind

conflictPlacesShow
  :: ConflictPlaces
  -> ((ShowTransition, ShowTransition), [ShowPlace])
conflictPlacesShow :: ConflictPlaces -> ((ShowTransition, ShowTransition), [ShowPlace])
conflictPlacesShow = ((Transition, Transition) -> (ShowTransition, ShowTransition))
-> ([Place] -> [ShowPlace])
-> ConflictPlaces
-> ((ShowTransition, ShowTransition), [ShowPlace])
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
  (Transition, Transition) -> (ShowTransition, ShowTransition)
sortedTransitionPair
  ((Place -> ShowPlace) -> [Place] -> [ShowPlace]
forall a b. (a -> b) -> [a] -> [b]
map Place -> ShowPlace
ShowPlace ([Place] -> [ShowPlace])
-> ([Place] -> [Place]) -> [Place] -> [ShowPlace]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Place] -> [Place]
forall a. Ord a => [a] -> [a]
sort)
  where
    sortedTransitionPair :: (Transition, Transition) -> (ShowTransition, ShowTransition)
sortedTransitionPair (Transition
t1, Transition
t2) =
      let (Transition
first, Transition
second) = if Transition
t1 Transition -> Transition -> Bool
forall a. Ord a => a -> a -> Bool
<= Transition
t2 then (Transition
t1, Transition
t2) else (Transition
t2, Transition
t1)
      in (Transition -> ShowTransition)
-> (Transition -> ShowTransition)
-> (Transition, Transition)
-> (ShowTransition, ShowTransition)
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 Transition -> ShowTransition
ShowTransition Transition -> ShowTransition
ShowTransition (Transition
first, Transition
second)

findConflictPlacesEvaluation
  :: (Alternative m, Monad m, OutputCapable m)
  => FindInstance n Conflict
  -> ConflictPlaces
  -> Rated m
findConflictPlacesEvaluation :: forall (m :: * -> *) n.
(Alternative m, Monad m, OutputCapable m) =>
FindInstance n Conflict -> ConflictPlaces -> Rated m
findConflictPlacesEvaluation FindInstance n Conflict
task ((Transition, Transition)
conflict, [Place]
ps) =
  Map Language String
-> Bool
-> (Transition, Transition)
-> (Transition, Transition)
-> LangM' m (Maybe String, Ratio Integer)
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)
conf (Transition, Transition)
conflict LangM' m (Maybe String, Ratio Integer)
-> ((Maybe String, Ratio Integer)
    -> GenericLangM Language m (Ratio Integer))
-> GenericLangM Language m (Ratio Integer)
forall (m :: * -> *) l a b.
Monad m =>
GenericLangM l m a
-> (a -> GenericLangM l m b) -> GenericLangM l m b
$>>= \(Maybe String
ms, Ratio Integer
res) -> do
  GenericLangM Language m () -> GenericLangM Language m ()
forall (m :: * -> *) l.
Alternative m =>
GenericLangM l m () -> GenericLangM l m ()
recoverFrom (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([Place] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Place]
inducing Bool -> Bool -> Bool
|| Ratio Integer
res Ratio Integer -> Ratio Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Ratio Integer
0) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
    [Place]
-> (Place -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Place]
ps' ((Place -> GenericLangM Language m ())
 -> GenericLangM Language m ())
-> (Place -> GenericLangM Language m ())
-> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ \Place
x -> Bool -> GenericLangM Language m () -> GenericLangM Language m ()
assert (Place
x Place -> [Place] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Place]
inducing) (GenericLangM Language m () -> GenericLangM Language m ())
-> GenericLangM Language m () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> GenericLangM Language m ()
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> GenericLangM Language m ())
-> State (Map Language String) () -> GenericLangM Language m ()
forall a b. (a -> b) -> a -> b
$ do
      let x' :: String
x' = ShowPlace -> String
forall a. Show a => a -> String
show (ShowPlace -> String) -> ShowPlace -> String
forall a b. (a -> b) -> a -> b
$ Place -> ShowPlace
ShowPlace Place
x
      String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
x' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" is a place causing the conflict?"
      String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
x' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ist eine den Konflikt verursachende Stelle?"
    Bool -> GenericLangM Language m () -> GenericLangM Language m ()
assert ([Place]
ps' [Place] -> [Place] -> Bool
forall a. Eq a => a -> a -> Bool
== [Place]
inducing) (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 submitted solution is correct and complete?"
      String -> State (Map Language String) ()
german String
"Die eingereichte Lösung ist korrekt und vollständig?"
    pure ()
  let result :: Ratio Integer
result = Ratio Integer -> Ratio Integer -> Ratio Integer
forall a. Ord a => a -> a -> a
min
        Ratio Integer
res
        (Ratio Integer -> Ratio Integer) -> Ratio Integer -> Ratio Integer
forall a b. (a -> b) -> a -> b
$ (Integer
base Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- [Place] -> Integer
forall {a}. [a] -> Integer
size [Place]
inducing Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ [Place] -> Integer
forall {a}. [a] -> Integer
size [Place]
correct Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- [Place] -> Integer
forall {a}. [a] -> Integer
size [Place]
wrong') Integer -> Integer -> Ratio Integer
forall a. Integral a => a -> a -> Ratio a
% Integer
base
  Ratio Integer
points <- ArticleToUse
-> Maybe String
-> Ratio Integer
-> GenericLangM Language m (Ratio Integer)
forall (m :: * -> *).
OutputCapable m =>
ArticleToUse -> Maybe String -> Ratio Integer -> Rated m
printSolutionAndAssert ArticleToUse
DefiniteArticle (String -> String
fixSolution (String -> String) -> Maybe String -> Maybe String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe String
ms) Ratio Integer
result
  pure Ratio Integer
points
  where
    assert :: Bool -> GenericLangM Language m () -> GenericLangM Language m ()
assert = Bool
-> Bool -> GenericLangM Language m () -> GenericLangM Language m ()
forall (m :: * -> *).
OutputCapable m =>
Bool -> Bool -> LangM m -> LangM m
continueOrAbort Bool
withSol
    conf :: (Transition, Transition)
conf = FindInstance n Conflict -> (Transition, Transition)
forall net p t. FindInstance net (PetriConflict p t) -> (t, t)
findConflictSolution FindInstance n Conflict
task
    inducing :: [Place]
inducing = Conflict -> [Place]
forall p t. PetriConflict p t -> [p]
conflictPlaces (FindInstance n Conflict -> Conflict
forall n a. FindInstance n a -> a
toFind FindInstance n Conflict
task)
    fixSolution :: String -> String
fixSolution
      | [Place] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Place]
inducing = String -> String
forall a. a -> a
id
      | Bool
otherwise    = String -> String -> String
forall a b. a -> b -> a
const (String -> String -> String) -> String -> String -> String
forall a b. (a -> b) -> a -> b
$ ((ShowTransition, ShowTransition), [ShowPlace]) -> String
forall a. Show a => a -> String
show (((ShowTransition, ShowTransition), [ShowPlace]) -> String)
-> ((ShowTransition, ShowTransition), [ShowPlace]) -> String
forall a b. (a -> b) -> a -> b
$ ConflictPlaces -> ((ShowTransition, ShowTransition), [ShowPlace])
conflictPlacesShow ((Transition, Transition)
conf, [Place]
inducing)
    withSol :: Bool
withSol = FindInstance n Conflict -> Bool
forall n a. FindInstance n a -> Bool
Find.showSolution FindInstance n Conflict
task
    ps' :: [Place]
ps' = [Place] -> [Place]
forall a. Ord a => [a] -> [a]
nubSort [Place]
ps
    ([Place]
correct, [Place]
wrong') = (Place -> Bool) -> [Place] -> ([Place], [Place])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Place -> [Place] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Place]
inducing) [Place]
ps
    base :: Integer
base = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> Int -> Integer
forall a b. (a -> b) -> a -> b
$ Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ FindInstance n Conflict -> Int
forall n a. FindInstance n a -> Int
numberOfPlaces FindInstance n Conflict
task
    size :: [a] -> Integer
size = Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Integer) -> ([a] -> Int) -> [a] -> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
    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
"have a conflict"
        String -> State (Map Language String) ()
german String
"haben einen Konflikt"

findConflictPlacesSolution :: FindInstance n (PetriConflict p t) -> ((t, t), [p])
findConflictPlacesSolution :: forall n p t. FindInstance n (PetriConflict p t) -> ((t, t), [p])
findConflictPlacesSolution FindInstance n (PetriConflict p t)
task =
  (FindInstance n (PetriConflict p t) -> (t, t)
forall net p t. FindInstance net (PetriConflict p t) -> (t, t)
findConflictSolution FindInstance n (PetriConflict p t)
task, PetriConflict p t -> [p]
forall p t. PetriConflict p t -> [p]
conflictPlaces (PetriConflict p t -> [p]) -> PetriConflict p t -> [p]
forall a b. (a -> b) -> a -> b
$ FindInstance n (PetriConflict p t) -> PetriConflict p t
forall n a. FindInstance n a -> a
toFind FindInstance n (PetriConflict p t)
task)

simplePickConflictTask
  :: (
    MonadCache m,
    MonadDiagrams m,
    MonadGraphviz m,
    MonadThrow m,
    OutputCapable m
    )
  => FilePath
  -> PickInstance SimplePetriNet
  -> LangM m
simplePickConflictTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
String -> PickInstance SimplePetriNet -> LangM m
simplePickConflictTask = 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
pickConflictTask

pickConflictTask
  :: (
    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
pickConflictTask :: 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
pickConflictTask 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 in conflict
      under the initial marking?
      |]
    String -> State (Map Language String) ()
german [iii|
      Welches dieser Petrinetze hat genau ein Paar von Transitionen,
      die unter der Startmarkierung in Konflikt stehen?
      |]
  (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 conflicting transitions.#{" "}
      |]
    String -> State (Map Language String) ()
german [iii|
      Geben Sie Ihre Antwort durch Angabe der Nummer des Petrinetzes an,
      das diese in Konflikt stehenden 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 in conflict
        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
        in Konflikt stehende 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 ()

findConflictGenerate
  :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n)
  => FindConflictConfig
  -> Int
  -> Int
  -- ^ Seed
  -> m (FindInstance (p n String) Conflict)
findConflictGenerate :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n) =>
FindConflictConfig
-> Int -> Int -> m (FindInstance (p n String) Conflict)
findConflictGenerate FindConflictConfig
config Int
segment = RandT StdGen m (FindInstance (p n String) Conflict)
-> StdGen -> m (FindInstance (p n String) Conflict)
forall (m :: * -> *) g a. Monad m => RandT g m a -> g -> m a
evalRandT RandT StdGen m (FindInstance (p n String) Conflict)
getInstance (StdGen -> m (FindInstance (p n String) Conflict))
-> (Int -> StdGen) -> Int -> m (FindInstance (p n String) Conflict)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> StdGen
mkStdGen
  where
    getInstance :: RandT StdGen m (FindInstance (p n String) Conflict)
getInstance = do
      (p n String, PetriConflict' String)
petriConflict <- FindConflictConfig
-> Int -> RandT StdGen m (p n String, PetriConflict' String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
FindConflictConfig
-> Int -> RandT g m (p n String, PetriConflict' String)
findConflict FindConflictConfig
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
$ FindConflictConfig -> GraphConfig
Find.graphConfig FindConflictConfig
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, PetriConflict' String) -> p n String
forall a b. (a, b) -> a
fst (p n String, PetriConflict' String)
petriConflict)) [DrawSettings]
ds
      RandT StdGen m (FindInstance (p n String) Conflict)
-> (DrawSettings
    -> RandT StdGen m (FindInstance (p n String) Conflict))
-> Maybe DrawSettings
-> RandT StdGen m (FindInstance (p n String) Conflict)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe RandT StdGen m (FindInstance (p n String) Conflict)
getInstance ((p n String
 -> PetriConflict' String
 -> DrawSettings
 -> RandT StdGen m (FindInstance (p n String) Conflict))
-> (p n String, PetriConflict' String)
-> DrawSettings
-> RandT StdGen m (FindInstance (p n String) Conflict)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry p n String
-> PetriConflict' String
-> DrawSettings
-> RandT StdGen m (FindInstance (p n String) Conflict)
forall {t :: (* -> *) -> * -> *} {m :: * -> *} {n}.
(MonadTrans t, MonadThrow m, Functor (t m)) =>
n
-> PetriConflict' String
-> DrawSettings
-> t m (FindInstance n Conflict)
toInstance (p n String, PetriConflict' String)
petriConflict) Maybe DrawSettings
d
    toInstance :: n
-> PetriConflict' String
-> DrawSettings
-> t m (FindInstance n Conflict)
toInstance n
petri PetriConflict' String
conflict DrawSettings
drawSettings = do
      Conflict
c' <- m Conflict -> t m Conflict
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 Conflict -> t m Conflict) -> m Conflict -> t m Conflict
forall a b. (a -> b) -> a -> b
$ (String -> m Place)
-> (String -> m Transition)
-> PetriConflict String String
-> m Conflict
forall (f :: * -> *) a c b d.
Applicative f =>
(a -> f c)
-> (b -> f d) -> PetriConflict a b -> f (PetriConflict c d)
forall (t :: * -> * -> *) (f :: * -> *) a c b d.
(Bitraversable t, Applicative f) =>
(a -> f c) -> (b -> f d) -> t a b -> f (t c d)
bitraverse
        ((Int -> Parser Place) -> String -> m Place
forall (m :: * -> *) a.
MonadThrow m =>
(Int -> Parser a) -> String -> m a
parseWith Int -> Parser Place
parsePlacePrec)
        ((Int -> Parser Transition) -> String -> m Transition
forall (m :: * -> *) a.
MonadThrow m =>
(Int -> Parser a) -> String -> m a
parseWith Int -> Parser Transition
parseTransitionPrec)
        (PetriConflict String String -> m Conflict)
-> PetriConflict String String -> m Conflict
forall a b. (a -> b) -> a -> b
$ PetriConflict' String -> PetriConflict String String
forall x. PetriConflict' x -> PetriConflict x x
toPetriConflict PetriConflict' String
conflict
      return $ FindInstance {
        $sel:drawFindWith:FindInstance :: DrawSettings
drawFindWith = DrawSettings
drawSettings,
        $sel:toFind:FindInstance :: Conflict
toFind = (([Place] -> Identity [Place]) -> Conflict -> Identity Conflict)
-> ([Place] -> [Place]) -> Conflict -> Conflict
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
over ([Place] -> Identity [Place]) -> Conflict -> Identity Conflict
forall p1 t p2 (f :: * -> *).
Functor f =>
([p1] -> f [p2]) -> PetriConflict p1 t -> f (PetriConflict p2 t)
lConflictPlaces [Place] -> [Place]
forall a. Ord a => [a] -> [a]
nubSort Conflict
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 = FindConflictConfig -> Bool
Find.printSolution FindConflictConfig
config,
        $sel:addText:FindInstance :: Maybe (Map Language String)
addText = FindConflictConfig -> Maybe (Map Language String)
Find.extraText FindConflictConfig
config
        }
    bc :: BasicConfig
bc = FindConflictConfig -> BasicConfig
Find.basicConfig FindConflictConfig
config

pickConflictGenerate
  :: (MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m, Net p n)
  => PickConflictConfig
  -> Int
  -> Int
  -> m (PickInstance (p n String))
pickConflictGenerate :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadAlloy m, MonadCatch m, MonadDiagrams m, MonadGraphviz m,
 Net p n) =>
PickConflictConfig -> Int -> Int -> m (PickInstance (p n String))
pickConflictGenerate = (PickConflictConfig
 -> Int
 -> RandT StdGen m [(p n String, Maybe (PetriConflict' String))])
-> (PickConflictConfig -> GraphConfig)
-> (PickConflictConfig -> Bool)
-> (PickConflictConfig -> Bool)
-> (PickConflictConfig -> Maybe (Map Language String))
-> PickConflictConfig
-> 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 PickConflictConfig
-> Int
-> RandT StdGen m [(p n String, Maybe (PetriConflict' String))]
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
PickConflictConfig
-> Int -> RandT g m [(p n String, Maybe (PetriConflict' String))]
pickConflict PickConflictConfig -> GraphConfig
gc PickConflictConfig -> Bool
ud PickConflictConfig -> Bool
ws PickConflictConfig -> Maybe (Map Language String)
et
  where
    gc :: PickConflictConfig -> GraphConfig
gc = PickConflictConfig -> GraphConfig
Pick.graphConfig
    ud :: PickConflictConfig -> Bool
ud = PickConflictConfig -> Bool
Pick.useDifferentGraphLayouts
    ws :: PickConflictConfig -> Bool
ws = PickConflictConfig -> Bool
Pick.printSolution
    et :: PickConflictConfig -> Maybe (Map Language String)
et = PickConflictConfig -> Maybe (Map Language String)
Pick.extraText

findConflict
  :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g)
  => FindConflictConfig
  -> Int
  -> RandT
    g
    m
    (p n String, PetriConflict' String)
findConflict :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
FindConflictConfig
-> Int -> RandT g m (p n String, PetriConflict' String)
findConflict = ((AlloyInstance -> m (PetriConflict' Object))
 -> AlloyInstance -> RandT g m (p n String, PetriConflict' String))
-> (FindConflictConfig -> String)
-> (AlloyInstance -> m (PetriConflict' Object))
-> (FindConflictConfig -> AlloyConfig)
-> FindConflictConfig
-> Int
-> RandT g m (p n String, PetriConflict' 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 (PetriConflict' Object))
-> AlloyInstance -> RandT g m (p n String, PetriConflict' 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
  FindConflictConfig -> String
petriNetFindConflict
  AlloyInstance -> m (PetriConflict' Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (PetriConflict' Object)
parseConflict
  FindConflictConfig -> AlloyConfig
Find.alloyConfig

petriNetFindConflict :: FindConflictConfig -> String
petriNetFindConflict :: FindConflictConfig -> String
petriNetFindConflict FindConflictConfig {
  BasicConfig
$sel:basicConfig:FindConflictConfig :: FindConflictConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  AdvConfig
advConfig :: AdvConfig
$sel:advConfig:FindConflictConfig :: FindConflictConfig -> AdvConfig
advConfig,
  ChangeConfig
changeConfig :: ChangeConfig
$sel:changeConfig:FindConflictConfig :: FindConflictConfig -> ChangeConfig
changeConfig,
  ConflictConfig
conflictConfig :: ConflictConfig
$sel:conflictConfig:FindConflictConfig :: FindConflictConfig -> ConflictConfig
conflictConfig,
  Maybe Bool
uniqueConflictPlace :: Maybe Bool
$sel:uniqueConflictPlace:FindConflictConfig :: FindConflictConfig -> Maybe Bool
uniqueConflictPlace
  }
  = BasicConfig
-> ChangeConfig
-> ConflictConfig
-> Maybe Bool
-> Either Bool AdvConfig
-> String
petriNetConflictAlloy
    BasicConfig
basicConfig
    ChangeConfig
changeConfig
    ConflictConfig
conflictConfig
    Maybe Bool
uniqueConflictPlace
    (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

pickConflict
  :: (MonadAlloy m, MonadThrow m, Net p n, RandomGen g)
  => PickConflictConfig
  -> Int
  -> RandT
    g
    m
    [(p n String, Maybe (PetriConflict' String))]
pickConflict :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) g.
(MonadAlloy m, MonadThrow m, Net p n, RandomGen g) =>
PickConflictConfig
-> Int -> RandT g m [(p n String, Maybe (PetriConflict' String))]
pickConflict = ((AlloyInstance -> RandT g m (PetriConflict' Object))
 -> AlloyInstance
 -> RandT g m [(p n String, Maybe (PetriConflict' String))])
-> (PickConflictConfig -> String)
-> (AlloyInstance -> RandT g m (PetriConflict' Object))
-> (PickConflictConfig -> AlloyConfig)
-> PickConflictConfig
-> Int
-> RandT g m [(p n String, Maybe (PetriConflict' 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 (PetriConflict' Object))
-> AlloyInstance
-> RandT g m [(p n String, Maybe (PetriConflict' 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
  PickConflictConfig -> String
petriNetPickConflict
  AlloyInstance -> RandT g m (PetriConflict' Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (PetriConflict' Object)
parseConflict
  PickConflictConfig -> AlloyConfig
Pick.alloyConfig

petriNetPickConflict :: PickConflictConfig -> String
petriNetPickConflict :: PickConflictConfig -> String
petriNetPickConflict PickConflictConfig {
  BasicConfig
basicConfig :: BasicConfig
$sel:basicConfig:PickConflictConfig :: PickConflictConfig -> BasicConfig
basicConfig,
  ChangeConfig
changeConfig :: ChangeConfig
$sel:changeConfig:PickConflictConfig :: PickConflictConfig -> ChangeConfig
changeConfig,
  ConflictConfig
conflictConfig :: ConflictConfig
$sel:conflictConfig:PickConflictConfig :: PickConflictConfig -> ConflictConfig
conflictConfig,
  Bool
prohibitSourceTransitions :: Bool
$sel:prohibitSourceTransitions:PickConflictConfig :: PickConflictConfig -> Bool
prohibitSourceTransitions,
  Maybe Bool
uniqueConflictPlace :: Maybe Bool
$sel:uniqueConflictPlace:PickConflictConfig :: PickConflictConfig -> Maybe Bool
uniqueConflictPlace
  }
  = BasicConfig
-> ChangeConfig
-> ConflictConfig
-> Maybe Bool
-> Either Bool AdvConfig
-> String
petriNetConflictAlloy
    BasicConfig
basicConfig
    ChangeConfig
changeConfig
    ConflictConfig
conflictConfig
    Maybe Bool
uniqueConflictPlace
    (Bool -> Either Bool AdvConfig
forall a b. a -> Either a b
Left Bool
prohibitSourceTransitions)

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

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

pred #{conflictPredicateName}[#{p} : some Places,#{defaultActiveTrans}#{activated} : set Transitions, #{t1}, #{t2} : Transitions] {
  \#Places = #{places basicC}
  \#Transitions = #{transitions basicC}
  #{compBasicConstraints activated basicC}
  #{compChange changeC}
  #{multiplePlaces uniqueConflictP}
  #{sourceTransitionConstraints}
  no x,y : givenTransitions, z : givenPlaces | conflictDefault[x,y,z]
  all q : #{p} | conflict[#{t1}, #{t2}, q]
  no q : (Places - #{p}) | conflict[#{t1}, #{t2}, q]
  all u,v : Transitions, q : Places |
    conflict[u,v,q] implies #{t1} + #{t2} = u + v
  #{preconditions ""}
  #{preconditions "Default"}
  #{conflictDistractor "" ""}
  #{conflictDistractor "given" "default"}
  #{compConstraints}
}

run #{conflictPredicateName} 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
""
    preconditions :: String -> String
    preconditions :: String -> String
preconditions String
which = ((Bool -> String) -> Maybe Bool -> String)
-> Maybe Bool -> (Bool -> String) -> String
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> String) -> Maybe Bool -> String
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (ConflictConfig -> Maybe Bool
addConflictCommonPreconditions ConflictConfig
conflictC)
      ((Bool -> String) -> String) -> (Bool -> String) -> String
forall a b. (a -> b) -> a -> b
$ \case
      Bool
True  -> [i|some (common#{which}Preconditions[#{t1}, #{t2}] - #{p})|]
      Bool
False -> [i|no (common#{which}Preconditions[#{t1}, #{t2}] - #{p})|]
    conflictDistractor :: String -> String -> String
    conflictDistractor :: String -> String -> String
conflictDistractor String
what String
which = ((Bool -> String) -> Maybe Bool -> String)
-> Maybe Bool -> (Bool -> String) -> String
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Bool -> String) -> Maybe Bool -> String
forall m a. Monoid m => (a -> m) -> Maybe a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (ConflictConfig -> Maybe Bool
withConflictDistractors ConflictConfig
conflictC) ((Bool -> String) -> String) -> (Bool -> String) -> String
forall a b. (a -> b) -> a -> b
$ \Bool
x ->
      [i|let ts = #{what}Transitions - #{t1} - #{t2} |
    |] String -> String -> String
forall a. [a] -> [a] -> [a]
++
        let op :: String
op = ConflictConfig -> Maybe Bool
conflictDistractorAddExtraPreconditions ConflictConfig
conflictC
                   Maybe Bool -> (Maybe Bool -> String) -> String
forall a b. a -> (a -> b) -> b
& String -> (Bool -> String) -> Maybe Bool -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
">=" (String -> String -> Bool -> String
forall a. a -> a -> Bool -> a
bool String
"=" String
">")
            prepend :: String -> String
prepend = if String -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
which then String -> String
forall a. a -> a
id else (String
which String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String) -> (String -> String) -> String -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
upperFirst
            tokens :: String
tokens  = String -> String
prepend String
"tokens"
            flow :: String
flow    = String -> String
prepend String
"flow"
            distractorConflictLike :: String
distractorConflictLike = ConflictConfig -> Bool
conflictDistractorOnlyConflictLike ConflictConfig
conflictC
              Bool -> (Bool -> String) -> String
forall a b. a -> (a -> b) -> b
& String -> String -> Bool -> String
forall a. a -> a -> Bool -> a
bool String
"" [i|all p : ps | p.#{tokens} >= p.#{flow}[t1] and p.#{tokens} >= p.#{flow}[t2]
        some p : ps | p.#{tokens} < plus[p.#{flow}[t1], p.#{flow}[t2]]|]
            distractorConcurrentLike :: String
distractorConcurrentLike = ConflictConfig -> Bool
conflictDistractorOnlyConcurrentLike ConflictConfig
conflictC
              Bool -> (Bool -> String) -> String
forall a b. a -> (a -> b) -> b
& String -> String -> Bool -> String
forall a. a -> a -> Bool -> a
bool String
"" [i|all p : ps | p.#{tokens} >= plus[p.#{flow}[t1], p.#{flow}[t2]]|]
        in if Bool
x
        then [i|some t1 : ts | one t2 : ts - t1 |
      let ps = common#{upperFirst which}Preconditions[t1, t2] {
        \#ps #{op} \##{p}
        #{distractorConflictLike}
        #{distractorConcurrentLike}
      }|]
        else [i|no t1, t2 : ts |
      let ps = common#{upperFirst which}Preconditions[t1, t2] |
        \#ps > 1 and all p : ps | p.#{tokens} >= p.#{flow}[t1] and p.#{tokens} >= p.#{flow}[t2]|]
    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
""
    multiplePlaces :: Maybe Bool -> String
multiplePlaces Maybe Bool
unique
      | Maybe Bool
unique Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
      = [i|one #{p}|]
      | Maybe Bool
unique Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
      = [i|not (one #{p})|]
      | Bool
otherwise
      = String
""
    p :: String
p  = String
places1
    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

conflictPredicateName :: String
conflictPredicateName :: String
conflictPredicateName = String
"showConflict"

conflictPlaces1 :: String
conflictPlaces1 :: String
conflictPlaces1 = String -> String -> String
skolemVariable String
conflictPredicateName String
places1

conflictTransition1 :: String
conflictTransition1 :: String
conflictTransition1 = String -> String -> String
skolemVariable String
conflictPredicateName String
transition1

conflictTransition2 :: String
conflictTransition2 :: String
conflictTransition2 = String -> String -> String
skolemVariable String
conflictPredicateName String
transition2

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

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

places1 :: String
places1 :: String
places1 = String
"places"

{-|
Parses the conflict Skolem variables for singleton of transitions and returns
both as tuple.
It returns an error message instead if unexpected behaviour occurs.
-}
parseConflict :: MonadThrow m => AlloyInstance -> m (PetriConflict' Object)
parseConflict :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (PetriConflict' Object)
parseConflict AlloyInstance
inst = do
  Set Object
tc1 <- AlloyInstance -> String -> String -> m (Set Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> String -> String -> m (Set Object)
unscopedSingleSig AlloyInstance
inst String
conflictTransition1 String
""
  Set Object
tc2 <- AlloyInstance -> String -> String -> m (Set Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> String -> String -> m (Set Object)
unscopedSingleSig AlloyInstance
inst String
conflictTransition2 String
""
  Set Object
pc  <- AlloyInstance -> String -> String -> m (Set Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> String -> String -> m (Set Object)
unscopedSingleSig AlloyInstance
inst String
conflictPlaces1 String
""
  PetriConflict Object Object -> PetriConflict' Object
forall x. PetriConflict x x -> PetriConflict' x
PetriConflict' (PetriConflict Object Object -> PetriConflict' Object)
-> ((Object, Object) -> PetriConflict Object Object)
-> (Object, Object)
-> PetriConflict' Object
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Object, Object) -> [Object] -> PetriConflict Object Object)
-> [Object] -> (Object, Object) -> PetriConflict Object Object
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Object, Object) -> [Object] -> PetriConflict Object Object
forall p t. (t, t) -> [p] -> PetriConflict p t
Conflict (Set Object -> [Object]
forall a. Set a -> [a]
Set.toList Set Object
pc)
    ((Object, Object) -> PetriConflict' Object)
-> m (Object, Object) -> m (PetriConflict' 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
tc1 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
tc2)

checkConflictConfig :: BasicConfig -> ConflictConfig -> Maybe String
checkConflictConfig :: BasicConfig -> ConflictConfig -> Maybe String
checkConflictConfig BasicConfig
bc ConflictConfig {
  Maybe Bool
$sel:addConflictCommonPreconditions:ConflictConfig :: ConflictConfig -> Maybe Bool
addConflictCommonPreconditions :: Maybe Bool
addConflictCommonPreconditions,
  Maybe Bool
$sel:withConflictDistractors:ConflictConfig :: ConflictConfig -> Maybe Bool
withConflictDistractors :: Maybe Bool
withConflictDistractors,
  Maybe Bool
$sel:conflictDistractorAddExtraPreconditions:ConflictConfig :: ConflictConfig -> Maybe Bool
conflictDistractorAddExtraPreconditions :: Maybe Bool
conflictDistractorAddExtraPreconditions,
  Bool
$sel:conflictDistractorOnlyConflictLike:ConflictConfig :: ConflictConfig -> Bool
conflictDistractorOnlyConflictLike :: Bool
conflictDistractorOnlyConflictLike,
  Bool
$sel:conflictDistractorOnlyConcurrentLike:ConflictConfig :: ConflictConfig -> Bool
conflictDistractorOnlyConcurrentLike :: Bool
conflictDistractorOnlyConcurrentLike
  }
  | Just Bool
True <- Maybe Bool
withConflictDistractors
  , Bool
conflictDistractorOnlyConflictLike Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Bool
conflictDistractorOnlyConcurrentLike
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"Either 'conflictDistractorOnlyConflictLike' or 'conflictDistractorOnlyConcurrentLike' hast to be set!"
  | Just Bool
True <- Maybe Bool
withConflictDistractors
  , BasicConfig -> Int
places BasicConfig
bc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minPlaces
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"Your current conflict configuration requires at least "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
minPlaces String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" places."
  | Just Bool
True <- Maybe Bool
withConflictDistractors
  , BasicConfig -> Int
transitions BasicConfig
bc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
minTransitions
  = String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ String
"Your current conflict configuration requires at least "
    String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
minTransitions String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" transitions."
  | Just Bool
True <- Maybe Bool
withConflictDistractors
  = Maybe String
forall a. Maybe a
Nothing
  | Just {} <- Maybe Bool
conflictDistractorAddExtraPreconditions
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'conflictDistractorAddExtraPreconditions' can only be set, if 'withConflictDistractors' is enforced."
  | Bool
conflictDistractorOnlyConflictLike
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'conflictDistractorOnlyConflictLike' can only be set, if 'withConflictDistractors' is enforced."
  | Bool
conflictDistractorOnlyConcurrentLike
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'conflictDistractorOnlyConcurrentLike' can only be set, if 'withConflictDistractors' is enforced."
  | Bool
otherwise
  = Maybe String
forall a. Maybe a
Nothing
  where
    minPlaces :: Int
minPlaces = (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> ([Int] -> Int) -> [Int] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$
      [Int
1 |  Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
addConflictCommonPreconditions]
      [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
1 | Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
==  Maybe Bool
withConflictDistractors]
      [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int
1
         | Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
withConflictDistractors
         , Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
conflictDistractorAddExtraPreconditions]
    minTransitions :: Int
minTransitions = Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Int] -> Int
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum
      [Int
2 | Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True Maybe Bool -> Maybe Bool -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe Bool
withConflictDistractors]

checkFindConflictConfig :: FindConflictConfig -> Maybe String
checkFindConflictConfig :: FindConflictConfig -> Maybe String
checkFindConflictConfig FindConflictConfig {
  BasicConfig
$sel:basicConfig:FindConflictConfig :: FindConflictConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  ChangeConfig
$sel:changeConfig:FindConflictConfig :: FindConflictConfig -> ChangeConfig
changeConfig :: ChangeConfig
changeConfig,
  ConflictConfig
$sel:conflictConfig:FindConflictConfig :: FindConflictConfig -> ConflictConfig
conflictConfig :: ConflictConfig
conflictConfig,
  GraphConfig
$sel:graphConfig:FindConflictConfig :: FindConflictConfig -> 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 -> ConflictConfig -> Maybe String
checkConflictConfig BasicConfig
basicConfig ConflictConfig
conflictConfig

checkPickConflictConfig :: PickConflictConfig -> Maybe String
checkPickConflictConfig :: PickConflictConfig -> Maybe String
checkPickConflictConfig PickConflictConfig {
  BasicConfig
$sel:basicConfig:PickConflictConfig :: PickConflictConfig -> BasicConfig
basicConfig :: BasicConfig
basicConfig,
  ChangeConfig
$sel:changeConfig:PickConflictConfig :: PickConflictConfig -> ChangeConfig
changeConfig :: ChangeConfig
changeConfig,
  ConflictConfig
$sel:conflictConfig:PickConflictConfig :: PickConflictConfig -> ConflictConfig
conflictConfig :: ConflictConfig
conflictConfig,
  GraphConfig
$sel:graphConfig:PickConflictConfig :: PickConflictConfig -> GraphConfig
graphConfig :: GraphConfig
graphConfig,
  Bool
$sel:useDifferentGraphLayouts:PickConflictConfig :: PickConflictConfig -> Bool
useDifferentGraphLayouts :: Bool
useDifferentGraphLayouts
  }
  = Bool
-> Int
-> BasicConfig
-> ChangeConfig
-> GraphConfig
-> Maybe String
checkConfigForPick
    Bool
useDifferentGraphLayouts
    Int
wrong
    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 -> ConflictConfig -> Maybe String
checkConflictConfig BasicConfig
basicConfig ConflictConfig
conflictConfig

defaultPickConflictInstance :: PickInstance SimplePetriNet
defaultPickConflictInstance :: PickInstance SimplePetriNet
defaultPickConflictInstance = 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
0, $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 = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(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 = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(String
"t3",Int
2)]}),
          (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
"s3",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
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty})]
        },
      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
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 = [(String, Int)] -> Map String Int
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList [(String
"t1",Int
1),(String
"t2",Int
1)]}),
          (String
"s3",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
"s4",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
"t3",Int
2)]}),
          (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
"s3",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
"s3",Int
1)]}),
          (String
"t3",SimpleTransition {$sel:flowOut:SimplePlace :: Map String Int
flowOut = Map String Int
forall k a. Map k a
M.empty})]
        },
      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
  }

defaultFindConflictInstance :: FindInstance SimplePetriNet Conflict
defaultFindConflictInstance :: FindInstance SimplePetriNet Conflict
defaultFindConflictInstance = 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 :: Conflict
toFind = Conflict {
    $sel:conflictTrans:Conflict :: (Transition, Transition)
conflictTrans = (Int -> Transition
Transition Int
1,Int -> Transition
Transition Int
3),
    $sel:conflictPlaces:Conflict :: [Place]
conflictPlaces = [Int -> Place
Place Int
4]
    },
  $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
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
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 = Map String Int
forall k a. Map k a
M.empty}),
      (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
M.fromList [(String
"t1",Int
1),(String
"t3",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
"s2",Int
2),(String
"s3",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
M.fromList [(String
"s3",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
"s3",Int
1)]})
      ]
    },
  $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
  }