PetriNet.hs 7.85 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
    (PetriNet,Place(..),Transition(..),Marking,FiringVector,
6
     renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
7
8
     name,showNetName,places,transitions,
     initialMarking,initial,initials,linitials,
9
     pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
10
     makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut,constructCut)
Philipp Meyer's avatar
Philipp Meyer committed
11
12
where

13
import qualified Data.Map as M
14
import Control.Arrow (first)
15
import Data.List (sort)
16

17
18
import Util

19
20
21
22
23
24
25
26
27
28
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)])

29
30
class (Ord a, Ord b) => Nodes a b | a -> b where
        lpre :: PetriNet -> a -> [(b, Integer)]
31
        lpre net = fst . context net
32
        lpost :: PetriNet -> a -> [(b, Integer)]
33
        lpost net = snd . context net
34
35
36
37
38
39
40
41
42
43
44
45
46
        pre :: PetriNet -> a -> [b]
        pre net = map fst . lpre net
        post :: PetriNet -> a -> [b]
        post net = map fst . lpost net
        lmpre :: PetriNet -> [a] -> [(b, Integer)]
        lmpre net = nubOrdBy fst . concatMap (lpre net)
        lmpost :: PetriNet -> [a] -> [(b, Integer)]
        lmpost net = nubOrdBy fst . concatMap (lpost net)
        mpre :: PetriNet -> [a] -> [b]
        mpre net = map fst . lmpre net
        mpost :: PetriNet -> [a] -> [b]
        mpost net = map fst . lmpost net
        context :: PetriNet -> a -> ([(b, Integer)], [(b, Integer)])
47
48
49
50
51
52
53
54
        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

55
56
type Marking = Vector Place
type FiringVector = Vector Transition
57

Philipp Meyer's avatar
Philipp Meyer committed
58
type Trap = [Place]
59
type Cut = ([[Transition]], [Transition])
60

Philipp Meyer's avatar
Philipp Meyer committed
61
62
data PetriNet = PetriNet {
        name :: String,
63
64
        places :: [Place],
        transitions :: [Transition],
65
66
        adjacencyP :: M.Map Place ([(Transition,Integer)], [(Transition,Integer)]),
        adjacencyT :: M.Map Transition ([(Place,Integer)], [(Place,Integer)]),
67
68
        initialMarking :: Marking,
        ghostTransitions :: [Transition]
Philipp Meyer's avatar
Philipp Meyer committed
69
70
}

71
initial :: PetriNet -> Place -> Integer
72
initial net = val (initialMarking net)
73
74
75

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

77
78
linitials :: PetriNet -> [(Place,Integer)]
linitials = items . initialMarking
79

80
81
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
82
83
               (if null (name net) then "" else " " ++ show (name net))

Philipp Meyer's avatar
Philipp Meyer committed
84
instance Show PetriNet where
85
        show net = showNetName net ++
86
87
88
89
90
91
92
93
94
95
96
                   "\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

97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
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,
113
                initialMarking = emap (renamePlace f) $ initialMarking net,
114
115
116
117
                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)
118

119
120
121
122
123
124
-- TODO: use strongly connected components and min cuts
constructCut :: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net x traps =
        (nubOrd (map (sort . filter (\t -> val x t > 0) . mpre net) traps),
         nubOrd (concatMap (filter (\t -> val x t == 0) . mpost net) traps))

125
126
-- TODO: better constructors, only one main constructor
-- TODO: enforce sorted lists
127
128
129
makePetriNet :: String -> [String] -> [String] ->
        [(String, String, Integer)] ->
        [(String, Integer)] -> [String] -> PetriNet
130
makePetriNet name places transitions arcs initial gs =
131
132
133
134
135
136
137
138
        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,
139
                initialMarking = buildVector (map (first Place) initial),
140
141
                ghostTransitions = map Transition gs
            }
142
        where
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
            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"
158
159
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)

160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
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,
176
                initialMarking = buildVector initial,
177
178
179
                ghostTransitions = gs
            }

180
181
182
makePetriNetWithTrans :: String -> [String] ->
        [(String, [(String, Integer)], [(String, Integer)])] ->
        [(String, Integer)] -> [String] -> PetriNet
183
makePetriNetWithTrans name places ts initial gs =
Philipp Meyer's avatar
Philipp Meyer committed
184
185
186
        let transitions = [ t | (t,_,_) <- ts ]
            arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
                   [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
187
        in  makePetriNet name places transitions arcs initial gs