Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

21.10.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

Commit 174936de authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Started using safer types for places and transition in Petri nets

parent e9de1d7a
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PetriNet
(Marking,tokens,buildMarking,
PetriNet,name,showNetName,places,transitions,initial,initialMarking,
pre,lpre,post,lpost,initials,context,arcs,ghostTransitions,
(PetriNet,Place,Transition,Marking,tokens,buildMarking,
name,showNetName,places,transitions,initial,initialMarking,
pre,lpre,post,lpost,initials,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans)
where
import qualified Data.Map as M
type Place = String
type Transition = String
type Node = String
newtype Marking = Marking { getMarkingMap :: M.Map Place Integer }
import Control.Arrow (first)
newtype Place = Place String deriving (Ord,Eq)
newtype Transition = Transition String deriving (Ord,Eq)
instance Show Place where
show (Place p) = p
instance Show Transition where
show (Transition t) = t
type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])
class Nodes a b | a -> b where
pre :: (Ord a) => PetriNet -> a -> [b]
pre net = map fst . fst . context net
post :: (Ord a) => PetriNet -> a -> [b]
post net = map fst . snd . context net
lpre :: (Ord a) => PetriNet -> a -> [(b, Integer)]
lpre net = fst . context net
lpost :: (Ord a) => PetriNet -> a -> [(b, Integer)]
lpost net = snd . context net
context :: (Ord a) => PetriNet -> a -> ([(b, Integer)], [(b, Integer)])
context net x = M.findWithDefault ([],[]) x (contextMap net)
contextMap :: PetriNet -> ContextMap a b
instance Nodes Place Transition where
contextMap = adjacencyP
instance Nodes Transition Place where
contextMap = adjacencyT
newtype Marking = Marking { getMarking :: M.Map Place Integer }
instance Show Marking where
show (Marking m) = unwords $ map showPlaceMarking $ M.toList m
show (Marking m) = show $ map showPlaceMarking $ M.toList m
where showPlaceMarking (n,i) =
n ++ (if i /= 1 then "[" ++ show i ++ "]" else "")
show n ++ (if i /= 1 then "(" ++ show i ++ ")" else "")
tokens :: Marking -> Place -> Integer
tokens m p = M.findWithDefault 0 p (getMarkingMap m)
tokens m p = M.findWithDefault 0 p (getMarking m)
buildMarking :: [(Place, Integer)] -> Marking
buildMarking xs = Marking $ M.fromList $ filter ((/=0) . snd) xs
buildMarking :: [(String, Integer)] -> Marking
buildMarking xs = Marking $ M.fromList $ map (first Place) $ filter ((/=0) . snd) xs
data PetriNet = PetriNet {
name :: String,
places :: [Place],
transitions :: [Transition],
adjacency :: M.Map Node ([(Node,Integer)], [(Node,Integer)]),
adjacencyP :: M.Map Place ([(Transition,Integer)], [(Transition,Integer)]),
adjacencyT :: M.Map Transition ([(Place,Integer)], [(Place,Integer)]),
initialMarking :: Marking,
ghostTransitions :: [Transition]
}
......@@ -37,27 +65,8 @@ data PetriNet = PetriNet {
initial :: PetriNet -> Place -> Integer
initial net = tokens (initialMarking net)
arcs :: PetriNet -> [(Node, Node, Integer)]
arcs net = concatMap (\(a,(_,bs)) -> map (\(b,w) -> (a,b,w)) bs)
(M.toList (adjacency net))
context :: PetriNet -> Node -> ([(Node, Integer)], [(Node, Integer)])
context net x = M.findWithDefault ([],[]) x (adjacency net)
pre :: PetriNet -> Node -> [Node]
pre net = map fst . fst . context net
lpre :: PetriNet -> Node -> [(Node, Integer)]
lpre net = fst . context net
post :: PetriNet -> Node -> [Node]
post net = map fst . snd . context net
lpost :: PetriNet -> Node -> [(Node, Integer)]
lpost net = snd . context net
initials :: PetriNet -> [(Place,Integer)]
initials net = M.toList (getMarkingMap (initialMarking net))
initials net = M.toList (getMarking (initialMarking net))
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
......@@ -65,32 +74,69 @@ showNetName net = "Petri net" ++
instance Show PetriNet where
show net = showNetName net ++
"\nPlaces: " ++ unwords (places net) ++
"\nTransitions: " ++ unwords (transitions net) ++
"\nArcs:\n" ++ unlines
(map (\(s,(l,r)) -> show l ++ " -> " ++
s ++ " -> " ++ show r)
(M.toList (adjacency net))) ++
"Initial: " ++ show (initialMarking net) ++
"\nGhost transitions: " ++ unwords (ghostTransitions net)
makePetriNet :: String -> [Place] -> [Transition] ->
[(Node, Node, Integer)] -> [(Place, Integer)] -> [Transition] -> PetriNet
"\nPlaces: " ++ show (places net) ++
"\nTransitions: " ++ show (transitions net) ++
"\nPlace arcs:\n" ++ unlines
(map showContext (M.toList (adjacencyP net))) ++
"\nTransition arcs:\n" ++ unlines
(map showContext (M.toList (adjacencyT net))) ++
"\nInitial: " ++ show (initialMarking net) ++
"\nGhost transitions: " ++ show (ghostTransitions net)
where showContext (s,(l,r)) =
show l ++ " -> " ++ show s ++ " -> " ++ show r
--makePetriNet :: String -> [Place] -> [Transition] ->
-- [(Place, ([(Transition, Integer)], [(Transition, Integer)]))] ->
-- [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
-- [(Place, Integer)] -> [Transition] -> PetriNet
--makePetriNet name places transitions placeArcs transitionArcs initial gs =
-- PetriNet { name=name, places=places, transitions=transitions,
-- adjacencyP=M.fromList (adjacencyFilter placeArcs),
-- adjacencyT=M.fromList (adjacencyFilter transitionArcs),
-- initialMarking=buildMarking initial,
-- ghostTransitions=gs }
-- where
-- adjacencyFilter = filter contextFilter
-- contextFilter (x,pre,post) =
-- (x,filter arcFilter pre, filter arcFilter post)
-- arcFilter (_,w) = w /= 0
makePetriNet :: String -> [String] -> [String] ->
[(String, String, Integer)] ->
[(String, Integer)] -> [String] -> PetriNet
makePetriNet name places transitions arcs initial gs =
let adjacency = foldl buildMap M.empty $ filter (\(_,_,w) -> w /= 0) arcs
in PetriNet { name=name, places=places, transitions=transitions,
adjacency=adjacency, initialMarking=buildMarking initial,
ghostTransitions=gs }
let (adP, adT) = foldl buildMaps (M.empty, M.empty)
(filter (\(_,_,w) -> w /= 0) arcs)
in PetriNet {
name = name,
places = map Place places,
transitions = map Transition transitions,
adjacencyP = adP,
adjacencyT = adT,
initialMarking = buildMarking initial,
ghostTransitions = map Transition gs
}
where
buildMap m (l,r,w) =
let m' = M.insertWith addArc l ([],[(r,w)]) m
m'' = M.insertWith addArc r ([(l,w)],[]) m'
in m''
buildMaps (mp,mt) (_,_,0) = (mp,mt)
buildMaps (mp,mt) (l,r,w) | l `elem` places && r `elem` transitions =
let mp' = M.insertWith addArc
(Place l) ([],[(Transition r, w)]) mp
mt' = M.insertWith addArc
(Transition r) ([(Place l, w)],[]) mt
in (mp',mt')
buildMaps (mp,mt) (l,r,w) | l `elem` transitions && r `elem` places =
let mt' = M.insertWith addArc
(Transition l) ([],[(Place r, w)]) mt
mp' = M.insertWith addArc
(Place r) ([(Transition l, w)],[]) mp
in (mp',mt')
buildMaps _ (l,r,_) = error $ "nodes " ++ l ++ " and " ++ r ++
" both places or transitions"
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
makePetriNetWithTrans :: String -> [Place] ->
[(Transition, [(Place, Integer)], [(Place, Integer)])] ->
[(Place, Integer)] -> [Transition] -> PetriNet
makePetriNetWithTrans :: String -> [String] ->
[(String, [(String, Integer)], [(String, Integer)])] ->
[(String, Integer)] -> [String] -> PetriNet
makePetriNetWithTrans name places ts initial gs =
let transitions = [ t | (t,_,_) <- ts ]
arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
......
module Printer
(validateId,intercalate)
(validateId,intercalate,renderPlace,renderTransition,renderShow)
where
import Data.Char
import Data.ByteString.Builder
import Data.Monoid
import PetriNet
validateId :: String -> String
validateId "" = "_"
validateId (x:xs) = (if isAlpha x then x else '_') :
......@@ -17,3 +19,11 @@ intercalate _ [] = mempty
intercalate sep (x:xs) = x <> go xs
where go = foldr (\y -> (<>) (sep <> y)) mempty
renderPlace :: Place -> Builder
renderPlace = renderShow
renderTransition :: Transition -> Builder
renderTransition = renderShow
renderShow :: (Show a) => a -> Builder
renderShow = stringUtf8 . show
......@@ -8,6 +8,7 @@ import qualified Data.ByteString.Lazy as L
import Data.ByteString.Builder
import Data.Monoid
import Printer
import PetriNet
-- TODO: mark initially labeled places
......@@ -18,17 +19,18 @@ renderNet net =
mconcat (map transLabel (transitions net)) <>
"}\n"
where
placeLabel p = stringUtf8 p <> " [label=\"" <> stringUtf8 p <>
placeLabel p = renderPlace p <> " [label=\"" <> renderPlace p <>
(if initial net p > 0 then
"(" <> integerDec (initial net p) <> ")"
else
""
) <> "\"];\n"
transLabel t = stringUtf8 t <> " [label=\"" <> stringUtf8 t <> "\", shape=box, " <>
transLabel t = renderTransition t <>
" [label=\"" <> renderTransition t <> "\", shape=box, " <>
"style=filled, fillcolor=\"#AAAAAA\"];\n" <>
mconcat (map (\p -> arcLabel (p,t)) (pre net t)) <>
mconcat (map (\p -> arcLabel (t,p)) (post net t))
arcLabel (a,b) = stringUtf8 a <> " -> " <> stringUtf8 b <> "\n"
arcLabel (a,b) = renderShow a <> " -> " <> renderShow b <> "\n"
printNet :: PetriNet -> L.ByteString
printNet = toLazyByteString . renderNet
......@@ -14,9 +14,9 @@ import Property
renderNet :: PetriNet -> Builder
renderNet net =
let showWeight (p,x) = stringUtf8 p <> ":" <> integerDec x
let showWeight (p,x) = renderPlace p <> ":" <> integerDec x
ps = "PLACE " <> intercalate ","
(map stringUtf8 (places net)) <> ";\n"
(map renderPlace (places net)) <> ";\n"
is = "MARKING " <> intercalate ","
(map showWeight (initials net)) <> ";\n"
makeTransition t =
......@@ -25,7 +25,7 @@ renderNet net =
(map showWeight preT) <> ";\n"
postS = "PRODUCE " <> intercalate ","
(map showWeight postT) <> ";\n"
in "TRANSITION " <> stringUtf8 t <> "\n" <> preS <> postS
in "TRANSITION " <> renderTransition t <> "\n" <> preS <> postS
ts = map makeTransition (transitions net)
in intercalate "\n" (ps:is:ts)
......
......@@ -59,7 +59,7 @@ renderDisjunction propname filename net f =
"FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename)))
<> " TYPE LOLA;\n" <>
"INITIAL " <> intercalate ","
(map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (initials net))
(map (\(p,i) -> renderPlace p <> ":" <> integerDec i) (initials net))
<> ";\n" <>
"FINAL COVER;\n" <>
"CONSTRAINTS " <> renderConjunction f <> ";"
......
......@@ -40,7 +40,7 @@ checkCommunicationFree net =
checkWeights t = all checkWeight (lpre net t)
checkWeight (_,w) = w <= 1
checkParallelT :: PetriNet -> String -> Bool
checkParallelT :: PetriNet -> Transition -> Bool
checkParallelT net t =
any postComp [(p,s) | p <- post net t, s <- post net t]
where postComp (p,s) =
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment