Used Z3 API for S-components

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

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

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)