Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

Commit 6a216738 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Changed to using Z3 API, first for state equation

parent c51c68df
......@@ -21,8 +21,8 @@ executable slapnet
main-is: Main.hs
other-modules:
-- other-extensions:
build-depends: base >=4 && <5, sbv, parsec, containers, transformers,
bytestring
build-depends: base >=4 && <5, parsec, containers, transformers,
bytestring, z3
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000
......@@ -24,9 +24,6 @@ import qualified Printer.SARA as SARAPrinter
import Property
import Solver
import Solver.StateEquation
import Solver.TrapConstraints
import Solver.TransitionInvariant
import Solver.SComponent
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
......@@ -292,7 +289,6 @@ checkProperty verbosity net refine p = do
verbosePut verbosity 3 $ show p
r <- case ptype p of
Safety -> checkSafetyProperty verbosity net refine (pformula p) []
Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
verbosePut verbosity 0 $ showPropertyName p ++
if r then " is satisfied."
else " may not be satisfied."
......@@ -301,7 +297,7 @@ checkProperty verbosity net refine p = do
checkSafetyProperty :: Int -> PetriNet -> Bool ->
Formula -> [[String]] -> IO Bool
checkSafetyProperty verbosity net refine f traps = do
r <- checkSat $ checkStateEquationSat net f traps
r <- checkSatInt $ checkStateEquationSat net f traps
case r of
Nothing -> return True
Just a -> do
......@@ -309,51 +305,7 @@ checkSafetyProperty verbosity net refine f traps = do
verbosePut verbosity 1 "Assignment found"
verbosePut verbosity 2 $ "Places marked: " ++ show assigned
verbosePut verbosity 3 $ "Assignment: " ++ show a
if refine then do
rt <- checkSat $ checkTrapSat net assigned
case rt of
Nothing -> do
verbosePut verbosity 1 "No trap found."
return False
Just at -> do
let trap = trapFromAssignment at
verbosePut verbosity 1 "Trap found"
verbosePut verbosity 2 $ "Places in trap: " ++
show trap
verbosePut verbosity 3 $ "Trap assignment: " ++
show at
checkSafetyProperty verbosity net refine f
(trap:traps)
else
return False
checkLivenessProperty :: Int -> PetriNet -> Bool ->
Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbosity net refine f strans = do
r <- checkSat $ checkTransitionInvariantSat net f strans
case r of
Nothing -> return True
Just ax -> do
let fired = firedTransitionsFromAssignment ax
verbosePut verbosity 1 "Assignment found"
verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
verbosePut verbosity 3 $ "Assignment: " ++ show ax
if refine then do
rt <- checkSat $ checkSComponentSat net fired ax
case rt of
Nothing -> do
verbosePut verbosity 1 "No S-component found"
return False
Just as -> do
let sOutIn = getSComponentOutIn net ax as
verbosePut verbosity 1 "S-component found"
verbosePut verbosity 2 $ "Out/In: " ++ show sOutIn
verbosePut verbosity 3 $ "S-Component assignment: " ++
show as
checkLivenessProperty verbosity net refine f
(sOutIn:strans)
else
return False
return False
main :: IO ()
main = do
......
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Solver
(checkSat,ModelSI,ModelSB,ModelI,ModelB,
Model(..),mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
(checkSat,checkSatInt,MModelS,MModelI,MModelB,
MModel(..),mVal,mValues,mElemsWith,mElemSum,CModel(..))
where
import Data.SBV
import Z3.Monad
import qualified Data.Map as M
import Control.Monad
newtype Model a = Model { getMap :: M.Map String a }
newtype MModel a = MModel { getMap :: M.Map String a }
instance Show a => Show (Model a) where
instance Show a => Show (MModel a) where
show = show . M.toList . getMap
type ModelSI = Model SInteger
type ModelSB = Model SBool
type ModelI = Model Integer
type ModelB = Model Bool
type MModelS = MModel AST
type MModelI = MModel Integer
type MModelB = MModel Bool
mVal :: Model a -> String -> a
class Z3Type a where
mkConcrete :: a -> Z3 AST
getConcrete :: AST -> Z3 a
instance Z3Type Integer where
mkConcrete = mkInt
getConcrete = getInt
mVal :: MModel a -> String -> a
mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x (getMap m)
mValues :: Model a -> [a]
mValues :: MModel a -> [a]
mValues m = M.elems $ getMap m
mElemsWith :: (a -> Bool) -> Model a -> [String]
mElemsWith :: (a -> Bool) -> MModel a -> [String]
mElemsWith f m = M.keys $ M.filter f $ getMap m
mElemSum :: (Num a) => Model a -> [String] -> a
mElemSum :: (Num a) => MModel a -> [String] -> a
mElemSum m xs = sum $ map (mVal m) xs
class SModel a where
mElem :: Model a -> String -> SBool
mNotElem :: Model a -> String -> SBool
mNotElem m x = bnot $ mElem m x
--class SMModel a where
-- mElem :: MModel a -> String -> Z3 AST
-- mNotElem :: MModel a -> String -> Z3 AST
-- mNotElem m x = mkNot =<< mElem m x
class CModel a where
cElem :: Model a -> String -> Bool
cNotElem :: Model a -> String -> Bool
cElem :: MModel a -> String -> Bool
cNotElem :: MModel a -> String -> Bool
cNotElem m x = not $ cElem m x
instance SModel SInteger where
mElem m x = mVal m x .> 0
mNotElem m x = mVal m x .== 0
instance SModel SBool where
mElem = mVal
mNotElem m x = bnot $ mVal m x
--instance SMModel AST where
-- mElem m x = (mVal m x `mkGt`) =<< mkInt 0
-- mNotElem m x = mkEq (mVal m x) =<< mkInt 0
--instance SMModel AST where
-- mElem = mVal
-- mNotElem m x = mkNot $ mVal m x
instance CModel Integer where
cElem m x = mVal m x > 0
cNotElem m x = mVal m x == 0
......@@ -52,21 +60,27 @@ instance CModel Bool where
cElem = mVal
cNotElem m x = not $ mVal m x
symConstraints :: SymWord a => [String] -> (Model (SBV a) -> SBool) ->
Symbolic SBool
symConstraints vars constraint = do
syms <- mapM exists vars
return $ constraint $ Model $ M.fromList $ vars `zip` syms
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
Maybe (Model a)
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ Model $ M.fromList $ vars `zip` m
checkSat :: Z3Type a => Z3 Sort -> ([String], MModel AST -> Z3 ()) ->
Z3 (Maybe (MModel a))
checkSat mkSort (vars, constraint) = do
sort <- mkSort
syms <- mapM (mkStringSymbol >=> flip mkConst sort) vars
let smodel = MModel $ M.fromList $ vars `zip` syms
constraint smodel
result <- getModel
case result of
(Unsat, Nothing) -> return Nothing
(Sat, Just m) -> do
ms <- evalT m syms
case ms of
Just xs -> do
vals <- mapM getConcrete xs
let cmodel = MModel $ M.fromList $ vars `zip` vals
return $ Just cmodel
Nothing -> error "Prover returned incomplete model"
(Undef, _) -> error "Prover returned unknown"
(Unsat, Just _) -> error "Prover returned unsat but a model"
(Sat, Nothing) -> error "Prover returned sat but no model"
checkSat :: (SatModel a, SymWord a) =>
([String], Model (SBV a) -> SBool) ->
IO (Maybe (Model a))
checkSat (vars, constraint) = do
result <- satWith z3{verbose=False} $ symConstraints vars constraint
return $ rebuildModel vars $ getModel result
checkSatInt :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel Integer))
checkSatInt problem = evalZ3 $ checkSat mkIntSort problem
......@@ -2,35 +2,49 @@ module Solver.Formula
(evaluateFormula)
where
import Data.SBV
import Z3.Monad
import Property
import Solver
evaluateTerm :: Term -> ModelSI -> SInteger
evaluateTerm (Var x) m = mVal m x
evaluateTerm (Const c) _ = literal c
evaluateTerm (Minus t) m = - evaluateTerm t m
evaluateTerm (t :+: u) m = evaluateTerm t m + evaluateTerm u m
evaluateTerm (t :-: u) m = evaluateTerm t m - evaluateTerm u m
evaluateTerm (t :*: u) m = evaluateTerm t m * evaluateTerm u m
evaluateTerm :: Term -> MModelS -> Z3 AST
evaluateTerm (Var x) m = return $ mVal m x
evaluateTerm (Const c) _ = mkInt c
evaluateTerm (Minus t) m = mkUnaryMinus =<< evaluateTerm t m
evaluateTerm (t :+: u) m = evalBinaryTerm m mkAdd t u
evaluateTerm (t :-: u) m = evalBinaryTerm m mkSub t u
evaluateTerm (t :*: u) m = evalBinaryTerm m mkMul t u
opToFunction :: Op -> SInteger -> SInteger -> SBool
opToFunction Gt = (.>)
opToFunction Ge = (.>=)
opToFunction Eq = (.==)
opToFunction Ne = (./=)
opToFunction Le = (.<=)
opToFunction Lt = (.<)
evalBinaryTerm :: MModelS -> ([AST] -> Z3 AST) -> Term -> Term -> Z3 AST
evalBinaryTerm m op t u = do
t' <- evaluateTerm t m
u' <- evaluateTerm u m
op [t',u']
evaluateLinIneq :: LinearInequation -> ModelSI -> SBool
evaluateLinIneq (LinIneq lhs op rhs) m =
opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m)
opToFunction :: Op -> AST -> AST -> Z3 AST
opToFunction Gt = mkGt
opToFunction Ge = mkGe
opToFunction Eq = mkEq
opToFunction Ne = \a b -> mkNot =<< mkEq a b
opToFunction Le = mkLe
opToFunction Lt = mkLt
evaluateFormula :: Formula -> ModelSI -> SBool
evaluateFormula FTrue _ = true
evaluateFormula FFalse _ = false
evaluateLinIneq :: LinearInequation -> MModelS -> Z3 AST
evaluateLinIneq (LinIneq lhs op rhs) m = do
lhs' <- evaluateTerm lhs m
rhs' <- evaluateTerm rhs m
opToFunction op lhs' rhs'
evaluateFormula :: Formula -> MModelS -> Z3 AST
evaluateFormula FTrue _ = mkTrue
evaluateFormula FFalse _ = mkFalse
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
evaluateFormula (Neg p) m = mkNot =<< evaluateFormula p m
evaluateFormula (p :&: q) m = do
p' <- evaluateFormula p m
q' <- evaluateFormula q m
mkAnd [p',q']
evaluateFormula (p :|: q) m = do
p' <- evaluateFormula p m
q' <- evaluateFormula q m
mkOr [p',q']
......@@ -3,40 +3,45 @@ module Solver.StateEquation
markedPlacesFromAssignment)
where
import Data.SBV
import Z3.Monad
import Control.Monad
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 .== mVal m p
addTransition (t,w) = literal w * mVal m t
nonnegativityConstraints :: ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
checkTraps :: [[String]] -> ModelSI -> SBool
checkTraps traps m = bAnd $ map checkTrapDelta traps
where checkTrapDelta trap = sum (map (mVal m) trap) .>= 1
checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
checkStateEquation net f traps m =
placeConstraints net m &&&
nonnegativityConstraints m &&&
checkTraps traps m &&&
evaluateFormula f m
placeConstraints :: PetriNet -> MModelS -> Z3 ()
placeConstraints net m = mapM_ (assertCnstr <=< checkPlaceEquation) $ places net
where checkPlaceEquation p = do
incoming <- mapM (addTransition 1 ) $ lpre net p
outgoing <- mapM (addTransition (-1)) $ lpost net p
pinit <- mkInt $ initial net p
sums <- mkAdd (pinit:(incoming ++ outgoing))
mkEq sums (mVal m p)
addTransition fac (t,w) =
mkInt (fac*w) >>= \w' -> mkMul [w', mVal m t]
nonnegativityConstraints :: MModelS -> Z3 ()
nonnegativityConstraints m = mapM_ (assertCnstr <=< geZero) $ mValues m
where geZero v = mkGe v =<< mkInt (0::Integer)
checkTraps :: [[String]] -> MModelS -> Z3 ()
checkTraps traps m = mapM_ (assertCnstr <=< checkTrap) traps
where checkTrap trap = mkAdd (map (mVal m) trap) >>=
(\v -> mkGe v =<< mkInt (1::Integer))
checkStateEquation :: PetriNet -> Formula -> [[String]] -> MModelS -> Z3 ()
checkStateEquation net f traps m = do
placeConstraints net m
nonnegativityConstraints m
checkTraps traps m
assertCnstr =<< evaluateFormula f m
checkStateEquationSat :: PetriNet -> Formula -> [[String]] ->
([String], ModelSI -> SBool)
([String], MModelS -> Z3 ())
checkStateEquationSat net f traps =
(places net ++ transitions net, checkStateEquation net f traps)
markedPlacesFromAssignment :: PetriNet -> ModelI -> [String]
markedPlacesFromAssignment :: PetriNet -> MModelI -> [String]
markedPlacesFromAssignment net a = filter (cElem a) $ places net
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