Skip to content
GitLab
Commit 4d7802a2 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Rewrote Petri net constructors

parent ce23a5be
Hide whitespace changes
Inline Side-by-side
src/Main.hs
View file @ 4d7802a2
......@@ -365,7 +365,7 @@ transformNet (net, props) TerminationByReachability =
(Var (primePlace p) :-: Var p) Ge (Const 0))
(places net))
-- TODO: map existing liveness properties
in (makePetriNetWith (name net) ps ts is gs, prop : props)
in (makePetriNetWithTrans (name net) ps ts is gs, prop : props)
transformNet (net, props) ValidateIdentifiers =
(renamePetriNetPlacesAndTransitions validateId net,
map (renameProperty validateId) props)
......@@ -439,19 +439,23 @@ checkSafetyProperty verbosity net refine invariant f = do
(Nothing, traps) ->
if invariant then do
r' <- checkSat verbosity $ checkSafetyInvariantSat net f traps
case r' of
Nothing -> do
verbosePut verbosity 0 "No invariant found"
return Unknown
Just inv -> do
verbosePut verbosity 0 "Invariant found"
mapM_ print inv
return Satisfied
printInvariant verbosity r'
else
return Satisfied
(Just _, _) ->
return Unknown
printInvariant :: (Show a) => Int -> Maybe [a] -> IO PropResult
printInvariant verbosity invResult =
case invResult of
Nothing -> do
verbosePut verbosity 0 "No invariant found"
return Unknown
Just inv -> do
verbosePut verbosity 0 "Invariant found"
mapM_ print inv
return Satisfied
checkSafetyProperty' :: Int -> PetriNet -> Bool ->
Formula Place -> [Trap] -> IO (Maybe Marking, [Trap])
checkSafetyProperty' verbosity net refine f traps = do
......@@ -482,14 +486,7 @@ checkLivenessProperty verbosity net refine invariant f = do
(Nothing, cuts) ->
if invariant then do
r' <- checkSat verbosity $ checkLivenessInvariantSat net f cuts
case r' of
Nothing -> do
verbosePut verbosity 0 "No invariant found"
return Unknown
Just inv -> do
verbosePut verbosity 0 "Invariant found"
mapM_ print inv
return Satisfied
printInvariant verbosity r'
else
return Satisfied
(Just _, _) ->
......
src/Parser/LOLA.hs
View file @ 4d7802a2
......@@ -10,7 +10,7 @@ import qualified Text.Parsec.Token as Token
import Parser
import Parser.LOLAFormula
import PetriNet (PetriNet,makePetriNetWithTrans)
import PetriNet (PetriNet,makePetriNetWithTransFromStrings)
import Property
languageDef :: LanguageDef ()
......@@ -57,7 +57,7 @@ net = do
initial <- option [] markingList
_ <- semi
ts <- many1 transition
return $ makePetriNetWithTrans "" ps ts initial []
return $ makePetriNetWithTransFromStrings "" ps ts initial []
placeLists :: Parser [String]
placeLists =
......@@ -80,7 +80,7 @@ marking = do
i <- option 1 (colon *> integer)
return (s, i)
transition :: Parser (String, [(String, Integer)], [(String, Integer)])
transition :: Parser (String, ([(String, Integer)], [(String, Integer)]))
transition = do
reserved "TRANSITION"
t <- ident
......@@ -92,7 +92,7 @@ transition = do
reserved "PRODUCE"
output <- option [] arcList
_ <- semi
return (t, input, output)
return (t, (input, output))
arcList :: Parser [(String, Integer)]
arcList = commaSep1 arc
......
src/Parser/MIST.hs
View file @ 4d7802a2
......@@ -12,7 +12,7 @@ import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
import PetriNet (PetriNet,makePetriNetWithTrans,Place(..))
import PetriNet (PetriNet,makePetriNetWithTransFromStrings,Place(..))
import Property
languageDef :: LanguageDef ()
......@@ -57,8 +57,8 @@ net = do
ts <- transitions
reserved "init"
(is,initTrans) <- initial
return $ makePetriNetWithTrans "" ps (initTrans ++ ts) is
[t | (t,_,_) <- initTrans]
return $ makePetriNetWithTransFromStrings "" ps (initTrans ++ ts) is
(map fst initTrans)
prop :: Parser Property
prop = do
......@@ -75,10 +75,10 @@ ineq = do
c <- integer
return $ LinearInequation (Var (Place x)) Ge (Const c)
transitions :: Parser [(String, [(String, Integer)], [(String, Integer)])]
transitions :: Parser [(String, ([(String, Integer)], [(String, Integer)]))]
transitions = do
ts <- many1 transition
return $ map (\(i,(l,r)) -> ("'t" ++ show i,l,r))
return $ map (\(i,(l,r)) -> ("'t" ++ show i,(l,r)))
([(1::Integer)..] `zip` ts)
transition :: Parser ([(String, Integer)], [(String, Integer)])
......@@ -105,12 +105,12 @@ transitionAssignment = do
return (i2,fac*n)
initial :: Parser ([(String, Integer)],
[(String, [(String, Integer)], [(String, Integer)])])
[(String, ([(String, Integer)], [(String, Integer)]))])
initial = do
xs <- commaSep1 initState
let inits = [(x,i) | (x,i,_) <- xs]
let covered = [x | (x,_,True) <- xs]
let initTrans = map (\(i,x) -> ("'init" ++ show i, [], [(x,1)]))
let initTrans = map (\(i,x) -> ("'init" ++ show i, ([], [(x,1)])))
([(1::Integer)..] `zip` covered)
return (inits, initTrans)
......
src/Parser/PNET.hs
View file @ 4d7802a2
......@@ -10,7 +10,7 @@ import Text.Parsec.Language (LanguageDef, emptyDef)
import qualified Text.Parsec.Token as Token
import Parser
import PetriNet (PetriNet,makePetriNet,Place(..),Transition(..))
import PetriNet (PetriNet,makePetriNetFromStrings,Place(..),Transition(..))
import Property
languageDef :: LanguageDef ()
......@@ -116,7 +116,7 @@ petriNet = do
name <- option "" ident
statements <- braces (many statement)
let (p,t,a,i) = foldl splitStatement ([],[],[],[]) statements
return $ makePetriNet name p t a i []
return $ makePetriNetFromStrings name p t a i []
where
splitStatement (ps,ts,as,is) stmnt = case stmnt of
Places p -> (p ++ ps,ts,as,is)
......
src/Parser/TPN.hs
View file @ 4d7802a2
......@@ -10,7 +10,7 @@ import qualified Text.Parsec.Token as Token
import Data.List (group,sort,genericLength)
import Parser
import PetriNet (PetriNet,makePetriNetWithTrans)
import PetriNet (PetriNet,makePetriNetWithTransFromStrings)
import Property
languageDef :: LanguageDef ()
......@@ -61,7 +61,7 @@ adjacencyList = do
xs <- many1 ident
return $ map (head &&& genericLength) $ group $ sort xs
transition :: Parser (String, [(String, Integer)], [(String, Integer)])
transition :: Parser (String, ([(String, Integer)], [(String, Integer)]))
transition = do
reserved "trans"
t <- ident
......@@ -69,7 +69,7 @@ transition = do
input <- option [] (reserved "in" *> adjacencyList)
output <- option [] (reserved "out" *> adjacencyList)
_ <- semi
return (t, input, output)
return (t, (input, output))
petriNet :: Parser PetriNet
petriNet = do
......@@ -77,7 +77,7 @@ petriNet = do
ts <- many transition
let places = [ p | (p,_) <- ps ]
initial = [ (p,i) | (p,Just i) <- ps ]
return $ makePetriNetWithTrans "" places ts initial []
return $ makePetriNetWithTransFromStrings "" places ts initial []
parseContent :: Parser (PetriNet,[Property])
parseContent = do
......
src/PetriNet.hs
View file @ 4d7802a2
......@@ -7,11 +7,13 @@ module PetriNet
name,showNetName,places,transitions,
initialMarking,initial,initials,linitials,
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut,
makePetriNet,makePetriNetWithTrans,
makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Cut,
constructCut)
where
import qualified Data.Map as M
import qualified Data.Set as S
import Control.Arrow (first,(***))
import Data.List (sort,(\\))
......@@ -27,7 +29,6 @@ instance Show Transition where
type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])
-- TODO: Use Map/Set for pre/post
class (Ord a, Ord b) => Nodes a b | a -> b where
lpre :: PetriNet -> a -> [(b, Integer)]
lpre net = fst . context net
......@@ -38,9 +39,9 @@ class (Ord a, Ord b) => Nodes a b | a -> b where
post :: PetriNet -> a -> [b]
post net = map fst . lpost net
lmpre :: PetriNet -> [a] -> [(b, Integer)]
lmpre net = nubOrdBy fst . concatMap (lpre net)
lmpre net = listMap . concatMap (lpre net)
lmpost :: PetriNet -> [a] -> [(b, Integer)]
lmpost net = nubOrdBy fst . concatMap (lpost net)
lmpost net = listMap . concatMap (lpost net)
mpre :: PetriNet -> [a] -> [b]
mpre net = map fst . lmpre net
mpost :: PetriNet -> [a] -> [b]
......@@ -97,6 +98,15 @@ instance Show PetriNet where
where showContext (s,(l,r)) =
show l ++ " -> " ++ show s ++ " -> " ++ show r
-- 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)
renamePlace :: (String -> String) -> Place -> Place
renamePlace f (Place p) = Place (f p)
......@@ -107,87 +117,95 @@ renamePetriNetPlacesAndTransitions :: (String -> String) -> PetriNet -> PetriNet
renamePetriNetPlacesAndTransitions f net =
PetriNet {
name = name net,
places = map (renamePlace f) $ places net,
transitions = map (renameTransition f) $ transitions net,
places =
listSet $ map (renamePlace f) $ places net,
transitions =
listSet $ map (renameTransition f) $ transitions net,
adjacencyP = mapAdjacency (renamePlace f) (renameTransition f) $
adjacencyP net,
adjacencyT = mapAdjacency (renameTransition f) (renamePlace f) $
adjacencyT net,
initialMarking = emap (renamePlace f) $ initialMarking net,
ghostTransitions = map (renameTransition f) $ ghostTransitions net
ghostTransitions =
listSet $ 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)
-- 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) = (nubOrd (map (sort *** sort) ts), nubOrd u)
mapContext f (pre, post) =
(listMap (map (first f) pre), listMap (map (first f) post))
-- TODO: better constructors, only one main constructor
-- TODO: enforce sorted lists
makePetriNet :: String -> [String] -> [String] ->
[(String, String, Integer)] ->
[(String, Integer)] -> [String] -> PetriNet
makePetriNet :: String -> [Place] -> [Transition] ->
[Either (Transition, Place, Integer) (Place, Transition, Integer)] ->
[(Place, Integer)] -> [Transition] -> PetriNet
makePetriNet name places transitions arcs initial gs =
let (adP, adT) = foldl buildMaps (M.empty, M.empty)
(filter (\(_,_,w) -> w /= 0) arcs)
in PetriNet {
PetriNet {
name = name,
places = map Place places,
transitions = map Transition transitions,
adjacencyP = adP,
adjacencyT = adT,
initialMarking = buildVector (map (first Place) initial),
ghostTransitions = map Transition gs
places = listSet places,
transitions = listSet transitions,
adjacencyP = M.map (listMap *** listMap) adP,
adjacencyT = M.map (listMap *** listMap)adT,
initialMarking = buildVector initial,
ghostTransitions = listSet gs
}
where
buildMaps (mp,mt) (_,_,0) = (mp,mt)
buildMaps (mp,mt) (l,r,w) | l `elem` places && r `elem` transitions =
(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)) =
let mp' = M.insertWith addArc
(Place l) ([],[(Transition r, w)]) mp
p ([],[(t,w)]) mp
mt' = M.insertWith addArc
(Transition r) ([(Place l, w)],[]) mt
t ([(p,w)],[]) mt
in (mp',mt')
buildMaps (mp,mt) (l,r,w) | l `elem` transitions && r `elem` places =
buildMaps (mp,mt) (Left (t,p,w)) =
let mt' = M.insertWith addArc
(Transition l) ([],[(Place r, w)]) mt
t ([],[(p,w)]) mt
mp' = M.insertWith addArc
(Place r) ([(Transition l, w)],[]) mp
p ([(t,w)],[]) mp
in (mp',mt')
buildMaps _ (l,r,_) = error $ "nodes " ++ l ++ " and " ++ r ++
" both places or transitions"
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
makePetriNetWith :: String -> [Place] ->
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] ->
[(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,
initialMarking = buildVector initial,
ghostTransitions = gs
}
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 ]
makePetriNetWithTrans :: String -> [String] ->
[(String, [(String, Integer)], [(String, Integer)])] ->
makePetriNetWithTransFromStrings :: String -> [String] ->
[(String, ([(String, Integer)], [(String, Integer)]))] ->
[(String, Integer)] -> [String] -> PetriNet
makePetriNetWithTrans name places ts initial gs =
let transitions = [ t | (t,_,_) <- ts ]
arcs = [ (i,t,w) | (t,is,_) <- ts, (i,w) <- is ] ++
[ (t,o,w) | (t,_,os) <- ts, (o,w) <- os ]
in makePetriNet name places transitions arcs initial gs
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))
src/Util.hs
View file @ 4d7802a2
......@@ -2,7 +2,7 @@
module Util
(verbosePut,elems,items,emap,prime,numPref,
nubOrd,nubOrdBy,val,vals,mval,zeroVal,positiveVal,sumVal,
listSet,listMap,val,vals,mval,zeroVal,positiveVal,sumVal,
makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
Vector,Model,VarMap,SIMap,SBMap,IMap,BMap,showWeighted)
where
......@@ -85,11 +85,12 @@ makeVector = Vector . M.filter (/=0)
- List functions
-}
nubOrd :: (Ord a) => [a] -> [a]
nubOrd = nubOrdBy id
listSet :: (Ord a) => [a] -> [a]
listSet = map head . group . sort
nubOrdBy :: (Ord b) => (a -> b) -> [a] -> [a]
nubOrdBy f = map head . groupBy ((==) `on` f) . sortBy (comparing f)
listMap :: (Ord a, Num b) => [(a,b)] -> [(a,b)]
listMap = map (foldl1 (\(x1,y1) (_,y2) -> (x1,y1 + y2))) .
groupBy ((==) `on` fst) . sortBy (comparing fst)
{-
- TODO: IO wrapper with options
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment