{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TupleSections #-}
{-# Language DuplicateRecordFields #-}
{-# Language QuasiQuotes #-}

module Modelling.PetriNet.Alloy (
  TaskGenerationException (..),
  compAdvConstraints,
  compBasicConstraints,
  compChange,
  connected,
  defaultConstraints,
  isolated,
  moduleHelpers,
  modulePetriAdditions,
  modulePetriConcepts,
  modulePetriConstraints,
  modulePetriSignature,
  petriScopeBitWidth,
  petriScopeMaxSeq,
  signatures,
  skolemVariable,
  taskInstance,
  unscopedSingleSig,
  ) where

import Capabilities.Alloy               (MonadAlloy, getInstances)
import Modelling.Auxiliary.Common (
  TaskGenerationException (NoInstanceAvailable),
  Object (Object),
  upperFirst,
  )
import Modelling.PetriNet.Types (
  AdvConfig (..),
  AlloyConfig,
  BasicConfig (..),
  ChangeConfig (..),
  )

import qualified Modelling.PetriNet.Types         as T (
  AlloyConfig (maxInstances, timeout)
  )

import Control.Monad                    (when)
import Control.Monad.Catch              (MonadThrow (throwM))
import Control.Monad.Random (
  RandT,
  Random (randomR),
  RandomGen,
  liftRandT,
  )
import Data.Composition                 ((.:))
import Data.FileEmbed                   (embedStringFile)
import Data.List                        (intercalate)
import Data.Set                         (Set)
import Data.String.Interpolate          (i)
import Language.Alloy.Call (
  AlloyInstance,
  getSingleAs,
  lookupSig,
  unscoped,
  )

petriScopeBitWidth :: BasicConfig -> Int
petriScopeBitWidth :: BasicConfig -> Int
petriScopeBitWidth BasicConfig
 { (Int, Int)
flowOverall :: (Int, Int)
$sel:flowOverall:BasicConfig :: BasicConfig -> (Int, Int)
flowOverall, Int
places :: Int
$sel:places:BasicConfig :: BasicConfig -> Int
places, (Int, Int)
tokensOverall :: (Int, Int)
$sel:tokensOverall:BasicConfig :: BasicConfig -> (Int, Int)
tokensOverall, Int
transitions :: Int
$sel:transitions:BasicConfig :: BasicConfig -> Int
transitions } =
  Double -> Int
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor
     (Double
2 Double -> Double -> Double
forall a. Num a => a -> a -> a
+ ((Double -> Double -> Double
forall a. Floating a => a -> a -> a
logBase :: Double -> Double -> Double) Double
2.0 (Double -> Double) -> (Int -> Double) -> Int -> Double
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral)
       ([Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum [(Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
flowOverall, (Int, Int) -> Int
forall a b. (a, b) -> b
snd (Int, Int)
tokensOverall, Int
places, Int
transitions])
     )

petriScopeMaxSeq :: BasicConfig -> Int
petriScopeMaxSeq :: BasicConfig -> Int
petriScopeMaxSeq BasicConfig{Int
$sel:places:BasicConfig :: BasicConfig -> Int
places :: Int
places,Int
$sel:transitions:BasicConfig :: BasicConfig -> Int
transitions :: Int
transitions} = Int
placesInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
transitions

modulePetriSignature :: String
modulePetriSignature :: [Char]
modulePetriSignature = Int -> [Char] -> [Char]
removeLines Int
2 $(embedStringFile "alloy/petri/PetriSignature.als")

modulePetriAdditions :: String
modulePetriAdditions :: [Char]
modulePetriAdditions = Int -> [Char] -> [Char]
removeLines Int
11 $(embedStringFile "alloy/petri/PetriAdditions.als")

moduleHelpers :: String
moduleHelpers :: [Char]
moduleHelpers = Int -> [Char] -> [Char]
removeLines Int
4 $(embedStringFile "alloy/petri/Helpers.als")

modulePetriConcepts :: String
modulePetriConcepts :: [Char]
modulePetriConcepts = Int -> [Char] -> [Char]
removeLines Int
5 $(embedStringFile "alloy/petri/PetriConcepts.als")

modulePetriConstraints :: String
modulePetriConstraints :: [Char]
modulePetriConstraints = Int -> [Char] -> [Char]
removeLines Int
5 $(embedStringFile "alloy/petri/PetriConstraints.als")

removeLines :: Int -> String -> String
removeLines :: Int -> [Char] -> [Char]
removeLines Int
n = [[Char]] -> [Char]
unlines ([[Char]] -> [Char]) -> ([Char] -> [[Char]]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [[Char]] -> [[Char]]
forall a. Int -> [a] -> [a]
drop Int
n ([[Char]] -> [[Char]])
-> ([Char] -> [[Char]]) -> [Char] -> [[Char]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [[Char]]
lines

{-|
A set of constraints enforcing settings of 'BasicConfig'.
(Besides 'defaultConstraints')
-}
compBasicConstraints
  :: String
  -- ^ The name of the Alloy variable for the set of activated Transitions.
  -> BasicConfig
  -- ^ the configuration to enforce.
  -> String
compBasicConstraints :: [Char] -> BasicConfig -> [Char]
compBasicConstraints = Bool -> [Char] -> BasicConfig -> [Char]
enforceConstraints Bool
False

{-|
A set of constraints enforcing settings of 'BasicConfig' for the net under
default conditions.
-}
defaultConstraints
  :: String
  -- ^ The name of the Alloy variable for the set of default activated Transitions.
  -> BasicConfig
  -- ^ the configuration to enforce.
  -> String
defaultConstraints :: [Char] -> BasicConfig -> [Char]
defaultConstraints = Bool -> [Char] -> BasicConfig -> [Char]
enforceConstraints Bool
True

enforceConstraints
  :: Bool
  -- ^ If to generate constraints under default conditions.
  -> String
  -- ^ The name of the Alloy variable for the set of activated Transitions.
  -> BasicConfig
  -- ^ the configuration to enforce.
  -> String
enforceConstraints :: Bool -> [Char] -> BasicConfig -> [Char]
enforceConstraints Bool
underDefault [Char]
activated BasicConfig {
  Int
atLeastActive :: Int
$sel:atLeastActive:BasicConfig :: BasicConfig -> Int
atLeastActive,
  Maybe Bool
isConnected :: Maybe Bool
$sel:isConnected:BasicConfig :: BasicConfig -> Maybe Bool
isConnected,
  (Int, Int)
$sel:flowOverall:BasicConfig :: BasicConfig -> (Int, Int)
flowOverall :: (Int, Int)
flowOverall,
  Int
maxFlowPerEdge :: Int
$sel:maxFlowPerEdge:BasicConfig :: BasicConfig -> Int
maxFlowPerEdge,
  Int
maxTokensPerPlace :: Int
$sel:maxTokensPerPlace:BasicConfig :: BasicConfig -> Int
maxTokensPerPlace,
  (Int, Int)
$sel:tokensOverall:BasicConfig :: BasicConfig -> (Int, Int)
tokensOverall :: (Int, Int)
tokensOverall
  } = [i|
  let t = (sum p : #{places} | p.#{tokens}) |
    #{fst tokensOverall} =< t and t =< #{snd tokensOverall}
  all p : #{places} | p.#{tokens} =< #{maxTokensPerPlace}
  all w : #{nodes}.#{flow}[#{nodes}] | w =< #{maxFlowPerEdge}
  let theFlow = (sum f, t : #{nodes} | f.#{flow}[t]) |
    #{fst flowOverall} =< theFlow and theFlow =< #{snd flowOverall}
  \##{activated} >= #{atLeastActive}
  theActivated#{upperFirst which}Transitions[#{activated}]
  #{connected (prepend "graphIsConnected") isConnected}
  #{isolated (prepend "noIsolatedNodes") isConnected}|]
  where
    ([Char] -> [Char]
given, [Char] -> [Char]
prepend, [Char]
which)
      | Bool
underDefault = (([Char]
"given" [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++), ([Char]
which [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++) ([Char] -> [Char]) -> ([Char] -> [Char]) -> [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> [Char]
upperFirst, [Char]
"default")
      | Bool
otherwise    = ([Char] -> [Char]
forall a. a -> a
id, [Char] -> [Char]
forall a. a -> a
id, [Char]
"")
    flow :: [Char]
flow = [Char] -> [Char]
prepend [Char]
"flow"
    nodes :: [Char]
nodes = [Char] -> [Char]
given [Char]
"Nodes"
    places :: [Char]
places = [Char] -> [Char]
given [Char]
"Places"
    tokens :: [Char]
tokens = [Char] -> [Char]
prepend [Char]
"tokens"

connected :: String -> Maybe Bool -> String
connected :: [Char] -> Maybe Bool -> [Char]
connected [Char]
p = [Char] -> (Bool -> [Char]) -> Maybe Bool -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
"" ((Bool -> [Char]) -> Maybe Bool -> [Char])
-> (Bool -> [Char]) -> Maybe Bool -> [Char]
forall a b. (a -> b) -> a -> b
$ \Bool
c -> (if Bool
c then [Char]
"" else [Char]
"not ") [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ [Char]
p

isolated :: String -> Maybe Bool -> String
isolated :: [Char] -> Maybe Bool -> [Char]
isolated [Char]
p = [Char] -> (Bool -> [Char]) -> Maybe Bool -> [Char]
forall b a. b -> (a -> b) -> Maybe a -> b
maybe [Char]
p ((Bool -> [Char]) -> Maybe Bool -> [Char])
-> (Bool -> [Char]) -> Maybe Bool -> [Char]
forall a b. (a -> b) -> a -> b
$ \Bool
c -> if Bool
c then [Char]
"" else [Char]
p

compAdvConstraints :: AdvConfig -> String
compAdvConstraints :: AdvConfig -> [Char]
compAdvConstraints AdvConfig
                        { Maybe Bool
presenceOfSelfLoops :: Maybe Bool
$sel:presenceOfSelfLoops:AdvConfig :: AdvConfig -> Maybe Bool
presenceOfSelfLoops, Maybe Bool
presenceOfSinkTransitions :: Maybe Bool
$sel:presenceOfSinkTransitions:AdvConfig :: AdvConfig -> Maybe Bool
presenceOfSinkTransitions
                        , Maybe Bool
presenceOfSourceTransitions :: Maybe Bool
$sel:presenceOfSourceTransitions:AdvConfig :: AdvConfig -> Maybe Bool
presenceOfSourceTransitions
                        } = [i|
  #{maybe "" petriLoops presenceOfSelfLoops}
  #{maybe "" petriSink presenceOfSinkTransitions}
  #{maybe "" petriSource presenceOfSourceTransitions}
|]
  where
    petriLoops :: Bool -> [Char]
petriLoops = \case
      Bool
True  -> [Char]
"some n : Nodes | selfLoop[n]"
      Bool
False -> [Char]
"no n : Nodes | selfLoop[n]"
    petriSink :: Bool -> [Char]
petriSink = \case
      Bool
True  -> [Char]
"some t : Transitions | sinkTransitions[t]"
      Bool
False -> [Char]
"no t : Transitions | sinkTransitions[t]"
    petriSource :: Bool -> [Char]
petriSource = \case
      Bool
True  -> [Char]
"some t : Transitions | sourceTransitions[t]"
      Bool
False -> [Char]
"no t : Transitions | sourceTransitions[t]"

compChange :: ChangeConfig -> String
compChange :: ChangeConfig -> [Char]
compChange ChangeConfig
                  {Int
flowChangeOverall :: Int
$sel:flowChangeOverall:ChangeConfig :: ChangeConfig -> Int
flowChangeOverall, Int
maxFlowChangePerEdge :: Int
$sel:maxFlowChangePerEdge:ChangeConfig :: ChangeConfig -> Int
maxFlowChangePerEdge
                  , Int
tokenChangeOverall :: Int
$sel:tokenChangeOverall:ChangeConfig :: ChangeConfig -> Int
tokenChangeOverall, Int
maxTokenChangePerPlace :: Int
$sel:maxTokenChangePerPlace:ChangeConfig :: ChangeConfig -> Int
maxTokenChangePerPlace
                  } = [i|
  (sum f, t : Nodes | abs[f.flowChange[t]]) = #{flowChangeOverall}
  maxFlowChangePerEdge[#{maxFlowChangePerEdge}]
  (sum p : Places | abs[p.tokenChange]) = #{tokenChangeOverall}
  maxTokenChangePerPlace[#{maxTokenChangePerPlace}]
|]

{-|
Generates signatures of the given kind, number of places and transitions.
-}
signatures
  :: String
  -- ^ What kind of signatures to generate
  -- (e.g., @"given"@ for @givenPlaces@ and @givenTransitions@)
  -> Int
  -- ^ How many places of that kind
  -> Int
  -- ^ How many transitions of that kind
  -> String
signatures :: [Char] -> Int -> Int -> [Char]
signatures [Char]
what Int
places Int
transitions = [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"\n"
  ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$  [ [i|one sig P#{x} extends #{what}Places {}|]
     | Int
x <- [Int
1 .. Int
places]]
  [[Char]] -> [[Char]] -> [[Char]]
forall a. [a] -> [a] -> [a]
++ [ [i|one sig T#{x} extends #{what}Transitions {}|]
     | Int
x <- [Int
1 .. Int
transitions]]

taskInstance
  :: (MonadThrow m, RandomGen g, MonadAlloy m)
  => (f
    -> AlloyInstance
    -> RandT g m a)
  -> (config -> String)
  -> f
  -> (config -> AlloyConfig)
  -> config
  -> Int
  -> RandT g m a
taskInstance :: forall (m :: * -> *) g f a config.
(MonadThrow m, RandomGen g, MonadAlloy m) =>
(f -> AlloyInstance -> RandT g m a)
-> (config -> [Char])
-> f
-> (config -> AlloyConfig)
-> config
-> Int
-> RandT g m a
taskInstance f -> AlloyInstance -> RandT g m a
taskF config -> [Char]
alloyF f
parseF config -> AlloyConfig
alloyC config
config Int
segment = do
  let is :: Maybe Integer
is = AlloyConfig -> Maybe Integer
T.maxInstances (config -> AlloyConfig
alloyC config
config)
  [AlloyInstance]
list <- Maybe Integer -> Maybe Int -> [Char] -> RandT g m [AlloyInstance]
forall (m :: * -> *).
MonadAlloy m =>
Maybe Integer -> Maybe Int -> [Char] -> m [AlloyInstance]
getInstances Maybe Integer
is (AlloyConfig -> Maybe Int
T.timeout (AlloyConfig -> Maybe Int) -> AlloyConfig -> Maybe Int
forall a b. (a -> b) -> a -> b
$ config -> AlloyConfig
alloyC config
config) (config -> [Char]
alloyF config
config)
  Bool -> RandT g m () -> RandT g m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ([AlloyInstance] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([AlloyInstance] -> Bool) -> [AlloyInstance] -> Bool
forall a b. (a -> b) -> a -> b
$ Int -> [AlloyInstance] -> [AlloyInstance]
forall a. Int -> [a] -> [a]
drop Int
segment [AlloyInstance]
list)
    (RandT g m () -> RandT g m ()) -> RandT g m () -> RandT g m ()
forall a b. (a -> b) -> a -> b
$ TaskGenerationException -> RandT g m ()
forall e a. Exception e => e -> RandT g m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM TaskGenerationException
NoInstanceAvailable
  AlloyInstance
inst <- case Integer -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Integer -> Int) -> Maybe Integer -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe Integer
is of
    Maybe Int
Nothing -> [AlloyInstance] -> RandT g m AlloyInstance
forall {m :: * -> *} {g} {b}.
(Monad m, RandomGen g) =>
[b] -> RandT g m b
randomInstance [AlloyInstance]
list
    Just Int
n -> do
      Int
x <- Int -> Int -> RandT g m Int
forall g (m :: * -> *).
(RandomGen g, Monad m) =>
Int -> Int -> RandT g m Int
randomInSegment Int
segment Int
n
      case Int -> [AlloyInstance] -> [AlloyInstance]
forall a. Int -> [a] -> [a]
drop Int
x [AlloyInstance]
list of
        AlloyInstance
x':[AlloyInstance]
_ -> AlloyInstance -> RandT g m AlloyInstance
forall a. a -> RandT g m a
forall (m :: * -> *) a. Monad m => a -> m a
return AlloyInstance
x'
        []   -> [AlloyInstance] -> RandT g m AlloyInstance
forall {m :: * -> *} {g} {b}.
(Monad m, RandomGen g) =>
[b] -> RandT g m b
randomInstance [AlloyInstance]
list
  f -> AlloyInstance -> RandT g m a
taskF f
parseF AlloyInstance
inst
  where
    randomInstance :: [b] -> RandT g m b
randomInstance [b]
list = do
      Int
n <- Int -> Int -> RandT g m Int
forall g (m :: * -> *).
(RandomGen g, Monad m) =>
Int -> Int -> RandT g m Int
randomInSegment Int
segment (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (([b] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [b]
list Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
segment Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
4))
      b -> RandT g m b
forall a. a -> RandT g m a
forall (m :: * -> *) a. Monad m => a -> m a
return (b -> RandT g m b) -> b -> RandT g m b
forall a b. (a -> b) -> a -> b
$ [b]
list [b] -> Int -> b
forall a. HasCallStack => [a] -> Int -> a
!! Int
n

randomInSegment :: (RandomGen g, Monad m) => Int -> Int -> RandT g m Int
randomInSegment :: forall g (m :: * -> *).
(RandomGen g, Monad m) =>
Int -> Int -> RandT g m Int
randomInSegment Int
segment Int
segLength = do
  Int
x <- (g -> m (Int, g)) -> RandT g m Int
forall g (m :: * -> *) a. (g -> m (a, g)) -> RandT g m a
liftRandT ((g -> m (Int, g)) -> RandT g m Int)
-> (g -> m (Int, g)) -> RandT g m Int
forall a b. (a -> b) -> a -> b
$ (Int, g) -> m (Int, g)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Int, g) -> m (Int, g)) -> (g -> (Int, g)) -> g -> m (Int, g)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Int) -> g -> (Int, g)
forall g. RandomGen g => (Int, Int) -> g -> (Int, g)
forall a g. (Random a, RandomGen g) => (a, a) -> g -> (a, g)
randomR ((Int
0,) (Int -> (Int, Int)) -> Int -> (Int, Int)
forall a b. (a -> b) -> a -> b
$ Int -> Int
forall a. Enum a => a -> a
pred Int
segLength)
  Int -> RandT g m Int
forall a. a -> RandT g m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Int -> RandT g m Int) -> Int -> RandT g m Int
forall a b. (a -> b) -> a -> b
$ Int
segment Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
4 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
x

unscopedSingleSig
  :: MonadThrow m
  => AlloyInstance
  -> String
  -> String
  -> m (Set Object)
unscopedSingleSig :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> [Char] -> [Char] -> m (Set Object)
unscopedSingleSig AlloyInstance
inst [Char]
st [Char]
nd = do
  AlloySig
sig <- Signature -> AlloyInstance -> m AlloySig
forall (m :: * -> *).
MonadThrow m =>
Signature -> AlloyInstance -> m AlloySig
lookupSig ([Char] -> Signature
unscoped [Char]
st) AlloyInstance
inst
  [Char] -> ([Char] -> Int -> m Object) -> AlloySig -> m (Set Object)
forall (m :: * -> *) a.
(MonadThrow m, Ord a) =>
[Char] -> ([Char] -> Int -> m a) -> AlloySig -> m (Set a)
getSingleAs [Char]
nd (Object -> m Object
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Object -> m Object)
-> ([Char] -> Int -> Object) -> [Char] -> Int -> m Object
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: [Char] -> Int -> Object
Object) AlloySig
sig

skolemVariable :: String -> String -> String
skolemVariable :: [Char] -> [Char] -> [Char]
skolemVariable [Char]
x [Char]
y = Char
'$' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
x [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Char
'_' Char -> [Char] -> [Char]
forall a. a -> [a] -> [a]
: [Char]
y