PetriNet.hs 8.6 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,
Philipp Meyer's avatar
Philipp Meyer committed
10
11
     makePetriNet,makePetriNetWithTrans,
     makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Cut,
12
     constructCut)
Philipp Meyer's avatar
Philipp Meyer committed
13
14
where

15
import qualified Data.Map as M
Philipp Meyer's avatar
Philipp Meyer committed
16
import qualified Data.Set as S
17
import Control.Arrow (first,(***))
18
import Data.List (sort,(\\))
19

20
21
import Util

22
23
24
25
26
27
28
29
30
31
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)])

32
33
class (Ord a, Ord b) => Nodes a b | a -> b where
        lpre :: PetriNet -> a -> [(b, Integer)]
34
        lpre net = fst . context net
35
        lpost :: PetriNet -> a -> [(b, Integer)]
36
        lpost net = snd . context net
37
38
39
40
41
        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)]
Philipp Meyer's avatar
Philipp Meyer committed
42
        lmpre net = listMap . concatMap (lpre net)
43
        lmpost :: PetriNet -> [a] -> [(b, Integer)]
Philipp Meyer's avatar
Philipp Meyer committed
44
        lmpost net = listMap . concatMap (lpost net)
45
46
47
48
49
        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)])
50
51
52
53
54
55
56
57
        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

58
59
type Marking = Vector Place
type FiringVector = Vector Transition
60

Philipp Meyer's avatar
Philipp Meyer committed
61
type Trap = [Place]
62
63
-- TODO: generalize cut type
type Cut = ([([Place], [Transition])], [Transition])
64

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

75
initial :: PetriNet -> Place -> Integer
76
initial net = val (initialMarking net)
77
78
79

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

81
82
linitials :: PetriNet -> [(Place,Integer)]
linitials = items . initialMarking
83

84
85
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
86
87
               (if null (name net) then "" else " " ++ show (name net))

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

Philipp Meyer's avatar
Philipp Meyer committed
101
102
103
104
105
106
107
108
109
-- TODO: better cuts, scc, min cut?
constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net _ traps =
            uniqueCut (map trapComponent traps, concatMap trapOutput traps)
        where trapComponent trap =
                  (trap, mpre net trap)
              trapOutput trap = mpost net trap \\ mpre net trap
              uniqueCut (ts, u) = (listSet (map (sort *** sort) ts), listSet u)

110
111
112
113
114
115
116
117
118
119
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,
Philipp Meyer's avatar
Philipp Meyer committed
120
121
122
123
                places      =
                    listSet $ map (renamePlace f) $ places net,
                transitions =
                    listSet $ map (renameTransition f) $ transitions net,
124
125
126
127
                adjacencyP  = mapAdjacency (renamePlace f) (renameTransition f) $
                    adjacencyP net,
                adjacencyT  = mapAdjacency (renameTransition f) (renamePlace f) $
                    adjacencyT net,
128
                initialMarking = emap (renamePlace f) $ initialMarking net,
Philipp Meyer's avatar
Philipp Meyer committed
129
130
                ghostTransitions =
                    listSet $ map (renameTransition f) $ ghostTransitions net
131
132
            }
        where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
Philipp Meyer's avatar
Philipp Meyer committed
133
134
              mapContext f (pre, post) =
                  (listMap (map (first f) pre), listMap (map (first f) post))
135

Philipp Meyer's avatar
Philipp Meyer committed
136
137
138
makePetriNet :: String -> [Place] -> [Transition] ->
        [Either (Transition, Place, Integer) (Place, Transition, Integer)] ->
        [(Place, Integer)] -> [Transition] -> PetriNet
139
makePetriNet name places transitions arcs initial gs =
Philipp Meyer's avatar
Philipp Meyer committed
140
            PetriNet {
141
                name = name,
Philipp Meyer's avatar
Philipp Meyer committed
142
143
144
145
146
147
                places = listSet places,
                transitions = listSet transitions,
                adjacencyP = M.map (listMap *** listMap) adP,
                adjacencyT = M.map (listMap *** listMap)adT,
                initialMarking = buildVector initial,
                ghostTransitions = listSet gs
148
            }
149
        where
Philipp Meyer's avatar
Philipp Meyer committed
150
151
152
153
            (adP, adT) = foldl buildMaps (M.empty, M.empty) arcs
            buildMaps (mp,mt) (Left (_,_,0)) = (mp,mt)
            buildMaps (mp,mt) (Right (_,_,0)) = (mp,mt)
            buildMaps (mp,mt) (Right (p,t,w)) =
154
                       let mp' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
155
                                    p ([],[(t,w)]) mp
156
                           mt' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
157
                                    t ([(p,w)],[]) mt
158
                       in  (mp',mt')
Philipp Meyer's avatar
Philipp Meyer committed
159
            buildMaps (mp,mt) (Left (t,p,w)) =
160
                       let mt' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
161
                                    t ([],[(p,w)]) mt
162
                           mp' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
163
                                    p ([(t,w)],[]) mp
164
                       in  (mp',mt')
165
166
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)

Philipp Meyer's avatar
Philipp Meyer committed
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
makePetriNetFromStrings :: String -> [String] -> [String] ->
        [(String, String, Integer)] ->
        [(String, Integer)] -> [String] -> PetriNet
makePetriNetFromStrings name places transitions arcs initial gs =
            makePetriNet
                name
                (map Place (S.toAscList placeSet))
                (map Transition (S.toAscList transitionSet))
                (map toEitherArc arcs)
                (map (first Place) initial)
                (map Transition gs)
        where
            placeSet = S.fromList places
            transitionSet = S.fromList transitions
            toEitherArc (l,r,w)
                | l `S.member` placeSet && r `S.member` transitionSet =
                        Right (Place l, Transition r, w)
            toEitherArc (l,r,w)
                | l `S.member` transitionSet && r `S.member` placeSet =
                        Left (Transition l, Place r, w)
            toEitherArc (l,r,_) = error $ "nodes " ++ l ++ " and " ++ r ++
                                                " both places or transitions"

makePetriNetWithTrans :: String -> [Place] ->
191
192
        [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
        [(Place, Integer)] -> [Transition] -> PetriNet
Philipp Meyer's avatar
Philipp Meyer committed
193
194
195
196
197
makePetriNetWithTrans name places ts =
            makePetriNet name places (map fst ts) arcs
        where
            arcs = [ Right (p,t,w) | (t,(is,_)) <- ts, (p,w) <- is ] ++
                   [ Left  (t,p,w) | (t,(_,os)) <- ts, (p,w) <- os ]
198

Philipp Meyer's avatar
Philipp Meyer committed
199
200
makePetriNetWithTransFromStrings :: String -> [String] ->
        [(String, ([(String, Integer)], [(String, Integer)]))] ->
201
        [(String, Integer)] -> [String] -> PetriNet
Philipp Meyer's avatar
Philipp Meyer committed
202
203
204
205
206
207
208
209
210
211
makePetriNetWithTransFromStrings name places arcs initial gs =
            makePetriNetWithTrans
                name
                (map Place places)
                (map toTArc arcs)
                (map (first Place) initial)
                (map Transition gs)
        where
            toTArc (t, (is, os)) =
                (Transition t, (map (first Place) is, map (first Place) os))