...
 
Commits (4)
......@@ -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
......@@ -224,7 +224,7 @@ transformNet (net, props) TerminationByReachability =
ps = ["'sigma", "'m1", "'m2"] ++
places net ++ map prime (places net)
is = [("'m1", 1)] ++
initials net ++ map (first prime) (initials net)
linitials net ++ map (first prime) (linitials net)
transformTransition t =
let (preT, postT) = context net t
pre' = [("'m1",1)] ++ preT ++ map (first prime) preT
......@@ -248,7 +248,7 @@ transformNet (net, props) TerminationByReachability =
transformNet (net, props) ValidateIdentifiers =
let ps = map validateId $ places net
ts = map validateId $ transitions net
is = map (first validateId) $ initials net
is = map (first validateId) $ linitials net
as = map (\(a,b,x) -> (validateId a, validateId b, x)) $ arcs net
gs = map validateId $ ghostTransitions net
net' = makePetriNet (name net) ps ts as is gs
......@@ -301,7 +301,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
......@@ -310,7 +310,7 @@ checkSafetyProperty verbosity net refine f traps = do
verbosePut verbosity 2 $ "Places marked: " ++ show assigned
verbosePut verbosity 3 $ "Assignment: " ++ show a
if refine then do
rt <- checkSat $ checkTrapSat net assigned
rt <- checkSatBool $ checkTrapSat net assigned
case rt of
Nothing -> do
verbosePut verbosity 1 "No trap found."
......@@ -330,7 +330,7 @@ checkSafetyProperty verbosity net refine f traps = do
checkLivenessProperty :: Int -> PetriNet -> Bool ->
Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbosity net refine f strans = do
r <- checkSat $ checkTransitionInvariantSat net f strans
r <- checkSatInt $ checkTransitionInvariantSat net f strans
case r of
Nothing -> return True
Just ax -> do
......@@ -339,7 +339,7 @@ checkLivenessProperty verbosity net refine f strans = do
verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
verbosePut verbosity 3 $ "Assignment: " ++ show ax
if refine then do
rt <- checkSat $ checkSComponentSat net fired ax
rt <- checkSatInt $ checkSComponentSat net fired ax
case rt of
Nothing -> do
verbosePut verbosity 1 "No S-component found"
......
......@@ -2,7 +2,7 @@
module PetriNet
(PetriNet,name,showNetName,places,transitions,initial,
pre,lpre,post,lpost,initials,context,arcs,ghostTransitions,
pre,lpre,post,lpost,initials,linitials,context,arcs,ghostTransitions,
makePetriNet,makePetriNetWithTrans)
where
......@@ -39,8 +39,11 @@ post net = map fst . snd . context net
lpost :: PetriNet -> String -> [(String, Integer)]
lpost net = snd . context net
initials :: PetriNet -> [(String,Integer)]
initials net = M.toList (initMap net)
initials :: PetriNet -> [String]
initials net = M.keys (initMap net)
linitials :: PetriNet -> [(String,Integer)]
linitials net = M.toList (initMap net)
showNetName :: PetriNet -> String
showNetName net = "Petri net" ++
......
......@@ -18,7 +18,7 @@ renderNet net =
ps = "PLACE " <> intercalate ","
(map stringUtf8 (places net)) <> ";\n"
is = "MARKING " <> intercalate ","
(map showWeight (initials net)) <> ";\n"
(map showWeight (linitials net)) <> ";\n"
makeTransition t =
let (preT,postT) = context net t
preS = "CONSUME " <> intercalate ","
......
......@@ -50,7 +50,7 @@ renderProperty filename net (Property propname Safety f) =
"FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename)))
<> " TYPE LOLA;\n" <>
"INITIAL " <> intercalate ","
(map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (initials net))
(map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (linitials net))
<> ";\n" <>
"FINAL COVER;\n" <>
"CONSTRAINTS " <> renderFormula f <> ";"
......
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Solver
(checkSat,ModelSI,ModelSB,ModelI,ModelB,
Model(..),mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
(checkSat,checkSatInt,checkSatBool,MModelS,MModelI,MModelB,
MModel(..),mVal,mValues,mElemsWith,mElemSum,mElem,mNotElem,
cElem,cNotElem,
Z3Type(..),mkOr',mkAnd',mkAdd',mkSub',mkMul')
where
import Data.SBV
import Z3.Monad
import Control.Monad
import qualified Data.Map as M
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 (Maybe Bool)
mVal :: Model a -> String -> a
class Z3Type a where
mkVal :: a -> Z3 AST
getVal :: AST -> Z3 a
instance Z3Type Integer where
mkVal = mkInt
getVal = getInt
instance Z3Type (Maybe Bool) where
mkVal x = case x of
Nothing -> error "can not make undefined constant"
Just True -> mkTrue
Just False -> mkFalse
getVal = getBool
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]
mElem :: MModelS -> String -> Z3 AST
mElem m x = (mVal m x `mkGt`) =<< mkInt (0::Integer)
mNotElem :: MModelS -> String -> Z3 AST
mNotElem m x = mkEq (mVal m x) =<< mkInt (0::Integer)
mElemsWith :: (a -> Bool) -> MModel a -> [String]
mElemsWith f m = M.keys $ M.filter f $ getMap m
mElemSum :: (Num a) => Model 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 CModel a where
cElem :: Model a -> String -> Bool
cNotElem :: Model 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 CModel Integer where
cElem m x = mVal m x > 0
cNotElem m x = mVal m x == 0
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 :: (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
mElemSum :: MModelS -> [String] -> Z3 AST
mElemSum m xs = mkAdd' $ map (mVal m) xs
cElem :: MModelI -> String -> Bool
cElem m x = mVal m x > 0
cNotElem :: MModelI -> String -> Bool
cNotElem m x = mVal m x == 0
mkOr' :: [AST] -> Z3 AST
mkOr' [] = mkFalse
mkOr' xs = mkOr xs
mkAnd' :: [AST] -> Z3 AST
mkAnd' [] = mkTrue
mkAnd' xs = mkAnd xs
mkAdd' :: [AST] -> Z3 AST
mkAdd' [] = mkInt (0::Integer)
mkAdd' xs = mkAdd xs
mkSub' :: [AST] -> Z3 AST
mkSub' [] = mkInt (0::Integer)
mkSub' xs = mkSub xs
mkMul' :: [AST] -> Z3 AST
mkMul' [] = mkInt (1::Integer)
mkMul' xs = mkMul xs
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 getVal 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"
checkSatInt :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel Integer))
checkSatInt = evalZ3 . checkSat mkIntSort
checkSatBool :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel (Maybe Bool)))
checkSatBool = evalZ3 . checkSat mkBoolSort
......@@ -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) _ = mkVal 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,7 +3,8 @@ module Solver.SComponent
getSComponentOutIn)
where
import Data.SBV
import Z3.Monad
import Control.Monad
import Data.List (partition)
import PetriNet
......@@ -12,66 +13,90 @@ import Solver
prime :: String -> String
prime = ('\'':)
checkPrePostPlaces :: PetriNet -> ModelSI -> SBool
checkPrePostPlaces :: PetriNet -> MModelS -> Z3 ()
checkPrePostPlaces net m =
bAnd $ map checkPrePostPlace $ places net
where checkPrePostPlace p =
let incoming = map (mElem m) $ pre net p
outgoing = map (mElem m) $ post net p
in mElem m p ==> bAnd incoming &&& bAnd outgoing
mapM_ (assertCnstr <=< checkPrePostPlace) $ places net
where checkPrePostPlace p = do
incoming <- mapM (mElem m) $ pre net p
outgoing <- mapM (mElem m) $ post net p
lhs <- mElem m p
rhs <- mkAnd' (incoming ++ outgoing)
mkImplies lhs rhs
checkPrePostTransitions :: PetriNet -> ModelSI -> SBool
checkPrePostTransitions :: PetriNet -> MModelS -> Z3 ()
checkPrePostTransitions net m =
bAnd $ map checkPrePostTransition $ transitions net
where checkPrePostTransition t =
let incoming = mElemSum m $ pre net t
outgoing = mElemSum m $ post net t
in mElem m t ==> incoming .== 1 &&& outgoing .== 1
mapM_ (assertCnstr <=< checkPrePostTransition) $ transitions net
where checkPrePostTransition t = do
incoming <- mElemSum m $ pre net t
outgoing <- mElemSum m $ post net t
in1 <- mkEq incoming =<< mkVal (1::Integer)
out1 <- mkEq outgoing =<< mkVal (1::Integer)
lhs <- mElem m t
rhs <- mkAnd [in1, out1]
mkImplies lhs rhs
checkSubsetTransitions :: [String] -> ModelSI -> SBool
checkSubsetTransitions fired m =
bAnd (map checkTransition fired) &&&
mElemSum m (map prime fired) .< mElemSum m fired
where checkTransition t =
mElem m (prime t) ==> mElem m t
checkSubsetTransitions :: [String] -> MModelS -> Z3 ()
checkSubsetTransitions fired m = do
mapM_ (assertCnstr <=< checkTransition) fired
fired'sum <- mElemSum m (map prime fired)
firedsum <- mElemSum m fired
assertCnstr =<< mkLt fired'sum firedsum
where checkTransition t = do
lhs <- mElem m (prime t)
rhs <- mElem m t
mkImplies lhs rhs
checkNotEmpty :: [String] -> ModelSI -> SBool
checkNotEmpty fired m = mElemSum m (map prime fired) .> 0
checkNotEmpty :: [String] -> MModelS -> Z3 ()
checkNotEmpty fired m = do
lhs <- mElemSum m (map prime fired)
assertCnstr =<< mkGt lhs =<< mkVal (0::Integer)
checkClosed :: PetriNet -> ModelI -> ModelSI -> SBool
checkClosed :: PetriNet -> MModelI -> MModelS -> Z3 ()
checkClosed net ax m =
bAnd (map checkPlaceClosed (places net))
where checkPlaceClosed p = mElem m p ==>
bAnd (map checkTransition
mapM_ (assertCnstr <=< checkPlaceClosed) $ places net
where checkPlaceClosed p = do
lhs <- mElem m p
rhs <- mkAnd' =<< mapM checkTransition
[(t,t') | t <- pre net p, t' <- post net p,
cElem ax t, cElem ax t' ])
checkTransition (t,t') =
mElem m (prime t) ==> mElem m (prime t')
cElem ax t, cElem ax t' ]
mkImplies lhs rhs
checkTransition (t,t') = do
lhs <- mElem m (prime t)
rhs <- mElem m (prime t')
mkImplies lhs rhs
checkTokens :: PetriNet -> ModelSI -> SBool
checkTokens net m =
sum (map addPlace (initials net)) .== 1
where addPlace (p,x) = literal x * mVal m p
checkTokens :: PetriNet -> MModelS -> Z3 ()
checkTokens net m = do
initS <- mapM addPlace (linitials net)
sums <- mkAdd' initS
assertCnstr =<< mkEq sums =<< mkVal (1::Integer)
where addPlace (p,x) =
mkVal x >>= \x' -> mkMul [x', mVal m p]
checkBinary :: ModelSI -> SBool
checkBinary m = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ mValues m
checkBinary :: MModelS -> Z3 ()
checkBinary m =
mapM_ (assertCnstr <=< checkBinaryVal) $ mValues m
where checkBinaryVal x = do
x0 <- mkEq x =<< mkVal (0::Integer)
x1 <- mkEq x =<< mkVal (1::Integer)
mkOr [x0,x1]
checkSComponent :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
checkSComponent net fired ax m =
checkPrePostPlaces net m &&&
checkPrePostTransitions net m &&&
checkSubsetTransitions fired m &&&
checkNotEmpty fired m &&&
checkClosed net ax m &&&
checkTokens net m &&&
checkSComponent :: PetriNet -> [String] -> MModelI -> MModelS -> Z3 ()
checkSComponent net fired ax m = do
checkPrePostPlaces net m
checkPrePostTransitions net m
checkSubsetTransitions fired m
checkNotEmpty fired m
checkClosed net ax m
checkTokens net m
checkBinary m
checkSComponentSat :: PetriNet -> [String] -> ModelI -> ([String], ModelSI -> SBool)
checkSComponentSat :: PetriNet -> [String] -> MModelI -> ([String], MModelS -> Z3 ())
checkSComponentSat net fired ax =
(places net ++ transitions net ++ map prime fired,
checkSComponent net fired ax)
getSComponentOutIn :: PetriNet -> ModelI -> ModelI -> ([String], [String])
getSComponentOutIn :: PetriNet -> MModelI -> MModelI -> ([String], [String])
getSComponentOutIn net ax as =
partition (cElem ax) $ filter (cElem as) (transitions net)
......@@ -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 <- mkVal $ initial net p
sums <- mkAdd (pinit:(incoming ++ outgoing))
mkEq sums (mVal m p)
addTransition fac (t,w) =
mkVal (fac*w) >>= \w' -> mkMul [w', mVal m t]
nonnegativityConstraints :: MModelS -> Z3 ()
nonnegativityConstraints m = mapM_ (assertCnstr <=< geZero) $ mValues m
where geZero v = mkGe v =<< mkVal (0::Integer)
checkTraps :: [[String]] -> MModelS -> Z3 ()
checkTraps traps m = mapM_ (assertCnstr <=< checkTrap) traps
where checkTrap trap = mkAdd (map (mVal m) trap) >>=
(\v -> mkGe v =<< mkVal (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
......@@ -3,47 +3,56 @@ module Solver.TransitionInvariant
firedTransitionsFromAssignment)
where
import Data.SBV
import Z3.Monad
import Control.Monad
import PetriNet
import Property
import Solver
import Solver.Formula
tInvariantConstraints :: PetriNet -> ModelSI -> SBool
tInvariantConstraints :: PetriNet -> MModelS -> Z3 ()
tInvariantConstraints net m =
bAnd $ map checkTransitionEquation $ places net
where checkTransitionEquation p =
let incoming = map addTransition $ lpre net p
outgoing = map addTransition $ lpost net p
in sum incoming - sum outgoing .>= 0
addTransition (t,w) = literal w * mVal m t
finalInvariantConstraints :: ModelSI -> SBool
finalInvariantConstraints m = sum (mValues m) .> 0
nonnegativityConstraints :: ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool
checkSComponentTransitions strans m = bAnd $ map checkInOut strans
where checkInOut (sOut,sIn) =
bAnd (map (\t -> mVal m t .> 0) sOut) ==>
bOr (map (\t -> mVal m t .> 0) sIn)
mapM_ (assertCnstr <=< checkTransitionEquation) $ places net
where checkTransitionEquation p = do
incoming <- mapM (addTransition 1 ) $ lpre net p
outgoing <- mapM (addTransition (-1)) $ lpost net p
sums <- mkAdd' (incoming ++ outgoing)
mkGe sums =<< mkVal (0::Integer)
addTransition fac (t,w) =
mkVal (fac*w) >>= \w' -> mkMul [w', mVal m t]
finalInvariantConstraints :: MModelS -> Z3 ()
finalInvariantConstraints m = do
sums <- mkAdd' (mValues m)
assertCnstr =<< mkGt sums =<< mkVal (0::Integer)
nonnegativityConstraints :: MModelS -> Z3 ()
nonnegativityConstraints m = mapM_ (assertCnstr <=< geZero) $ mValues m
where geZero v = mkGe v =<< mkVal (0::Integer)
checkSComponentTransitions :: [([String],[String])] -> MModelS -> Z3 ()
checkSComponentTransitions strans m = mapM_ (assertCnstr <=< checkInOut) strans
where checkInOut (sOut,sIn) = do
lhs <- mkAnd' =<<
mapM (\t -> mkGt (mVal m t) =<< mkVal (0::Integer)) sOut
rhs <- mkOr' =<<
mapM (\t -> mkGt (mVal m t) =<< mkVal (0::Integer)) sIn
mkImplies lhs rhs
checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] ->
ModelSI -> SBool
checkTransitionInvariant net f strans m =
tInvariantConstraints net m &&&
nonnegativityConstraints m &&&
finalInvariantConstraints m &&&
checkSComponentTransitions strans m &&&
evaluateFormula f m
MModelS -> Z3 ()
checkTransitionInvariant net f strans m = do
tInvariantConstraints net m
nonnegativityConstraints m
finalInvariantConstraints m
checkSComponentTransitions strans m
assertCnstr =<< evaluateFormula f m
checkTransitionInvariantSat :: PetriNet -> Formula -> [([String],[String])] ->
([String], ModelSI -> SBool)
([String], MModelS -> Z3 ())
checkTransitionInvariantSat net f strans =
(transitions net, checkTransitionInvariant net f strans)
firedTransitionsFromAssignment :: ModelI -> [String]
firedTransitionsFromAssignment :: MModelI -> [String]
firedTransitionsFromAssignment = mElemsWith (> 0)
......@@ -4,35 +4,36 @@ module Solver.TrapConstraints
)
where
import Data.SBV
import Z3.Monad
import Control.Monad
import PetriNet
import Solver
trapConstraints :: PetriNet -> ModelSB -> SBool
trapConstraints net m =
bAnd $ map trapConstraint $ transitions net
where trapConstraint t =
bOr (map (mElem m) $ pre net t) ==> bOr (map (mElem m) $ post net t)
trapConstraints :: PetriNet -> MModelS -> Z3 ()
trapConstraints net m = mapM_ (assertCnstr <=< trapConstraint) $ transitions net
where trapConstraint t = do
lhs <- mkOr' (map (mVal m) $ pre net t)
rhs <- mkOr' (map (mVal m) $ post net t)
mkImplies lhs rhs
trapInitiallyMarked :: PetriNet -> ModelSB -> SBool
trapInitiallyMarked net m =
let marked = map fst $ filter (( > 0) . snd) $ initials net
in bOr $ map (mElem m) marked
trapInitiallyMarked :: PetriNet -> MModelS -> Z3 ()
trapInitiallyMarked net m = assertCnstr =<< mkOr' (map (mVal m) (initials net))
trapUnassigned :: [String] -> ModelSB -> SBool
trapUnassigned assigned m = bAnd $ map (mNotElem m) assigned
trapUnassigned :: [String] -> MModelS -> Z3 ()
trapUnassigned assigned m = mapM_ (assertCnstr <=< (mkNot . mVal m)) assigned
checkTrap :: PetriNet -> [String] -> ModelSB -> SBool
checkTrap net assigned m =
trapConstraints net m &&&
trapInitiallyMarked net m &&&
checkTrap :: PetriNet -> [String] -> MModelS -> Z3 ()
checkTrap net assigned m = do
trapConstraints net m
trapInitiallyMarked net m
trapUnassigned assigned m
checkTrapSat :: PetriNet -> [String] -> ([String], ModelSB -> SBool)
checkTrapSat :: PetriNet -> [String] -> ([String], MModelS -> Z3 ())
checkTrapSat net assigned =
(places net, checkTrap net assigned)
trapFromAssignment :: ModelB -> [String]
trapFromAssignment = mElemsWith id
trapFromAssignment :: MModelB -> [String]
trapFromAssignment = mElemsWith (\x -> case x of Just True -> True
_ -> False )