{-# 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 (
  ExtraText(..),
  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
    )
  => Bool
  -> FilePath
  -> FindInstance SimplePetriNet Conflict
  -> LangM m
simpleFindConflictPlacesTask :: forall (m :: * -> *).
(MonadCache m, MonadDiagrams m, MonadGraphviz m, MonadThrow m,
 OutputCapable m) =>
Bool -> String -> FindInstance SimplePetriNet Conflict -> LangM m
simpleFindConflictPlacesTask = Bool -> 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) =>
Bool -> 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
    )
  => Bool
  -> 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) =>
Bool -> String -> FindInstance (p n String) Conflict -> LangM m
findConflictPlacesTask Bool
showInputHelp 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?"
  if Bool -> Bool
not Bool
showInputHelp then
    LangM m -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
GenericLangM l m () -> GenericLangM l m ()
paragraph (LangM m -> LangM m) -> LangM m -> LangM m
forall a b. (a -> b) -> a -> b
$ State (Map Language String) () -> LangM m
forall l (m :: * -> *).
GenericOutputCapable l m =>
State (Map l String) () -> GenericLangM l m ()
translate (State (Map Language String) () -> LangM m)
-> State (Map Language String) () -> LangM m
forall a b. (a -> b) -> a -> b
$ do
     String -> State (Map Language String) ()
english [i|You have to indicate all the places that induce the conflict, i.e., all those common places within the
preconditions which each separately do not have enough tokens for firing the two transitions at the same time.|]
     String -> State (Map Language String) ()
german [i|Sie müssen alle Stellen angeben, die den Konflikt verursachen, also all jene gemeinsamen Stellen in den Vorbedingungen,
die jeweils einzeln nicht ausreichend Marken zum gleichzeitigen Feuern der beiden Transitionen haben.|]
  else 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
forall (m :: * -> *). OutputCapable m => LangM m
hoveringInformation
  ExtraText -> LangM m
forall (m :: * -> *). OutputCapable m => ExtraText -> LangM m
extra (ExtraText -> LangM m) -> ExtraText -> LangM m
forall a b. (a -> b) -> a -> b
$ FindInstance (p n String) Conflict -> ExtraText
forall n a. FindInstance n a -> ExtraText
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 :: ExtraText
addText = ExtraText
NoExtraText
  }