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 b113299f authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Using adjacency lists for representing Petri nets

parent a4645dde
......@@ -23,6 +23,6 @@ executable slapnet
PetriNet
Parser
-- other-extensions:
build-depends: base >=4.6 && <4.7, sbv, parsec
build-depends: base >=4.6 && <4.7, sbv, parsec, containers
hs-source-dirs: src
default-language: Haskell2010
......@@ -16,7 +16,7 @@ main = do
putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
putStrLn $ "Reading \"" ++ file ++ "\""
(net,properties) <- parseFile file
putStrLn $ "Analyzing " ++ show net
putStrLn $ "Analyzing " ++ showName net
mapM_ (\p -> do
putStrLn $ "Checking " ++ show p
putStrLn $ show $ checkProperty net p
......
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PetriNet
(PetriNet,name,places,transitions,
(PetriNet,showName,places,transitions,initial,
pre,lpre,post,lpost,
makePetriNet)
where
import qualified Data.Map as M
data PetriNet = PetriNet {
name :: String,
places :: [String],
transitions :: [String],
arcs :: [(String,String,Integer)],
adjacency :: M.Map String ([(String,Integer)], [(String,Integer)]),
initial :: [(String,Integer)]
}
context :: PetriNet -> String -> ([(String, Integer)], [(String, Integer)])
context net x = M.findWithDefault ([],[]) x (adjacency net)
pre :: PetriNet -> String -> [String]
pre net = map fst . fst . context net
lpre :: PetriNet -> String -> [(String, Integer)]
lpre net = fst . context net
post :: PetriNet -> String -> [String]
post net = map fst . snd . context net
lpost :: PetriNet -> String -> [(String, Integer)]
lpost net = snd . context net
showName :: PetriNet -> String
showName net = "Petri net" ++
(if null (name net) then "" else " " ++ show (name net))
instance Show PetriNet where
show net = "Petri net" ++
(if null (name net) then "" else " " ++ show (name net)) ++
show net = showName net ++
"\nPlaces: " ++ unwords (places net) ++
"\nTransitions: " ++ unwords (transitions net) ++
"\nArcs:\n" ++ unlines
(map (\(l,r,w) -> l ++ " ->" ++
(if w /= 1 then "[" ++ show w ++ "]" else []) ++
" " ++ r)
(arcs net)) ++
(map (\(s,(l,r)) -> show l ++ " -> " ++
s ++ " -> " ++ show r)
(M.toList (adjacency net))) ++
"Initial: " ++ unwords
(map (\(n,i) -> n ++
(if i /= 1 then "[" ++ show i ++ "]" else []))
(initial net))
makePetriNet :: String -> [String] -> [String] ->
[(String, String,Integer)] -> [(String, Integer)] -> PetriNet
[(String, String, Integer)] -> [(String, Integer)] -> PetriNet
makePetriNet name places transitions arcs initial =
PetriNet { name=name, places=places, transitions=transitions,
arcs=arcs, initial=initial }
let adjacency = foldl buildMap M.empty arcs
in PetriNet { name=name, places=places, transitions=transitions,
adjacency=adjacency, initial=initial }
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''
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
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