Commit d6b41fdc authored by Philipp Meyer's avatar Philipp Meyer

Fixed bug for the transition invariant constraints

parent 35a60e57
......@@ -51,7 +51,7 @@ checkLivenessProperty net f = do
checkProperty :: PetriNet -> Property -> IO Bool
checkProperty net p = do
--putStrLn $ "\nChecking " ++ showPropertyName p
putStrLn $ "\nChecking " ++ showPropertyName p
r <- case ptype p of
Safety -> checkSafetyProperty net (pformula p) []
Liveness -> checkLivenessProperty net (pformula p)
......
......@@ -68,10 +68,8 @@ data Property = Property {
instance Show Property where
show p =
show (ptype p) ++ " property " ++
(if null (pname p) then "" else show (pname p) ++ " ") ++
"{ " ++ show (pformula p) ++ " }"
showPropertyName p ++ " { " ++ show (pformula p) ++ " }"
showPropertyName :: Property -> String
showPropertyName p = "property" ++
showPropertyName p = show (ptype p) ++ " property" ++
(if null (pname p) then "" else " " ++ show (pname p))
......@@ -17,7 +17,7 @@ tInvariantConstraints net m =
where checkTransitionEquation p =
let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p
in sum outgoing - sum incoming .>= 0
in sum incoming - sum outgoing .>= 0
addTransition (t,w) = literal w * (m M.! t)
finalInvariantConstraints :: ModelSI -> SBool
......
Markdown is supported
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