diff --git a/src/Main.hs b/src/Main.hs index 04f78e390c5f29c6ba406ff5dbcd63bf8e6adaee..ced4916f12c0b6bb25df1f4ee475984ff736c03b 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -26,7 +26,7 @@ import Solver import Solver.StateEquation import Solver.TrapConstraints import Solver.TransitionInvariant ---import Solver.SComponent +import Solver.SComponent data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read) @@ -339,17 +339,17 @@ 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 <- return Nothing -- checkSat \$ checkSComponentSat net fired ax + rt <- checkSatInt \$ checkSComponentSat net fired ax case rt of Nothing -> do verbosePut verbosity 1 "No S-component found" return False Just as -> do - let sOutIn = undefined -- 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 + 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 diff --git a/src/Solver.hs b/src/Solver.hs index 8dfe39ef937309e50a0030596059f51a25a6861b..3855b43b94c01f97c9b6638dc05fae9c676b71b0 100644 --- a/src/Solver.hs +++ b/src/Solver.hs @@ -2,7 +2,8 @@ module Solver (checkSat,checkSatInt,checkSatBool,MModelS,MModelI,MModelB, - MModel(..),mVal,mValues,mElemsWith,mElemSum,CModel(..), + MModel(..),mVal,mValues,mElemsWith,mElemSum,mElem,mNotElem, + cElem,cNotElem, Z3Type(..),mkOr',mkAnd',mkAdd',mkSub',mkMul') where @@ -40,11 +41,23 @@ mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x (getMap m) mValues :: MModel a -> [a] mValues m = M.elems \$ getMap m +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) => MModel a -> [String] -> a -mElemSum m xs = sum \$ map (mVal m) xs +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 @@ -66,28 +79,6 @@ mkMul' :: [AST] -> Z3 AST mkMul' [] = mkInt (1::Integer) mkMul' xs = mkMul xs ---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 :: MModel a -> String -> Bool - cNotElem :: MModel a -> String -> Bool - cNotElem m x = not \$ cElem 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 -instance CModel Bool where - cElem = mVal - cNotElem m x = not \$ mVal m x - checkSat :: Z3Type a => Z3 Sort -> ([String], MModel AST -> Z3 ()) -> Z3 (Maybe (MModel a)) checkSat mkSort (vars, constraint) = do diff --git a/src/Solver/SComponent.hs b/src/Solver/SComponent.hs index 007a843f1376ad9772ae4684f390e6dab550ef16..d7acebf62fc5efd271ff5763cf78d1bf0ebb471a 100644 --- a/src/Solver/SComponent.hs +++ b/src/Solver/SComponent.hs @@ -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)