PetriNet.hs 3.33 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
2
3
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module PetriNet
4
    (PetriNet,name,showNetName,places,transitions,initial,
5
     pre,lpre,post,lpost,initials,context,arcs,ghostTransitions,
Philipp Meyer's avatar
Philipp Meyer committed
6
     makePetriNet,makePetriNetWithTrans)
Philipp Meyer's avatar
Philipp Meyer committed
7
8
where

9
10
import qualified Data.Map as M

Philipp Meyer's avatar
Philipp Meyer committed
11
12
13
14
data PetriNet = PetriNet {
        name :: String,
        places :: [String],
        transitions :: [String],
15
        adjacency :: M.Map String ([(String,Integer)], [(String,Integer)]),
16
17
        initMap :: M.Map String Integer,
        ghostTransitions :: [String]
Philipp Meyer's avatar
Philipp Meyer committed
18
19
}

20
21
22
initial :: PetriNet -> String -> Integer
initial net p = M.findWithDefault 0 p (initMap net)

23
24
25
26
arcs :: PetriNet -> [(String, String, Integer)]
arcs net = concatMap (\(a,(_,bs)) -> map (\(b,w) -> (a,b,w)) bs)
                           (M.toList (adjacency net))

27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
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

42
43
44
initials :: PetriNet -> [(String,Integer)]
initials net = M.toList (initMap net)

45
46
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
47
48
               (if null (name net) then "" else " " ++ show (name net))

Philipp Meyer's avatar
Philipp Meyer committed
49
instance Show PetriNet where
50
        show net = showNetName net ++
51
52
53
                   "\nPlaces: " ++ unwords (places net) ++
                   "\nTransitions: " ++ unwords (transitions net) ++
                   "\nArcs:\n" ++ unlines
54
55
56
                        (map (\(s,(l,r)) -> show l ++ " -> " ++
                            s ++ " -> " ++ show r)
                        (M.toList (adjacency net))) ++
Philipp Meyer's avatar
Philipp Meyer committed
57
58
59
                   "Initial: " ++ unwords
                        (map (\(n,i) -> n ++
                            (if i /= 1 then "[" ++ show i ++ "]" else []))
60
61
                        (M.toList (initMap net))) ++
                   "\nGhost transitions: " ++ unwords (ghostTransitions net)
Philipp Meyer's avatar
Philipp Meyer committed
62
63

makePetriNet :: String -> [String] -> [String] ->
64
65
66
67
        [(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
            initMap = M.fromList $ filter ((/=0) . snd) initial
68
        in  PetriNet { name=name, places=places, transitions=transitions,
69
70
                       adjacency=adjacency, initMap=initMap,
                       ghostTransitions=gs }
71
72
73
74
75
76
77
        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)

Philipp Meyer's avatar
Philipp Meyer committed
78
79
makePetriNetWithTrans :: String -> [String] ->
        [(String, [(String, Integer)], [(String, Integer)])] ->
80
81
        [(String, Integer)] -> [String] -> PetriNet
makePetriNetWithTrans name places ts initial gs =
Philipp Meyer's avatar
Philipp Meyer committed
82
83
84
        let transitions = [ t | (t,_,_) <- ts ]
            arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
                   [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
85
        in  makePetriNet name places transitions arcs initial gs