Rewrote trap constraints

src/Main.hs

@@ -28,7 +28,7 @@ import Property
 import Structure
 import Solver
 import Solver.StateEquation
---import Solver.TrapConstraints
+import Solver.TrapConstraints
 --import Solver.TransitionInvariant
 --import Solver.SubnetEmptyTrap
 --import Solver.LivenessInvariant
@@ -447,16 +447,15 @@ checkSafetyProperty verbosity net refine invariant f = do
 checkSafetyProperty' :: Int -> PetriNet -> Bool ->
         Formula Place -> [Trap] -> IO (Maybe Marking, [Trap])
 checkSafetyProperty' verbosity net refine f traps = do
-        r <- checkSat2 verbosity $ checkStateEquationSat net f traps
+        r <- checkSat verbosity $ checkStateEquationSat net f traps
         case r of
             Nothing -> return (Nothing, traps)
             Just m ->
                 if refine then
-                    return (Just m, traps)
-                    --refineSafetyProperty verbosity net f traps m
+                    refineSafetyProperty verbosity net f traps m
                 else
                     return (Just m, traps)
-{-
+
 refineSafetyProperty :: Int -> PetriNet ->
         Formula Place -> [Trap] -> Marking -> IO (Maybe Marking, [Trap])
 refineSafetyProperty verbosity net f traps m = do
@@ -466,7 +465,7 @@ refineSafetyProperty verbosity net f traps m = do
                 return (Just m, traps)
             Just trap ->
                 checkSafetyProperty' verbosity net True f (trap:traps)
-
+{-
 checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
         Formula Transition -> IO PropResult
 checkLivenessProperty verbosity net refine invariant f = do

src/Solver.hs

@@ -4,8 +4,8 @@ module Solver
     (prime,checkSat,ModelReader,val,vals,positiveVal,zeroVal,
      sumVal, getNames,makeVarMap,makeVarMapWith,mval,
      IntConstraint,BoolConstraint,IntResult,BoolResult,
-     Model,ConstraintProblem,ConstraintProblem2,checkSat2,
-     SIMap,SBMap,IMap,BMap)
+     Model,ConstraintProblem,
+     SIMap,SBMap,IMap,BMap,VarMap)
 where
 
 import Data.SBV
@@ -32,10 +32,6 @@ type IntResult a = ModelReader Integer a
 type BoolResult a = ModelReader Bool a
 
 type ConstraintProblem a b =
-        (String, String, [String], ModelReader (SBV a) SBool, ModelReader a b)
-
--- TODO try this out
-type ConstraintProblem2 a b =
         (String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
 
 val :: (Ord a) => M.Map a b -> a -> b
@@ -62,85 +58,26 @@ makeVarMap = makeVarMapWith id
 makeVarMapWith :: (Show a, Ord a) => (String -> String) -> [a] -> VarMap a
 makeVarMapWith f xs = M.fromList $ xs `zip` map (f . show) xs
 
-prime :: String -> String
-prime = ('\'':)
-{-
-mVal :: Model a -> String -> a
-mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x m
-
-mValues :: Model a -> [a]
-mValues = M.elems
-
-mElemsWith :: (a -> Bool) -> Model a -> [String]
-mElemsWith f m = M.keys $ M.filter f 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] -> ModelReader (SBV a) SBool ->
-        Symbolic SBool
-symConstraints vars constraint = do
-        syms <- mapM exists vars
-        return $ runReader constraint $ 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 $ M.fromList $ vars `zip` m
 
-checkSat :: (SatModel a, SymWord a, Show a, Show b) => Int ->
-        ConstraintProblem a b -> IO (Maybe b)
-checkSat verbosity (problemName, resultName, vars, constraint, interpretation) = do
-        verbosePut verbosity 1 $ "Checking SAT of " ++ problemName
-        result <- satWith z3{verbose=verbosity >= 4} $
-            symConstraints vars constraint
-        case rebuildModel vars (getModel result) of
-            Nothing -> do
-                verbosePut verbosity 2 "- unsat"
-                return Nothing
-            Just rawModel -> do
-                verbosePut verbosity 2 "- sat"
-                let model = runReader interpretation rawModel
-                verbosePut verbosity 3 $ "- " ++ resultName ++ ": " ++ show model
-                return $ Just model
-
-symConstraints2 :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
+symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
         Symbolic SBool
-symConstraints2 vars constraint = do
+symConstraints vars constraint = do
         syms <- mapM exists vars
         let symMap = M.fromList $ vars `zip` syms
         let fm x = symMap M.! x
         return $ constraint fm
 
-checkSat2 :: (SatModel a, SymWord a, Show a, Show b) => Int ->
-        ConstraintProblem2 a b -> IO (Maybe b)
-checkSat2 verbosity (problemName, resultName, vars, constraint, interpretation) = do
+checkSat :: (SatModel a, SymWord a, Show a, Show b) => Int ->
+        ConstraintProblem a b -> IO (Maybe b)
+checkSat verbosity (problemName, resultName, vars, constraint, interpretation) = do
         verbosePut verbosity 1 $ "Checking SAT of " ++ problemName
         result <- satWith z3{verbose=verbosity >= 4} $
-                    symConstraints2 vars constraint
+                    symConstraints vars constraint
         case rebuildModel vars (getModel result) of
             Nothing -> do
                 verbosePut verbosity 2 "- unsat"

src/Solver/StateEquation.hs

@@ -41,7 +41,7 @@ checkStateEquation net f m x traps =
         evaluateFormula f m
 
 checkStateEquationSat :: PetriNet -> Formula Place -> [Trap] ->
-        ConstraintProblem2 Integer Marking
+        ConstraintProblem Integer Marking
 checkStateEquationSat net f traps =
         let m = makeVarMap $ places net
             x = makeVarMap $ transitions net

src/Solver/TrapConstraints.hs

@@ -3,46 +3,38 @@ module Solver.TrapConstraints
 where
 
 import Data.SBV
-import Control.Monad
 import qualified Data.Map as M
 
 import Util
 import PetriNet
 import Solver
 
-trapConstraints :: PetriNet -> VarMap Place -> BoolConstraint
+trapConstraints :: PetriNet -> SBMap Place -> SBool
 trapConstraints net b =
-            liftM bAnd $ mapM trapConstraint $ transitions net
-        where trapConstraint t = do
-                cPre <- mapM (val b) $ pre net t
-                cPost <- mapM (val b) $ post net t
-                return $ bOr cPre ==> bOr cPost
-
-trapInitiallyMarked :: PetriNet -> VarMap Place -> BoolConstraint
-trapInitiallyMarked net b =
-        liftM bOr $ mapM (val b) $ initials net
-
-trapUnassigned :: Marking -> VarMap Place -> BoolConstraint
-trapUnassigned m b =
-        liftM bAnd $ mapM (liftM bnot . val b) $ elems m
-
-checkTrap :: PetriNet -> Marking -> VarMap Place -> BoolConstraint
-checkTrap net m b = do
-        c1 <- trapConstraints net b
-        c2 <- trapInitiallyMarked net b
-        c3 <- trapUnassigned m b
-        return $ c1 &&& c2 &&& c3
+            bAnd $ map trapConstraint $ transitions net
+        where trapConstraint t =
+                  bOr (mval b (pre net t)) ==> bOr (mval b (post net t))
+
+trapInitiallyMarked :: PetriNet -> SBMap Place -> SBool
+trapInitiallyMarked net b = bOr $ mval b $ initials net
+
+trapUnassigned :: Marking -> SBMap Place -> SBool
+trapUnassigned m b = bAnd $ map (bnot . val b) $ elems m
+
+checkTrap :: PetriNet -> Marking -> SBMap Place -> SBool
+checkTrap net m b =
+        trapConstraints net b &&&
+        trapInitiallyMarked net b &&&
+        trapUnassigned m b
 
 checkTrapSat :: PetriNet -> Marking -> ConstraintProblem Bool Trap
 checkTrapSat net m =
         let b = makeVarMap $ places net
         in  ("trap constraints", "trap",
              getNames b,
-             checkTrap net m b,
-             trapFromAssignment b)
+             \fm -> checkTrap net m (fmap fm b),
+             \fm -> trapFromAssignment (fmap fm b))
 
-trapFromAssignment :: VarMap Place -> BoolResult Trap
-trapFromAssignment b = do
-        bm <- valMap b
-        return $ M.keys $ M.filter id bm
+trapFromAssignment :: BMap Place -> Trap
+trapFromAssignment b = M.keys $ M.filter id b
 

src/Util.hs

 module Util
     (verbosePut,Vector,value,elems,items,buildVector,makeVector,vmap,
-     nubOrd,nubOrdBy)
+     nubOrd,nubOrdBy,prime)
 where
 
 import qualified Data.Map as M
@@ -13,6 +13,8 @@ verbosePut :: Int -> Int -> String -> IO ()
 verbosePut verbosity level str =
         when (verbosity >= level) (putStrLn str)
 
+prime :: String -> String
+prime = ('\'':)
 
 newtype Vector a = Vector { getVector :: M.Map a Integer }