Commit 93e8965f authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Refactoring of solvers and main structure

parent 2dd17b45
......@@ -6,39 +6,77 @@ import Parser (parseFile)
import PetriNet
import Property
import Solver
import Solver.StateEquation
import Solver.TransitionInvariant
import Solver.TrapConstraints
checkProperty :: PetriNet -> Property -> IO ()
checkProperty net p = do
r <- checkPropertyConstraintsSat net p []
case r of
Nothing -> putStrLn "Property satisfied"
Just m -> putStrLn "Property may not satisfied, model:" >> print m
-- TODO: check type of property and only do trap refinement for safety
-- properties
checkPropertyWithTrapRefinement :: PetriNet -> Property -> [[String]] -> IO ()
checkPropertyWithTrapRefinement net p traps = do
r <- checkPropertyConstraintsSat net p traps
checkSafetyProperty :: PetriNet -> Formula -> [[String]] -> IO Bool
checkSafetyProperty net f traps = do
r <- checkSat $ checkStateEquationSat net f traps
case r of
Nothing -> return True
Just a -> do
--print a
let assigned = markedPlacesFromAssignment net a
putStrLn $ "Assignment found marking " ++ show assigned
rt <- checkSat $ checkTrapSat net assigned
case rt of
Nothing -> do
putStrLn "No trap found."
return False
Just at -> do
let trap = trapFromAssignment at
putStrLn $ "Trap found with places " ++ show trap
checkSafetyProperty net f (trap:traps)
checkLivenessProperty :: PetriNet -> Formula -> IO Bool
checkLivenessProperty net f = do
r <- checkSat $ checkTransitionInvariantSat net f
case r of
Nothing -> putStrLn "Property satisfied"
Nothing -> return True
Just m -> do
putStrLn "Property not satisfied, model:" >> print m
r2 <- checkTrapConstraintsSat net m
case r2 of
Nothing -> putStrLn "No trap found"
Just m2 -> do
let trap = map fst $ filter snd m2
putStrLn "Trap found:" >> print trap
checkPropertyWithTrapRefinement net p (trap:traps)
putStrLn "Assignment found:"
print m
return False
checkProperty :: PetriNet -> Property -> IO Bool
checkProperty net p = do
r <- case ptype p of
Safety -> checkSafetyProperty net (pformula p) []
Liveness -> checkLivenessProperty net (pformula p)
putStrLn $ if r then "Property is satisfied."
else "Property may not be satisfied."
return r
--checkPropertyWithTrapRefinement :: PetriNet -> Property -> [[String]] -> IO ()
--checkPropertyWithTrapRefinement net p traps = do
-- r <- checkPropertyConstraintsSat net p traps
-- case r of
-- Nothing -> putStrLn "Property is satisfied"
-- Just m -> do
-- putStrLn "Property may not satisfied, model:" >> print m
-- r2 <- checkTrapConstraintsSat net m
-- case r2 of
-- Nothing -> putStrLn "No trap found"
-- Just m2 -> do
-- let trap = map fst $ filter snd m2
-- putStrLn "Trap found:" >> print trap
-- checkPropertyWithTrapRefinement net p (trap:traps)
main :: IO ()
main = do
args <- getArgs
let file = head args
putStrLn "Safety and Liveness Analysis of Petri Nets with SMT solvers"
putStrLn "SLAPnet - Safety and Liveness Analysis of Petri Nets with SMT solvers\n"
putStrLn $ "Reading \"" ++ file ++ "\""
(net,properties) <- parseFile file
putStrLn $ "Analyzing " ++ showName net
mapM_ (\p -> do
putStrLn $ "Checking " ++ show p
checkPropertyWithTrapRefinement net p []
putStrLn $ "\nChecking " ++ show p
checkProperty net p
) properties
module Solver
(checkSat,checkPropertyConstraintsSat,checkTrapConstraintsSat)
(checkSat,ModelSI,ModelSB,ModelI,ModelB)
where
import Data.SBV
import qualified Data.Map as M
import PetriNet
import Property
type ModelSI = M.Map String SInteger
type ModelSB = M.Map String SBool
type ModelI = M.Map String Integer
--type ModelB = M.Map String Bool
type ModelLI = [(String, Integer)]
type ModelLB = [(String, Bool)]
evaluateTerm :: ModelSI -> Term -> SInteger
evaluateTerm m (Term xs) = sum $ map evaluateLinAtom xs
where evaluateLinAtom (Var c x) = literal c * m M.! x
evaluateLinAtom (Const c) = literal c
opToFunction :: Op -> SInteger -> SInteger -> SBool
opToFunction Gt = (.>)
opToFunction Ge = (.>=)
opToFunction Eq = (.==)
opToFunction Le = (.<=)
opToFunction Lt = (.<)
evaluateLinIneq :: ModelSI -> LinearInequation -> SBool
evaluateLinIneq m (LinIneq lhs op rhs) =
opToFunction op (evaluateTerm m lhs) (evaluateTerm m rhs)
evaluateFormula :: ModelSI -> Formula -> SBool
evaluateFormula m (Atom a) = evaluateLinIneq m a
evaluateFormula m (Neg p) = bnot $ evaluateFormula m p
evaluateFormula m (p :&: q) = evaluateFormula m p &&& evaluateFormula m q
evaluateFormula m (p :|: q) = evaluateFormula m p ||| evaluateFormula m q
checkNonnegativityConstraints :: ModelSI -> PetriNet -> SBool
checkNonnegativityConstraints m net =
bAnd $ map checkPT $ places net ++ transitions net
where checkPT x = (m M.! x) .>= 0
checkPlaceEquation :: ModelSI -> PetriNet -> String -> SBool
checkPlaceEquation m net p =
let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p
pinit = literal $ initial net p
in pinit + sum incoming - sum outgoing .== (m M.! p)
where addTransition (t,w) = literal w * (m M.! t)
checkStateConstraints :: ModelSI -> PetriNet -> SBool
checkStateConstraints m net =
bAnd $ map (checkPlaceEquation m net) $ places net
checkTransitionEquation :: ModelSI -> PetriNet -> String -> SBool
checkTransitionEquation m net t =
let incoming = map addPlace $ lpre net t
outgoing = map addPlace $ lpost net t
in sum outgoing - sum incoming .>= 0
where addPlace (p,w) = literal w * (m M.! p)
type ModelB = M.Map String Bool
--type ModelLI = [(String, Integer)]
--type ModelLB = [(String, Bool)]
checkTInvariantConstraints :: ModelSI -> PetriNet -> SBool
checkTInvariantConstraints m net =
bAnd $ map (checkTransitionEquation m net) $ transitions net
checkTrapConstraints :: ModelSB -> PetriNet -> SBool
checkTrapConstraints m net =
bAnd $ map trapConstraint $ transitions net
where trapConstraint t =
bOr (map (m M.!) $ pre net t) ==> bOr (map (m M.!) $ post net t)
checkTrapMarked :: ModelSB -> PetriNet -> SBool
checkTrapMarked m net =
let marked = map fst $ filter (( > 0) . snd) $ initials net
in bOr $ map (m M.!) marked
checkTrapUnassigned :: ModelSB -> ModelI -> PetriNet -> SBool
checkTrapUnassigned mt ma net =
let assigned = filter (( > 0) . (ma M.!)) $ places net
in bAnd $ map (bnot . (mt M.!)) assigned
checkAllTrapConstraints :: ModelSB -> ModelI -> PetriNet -> SBool
checkAllTrapConstraints mt ma net =
let tc = checkTrapConstraints mt net
tm = checkTrapMarked mt net
tu = checkTrapUnassigned mt ma net
in tc &&& tm &&& tu
checkTrapDeltaConstraints :: ModelSI -> [String] -> SBool
checkTrapDeltaConstraints m trap =
let tokens = map (m M.!) trap
in sum tokens .>= 1
checkPropertyConstraints :: ModelSI -> PetriNet -> Property -> SBool
checkPropertyConstraints m net p =
let netConstraints = case ptype p of
Safety -> checkStateConstraints m net
Liveness -> checkTInvariantConstraints m net
nonnegativityConstraint = checkNonnegativityConstraints m net
propertyConstraint = evaluateFormula m (pformula p)
in netConstraints &&& nonnegativityConstraint &&& propertyConstraint
checkPropertyPlusTrapConstraints :: ModelSI -> PetriNet -> Property ->
[[String]] -> SBool
checkPropertyPlusTrapConstraints m net p traps =
let propConstraints = checkPropertyConstraints m net p
trapConstraints = map (checkTrapDeltaConstraints m) traps
in propConstraints &&& bAnd trapConstraints
symConstraints :: SymWord a => [String] -> ([(String, SBV a)] -> SBool) ->
symConstraints :: SymWord a => [String] -> (M.Map String (SBV a) -> SBool) ->
Symbolic SBool
symConstraints vars constraint = do
syms <- mapM exists vars
return $ constraint (vars `zip` syms)
return $ constraint $ M.fromList $ vars `zip` syms
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) -> Maybe [(String,a)]
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
Maybe (M.Map String a)
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ vars `zip` m
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m
checkSat :: (SatModel a, SymWord a) => [String] ->
([(String, SBV a)] -> SBool) -> IO (Maybe [(String,a)])
checkSat vars constraint = do
checkSat :: (SatModel a, SymWord a) =>
([String], M.Map String (SBV a) -> SBool) ->
IO (Maybe (M.Map String a))
checkSat (vars, constraint) = do
result <- sat $ symConstraints vars constraint
return $ rebuildModel vars $ getModel result
checkPropertyConstraintsSat :: PetriNet -> Property -> [[String]] -> IO (Maybe ModelLI)
checkPropertyConstraintsSat net p traps =
let vars = places net ++ transitions net
cons m = checkPropertyPlusTrapConstraints (M.fromList m) net p traps
in checkSat vars cons
checkTrapConstraintsSat :: PetriNet -> ModelLI -> IO (Maybe ModelLB)
checkTrapConstraintsSat net ma =
let vars = places net
cons m = checkAllTrapConstraints (M.fromList m) (M.fromList ma) net
in checkSat vars cons
-- TODO: separate place and transition variables
--checkPropertyConstraintsSat :: PetriNet -> Property -> [[String]] -> IO (Maybe ModelLI)
--checkPropertyConstraintsSat net p traps =
-- let vars = places net ++ transitions net
-- cons m = checkPropertyPlusTrapConstraints (M.fromList m) net p traps
-- in checkSat vars cons
--checkTrapConstraintsSat :: PetriNet -> ModelLI -> IO (Maybe ModelLB)
--checkTrapConstraintsSat net ma =
-- let vars = places net
-- cons m = checkAllTrapConstraints (M.fromList m) (M.fromList ma) net
-- in checkSat vars cons
module Solver.Formula
(evaluateFormula)
where
import Data.SBV
import qualified Data.Map as M
import Property
import Solver
evaluateTerm :: Term -> ModelSI -> SInteger
evaluateTerm (Term xs) m = sum $ map evaluateLinAtom xs
where evaluateLinAtom (Var c x) = literal c * m M.! x
evaluateLinAtom (Const c) = literal c
opToFunction :: Op -> SInteger -> SInteger -> SBool
opToFunction Gt = (.>)
opToFunction Ge = (.>=)
opToFunction Eq = (.==)
opToFunction Le = (.<=)
opToFunction Lt = (.<)
evaluateLinIneq :: LinearInequation -> ModelSI -> SBool
evaluateLinIneq (LinIneq lhs op rhs) m =
opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m)
evaluateFormula :: Formula -> ModelSI -> SBool
evaluateFormula (Atom a) m = evaluateLinIneq a m
evaluateFormula (Neg p) m = bnot $ evaluateFormula p m
evaluateFormula (p :&: q) m = evaluateFormula p m &&& evaluateFormula q m
evaluateFormula (p :|: q) m = evaluateFormula p m ||| evaluateFormula q m
module Solver.StateEquation
(checkStateEquation,checkStateEquationSat,
markedPlacesFromAssignment)
where
import Data.SBV
import qualified Data.Map as M
import PetriNet
import Property
import Solver
import Solver.Formula
placeConstraints :: PetriNet -> ModelSI -> SBool
placeConstraints net m =
bAnd $ map checkPlaceEquation $ places net
where checkPlaceEquation p =
let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p
pinit = literal $ initial net p
in pinit + sum incoming - sum outgoing .== (m M.! p)
addTransition (t,w) = literal w * (m M.! t)
nonnegativityConstraints :: PetriNet -> ModelSI -> SBool
nonnegativityConstraints net m =
bAnd $ map checkPT $ places net ++ transitions net
where checkPT x = (m M.! x) .>= 0
checkTraps :: [[String]] -> ModelSI -> SBool
checkTraps traps m =
bAnd $ map checkTrapDelta traps
where checkTrapDelta trap = sum (map (m M.!) trap) .>= 1
checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
checkStateEquation net f traps m =
placeConstraints net m &&&
nonnegativityConstraints net m &&&
checkTraps traps m &&&
evaluateFormula f m
checkStateEquationSat :: PetriNet -> Formula -> [[String]] ->
([String], ModelSI -> SBool)
checkStateEquationSat net f traps =
(places net ++ transitions net, checkStateEquation net f traps)
markedPlacesFromAssignment :: PetriNet -> ModelI -> [String]
markedPlacesFromAssignment net a = filter (( > 0) . (a M.!)) $ places net
module Solver.TransitionInvariant
(checkTransitionInvariant,checkTransitionInvariantSat)
where
import Data.SBV
import qualified Data.Map as M
import PetriNet
import Property
import Solver
import Solver.Formula
tInvariantConstraints :: PetriNet -> ModelSI -> SBool
tInvariantConstraints net m =
bAnd $ map checkTransitionEquation $ places net
where checkTransitionEquation p =
let incoming = map addPlace $ lpre net p
outgoing = map addPlace $ lpost net p
in sum outgoing - sum incoming .>= 0
addPlace (t,w) = literal w * (m M.! t)
nonnegativityConstraints :: PetriNet -> ModelSI -> SBool
nonnegativityConstraints net m =
bAnd $ map checkT $ transitions net
where checkT t = (m M.! t) .>= 0
checkTransitionInvariant :: PetriNet -> Formula -> ModelSI -> SBool
checkTransitionInvariant net f m =
tInvariantConstraints net m &&&
nonnegativityConstraints net m &&&
evaluateFormula f m
checkTransitionInvariantSat :: PetriNet -> Formula -> ([String], ModelSI -> SBool)
checkTransitionInvariantSat net f =
(transitions net, checkTransitionInvariant net f)
module Solver.TrapConstraints
(checkTrap,checkTrapSat,
trapFromAssignment
)
where
import Data.SBV
import qualified Data.Map as M
import PetriNet
import Solver
trapConstraints :: PetriNet -> ModelSB -> SBool
trapConstraints net m =
bAnd $ map trapConstraint $ transitions net
where trapConstraint t =
bOr (map (m M.!) $ pre net t) ==> bOr (map (m M.!) $ post net t)
trapInitiallyMarked :: PetriNet -> ModelSB -> SBool
trapInitiallyMarked net m =
let marked = map fst $ filter (( > 0) . snd) $ initials net
in bOr $ map (m M.!) marked
trapUnassigned :: [String] -> ModelSB -> SBool
trapUnassigned assigned m = bAnd $ map (bnot . (m M.!)) assigned
checkTrap :: PetriNet -> [String] -> ModelSB -> SBool
checkTrap net assigned m =
trapConstraints net m &&&
trapInitiallyMarked net m &&&
trapUnassigned assigned m
checkTrapSat :: PetriNet -> [String] -> ([String], ModelSB -> SBool)
checkTrapSat net assigned =
(places net, checkTrap net assigned)
trapFromAssignment :: ModelB -> [String]
trapFromAssignment a = M.keys $ M.filter id a
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