Commit d491c666 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Removed implicit properties no deadlock unless and workflow

parent dcd33cf2
...@@ -25,10 +25,8 @@ import Solver.SComponent ...@@ -25,10 +25,8 @@ import Solver.SComponent
data InputFormat = PNET | LOLA | TPN deriving (Show,Read) data InputFormat = PNET | LOLA | TPN deriving (Show,Read)
data ImplicitProperty = Termination data ImplicitProperty = Termination
| NoDeadlock | NoDeadlockUnless String | NoDeadlock | NoDeadlockUnlessFinal
| NoDeadlockUnlessFinal
| ProperTermination | ProperTermination
| Workflow
| Safe | Bounded Integer | Safe | Bounded Integer
deriving (Show,Read) deriving (Show,Read)
...@@ -63,12 +61,6 @@ options = ...@@ -63,12 +61,6 @@ options =
(NoArg (\opt -> Right opt { inputFormat = TPN })) (NoArg (\opt -> Right opt { inputFormat = TPN }))
"Use the tpn input format" "Use the tpn input format"
, Option "" ["workflow"]
(NoArg (\opt -> Right opt {
optProperties = Workflow : optProperties opt
}))
"Check that the net is a workflow net"
, Option "" ["termination"] , Option "" ["termination"]
(NoArg (\opt -> Right opt { (NoArg (\opt -> Right opt {
optProperties = Termination : optProperties opt optProperties = Termination : optProperties opt
...@@ -94,14 +86,6 @@ options = ...@@ -94,14 +86,6 @@ options =
("Prove that there is no deadlock unless\n" ++ ("Prove that there is no deadlock unless\n" ++
"only final places are marked") "only final places are marked")
, Option "" ["no-deadlock-unless"]
(ReqArg (\arg opt -> Right opt {
optProperties = NoDeadlockUnless arg : optProperties opt
})
"FILE")
("Prove that there is no deadlock unless\n" ++
"the formula given in FILE is satisfied")
, Option "" ["safe"] , Option "" ["safe"]
(NoArg (\opt -> Right opt { (NoArg (\opt -> Right opt {
optProperties = Safe : optProperties opt optProperties = Safe : optProperties opt
...@@ -159,7 +143,7 @@ checkFile parser verbosity refine implicitProperties file = do ...@@ -159,7 +143,7 @@ checkFile parser verbosity refine implicitProperties file = do
verbosePut verbosity 2 $ verbosePut verbosity 2 $
"Places: " ++ show (length $ places net) ++ "\n" ++ "Places: " ++ show (length $ places net) ++ "\n" ++
"Transitions: " ++ show (length $ transitions net) "Transitions: " ++ show (length $ transitions net)
addedProperties <- mapM (makeImplicitProperty net) implicitProperties let addedProperties = map (makeImplicitProperty net) implicitProperties
rs <- mapM (checkProperty verbosity net refine) rs <- mapM (checkProperty verbosity net refine)
(addedProperties ++ properties) (addedProperties ++ properties)
verbosePut verbosity 0 "" verbosePut verbosity 0 ""
...@@ -168,47 +152,33 @@ checkFile parser verbosity refine implicitProperties file = do ...@@ -168,47 +152,33 @@ checkFile parser verbosity refine implicitProperties file = do
placeOp :: Op -> (String, Integer) -> Formula placeOp :: Op -> (String, Integer) -> Formula
placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w) placeOp op (p,w) = Atom $ LinIneq (Var p) op (Const w)
makeImplicitProperty :: PetriNet -> ImplicitProperty -> IO Property makeImplicitProperty :: PetriNet -> ImplicitProperty -> Property
makeImplicitProperty net Workflow = do
let sources = filter (null . lpre net) (places net)
let sinks = filter (null . lpost net) (places net)
putStrLn "Sources:"
print sources
putStrLn "Sinks:"
print sinks
return $ Property "workflow" Safety $
if length sources == 1 && length sinks == 1 then FFalse else FTrue
makeImplicitProperty _ Termination = makeImplicitProperty _ Termination =
return $ Property "termination" Liveness FTrue Property "termination" Liveness FTrue
makeImplicitProperty net ProperTermination = do makeImplicitProperty net ProperTermination =
let (finals, nonfinals) = partition (null . lpost net) (places net) let (finals, nonfinals) = partition (null . lpost net) (places net)
return $ Property "proper termination" Safety in Property "proper termination" Safety
(foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&: (foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) finals) :&:
foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals))
makeImplicitProperty net NoDeadlock = makeImplicitProperty net NoDeadlock =
return $ Property "no deadlock" Safety $ Property "no deadlock" Safety $
foldl (:&:) FTrue foldl (:&:) FTrue
(map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net) (map (foldl (:|:) FFalse . map (placeOp Lt) . lpre net)
(transitions net)) (transitions net))
makeImplicitProperty net NoDeadlockUnlessFinal = do makeImplicitProperty net NoDeadlockUnlessFinal =
nodeadlock <- makeImplicitProperty net NoDeadlock let nodeadlock = makeImplicitProperty net NoDeadlock
let (finals, nonfinals) = partition (null . lpost net) (places net) (finals, nonfinals) = partition (null . lpost net) (places net)
return $ Property "no deadlock unless final" Safety $ in Property "no deadlock unless final" Safety $
(foldl (:&:) FTrue (map (\p -> placeOp Eq (p,0)) finals) :|: (foldl (:&:) FTrue (map (\p -> placeOp Eq (p,0)) finals) :|:
foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&: foldl (:|:) FFalse (map (\p -> placeOp Gt (p,0)) nonfinals)) :&:
pformula nodeadlock pformula nodeadlock
makeImplicitProperty net (NoDeadlockUnless file) = do
nodeadlock <- makeImplicitProperty net NoDeadlock
property <- parseFile LOLA.parseFormula file
return $ Property "no deadlock unless" Safety $
Neg property :&: pformula nodeadlock
makeImplicitProperty net (Bounded k) = makeImplicitProperty net (Bounded k) =
return $ Property (show k ++ "-bounded") Safety $ Property (show k ++ "-bounded") Safety $
foldl (:|:) FFalse foldl (:|:) FFalse
(map (\p -> placeOp Gt (p,k)) (places net)) (map (\p -> placeOp Gt (p,k)) (places net))
makeImplicitProperty net Safe = do makeImplicitProperty net Safe =
bounded <- makeImplicitProperty net (Bounded 1) let bounded = makeImplicitProperty net (Bounded 1)
return $ Property "safe" Safety $ pformula bounded in Property "safe" Safety $ pformula bounded
checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool checkProperty :: Int -> PetriNet -> Bool -> Property -> IO Bool
checkProperty verbosity net refine p = do checkProperty verbosity net refine p = do
......
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