{-# LANGUAGE RecordWildCards #-}
{-|
A module for parsing Petri Alloy instances into Haskell representations defined
by the 'Modelling.PetriNet.Types' module.
The instances contain valid and invalid Petri nets that is why these are parsed
into types as 'Net' which allow representing some invalid representations
of graphs which are similar to Petri nets.
-}
module Modelling.PetriNet.Parser (
  NoSingletonException (..),
  asSingleton,
  convertPetri,
  netToGr,
  parseChange,
  parseNet,
  parseRenamedNet,
  simpleNameMap, simpleRename, simpleRenameWith,
  ) where

import qualified Modelling.PetriNet.Types         as PN (
  Net (nodes),
  )

import qualified Data.Bimap                       as BM (
  fromList, lookup,
  )
import qualified Data.Set                         as Set (
  Set, findMin, fromList, lookupMin, null, size, toList,
  )
import qualified Data.Map.Lazy                    as Map (
  findIndex,
  foldlWithKey',
  foldrWithKey,
  lookup,
  )

import Modelling.Auxiliary.Common       (Object (Object, oName, oIndex), toMap)
import Modelling.PetriNet.Types (
  Net (emptyNet, outFlow, alterFlow, alterNode, traverseNet),
  Petri,
  PetriChange (..),
  PetriNode (..),
  maybeInitial,
  petriLikeToPetri,
  )

import Control.Arrow                    (second)
import Control.Monad.Catch              (Exception, MonadThrow (throwM))
import Data.Bimap                       (Bimap)
import Data.Graph.Inductive.Graph       (mkGraph)
import Data.Graph.Inductive.PatriciaTree
  (Gr)
import Data.Set                         (Set)
import Data.Map                         (Map)
import Data.Composition                 ((.:))
import Language.Alloy.Call (
  AlloyInstance,
  getDoubleAs,
  getSingleAs,
  getTripleAs,
  lookupSig,
  scoped,
  )

{-|
Given the name of a flow set and a token set the given alloy instance is parsed
to a 'Net' graph and a 'Petri' is returned if the instance is indeed a
valid Petri net (after applying 'petriLikeToPetri').
-}
convertPetri
  :: MonadThrow m
  => String              -- ^ the name of the flow set
  -> String              -- ^ the name of the token set
  -> AlloyInstance       -- ^ the Petri net 'AlloyInstance'
  -> m Petri
convertPetri :: forall (m :: * -> *).
MonadThrow m =>
String -> String -> AlloyInstance -> m Petri
convertPetri String
f String
t AlloyInstance
inst = do
  PetriLike Node Object
p <- String -> String -> AlloyInstance -> m (PetriLike Node Object)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadThrow m, Net p n) =>
String -> String -> AlloyInstance -> m (p n Object)
parseNet String
f String
t AlloyInstance
inst
  PetriLike Node Object -> m Petri
forall (m :: * -> *) a.
(MonadThrow m, Ord a) =>
PetriLike Node a -> m Petri
petriLikeToPetri PetriLike Node Object
p

{-|
Parse a 'Net' graph from an 'AlloyInstance' given the instances flow and
token set names.
And return an already renamed Petri net.
-}
parseRenamedNet
  :: (MonadThrow m, Net p n)
  => String
  -> String
  -> AlloyInstance
  -> m (p n String)
parseRenamedNet :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadThrow m, Net p n) =>
String -> String -> AlloyInstance -> m (p n String)
parseRenamedNet String
flowSetName String
tokenSetName AlloyInstance
inst = do
  p n Object
petriLike <- String -> String -> AlloyInstance -> m (p n Object)
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadThrow m, Net p n) =>
String -> String -> AlloyInstance -> m (p n Object)
parseNet String
flowSetName String
tokenSetName AlloyInstance
inst
  let rename :: Object -> m String
rename = p n Object -> Object -> m String
forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(MonadThrow m, Net p n, Ord a) =>
p n a -> a -> m String
simpleRenameWith p n Object
petriLike
  (Object -> m String) -> p n Object -> m (p n String)
forall (f :: * -> *) b a.
(Applicative f, Ord b) =>
(a -> f b) -> p n a -> f (p n b)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) (f :: * -> *) b a.
(Net p n, Applicative f, Ord b) =>
(a -> f b) -> p n a -> f (p n b)
traverseNet Object -> m String
rename p n Object
petriLike

{-|
Transform a given value into a 'String' by replacing it according to the
'simpleNameMap' retrieved by the given 'Net'.
-}
simpleRenameWith :: (MonadThrow m, Net p n, Ord a) => p n a -> a -> m String
simpleRenameWith :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(MonadThrow m, Net p n, Ord a) =>
p n a -> a -> m String
simpleRenameWith p n a
petriLike a
x = do
  let nameMap :: Bimap a String
nameMap = p n a -> Bimap a String
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Bimap a String
simpleNameMap p n a
petriLike
  a -> Bimap a String -> m String
forall a b (m :: * -> *).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
BM.lookup a
x Bimap a String
nameMap

{-|
Parse a `Net' graph from an 'AlloyInstance' given the instances flow and
token set names.
-}
parseNet
  :: (MonadThrow m, Net p n)
  => String                           -- ^ the name of the flow set
  -> String                           -- ^ the name of the token set
  -> AlloyInstance                    -- ^ the Petri net 'AlloyInstance'
  -> m (p n Object)
parseNet :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *).
(MonadThrow m, Net p n) =>
String -> String -> AlloyInstance -> m (p n Object)
parseNet String
flowSetName String
tokenSetName AlloyInstance
inst = do
  Set Object
nodes  <- AlloyInstance -> String -> String -> String -> m (Set Object)
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> String -> String -> String -> m (Set Object)
singleSig AlloyInstance
inst String
"this" String
"Nodes" String
""
  Set (Object, Object)
rawTokens <- AlloyInstance
-> String -> String -> String -> m (Set (Object, Object))
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance
-> String -> String -> String -> m (Set (Object, Object))
doubleSig AlloyInstance
inst String
"this" String
"Places" String
tokenSetName
  let tokens :: Map Object (Set Int)
tokens = ((Object, Object) -> (Object, Int))
-> Set (Object, Object) -> Map Object (Set Int)
forall b c a.
(Ord b, Ord c) =>
(a -> (b, c)) -> Set a -> Map b (Set c)
relToMap ((Object -> Int) -> (Object, Object) -> (Object, Int)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Object -> Int
oIndex) Set (Object, Object)
rawTokens
  Set (Object, Object, Object)
flow   <- AlloyInstance
-> String -> String -> String -> m (Set (Object, Object, Object))
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance
-> String -> String -> String -> m (Set (Object, Object, Object))
tripleSig AlloyInstance
inst String
"this" String
"Nodes" String
flowSetName
  p n Object -> m (p n Object)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return
    (p n Object -> m (p n Object))
-> (p n Object -> p n Object) -> p n Object -> m (p n Object)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Object, Object, Object) -> p n Object -> p n Object)
-> Set (Object, Object, Object) -> p n Object -> p n Object
forall {t :: * -> *} {a} {c}.
Foldable t =>
(a -> c -> c) -> t a -> c -> c
foldrFlip (\(Object
x, Object
y, Object
z) -> Object -> Int -> Object -> p n Object -> p n Object
forall a. Ord a => a -> Int -> a -> p n a -> p n a
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> Int -> a -> p n a -> p n a
alterFlow Object
x (Object -> Int
oIndex Object
z) Object
y) Set (Object, Object, Object)
flow
    (p n Object -> p n Object)
-> (p n Object -> p n Object) -> p n Object -> p n Object
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Object -> p n Object -> p n Object)
-> Set Object -> p n Object -> p n Object
forall {t :: * -> *} {a} {c}.
Foldable t =>
(a -> c -> c) -> t a -> c -> c
foldrFlip
      (\Object
x -> Object -> Maybe Int -> p n Object -> p n Object
forall a. Ord a => a -> Maybe Int -> p n a -> p n a
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> Maybe Int -> p n a -> p n a
alterNode Object
x (Maybe Int -> p n Object -> p n Object)
-> Maybe Int -> p n Object -> p n Object
forall a b. (a -> b) -> a -> b
$ Object -> Map Object (Set Int) -> Maybe (Set Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Object
x Map Object (Set Int)
tokens Maybe (Set Int) -> (Set Int -> Maybe Int) -> Maybe Int
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Set Int -> Maybe Int
forall a. Set a -> Maybe a
Set.lookupMin)
      Set Object
nodes
    (p n Object -> m (p n Object)) -> p n Object -> m (p n Object)
forall a b. (a -> b) -> a -> b
$ p n Object
forall a. p n a
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a. Net p n => p n a
emptyNet
  where
    foldrFlip :: (a -> c -> c) -> t a -> c -> c
foldrFlip a -> c -> c
f = (c -> t a -> c) -> t a -> c -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((c -> t a -> c) -> t a -> c -> c)
-> (c -> t a -> c) -> t a -> c -> c
forall a b. (a -> b) -> a -> b
$ (a -> c -> c) -> c -> t a -> c
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr a -> c -> c
f

relToMap :: (Ord b, Ord c) => (a -> (b, c)) -> Set a -> Map b (Set c)
relToMap :: forall b c a.
(Ord b, Ord c) =>
(a -> (b, c)) -> Set a -> Map b (Set c)
relToMap a -> (b, c)
f = Set (b, c) -> Map b (Set c)
forall a b. (Ord a, Ord b) => Set (a, b) -> Map a (Set b)
toMap (Set (b, c) -> Map b (Set c))
-> (Set a -> Set (b, c)) -> Set a -> Map b (Set c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(b, c)] -> Set (b, c)
forall a. Ord a => [a] -> Set a
Set.fromList ([(b, c)] -> Set (b, c))
-> (Set a -> [(b, c)]) -> Set a -> Set (b, c)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a -> (b, c)) -> [a] -> [(b, c)]
forall a b. (a -> b) -> [a] -> [b]
map a -> (b, c)
f ([a] -> [(b, c)]) -> (Set a -> [a]) -> Set a -> [(b, c)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set a -> [a]
forall a. Set a -> [a]
Set.toList

{-|
Transform an 'Object' into a 'String' by replacing the prefix.
Returns 'Either':

 * an error message if no matching prefix was found
 * or the resulting 'String'
-}
simpleRename :: Object -> Either String String
simpleRename :: Object -> Either String String
simpleRename Object
x = case Object -> String
oName Object
x of
  String
"addedPlaces"      -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ Char
'a'Char -> String -> String
forall a. a -> [a] -> [a]
:Char
'S'Char -> String -> String
forall a. a -> [a] -> [a]
:String
y
  String
"addedTransitions" -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ Char
'a'Char -> String -> String
forall a. a -> [a] -> [a]
:Char
'T'Char -> String -> String
forall a. a -> [a] -> [a]
:String
y
  String
"givenPlaces"      -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ Char
'S'Char -> String -> String
forall a. a -> [a] -> [a]
:String
y
  String
"givenTransitions" -> String -> Either String String
forall a b. b -> Either a b
Right (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ Char
'T'Char -> String -> String
forall a. a -> [a] -> [a]
:String
y
  String
_                  ->
    String -> Either String String
forall a b. a -> Either a b
Left (String -> Either String String) -> String -> Either String String
forall a b. (a -> b) -> a -> b
$ String
"simpleRename: Could not rename " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Object -> String
oName Object
x String -> String -> String
forall a. [a] -> [a] -> [a]
++ Char
'$' Char -> String -> String
forall a. a -> [a] -> [a]
: String
y
  where
    y :: String
y = Int -> String
forall a. Show a => a -> String
show (Object -> Int
oIndex Object
x)

{-|
Parses a 'PetriChange' given an 'AlloyInstance'.
On error a 'Left' error message will be returned.
-}
parseChange :: MonadThrow m => AlloyInstance -> m (PetriChange Object)
parseChange :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance -> m (PetriChange Object)
parseChange AlloyInstance
inst = do
  Set (Object, Object, Object)
flow <- AlloyInstance
-> String -> String -> String -> m (Set (Object, Object, Object))
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance
-> String -> String -> String -> m (Set (Object, Object, Object))
tripleSig AlloyInstance
inst String
"this" String
"Nodes" String
"flowChange"
  Set (Object, Object)
token <- AlloyInstance
-> String -> String -> String -> m (Set (Object, Object))
forall (m :: * -> *).
MonadThrow m =>
AlloyInstance
-> String -> String -> String -> m (Set (Object, Object))
doubleSig AlloyInstance
inst String
"this" String
"Places" String
"tokenChange"
  let tokenMap :: Map Object (Set Int)
tokenMap = ((Object, Object) -> (Object, Int))
-> Set (Object, Object) -> Map Object (Set Int)
forall b c a.
(Ord b, Ord c) =>
(a -> (b, c)) -> Set a -> Map b (Set c)
relToMap ((Object -> Int) -> (Object, Object) -> (Object, Int)
forall b c d. (b -> c) -> (d, b) -> (d, c)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second Object -> Int
oIndex) Set (Object, Object)
token
  Map Object Int
tokenChange <- Set Int -> m Int
forall (m :: * -> *) b. MonadThrow m => Set b -> m b
asSingleton (Set Int -> m Int) -> Map Object (Set Int) -> m (Map Object Int)
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) -> Map Object a -> m (Map Object b)
`mapM` Map Object (Set Int)
tokenMap
  let flowMap :: Map Object (Set (Object, Int))
flowMap = ((Object, Object, Object) -> (Object, (Object, Int)))
-> Set (Object, Object, Object) -> Map Object (Set (Object, Int))
forall b c a.
(Ord b, Ord c) =>
(a -> (b, c)) -> Set a -> Map b (Set c)
relToMap (Object, Object, Object) -> (Object, (Object, Int))
forall {a} {a}. (a, a, Object) -> (a, (a, Int))
tripleToOut Set (Object, Object, Object)
flow
  let flowMap' :: Map Object (Map Object (Set Int))
flowMap' = ((Object, Int) -> (Object, Int))
-> Set (Object, Int) -> Map Object (Set Int)
forall b c a.
(Ord b, Ord c) =>
(a -> (b, c)) -> Set a -> Map b (Set c)
relToMap (Object, Int) -> (Object, Int)
forall a. a -> a
id (Set (Object, Int) -> Map Object (Set Int))
-> Map Object (Set (Object, Int))
-> Map Object (Map Object (Set Int))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Object (Set (Object, Int))
flowMap
  Map Object (Map Object Int)
flowChange  <- (Set Int -> m Int) -> Map Object (Set Int) -> m (Map Object Int)
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) -> Map Object a -> m (Map Object b)
mapM Set Int -> m Int
forall (m :: * -> *) b. MonadThrow m => Set b -> m b
asSingleton (Map Object (Set Int) -> m (Map Object Int))
-> Map Object (Map Object (Set Int))
-> m (Map Object (Map Object Int))
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) -> Map Object a -> m (Map Object b)
`mapM` Map Object (Map Object (Set Int))
flowMap'
  PetriChange Object -> m (PetriChange Object)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (PetriChange Object -> m (PetriChange Object))
-> PetriChange Object -> m (PetriChange Object)
forall a b. (a -> b) -> a -> b
$ Change {Map Object Int
Map Object (Map Object Int)
tokenChange :: Map Object Int
flowChange :: Map Object (Map Object Int)
$sel:tokenChange:Change :: Map Object Int
$sel:flowChange:Change :: Map Object (Map Object Int)
..}
  where
    tripleToOut :: (a, a, Object) -> (a, (a, Int))
tripleToOut (a
x, a
y, Object
z) = (a
x, (a
y, Object -> Int
oIndex Object
z))

data NoSingletonException
  = UnexpectedEmptySet
  | UnexpectedMultipleElements
  deriving Int -> NoSingletonException -> String -> String
[NoSingletonException] -> String -> String
NoSingletonException -> String
(Int -> NoSingletonException -> String -> String)
-> (NoSingletonException -> String)
-> ([NoSingletonException] -> String -> String)
-> Show NoSingletonException
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
$cshowsPrec :: Int -> NoSingletonException -> String -> String
showsPrec :: Int -> NoSingletonException -> String -> String
$cshow :: NoSingletonException -> String
show :: NoSingletonException -> String
$cshowList :: [NoSingletonException] -> String -> String
showList :: [NoSingletonException] -> String -> String
Show

instance Exception NoSingletonException

{-|
Convert a singleton 'Set' into its single value.
Returns a 'Left' error message if the 'Set' is empty or contains more than one
single element.
-}
asSingleton :: MonadThrow m => Set b -> m b
asSingleton :: forall (m :: * -> *) b. MonadThrow m => Set b -> m b
asSingleton Set b
s
  | Set b -> Bool
forall a. Set a -> Bool
Set.null Set b
s
  = NoSingletonException -> m b
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM NoSingletonException
UnexpectedEmptySet
  | Set b -> Int
forall a. Set a -> Int
Set.size Set b
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
1
  = NoSingletonException -> m b
forall e a. Exception e => e -> m a
forall (m :: * -> *) e a. (MonadThrow m, Exception e) => e -> m a
throwM NoSingletonException
UnexpectedMultipleElements
  | Bool
otherwise
  = b -> m b
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (b -> m b) -> b -> m b
forall a b. (a -> b) -> a -> b
$ Set b -> b
forall a. Set a -> a
Set.findMin Set b
s

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

doubleSig
  :: MonadThrow m
  => AlloyInstance
  -> String
  -> String
  -> String
  -> m (Set.Set (Object,Object))
doubleSig :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance
-> String -> String -> String -> m (Set (Object, Object))
doubleSig AlloyInstance
inst String
st String
nd String
rd = do
  AlloySig
sig <- Signature -> AlloyInstance -> m AlloySig
forall (m :: * -> *).
MonadThrow m =>
Signature -> AlloyInstance -> m AlloySig
lookupSig (String -> String -> Signature
scoped String
st String
nd) AlloyInstance
inst
  let obj :: String -> Int -> m Object
obj = Object -> m Object
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Object -> m Object)
-> (String -> Int -> Object) -> String -> Int -> m Object
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: String -> Int -> Object
Object
  String
-> (String -> Int -> m Object)
-> (String -> Int -> m Object)
-> AlloySig
-> m (Set (Object, Object))
forall (m :: * -> *) a b.
(MonadThrow m, Ord a, Ord b) =>
String
-> (String -> Int -> m a)
-> (String -> Int -> m b)
-> AlloySig
-> m (Set (a, b))
getDoubleAs String
rd String -> Int -> m Object
obj String -> Int -> m Object
obj AlloySig
sig

tripleSig
  :: MonadThrow m
  => AlloyInstance
  -> String
  -> String
  -> String
  -> m (Set.Set (Object,Object,Object))
tripleSig :: forall (m :: * -> *).
MonadThrow m =>
AlloyInstance
-> String -> String -> String -> m (Set (Object, Object, Object))
tripleSig AlloyInstance
inst String
st String
nd String
rd = do
  AlloySig
sig <- Signature -> AlloyInstance -> m AlloySig
forall (m :: * -> *).
MonadThrow m =>
Signature -> AlloyInstance -> m AlloySig
lookupSig (String -> String -> Signature
scoped String
st String
nd) AlloyInstance
inst
  let obj :: String -> Int -> m Object
obj = Object -> m Object
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Object -> m Object)
-> (String -> Int -> Object) -> String -> Int -> m Object
forall c d a b. (c -> d) -> (a -> b -> c) -> a -> b -> d
.: String -> Int -> Object
Object
  String
-> (String -> Int -> m Object)
-> (String -> Int -> m Object)
-> (String -> Int -> m Object)
-> AlloySig
-> m (Set (Object, Object, Object))
forall (m :: * -> *) a b c.
(MonadThrow m, Ord a, Ord b, Ord c) =>
String
-> (String -> Int -> m a)
-> (String -> Int -> m b)
-> (String -> Int -> m c)
-> AlloySig
-> m (Set (a, b, c))
getTripleAs String
rd String -> Int -> m Object
obj String -> Int -> m Object
obj String -> Int -> m Object
obj AlloySig
sig

{-|
Retrieve a simple naming map from a given 'Net'.
The newly created names for naming every 'PetriNode' of the 'Net' are unique
for each individually 'PetriNode'.
Furthermore, each place node's names prefix is a @s@, while each
transition node's name is preceded by a @t@.
These prefixes are followed by numbers starting at 1 and reaching to the number
of place nodes and transition nodes respectively.
-}
simpleNameMap :: (Net p n, Ord a) => p n a -> Bimap a String
simpleNameMap :: forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Bimap a String
simpleNameMap p n a
pl = [(a, String)] -> Bimap a String
forall a b. (Ord a, Ord b) => [(a, b)] -> Bimap a b
BM.fromList ([(a, String)] -> Bimap a String)
-> (([(a, String)], (Integer, Integer)) -> [(a, String)])
-> ([(a, String)], (Integer, Integer))
-> Bimap a String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([(a, String)], (Integer, Integer)) -> [(a, String)]
forall a b. (a, b) -> a
fst (([(a, String)], (Integer, Integer)) -> Bimap a String)
-> (Map a (n a) -> ([(a, String)], (Integer, Integer)))
-> Map a (n a)
-> Bimap a String
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  (([(a, String)], (Integer, Integer))
 -> a -> n a -> ([(a, String)], (Integer, Integer)))
-> ([(a, String)], (Integer, Integer))
-> Map a (n a)
-> ([(a, String)], (Integer, Integer))
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey'
  ([(a, String)], (Integer, Integer))
-> a -> n a -> ([(a, String)], (Integer, Integer))
forall {n :: * -> *} {a} {b} {a} {a}.
(PetriNode n, Num a, Num b, Show a, Show b) =>
([(a, String)], (a, b)) -> a -> n a -> ([(a, String)], (a, b))
nameIncreasingly
  ([], (Integer
1 :: Integer, Integer
1 :: Integer))
  (Map a (n a) -> Bimap a String) -> Map a (n a) -> Bimap a String
forall a b. (a -> b) -> a -> b
$ p n a -> Map a (n a)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
PN.nodes p n a
pl
  where
    nameIncreasingly :: ([(a, String)], (a, b)) -> a -> n a -> ([(a, String)], (a, b))
nameIncreasingly ([(a, String)]
ys, (a
p, b
t)) a
k n a
x =
      let (String
k', a
p', b
t') = n a -> a -> b -> (String, a, b)
forall {n :: * -> *} {b} {a} {a}.
(PetriNode n, Num b, Num a, Show b, Show a) =>
n a -> b -> a -> (String, b, a)
step n a
x a
p b
t
      in ((a
k, String
k')(a, String) -> [(a, String)] -> [(a, String)]
forall a. a -> [a] -> [a]
:[(a, String)]
ys, (a
p', b
t'))
    step :: n a -> b -> a -> (String, b, a)
step n a
n b
p a
t
      | n a -> Bool
forall a. n a -> Bool
forall (n :: * -> *) a. PetriNode n => n a -> Bool
isPlaceNode n a
n = (Char
's'Char -> String -> String
forall a. a -> [a] -> [a]
:b -> String
forall a. Show a => a -> String
show b
p, b
p b -> b -> b
forall a. Num a => a -> a -> a
+ b
1, a
t)
      | Bool
otherwise     = (Char
't'Char -> String -> String
forall a. a -> [a] -> [a]
:a -> String
forall a. Show a => a -> String
show a
t, b
p, a
t a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)

{-|
Convert a 'Net' into a 'Gr' enabling to draw it using graphviz.
-}
netToGr
  :: (Monad m, Net p n, Ord a)
  => p n a
  -> m (Gr (a, Maybe Int) Int)
netToGr :: forall (m :: * -> *) (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Monad m, Net p n, Ord a) =>
p n a -> m (Gr (a, Maybe Int) Int)
netToGr p n a
petriLike = do
  [(Int, (a, Maybe Int))]
nodes <- (a
 -> n a -> m [(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))])
-> m [(Int, (a, Maybe Int))]
-> Map a (n a)
-> m [(Int, (a, Maybe Int))]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey a -> n a -> m [(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))]
forall {m :: * -> *} {n :: * -> *} {a}.
(Monad m, PetriNode n) =>
a -> n a -> m [(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))]
convertNode ([(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []) (Map a (n a) -> m [(Int, (a, Maybe Int))])
-> Map a (n a) -> m [(Int, (a, Maybe Int))]
forall a b. (a -> b) -> a -> b
$ p n a -> Map a (n a)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
PN.nodes p n a
petriLike
  let edges :: [(Int, Int, Int)]
edges = (a -> n a -> [(Int, Int, Int)] -> [(Int, Int, Int)])
-> [(Int, Int, Int)] -> Map a (n a) -> [(Int, Int, Int)]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey a -> n a -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall {p}. a -> p -> [(Int, Int, Int)] -> [(Int, Int, Int)]
convertTransition [] (Map a (n a) -> [(Int, Int, Int)])
-> Map a (n a) -> [(Int, Int, Int)]
forall a b. (a -> b) -> a -> b
$ p n a -> Map a (n a)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
PN.nodes p n a
petriLike
  Gr (a, Maybe Int) Int -> m (Gr (a, Maybe Int) Int)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Gr (a, Maybe Int) Int -> m (Gr (a, Maybe Int) Int))
-> Gr (a, Maybe Int) Int -> m (Gr (a, Maybe Int) Int)
forall a b. (a -> b) -> a -> b
$ [(Int, (a, Maybe Int))]
-> [(Int, Int, Int)] -> Gr (a, Maybe Int) Int
forall a b. [LNode a] -> [LEdge b] -> Gr a b
forall (gr :: * -> * -> *) a b.
Graph gr =>
[LNode a] -> [LEdge b] -> gr a b
mkGraph [(Int, (a, Maybe Int))]
nodes [(Int, Int, Int)]
edges
  where
    convertNode :: a -> n a -> m [(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))]
convertNode a
k n a
x m [(Int, (a, Maybe Int))]
ns = do
      [(Int, (a, Maybe Int))]
ns' <- m [(Int, (a, Maybe Int))]
ns
      [(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ([(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))])
-> [(Int, (a, Maybe Int))] -> m [(Int, (a, Maybe Int))]
forall a b. (a -> b) -> a -> b
$ (a -> Int
indexOf a
k, (a
k, n a -> Maybe Int
forall (n :: * -> *) a. PetriNode n => n a -> Maybe Int
maybeInitial n a
x))(Int, (a, Maybe Int))
-> [(Int, (a, Maybe Int))] -> [(Int, (a, Maybe Int))]
forall a. a -> [a] -> [a]
:[(Int, (a, Maybe Int))]
ns'
    convertTransition :: a -> p -> [(Int, Int, Int)] -> [(Int, Int, Int)]
convertTransition a
k p
_ [(Int, Int, Int)]
ns =
      (a -> Int -> [(Int, Int, Int)] -> [(Int, Int, Int)])
-> [(Int, Int, Int)] -> Map a Int -> [(Int, Int, Int)]
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (a -> a -> Int -> [(Int, Int, Int)] -> [(Int, Int, Int)]
forall {c}. a -> a -> c -> [(Int, Int, c)] -> [(Int, Int, c)]
convertEdge a
k) [(Int, Int, Int)]
ns (Map a Int -> [(Int, Int, Int)]) -> Map a Int -> [(Int, Int, Int)]
forall a b. (a -> b) -> a -> b
$ a -> p n a -> Map a Int
forall a. Ord a => a -> p n a -> Map a Int
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
a -> p n a -> Map a Int
outFlow a
k p n a
petriLike
    indexOf :: a -> Int
indexOf a
x = a -> Map a (n a) -> Int
forall k a. Ord k => k -> Map k a -> Int
Map.findIndex a
x (Map a (n a) -> Int) -> Map a (n a) -> Int
forall a b. (a -> b) -> a -> b
$ p n a -> Map a (n a)
forall a. Ord a => p n a -> Map a (n a)
forall (p :: (* -> *) -> * -> *) (n :: * -> *) a.
(Net p n, Ord a) =>
p n a -> Map a (n a)
PN.nodes p n a
petriLike
    convertEdge :: a -> a -> c -> [(Int, Int, c)] -> [(Int, Int, c)]
convertEdge a
source a
target c
flow [(Int, Int, c)]
rs =
      (a -> Int
indexOf a
source, a -> Int
indexOf a
target, c
flow) (Int, Int, c) -> [(Int, Int, c)] -> [(Int, Int, c)]
forall a. a -> [a] -> [a]
: [(Int, Int, c)]
rs