{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TupleSections #-}
{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}

module Modelling.PetriNet.ConflictPlaces (
  checkFindConflictPlacesConfig,
  conflictInitial,
  defaultFindConflictPlacesConfig,
  defaultFindConflictPlacesInstance,
  findConflictPlacesSyntax,
  findConflictPlacesTask,
  parseConflictPlacesPrec,
  simpleFindConflictPlacesTask,
  ) where

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

import Capabilities.Cache               (MonadCache)
import Capabilities.Diagrams            (MonadDiagrams)
import Capabilities.Graphviz            (MonadGraphviz)
import Modelling.Auxiliary.Output (
  hoveringInformation,
  extra,
  )
import Modelling.PetriNet.Conflict (
  ConflictPlaces,
  checkConflictConfig,
  conflictPlacesShow,
  findConflictSyntax,
  )
import Modelling.PetriNet.Find (
  FindInstance (..),
  checkConfigForFind,
  drawFindWith,
  findInitial,
  )
import Modelling.PetriNet.Diagram (
  cacheNet,
  )
import Modelling.PetriNet.Reach.Type (
  Place (Place),
  ShowPlace (ShowPlace),
  Transition (Transition),
  parsePlacePrec,
  parseTransitionPrec,
  )
import Modelling.PetriNet.Types (
  Conflict,
  DrawSettings (..),
  FindConflictConfig (..),
  GraphConfig (..),
  Net,
  PetriConflict (..),
  PetriLike (..),
  SimpleNode (..),
  SimplePetriNet,
  defaultFindConflictConfig,
  lGraphConfig,
  lHidePlaceNames,
  )

import Control.Applicative              ((<|>))
import Control.Lens                     ((.~))
import Control.Monad                    (void)
import Control.Monad.Catch              (MonadThrow)
import Control.OutputCapable.Blocks (
  GenericOutputCapable (..),
  LangM',
  LangM,
  OutputCapable,
  ($=<<),
  continueOrAbort,
  english,
  german,
  translate,
  )
import Data.Bifunctor                   (Bifunctor (bimap))
import Data.Data                        (Data, Typeable)
import Data.Function                    ((&))
import Data.Foldable                    (for_)
import Data.GraphViz.Commands           (GraphvizCommand (Circo))
import Data.String.Interpolate          (i)
import Text.Parsec (
  char,
  endBy1,
  optionMaybe,
  optional,
  spaces,
  )
import Text.Parsec.String               (Parser)

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

findConflictPlacesTask
  :: (
    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
findConflictPlacesTask :: 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
findConflictPlacesTask 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, and because of which conflict-causing place(s), under the initial marking?"
    String -> State (Map Language String) ()
german String
"Welches Paar von Transitionen steht in Konflikt, und wegen welcher konfliktverursachenden Stelle(n), unter der Startmarkierung?"
  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 indicating a pair of conflicting transitions and a list of all the places that induce the conflict. "
      String -> State (Map Language String) ()
german String
"Geben Sie Ihre Antwort durch Angabe eines Paars von in Konflikt stehenden Transitionen und einer Liste aller Stellen, die den Konflikt verursachen. "
    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), [ShowPlace])
ts = ConflictPlaces -> ((ShowTransition, ShowTransition), [ShowPlace])
conflictPlacesShow ConflictPlaces
conflictInitial
    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), [ShowPlace]) -> String
forall a. Show a => a -> String
show ((ShowTransition, ShowTransition), [ShowPlace])
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), [String
p1, String
p2]) = ((ShowTransition, ShowTransition) -> (String, String))
-> ([ShowPlace] -> [String])
-> ((ShowTransition, ShowTransition), [ShowPlace])
-> ((String, 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)
-> (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)
            ((ShowPlace -> String) -> [ShowPlace] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map ShowPlace -> String
forall a. Show a => a -> String
show)
            ((ShowTransition, ShowTransition), [ShowPlace])
ts
      String -> State (Map Language String) ()
english [i| as answer would mean that transitions #{t1} and #{t2} are in conflict under the initial marking
and that places #{p1} and #{p2} are all those common places within the preconditions
which each separately do not have enough tokens for firing #{t1} and #{t2} at the same time. |]
      String -> State (Map Language String) ()
german [i| als Antwort würde bedeuten, dass Transitionen #{t1} und #{t2} unter der Startmarkierung in Konflikt stehen
und dass die Stellen #{p1} und #{p2} all jene gemeinsamen Stellen in den Vorbedingungen sind,
die jeweils einzeln nicht ausreichend Marken zum gleichzeitigen Feuern der Transitionen #{t1} und #{t2} haben. |]
    State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
      String -> State (Map Language String) ()
english [i|The order of transitions within the firstly indicated pair does not matter here.
The order of places within the listing of places inducing the conflict is irrelevant as well.|]
      String -> State (Map Language String) ()
german [i|Die Reihenfolge der Transitionen innerhalb des zuerst angegebenen Paars spielt hierbei keine Rolle.
Die Reihenfolge von Stellen innerhalb der Auflistung der den Konflikt verursachenden Stellen spielt ebenso 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)
addText FindInstance (p n String) Conflict
task
  pure ()

conflictInitial :: ConflictPlaces
conflictInitial :: ConflictPlaces
conflictInitial = ((Transition, Transition)
findInitial, [Int -> Place
Place Int
0, Int -> Place
Place Int
1])

findConflictPlacesSyntax
  :: OutputCapable m
  => FindInstance net Conflict
  -> ConflictPlaces
  -> LangM' m ()
findConflictPlacesSyntax :: forall (m :: * -> *) net.
OutputCapable m =>
FindInstance net Conflict -> ConflictPlaces -> LangM' m ()
findConflictPlacesSyntax FindInstance net Conflict
task ((Transition, Transition)
conflict, [Place]
ps) = do
  FindInstance net Conflict
-> (Transition, Transition) -> LangM' m ()
forall (m :: * -> *) net.
OutputCapable m =>
FindInstance net Conflict
-> (Transition, Transition) -> LangM' m ()
findConflictSyntax FindInstance net Conflict
task (Transition, Transition)
conflict
  [Place] -> (Place -> LangM' m ()) -> LangM' m ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
t a -> (a -> f b) -> f ()
for_ [Place]
ps ((Place -> LangM' m ()) -> LangM' m ())
-> (Place -> LangM' m ()) -> LangM' m ()
forall a b. (a -> b) -> a -> b
$ \Place
x -> Bool -> LangM' m () -> LangM' m ()
assert (Place -> Bool
isValidPlace Place
x) (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
    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 of the given Petri net?"
    String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
x' String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" ist eine Stelle des gegebenen Petrinetzes?"
  pure ()
  where
    isValidPlace :: Place -> Bool
isValidPlace (Place Int
x) = Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
1 Bool -> Bool -> Bool
&& Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= FindInstance net Conflict -> Int
forall n a. FindInstance n a -> Int
numberOfPlaces FindInstance net Conflict
task
    assert :: Bool -> LangM' m () -> LangM' m ()
assert = Bool -> Bool -> LangM' m () -> LangM' m ()
forall (m :: * -> *).
OutputCapable m =>
Bool -> Bool -> LangM m -> LangM m
continueOrAbort Bool
False

parseConflictPlacesPrec :: Int -> Parser ConflictPlaces
parseConflictPlacesPrec :: Int -> Parser ConflictPlaces
parseConflictPlacesPrec Int
_  = do
  ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  Maybe Char
mo <- ParsecT String () Identity Char
-> ParsecT String () Identity (Maybe Char)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'(')
  Either (Transition, Transition) [Place]
x <- (Transition, Transition) -> Either (Transition, Transition) [Place]
forall a b. a -> Either a b
Left ((Transition, Transition)
 -> Either (Transition, Transition) [Place])
-> ParsecT String () Identity (Transition, Transition)
-> ParsecT
     String () Identity (Either (Transition, Transition) [Place])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Char -> ParsecT String () Identity (Transition, Transition)
forall {a}.
Maybe a -> ParsecT String () Identity (Transition, Transition)
parseConflict Maybe Char
mo
    ParsecT
  String () Identity (Either (Transition, Transition) [Place])
-> ParsecT
     String () Identity (Either (Transition, Transition) [Place])
-> ParsecT
     String () Identity (Either (Transition, Transition) [Place])
forall a.
ParsecT String () Identity a
-> ParsecT String () Identity a -> ParsecT String () Identity a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> [Place] -> Either (Transition, Transition) [Place]
forall a b. b -> Either a b
Right ([Place] -> Either (Transition, Transition) [Place])
-> ParsecT String () Identity [Place]
-> ParsecT
     String () Identity (Either (Transition, Transition) [Place])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String () Identity [Place]
parsePlaces
  ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  ParsecT String () Identity Char -> ParsecT String () Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
',')
  ConflictPlaces
y <- ((Transition, Transition) -> Parser ConflictPlaces)
-> ([Place] -> Parser ConflictPlaces)
-> Either (Transition, Transition) [Place]
-> Parser ConflictPlaces
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (\(Transition, Transition)
y -> ((Transition, Transition)
y,) ([Place] -> ConflictPlaces)
-> ParsecT String () Identity [Place] -> Parser ConflictPlaces
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ParsecT String () Identity [Place]
parsePlaces) (\[Place]
y -> (,[Place]
y) ((Transition, Transition) -> ConflictPlaces)
-> ParsecT String () Identity (Transition, Transition)
-> Parser ConflictPlaces
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Any -> ParsecT String () Identity (Transition, Transition)
forall {a}.
Maybe a -> ParsecT String () Identity (Transition, Transition)
parseConflict Maybe Any
forall a. Maybe a
Nothing) Either (Transition, Transition) [Place]
x
  ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  ParsecT String () Identity Char -> ParsecT String () Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')')
  ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
  return ConflictPlaces
y
  where
    parseConflict :: Maybe a -> ParsecT String () Identity (Transition, Transition)
parseConflict Maybe a
mo = do
      ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      (ParsecT String () Identity Char -> ParsecT String () Identity ())
-> (a
    -> ParsecT String () Identity Char
    -> ParsecT String () Identity ())
-> Maybe a
-> ParsecT String () Identity Char
-> ParsecT String () Identity ()
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ParsecT String () Identity Char -> ParsecT String () Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void ((ParsecT String () Identity Char -> ParsecT String () Identity ())
-> a
-> ParsecT String () Identity Char
-> ParsecT String () Identity ()
forall a b. a -> b -> a
const ParsecT String () Identity Char -> ParsecT String () Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional) Maybe a
mo (ParsecT String () Identity Char -> ParsecT String () Identity ())
-> ParsecT String () Identity Char -> ParsecT String () Identity ()
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'('
      Transition
t1 <- Int -> Parser Transition
parseTransitionPrec Int
0
      ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      ParsecT String () Identity Char -> ParsecT String () Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT String () Identity Char -> ParsecT String () Identity ())
-> ParsecT String () Identity Char -> ParsecT String () Identity ()
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
','
      Transition
t2 <- Int -> Parser Transition
parseTransitionPrec Int
0
      ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      ParsecT String () Identity Char -> ParsecT String () Identity ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ParsecT String () Identity Char -> ParsecT String () Identity ())
-> ParsecT String () Identity Char -> ParsecT String () Identity ()
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
')'
      return (Transition
t1, Transition
t2)
    parsePlaces :: ParsecT String () Identity [Place]
parsePlaces =
      ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces
      ParsecT String () Identity ()
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
'['
      ParsecT String () Identity Char
-> ParsecT String () Identity [Place]
-> ParsecT String () Identity [Place]
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> Int -> Parser Place
parsePlacePrec Int
0 Parser Place
-> ParsecT String () Identity ()
-> ParsecT String () Identity [Place]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
`endBy1` (ParsecT String () Identity ()
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m ()
spaces ParsecT String () Identity ()
-> ParsecT String () Identity () -> ParsecT String () Identity ()
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* ParsecT String () Identity Char -> ParsecT String () Identity ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
','))
      ParsecT String () Identity [Place]
-> ParsecT String () Identity Char
-> ParsecT String () Identity [Place]
forall a b.
ParsecT String () Identity a
-> ParsecT String () Identity b -> ParsecT String () Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<*  Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
']'

defaultFindConflictPlacesConfig :: FindConflictConfig
defaultFindConflictPlacesConfig :: FindConflictConfig
defaultFindConflictPlacesConfig = FindConflictConfig
defaultFindConflictConfig
  FindConflictConfig
-> (FindConflictConfig -> FindConflictConfig) -> FindConflictConfig
forall a b. a -> (a -> b) -> b
& (GraphConfig -> Identity GraphConfig)
-> FindConflictConfig -> Identity FindConflictConfig
Lens' FindConflictConfig GraphConfig
lGraphConfig ((GraphConfig -> Identity GraphConfig)
 -> FindConflictConfig -> Identity FindConflictConfig)
-> ((Bool -> Identity Bool) -> GraphConfig -> Identity GraphConfig)
-> (Bool -> Identity Bool)
-> FindConflictConfig
-> Identity FindConflictConfig
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Bool -> Identity Bool) -> GraphConfig -> Identity GraphConfig
Lens' GraphConfig Bool
lHidePlaceNames ((Bool -> Identity Bool)
 -> FindConflictConfig -> Identity FindConflictConfig)
-> Bool -> FindConflictConfig -> FindConflictConfig
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Bool
False

checkFindConflictPlacesConfig :: FindConflictConfig -> Maybe String
checkFindConflictPlacesConfig :: FindConflictConfig -> Maybe String
checkFindConflictPlacesConfig FindConflictConfig {
  BasicConfig
basicConfig :: BasicConfig
$sel:basicConfig:FindConflictConfig :: FindConflictConfig -> BasicConfig
basicConfig,
  ChangeConfig
changeConfig :: ChangeConfig
$sel:changeConfig:FindConflictConfig :: FindConflictConfig -> ChangeConfig
changeConfig,
  ConflictConfig
conflictConfig :: ConflictConfig
$sel:conflictConfig:FindConflictConfig :: FindConflictConfig -> ConflictConfig
conflictConfig,
  GraphConfig
graphConfig :: GraphConfig
$sel:graphConfig:FindConflictConfig :: FindConflictConfig -> GraphConfig
graphConfig
  }
  = GraphConfig -> Maybe String
prohibitHidePlaceNames GraphConfig
graphConfig
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> BasicConfig -> ChangeConfig -> 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

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

defaultFindConflictPlacesInstance :: FindInstance SimplePetriNet Conflict
defaultFindConflictPlacesInstance :: FindInstance SimplePetriNet Conflict
defaultFindConflictPlacesInstance = FindInstance {
  $sel:drawFindWith:FindInstance :: DrawSettings
drawFindWith = DrawSettings {
    $sel:withPlaceNames:DrawSettings :: Bool
withPlaceNames = Bool
True,
    $sel:withSvgHighlighting:DrawSettings :: Bool
withSvgHighlighting = Bool
True,
    $sel:withTransitionNames:DrawSettings :: Bool
withTransitionNames = Bool
True,
    $sel:with1Weights:DrawSettings :: Bool
with1Weights = Bool
False,
    $sel:withGraphvizCommand:DrawSettings :: GraphvizCommand
withGraphvizCommand = GraphvizCommand
Circo
    },
  $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
  }