{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}

module Modelling.PetriNet.Find (
  FindInstance (..),
  checkFindBasicConfig,
  checkConfigForFind,
  findInitial,
  findTaskInstance,
  lToFind,
  toFindEvaluation,
  toFindSyntax,
  ) where

import qualified Data.Bimap                       as BM (lookup)

import Modelling.Auxiliary.Common       (Object)
import Modelling.Auxiliary.Output (
  addPretext,
  )
import Modelling.PetriNet.Diagram (
  getNet,
  )
import Modelling.PetriNet.Reach.Type (
  ShowTransition (ShowTransition),
  Transition (Transition),
  )
import Modelling.PetriNet.Types (
  BasicConfig (..),
  ChangeConfig (..),
  DrawSettings (..),
  GraphConfig (..),
  Net (..),
  checkBasicConfig,
  checkChangeConfig,
  shuffleNames,
  transitionPairShow,
  )

import Control.Applicative              (Alternative ((<|>)))
import Control.Lens                     (makeLensesFor)
import Control.Monad.Catch              (MonadThrow)
import Control.OutputCapable.Blocks (
  LangM',
  Language (English, German),
  OutputCapable,
  continueOrAbort,
  english,
  german,
  localise,
  translate,
  )
import Control.Monad.Random (
  RandT,
  RandomGen,
  )
import Control.Monad.Trans.Class        (MonadTrans (lift))
import Data.Map                         (Map)
import Language.Alloy.Call (
  AlloyInstance,
  )
import GHC.Generics                     (Generic)

data FindInstance n a = FindInstance {
  forall n a. FindInstance n a -> DrawSettings
drawFindWith :: !DrawSettings,
  forall n a. FindInstance n a -> a
toFind :: !a,
  forall n a. FindInstance n a -> n
net :: !n,
  forall n a. FindInstance n a -> Int
numberOfPlaces :: !Int,
  forall n a. FindInstance n a -> Int
numberOfTransitions :: !Int,
  forall n a. FindInstance n a -> Bool
showSolution :: !Bool,
  forall n a. FindInstance n a -> Maybe (Map Language String)
addText :: !(Maybe (Map Language String))
  }
  deriving ((forall a b. (a -> b) -> FindInstance n a -> FindInstance n b)
-> (forall a b. a -> FindInstance n b -> FindInstance n a)
-> Functor (FindInstance n)
forall a b. a -> FindInstance n b -> FindInstance n a
forall a b. (a -> b) -> FindInstance n a -> FindInstance n b
forall n a b. a -> FindInstance n b -> FindInstance n a
forall n a b. (a -> b) -> FindInstance n a -> FindInstance n b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall n a b. (a -> b) -> FindInstance n a -> FindInstance n b
fmap :: forall a b. (a -> b) -> FindInstance n a -> FindInstance n b
$c<$ :: forall n a b. a -> FindInstance n b -> FindInstance n a
<$ :: forall a b. a -> FindInstance n b -> FindInstance n a
Functor, (forall x. FindInstance n a -> Rep (FindInstance n a) x)
-> (forall x. Rep (FindInstance n a) x -> FindInstance n a)
-> Generic (FindInstance n a)
forall x. Rep (FindInstance n a) x -> FindInstance n a
forall x. FindInstance n a -> Rep (FindInstance n a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall n a x. Rep (FindInstance n a) x -> FindInstance n a
forall n a x. FindInstance n a -> Rep (FindInstance n a) x
$cfrom :: forall n a x. FindInstance n a -> Rep (FindInstance n a) x
from :: forall x. FindInstance n a -> Rep (FindInstance n a) x
$cto :: forall n a x. Rep (FindInstance n a) x -> FindInstance n a
to :: forall x. Rep (FindInstance n a) x -> FindInstance n a
Generic, ReadPrec [FindInstance n a]
ReadPrec (FindInstance n a)
Int -> ReadS (FindInstance n a)
ReadS [FindInstance n a]
(Int -> ReadS (FindInstance n a))
-> ReadS [FindInstance n a]
-> ReadPrec (FindInstance n a)
-> ReadPrec [FindInstance n a]
-> Read (FindInstance n a)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall n a. (Read a, Read n) => ReadPrec [FindInstance n a]
forall n a. (Read a, Read n) => ReadPrec (FindInstance n a)
forall n a. (Read a, Read n) => Int -> ReadS (FindInstance n a)
forall n a. (Read a, Read n) => ReadS [FindInstance n a]
$creadsPrec :: forall n a. (Read a, Read n) => Int -> ReadS (FindInstance n a)
readsPrec :: Int -> ReadS (FindInstance n a)
$creadList :: forall n a. (Read a, Read n) => ReadS [FindInstance n a]
readList :: ReadS [FindInstance n a]
$creadPrec :: forall n a. (Read a, Read n) => ReadPrec (FindInstance n a)
readPrec :: ReadPrec (FindInstance n a)
$creadListPrec :: forall n a. (Read a, Read n) => ReadPrec [FindInstance n a]
readListPrec :: ReadPrec [FindInstance n a]
Read, Int -> FindInstance n a -> ShowS
[FindInstance n a] -> ShowS
FindInstance n a -> String
(Int -> FindInstance n a -> ShowS)
-> (FindInstance n a -> String)
-> ([FindInstance n a] -> ShowS)
-> Show (FindInstance n a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n a. (Show a, Show n) => Int -> FindInstance n a -> ShowS
forall n a. (Show a, Show n) => [FindInstance n a] -> ShowS
forall n a. (Show a, Show n) => FindInstance n a -> String
$cshowsPrec :: forall n a. (Show a, Show n) => Int -> FindInstance n a -> ShowS
showsPrec :: Int -> FindInstance n a -> ShowS
$cshow :: forall n a. (Show a, Show n) => FindInstance n a -> String
show :: FindInstance n a -> String
$cshowList :: forall n a. (Show a, Show n) => [FindInstance n a] -> ShowS
showList :: [FindInstance n a] -> ShowS
Show)

makeLensesFor [("toFind", "lToFind")] ''FindInstance

findInitial :: (Transition, Transition)
findInitial :: (Transition, Transition)
findInitial = (Int -> Transition
Transition Int
0, Int -> Transition
Transition Int
1)

toFindSyntax
  :: OutputCapable m
  => Bool
  -> Int
  -> (Transition, Transition)
  -> LangM' m ()
toFindSyntax :: forall (m :: * -> *).
OutputCapable m =>
Bool -> Int -> (Transition, Transition) -> LangM' m ()
toFindSyntax Bool
withSol Int
n (Transition
fi, Transition
si) = LangM' m () -> LangM' m ()
forall (m :: * -> *) a. OutputCapable m => LangM' m a -> LangM' m a
addPretext (LangM' m () -> LangM' m ()) -> LangM' m () -> LangM' m ()
forall a b. (a -> b) -> a -> b
$ do
  Transition -> LangM' m ()
assertTransition Transition
fi
  Transition -> LangM' m ()
assertTransition Transition
si
  pure ()
  where
    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
withSol
    assertTransition :: Transition -> LangM' m ()
assertTransition Transition
t = Bool -> LangM' m () -> LangM' m ()
assert (Transition -> Bool
isValidTransition Transition
t) (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 t' :: String
t' = ShowTransition -> String
forall a. Show a => a -> String
show (ShowTransition -> String) -> ShowTransition -> String
forall a b. (a -> b) -> a -> b
$ Transition -> ShowTransition
ShowTransition Transition
t
      String -> State (Map Language String) ()
english (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
t' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" is a transition 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
t' String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" ist eine Transition des gegebenen Petrinetzes?"
    isValidTransition :: Transition -> Bool
isValidTransition (Transition 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
<= Int
n

findTaskInstance
  :: (MonadThrow m, Net p n, RandomGen g, Traversable t)
  => (AlloyInstance -> m (t Object))
  -> AlloyInstance
  -> RandT g m (p n String, t String)
findTaskInstance :: 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 AlloyInstance -> m (t Object)
f AlloyInstance
inst = do
  (p n String
pl, t String
t) <- m (p n String, t String) -> RandT g m (p n String, t String)
forall (m :: * -> *) a. Monad m => m a -> RandT g m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (p n String, t String) -> RandT g m (p n String, t String))
-> m (p n String, t String) -> RandT g m (p n String, t String)
forall a b. (a -> b) -> a -> b
$ (AlloyInstance -> m (t Object))
-> AlloyInstance -> m (p n String, t String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *)
       (t :: * -> *).
(MonadThrow m, Net p n, Traversable t) =>
(AlloyInstance -> m (t Object))
-> AlloyInstance -> m (p n String, t String)
getNet AlloyInstance -> m (t Object)
f AlloyInstance
inst
  (p n String
pl', Bimap String String
mapping) <- p n String -> RandT g m (p n String, Bimap String String)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) a g.
(MonadThrow m, Net p n, Ord a, RandomGen g) =>
p n a -> RandT g m (p n a, Bimap a a)
shuffleNames p n String
pl
  t String
t'  <- m (t String) -> RandT g m (t String)
forall (m :: * -> *) a. Monad m => m a -> RandT g m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (m (t String) -> RandT g m (t String))
-> m (t String) -> RandT g m (t String)
forall a b. (a -> b) -> a -> b
$ (String -> Bimap String String -> m String
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
`BM.lookup` Bimap String String
mapping) (String -> m String) -> t String -> m (t String)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> t a -> m (t b)
`mapM` t String
t
  return (p n String
pl', t String
t')

toFindEvaluation
  :: (Num a, OutputCapable m)
  => Map Language String
  -> Bool
  -> (Transition, Transition)
  -> (Transition, Transition)
  -> LangM' m (Maybe String, a)
toFindEvaluation :: 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
ft, Transition
st) (Transition
fi, Transition
si) = do
  let correct :: Bool
correct = Transition
ft Transition -> Transition -> Bool
forall a. Eq a => a -> a -> Bool
== Transition
fi Bool -> Bool -> Bool
&& Transition
st Transition -> Transition -> Bool
forall a. Eq a => a -> a -> Bool
== Transition
si Bool -> Bool -> Bool
|| Transition
ft Transition -> Transition -> Bool
forall a. Eq a => a -> a -> Bool
== Transition
si Bool -> Bool -> Bool
&& Transition
st Transition -> Transition -> Bool
forall a. Eq a => a -> a -> Bool
== Transition
fi
      points :: a
points = if Bool
correct then a
1 else a
0
      maybeSolutionString :: Maybe String
maybeSolutionString =
        if Bool
withSol
        then String -> Maybe String
forall a. a -> Maybe a
Just (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ (ShowTransition, ShowTransition) -> String
forall a. Show a => a -> String
show ((ShowTransition, ShowTransition) -> String)
-> (ShowTransition, ShowTransition) -> String
forall a b. (a -> b) -> a -> b
$ (Transition, Transition) -> (ShowTransition, ShowTransition)
transitionPairShow (Transition
ft, Transition
st)
        else Maybe String
forall a. Maybe a
Nothing
  Bool -> LangM m -> LangM m
assert Bool
correct (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 -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
"The indicated transitions " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Language -> Map Language String -> String
localise Language
English Map Language String
what String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"?"
    String -> State (Map Language String) ()
german (String -> State (Map Language String) ())
-> String -> State (Map Language String) ()
forall a b. (a -> b) -> a -> b
$ String
"Die angegebenen Transitionen " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Language -> Map Language String -> String
localise Language
German Map Language String
what String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"?"
  pure (Maybe String
maybeSolutionString, a
points)
  where
    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
withSol

checkFindBasicConfig :: BasicConfig -> Maybe String
checkFindBasicConfig :: BasicConfig -> Maybe String
checkFindBasicConfig BasicConfig { Int
atLeastActive :: Int
$sel:atLeastActive:BasicConfig :: BasicConfig -> Int
atLeastActive }
 | Int
atLeastActive Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
2
  = String -> Maybe String
forall a. a -> Maybe a
Just String
"The parameter 'atLeastActive' must be at least 2 to create the task."
 | Bool
otherwise = Maybe String
forall a. Maybe a
Nothing

checkConfigForFind :: BasicConfig -> ChangeConfig -> GraphConfig -> Maybe String
checkConfigForFind :: BasicConfig -> ChangeConfig -> GraphConfig -> Maybe String
checkConfigForFind BasicConfig
basic ChangeConfig
change GraphConfig
graph =
  BasicConfig -> Maybe String
checkFindBasicConfig BasicConfig
basic
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> GraphConfig -> Maybe String
prohibitHideTransitionNames GraphConfig
graph
  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 -> Maybe String
checkBasicConfig BasicConfig
basic
  Maybe String -> Maybe String -> Maybe String
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> BasicConfig -> ChangeConfig -> Maybe String
checkChangeConfig BasicConfig
basic ChangeConfig
change

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