PetriNet.hs 7.95 KB
Newer Older
1
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
Philipp Meyer's avatar
Philipp Meyer committed
2
3
4
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module PetriNet
5
6
    (PetriNet,Place(..),Transition(..),Marking,buildVector,
     value,elems,items,makeVector,FiringVector,
7
     renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
8
9
10
     name,showNetName,places,transitions,initialMarking,initial,initials,linitials,
     pre,lpre,post,lpost,context,ghostTransitions,
     makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut)
Philipp Meyer's avatar
Philipp Meyer committed
11
12
where

13
import qualified Data.Map as M
Philipp Meyer's avatar
Philipp Meyer committed
14
import Data.List (intercalate)
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
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

45
newtype Vector a = Vector { getVector :: M.Map a Integer }
46

47
48
type Marking = Vector Place
type FiringVector = Vector Transition
49

50
51
52
53
54
instance (Show a) => Show (Vector a) where
        show (Vector v) =
                "[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
            where showEntry (v,x) =
                    show v ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
55

56
57
value :: (Ord a) => Vector a -> a -> Integer
value v x = M.findWithDefault 0 x (getVector v)
Philipp Meyer's avatar
Philipp Meyer committed
58

59
60
elems :: (Ord a) => Vector a -> [a]
elems = M.keys . getVector
Philipp Meyer's avatar
Philipp Meyer committed
61

62
63
items :: Vector a -> [(a,Integer)]
items = M.toList . getVector
Philipp Meyer's avatar
Philipp Meyer committed
64

65
66
67
68
69
buildVector :: (Ord a) => [(a, Integer)] -> Vector a
buildVector = makeVector . M.fromList

makeVector :: (Ord a) => M.Map a Integer -> Vector a
makeVector = Vector . M.filter (/=0)
Philipp Meyer's avatar
Philipp Meyer committed
70
71

type Trap = [Place]
72
type Cut = ([[Transition]], [Transition])
73

Philipp Meyer's avatar
Philipp Meyer committed
74
75
data PetriNet = PetriNet {
        name :: String,
76
77
        places :: [Place],
        transitions :: [Transition],
78
79
        adjacencyP :: M.Map Place ([(Transition,Integer)], [(Transition,Integer)]),
        adjacencyT :: M.Map Transition ([(Place,Integer)], [(Place,Integer)]),
80
81
        initialMarking :: Marking,
        ghostTransitions :: [Transition]
Philipp Meyer's avatar
Philipp Meyer committed
82
83
}

84
initial :: PetriNet -> Place -> Integer
85
86
87
88
initial net = value (initialMarking net)

initials :: PetriNet -> [Place]
initials = elems . initialMarking
89

90
91
linitials :: PetriNet -> [(Place,Integer)]
linitials = items . initialMarking
92

93
94
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
95
96
               (if null (name net) then "" else " " ++ show (name net))

Philipp Meyer's avatar
Philipp Meyer committed
97
instance Show PetriNet where
98
        show net = showNetName net ++
99
100
101
102
103
104
105
106
107
108
109
                   "\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

110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
renamePlace :: (String -> String) -> Place -> Place
renamePlace f (Place p) = Place (f p)

renameTransition :: (String -> String) -> Transition -> Transition
renameTransition f (Transition t) = Transition (f t)

renamePetriNetPlacesAndTransitions :: (String -> String) -> PetriNet -> PetriNet
renamePetriNetPlacesAndTransitions f net =
            PetriNet {
                name = name net,
                places      = map (renamePlace f) $ places net,
                transitions = map (renameTransition f) $ transitions net,
                adjacencyP  = mapAdjacency (renamePlace f) (renameTransition f) $
                    adjacencyP net,
                adjacencyT  = mapAdjacency (renameTransition f) (renamePlace f) $
                    adjacencyT net,
126
127
                initialMarking = Vector $
                    M.mapKeys (renamePlace f) $ getVector $ initialMarking net,
128
129
130
131
                ghostTransitions = map (renameTransition f) $ ghostTransitions net
            }
        where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
              mapContext f (pre, post) = (map (first f) pre, map (first f) post)
132
133
134
135

makePetriNet :: String -> [String] -> [String] ->
        [(String, String, Integer)] ->
        [(String, Integer)] -> [String] -> PetriNet
136
makePetriNet name places transitions arcs initial gs =
137
138
139
140
141
142
143
144
        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,
145
                initialMarking = buildVector (map (first Place) initial),
146
147
                ghostTransitions = map Transition gs
            }
148
        where
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
            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"
164
165
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)

166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
-- TODO: better constructors
makePetriNetWith :: String -> [Place] ->
        [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
        [(Place, Integer)] -> [Transition] -> PetriNet
makePetriNetWith name places ts initial gs =
        let transitions = map fst ts
            buildMap m (p,c) = M.insertWith addArc p c m
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
            placeArcs = [ (i,([],[(t,w)])) | (t,(is,_)) <- ts, (i,w) <- is ] ++
                        [ (o,([(t,w)],[])) | (t,(_,os)) <- ts, (o,w) <- os ]
            placeMap = foldl buildMap M.empty placeArcs
        in  PetriNet {
                name = name,
                places = places,
                transitions = transitions,
                adjacencyP = placeMap,
                adjacencyT = M.fromList ts,
183
                initialMarking = buildVector initial,
184
185
186
                ghostTransitions = gs
            }

187
188
189
makePetriNetWithTrans :: String -> [String] ->
        [(String, [(String, Integer)], [(String, Integer)])] ->
        [(String, Integer)] -> [String] -> PetriNet
190
makePetriNetWithTrans name places ts initial gs =
Philipp Meyer's avatar
Philipp Meyer committed
191
192
193
        let transitions = [ t | (t,_,_) <- ts ]
            arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
                   [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
194
        in  makePetriNet name places transitions arcs initial gs