PetriNet.hs 9.52 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
     makePetriNet,makePetriNetWithTrans,
11
     makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Siphon,Cut,
12
     constructCut,SimpleCut,Invariant(..))
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
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

30
31
type SimpleCut = (S.Set Transition, [S.Set Transition])

32
33
type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])

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

60
61
type Marking = Vector Place
type FiringVector = Vector Transition
62

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

68
69
70
class Invariant a where
        invariantSize :: a -> Int

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

81
initial :: PetriNet -> Place -> Integer
82
initial net = val (initialMarking net)
83
84
85

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

87
88
linitials :: PetriNet -> [(Place,Integer)]
linitials = items . initialMarking
89

90
91
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
92
93
               (if null (name net) then "" else " " ++ show (name net))

Philipp Meyer's avatar
Philipp Meyer committed
94
instance Show PetriNet where
95
        show net = showNetName net ++
96
97
98
99
100
101
102
103
104
105
106
                   "\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
107
-- TODO: better cuts, scc, min cut?
108

109
constructCut :: PetriNet -> FiringVector -> [Trap] -> Cut
110
constructCut net _ traps = (trapComponents, trapOutputs)
111
        where trapComponent trap = (sort trap, sort (mpre net trap) \\ trapOutputs) :: ([Place], [Transition])
112
              trapComponents = listSet $ map trapComponent traps
Philipp Meyer's avatar
Philipp Meyer committed
113
              trapOutput trap = mpost net trap \\ mpre net trap
114
              trapOutputs = listSet $ concatMap trapOutput traps
115
{-
116
constructCut :: PetriNet -> FiringVector -> [Trap] -> Cut
117
118
119
constructCut net x _ = (map (\t -> ([],[t])) tPositive, tNegative)
        where tPositive = elems x
              tNegative = transitions net \\ tPositive
120
-}
Philipp Meyer's avatar
Philipp Meyer committed
121

122
123
124
125
126
127
128
129
130
131
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
132
133
134
135
                places      =
                    listSet $ map (renamePlace f) $ places net,
                transitions =
                    listSet $ map (renameTransition f) $ transitions net,
136
137
138
139
                adjacencyP  = mapAdjacency (renamePlace f) (renameTransition f) $
                    adjacencyP net,
                adjacencyT  = mapAdjacency (renameTransition f) (renamePlace f) $
                    adjacencyT net,
140
                initialMarking = emap (renamePlace f) $ initialMarking net,
Philipp Meyer's avatar
Philipp Meyer committed
141
142
                ghostTransitions =
                    listSet $ map (renameTransition f) $ ghostTransitions net
143
144
            }
        where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
Philipp Meyer's avatar
Philipp Meyer committed
145
146
              mapContext f (pre, post) =
                  (listMap (map (first f) pre), listMap (map (first f) post))
147

Philipp Meyer's avatar
Philipp Meyer committed
148
149
150
makePetriNet :: String -> [Place] -> [Transition] ->
        [Either (Transition, Place, Integer) (Place, Transition, Integer)] ->
        [(Place, Integer)] -> [Transition] -> PetriNet
151
makePetriNet name places transitions arcs initial gs =
Philipp Meyer's avatar
Philipp Meyer committed
152
            PetriNet {
153
                name = name,
Philipp Meyer's avatar
Philipp Meyer committed
154
155
156
157
158
159
                places = listSet places,
                transitions = listSet transitions,
                adjacencyP = M.map (listMap *** listMap) adP,
                adjacencyT = M.map (listMap *** listMap)adT,
                initialMarking = buildVector initial,
                ghostTransitions = listSet gs
160
            }
161
        where
Philipp Meyer's avatar
Philipp Meyer committed
162
163
164
165
            (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)) =
166
                       let mp' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
167
                                    p ([],[(t,w)]) mp
168
                           mt' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
169
                                    t ([(p,w)],[]) mt
170
                       in  (mp',mt')
Philipp Meyer's avatar
Philipp Meyer committed
171
            buildMaps (mp,mt) (Left (t,p,w)) =
172
                       let mt' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
173
                                    t ([],[(p,w)]) mt
174
                           mp' = M.insertWith addArc
Philipp Meyer's avatar
Philipp Meyer committed
175
                                    p ([(t,w)],[]) mp
176
                       in  (mp',mt')
177
178
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)

Philipp Meyer's avatar
Philipp Meyer committed
179
180
181
182
183
184
185
186
187
188
189
190
191
192
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
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
            toEitherArc (l,r,w) =
                let lp = l `S.member` placeSet
                    lt = l `S.member` transitionSet
                    rp = r `S.member` placeSet
                    rt = r `S.member` transitionSet
                in  case (lp,lt,rp,rt) of
                        (True,False,False,True) ->
                            Right (Place l, Transition r, w)
                        (False,True,True,False) ->
                            Left (Transition l, Place r, w)
                        (False,False,_,_) ->
                            error $ l ++ " not a declared place or transition "
                        (_,_,False,False) ->
                            error $ r ++ " not a declared place or transition "
                        (True,_,True,_) ->
                            error $ l ++ " and " ++ r ++ " both places"
                        (_,True,_,True) ->
                            error $ l ++ " and " ++ r ++ " both transitions"
Philipp Meyer's avatar
Philipp Meyer committed
211
212

makePetriNetWithTrans :: String -> [Place] ->
213
214
        [(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
        [(Place, Integer)] -> [Transition] -> PetriNet
Philipp Meyer's avatar
Philipp Meyer committed
215
216
217
218
219
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 ]
220

Philipp Meyer's avatar
Philipp Meyer committed
221
222
makePetriNetWithTransFromStrings :: String -> [String] ->
        [(String, ([(String, Integer)], [(String, Integer)]))] ->
223
        [(String, Integer)] -> [String] -> PetriNet
Philipp Meyer's avatar
Philipp Meyer committed
224
225
226
227
228
229
230
231
232
233
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))