PetriNet.hs 7.78 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,tokens,buildMarking,
Philipp Meyer's avatar
Philipp Meyer committed
6
     marked,lmarked,makeMarking,
7
     renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
8
9
     name,showNetName,places,transitions,initial,initialMarking,
     pre,lpre,post,lpost,initials,context,ghostTransitions,
Philipp Meyer's avatar
Philipp Meyer committed
10
     makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap)
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
45
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

newtype Marking = Marking { getMarking :: M.Map Place Integer }
46
47

instance Show Marking where
Philipp Meyer's avatar
Philipp Meyer committed
48
49
        show (Marking m) =
                "[" ++ intercalate "," (map showPlaceMarking (M.toList m)) ++ "]"
50
            where showPlaceMarking (n,i) =
51
                    show n ++ (if i /= 1 then "(" ++ show i ++ ")" else "")
52
53

tokens :: Marking -> Place -> Integer
54
tokens m p = M.findWithDefault 0 p (getMarking m)
55

Philipp Meyer's avatar
Philipp Meyer committed
56
57
58
59
60
61
62
63
64
65
66
67
68
buildMarking :: [(Place, Integer)] -> Marking
buildMarking = makeMarking . M.fromList

makeMarking :: M.Map Place Integer -> Marking
makeMarking = Marking . M.filter (/=0)

marked :: Marking -> [Place]
marked = M.keys . getMarking

lmarked :: Marking -> [(Place,Integer)]
lmarked = M.toList . getMarking

type Trap = [Place]
69

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

80
81
initial :: PetriNet -> Place -> Integer
initial net = tokens (initialMarking net)
82

83
initials :: PetriNet -> [(Place,Integer)]
84
initials net = M.toList (getMarking (initialMarking net))
85

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

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

103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
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,
                initialMarking = Marking $
                    M.mapKeys (renamePlace f) $ getMarking $ initialMarking net,
                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)
125
126
127
128

makePetriNet :: String -> [String] -> [String] ->
        [(String, String, Integer)] ->
        [(String, Integer)] -> [String] -> PetriNet
129
makePetriNet name places transitions arcs initial gs =
130
131
132
133
134
135
136
137
        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,
Philipp Meyer's avatar
Philipp Meyer committed
138
                initialMarking = buildMarking (map (first Place) initial),
139
140
                ghostTransitions = map Transition gs
            }
141
        where
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
            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"
157
158
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)

159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
-- 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,
Philipp Meyer's avatar
Philipp Meyer committed
176
                initialMarking = buildMarking 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