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

Added non-negativity constraints

parent 44774004
......@@ -39,6 +39,12 @@ evaluateFormula m (p :|: q) = do
r2 <- evaluateFormula m q
return $ r1 ||| r2
checkNonnegativityConstraints :: Model -> PetriNet -> Symbolic SBool
checkNonnegativityConstraints m net = do
pts <- mapM checkPT $ places net ++ transitions net
return $ bAnd pts
where checkPT x = return $ (m M.! x) .>= 0
checkPlaceEquation :: Model -> PetriNet -> String -> Symbolic SBool
checkPlaceEquation m net p = do
incoming <- mapM addTransition $ lpre net p
......@@ -76,8 +82,9 @@ checkConstraints net p = do
r1 <- case ptype p of
Safety -> checkStateConstraints model net
Liveness -> checkTInvariantConstraints model net
r2 <- evaluateFormula model (pformula p)
return $ r1 &&& r2
r2 <- checkNonnegativityConstraints model net
r3 <- evaluateFormula model (pformula p)
return $ r1 &&& r2 &&& r3
checkSat :: PetriNet -> Property -> IO (Maybe (M.Map String Integer))
checkSat net p = do
......
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