PetriNet.hs 3.71 KB
Newer Older
Philipp Meyer's avatar
Philipp Meyer committed
1
2
3
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

module PetriNet
4
5
    (Marking,tokens,buildMarking,
     PetriNet,name,showNetName,places,transitions,initial,initialMarking,
6
     pre,lpre,post,lpost,initials,context,arcs,ghostTransitions,
Philipp Meyer's avatar
Philipp Meyer committed
7
     makePetriNet,makePetriNetWithTrans)
Philipp Meyer's avatar
Philipp Meyer committed
8
9
where

10
11
import qualified Data.Map as M

12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
type Place = String
type Transition = String
type Node = String
newtype Marking = Marking { getMarkingMap :: M.Map Place Integer }

instance Show Marking where
        show (Marking m) = unwords $ map showPlaceMarking $ M.toList m
            where showPlaceMarking (n,i) =
                    n ++ (if i /= 1 then "[" ++ show i ++ "]" else "")

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

buildMarking :: [(Place, Integer)] -> Marking
buildMarking xs = Marking $ M.fromList $ filter ((/=0) . snd) xs

Philipp Meyer's avatar
Philipp Meyer committed
28
29
data PetriNet = PetriNet {
        name :: String,
30
31
32
33
34
        places :: [Place],
        transitions :: [Transition],
        adjacency :: M.Map Node ([(Node,Integer)], [(Node,Integer)]),
        initialMarking :: Marking,
        ghostTransitions :: [Transition]
Philipp Meyer's avatar
Philipp Meyer committed
35
36
}

37
38
initial :: PetriNet -> Place -> Integer
initial net = tokens (initialMarking net)
39

40
arcs :: PetriNet -> [(Node, Node, Integer)]
41
42
43
arcs net = concatMap (\(a,(_,bs)) -> map (\(b,w) -> (a,b,w)) bs)
                           (M.toList (adjacency net))

44
context :: PetriNet -> Node -> ([(Node, Integer)], [(Node, Integer)])
45
46
context net x = M.findWithDefault ([],[]) x (adjacency net)

47
pre :: PetriNet -> Node -> [Node]
48
49
pre net = map fst . fst . context net

50
lpre :: PetriNet -> Node -> [(Node, Integer)]
51
52
lpre net = fst . context net

53
post :: PetriNet -> Node -> [Node]
54
55
post net = map fst . snd . context net

56
lpost :: PetriNet -> Node -> [(Node, Integer)]
57
58
lpost net = snd . context net

59
60
initials :: PetriNet -> [(Place,Integer)]
initials net = M.toList (getMarkingMap (initialMarking net))
61

62
63
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
64
65
               (if null (name net) then "" else " " ++ show (name net))

Philipp Meyer's avatar
Philipp Meyer committed
66
instance Show PetriNet where
67
        show net = showNetName net ++
68
69
70
                   "\nPlaces: " ++ unwords (places net) ++
                   "\nTransitions: " ++ unwords (transitions net) ++
                   "\nArcs:\n" ++ unlines
71
72
73
                        (map (\(s,(l,r)) -> show l ++ " -> " ++
                            s ++ " -> " ++ show r)
                        (M.toList (adjacency net))) ++
74
                   "Initial: " ++ show (initialMarking net) ++
75
                   "\nGhost transitions: " ++ unwords (ghostTransitions net)
Philipp Meyer's avatar
Philipp Meyer committed
76

77
78
makePetriNet :: String -> [Place] -> [Transition] ->
        [(Node, Node, Integer)] -> [(Place, Integer)] -> [Transition] -> PetriNet
79
80
makePetriNet name places transitions arcs initial gs =
        let adjacency = foldl buildMap M.empty $ filter (\(_,_,w) -> w /= 0) arcs
81
        in  PetriNet { name=name, places=places, transitions=transitions,
82
                       adjacency=adjacency, initialMarking=buildMarking initial,
83
                       ghostTransitions=gs }
84
85
86
87
88
89
90
        where
            buildMap m (l,r,w) =
              let m'  = M.insertWith addArc l ([],[(r,w)]) m
                  m'' = M.insertWith addArc r ([(l,w)],[]) m'
              in  m''
            addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)

91
92
93
makePetriNetWithTrans :: String -> [Place] ->
        [(Transition, [(Place, Integer)], [(Place, Integer)])] ->
        [(Place, Integer)] -> [Transition] -> PetriNet
94
makePetriNetWithTrans name places ts initial gs =
Philipp Meyer's avatar
Philipp Meyer committed
95
96
97
        let transitions = [ t | (t,_,_) <- ts ]
            arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
                   [ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
98
        in  makePetriNet name places transitions arcs initial gs