Rewrote state equation constraints

src/Main.hs

@@ -28,11 +28,11 @@ import Property
 import Structure
 import Solver
 import Solver.StateEquation
-import Solver.TrapConstraints
-import Solver.TransitionInvariant
-import Solver.SubnetEmptyTrap
+--import Solver.TrapConstraints
+--import Solver.TransitionInvariant
+--import Solver.SubnetEmptyTrap
 --import Solver.LivenessInvariant
-import Solver.SComponent
+--import Solver.SComponent
 --import Solver.CommFreeReachability
 
 data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
@@ -421,7 +421,7 @@ checkProperty verbosity net refine invariant p = do
         verbosePut verbosity 3 $ show p
         r <- case pcont p of
             (Safety pf) -> checkSafetyProperty verbosity net refine invariant pf
-            (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
+--            (Liveness pf) -> checkLivenessProperty verbosity net refine invariant pf
             (Structural ps) -> checkStructuralProperty verbosity net ps
         verbosePut verbosity 0 $ showPropertyName p ++ " " ++
             case r of
@@ -447,15 +447,16 @@ 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 <- checkSat verbosity $ checkStateEquationSat net f traps
+        r <- checkSat2 verbosity $ checkStateEquationSat net f traps
         case r of
             Nothing -> return (Nothing, traps)
             Just m ->
                 if refine then
-                    refineSafetyProperty verbosity net f traps m
+                    return (Just m, traps)
+                    --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
@@ -479,6 +480,7 @@ checkLivenessProperty verbosity net refine invariant f = do
                     return Satisfied
             (Just _, _) ->
                 return Unknown
+-}
 {-
 generateLivenessInvariant :: Int -> PetriNet ->
         Formula -> [SCompCut] -> IO PropResult
@@ -493,6 +495,7 @@ generateLivenessInvariant verbosity net f comps = do
                 mapM_ print inv
                 return Satisfied
 -}
+{-
 checkLivenessProperty' :: Int -> PetriNet -> Bool ->
         Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
 checkLivenessProperty' verbosity net refine f cuts = do
@@ -551,7 +554,7 @@ generateLivenessRefinement :: PetriNet -> FiringVector -> [Trap] -> Cut
 generateLivenessRefinement net x traps =
         (map (filter (\t -> value x t > 0) . mpre net) traps,
          nubOrd (concatMap (filter (\t -> value x t == 0) . mpost net) traps))
-
+-}
 checkStructuralProperty :: Int -> PetriNet -> Structure -> IO PropResult
 checkStructuralProperty _ net struct =
         if checkStructure net struct then

src/Solver.hs

 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 
 module Solver
-    (prime,checkSat,ModelReader,val,vals,valMap,VarMap,positiveVal,zeroVal,
+    (prime,checkSat,ModelReader,val,vals,positiveVal,zeroVal,
      sumVal, getNames,makeVarMap,makeVarMapWith,mval,
      IntConstraint,BoolConstraint,IntResult,BoolResult,
-     Model,ConstraintProblem,ConstraintProblem2)
+     Model,ConstraintProblem,ConstraintProblem2,checkSat2,
+     SIMap,SBMap,IMap,BMap)
 where
 
 import Data.SBV
@@ -16,6 +17,11 @@ import Util
 type Model a = M.Map String a
 type VarMap a = M.Map a String
 
+type SIMap a = M.Map a SInteger
+type SBMap a = M.Map a SBool
+type IMap a = M.Map a Integer
+type BMap a = M.Map a Bool
+
 getNames :: VarMap a -> [String]
 getNames = M.elems
 
@@ -30,35 +36,25 @@ type ConstraintProblem a b =
 
 -- TODO try this out
 type ConstraintProblem2 a b =
-        (String, String, [String],
-         (String -> SBV a) -> SBool, (String -> a) -> b)
-
-val :: (Ord a) => VarMap a -> a -> ModelReader b b
-val ma x = do
-        mb <- ask
-        return $ mb M.! (ma M.! x)
+        (String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
 
-mval :: (Ord a) => VarMap a -> [a] -> ModelReader b [b]
-mval = mapM . val
+val :: (Ord a) => M.Map a b -> a -> b
+val = (M.!)
 
-zeroVal :: (Ord a) => VarMap a -> a -> ModelReader SInteger SBool
-zeroVal ma = liftM (.==0) . val ma
+mval :: (Ord a) => M.Map a b -> [a] -> [b]
+mval = map . val
 
-positiveVal :: (Ord a) => VarMap a -> a -> ModelReader SInteger SBool
-positiveVal ma = liftM (.>0) . val ma
+zeroVal :: (Ord a) => M.Map a SInteger -> a -> SBool
+zeroVal m x = val m x .== 0
 
-sumVal :: (Ord a, Num b) => VarMap a -> ModelReader b b
-sumVal = liftM sum . vals
+positiveVal :: (Ord a) => M.Map a SInteger -> a -> SBool
+positiveVal m x = val m x .> 0
 
-valMap :: (Ord a) => VarMap a -> ModelReader b (M.Map a b)
-valMap ma = do
-        mb <- ask
-        return $ M.map (mb M.!) ma
+sumVal :: (Ord a, Num b) => M.Map a b -> b
+sumVal = sum . vals
 
-vals :: (Ord a) => VarMap a -> ModelReader b [b]
-vals ma = do
-        mb <- ask
-        return $ M.elems $ M.map (mb M.!) ma
+vals :: (Ord a) => M.Map a b -> [b]
+vals = M.elems
 
 makeVarMap :: (Show a, Ord a) => [a] -> VarMap a
 makeVarMap = makeVarMapWith id
@@ -131,3 +127,28 @@ checkSat verbosity (problemName, resultName, vars, constraint, interpretation) =
                 verbosePut verbosity 3 $ "- " ++ resultName ++ ": " ++ show model
                 return $ Just model
 
+symConstraints2 :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
+        Symbolic SBool
+symConstraints2 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
+        verbosePut verbosity 1 $ "Checking SAT of " ++ problemName
+        result <- satWith z3{verbose=verbosity >= 4} $
+                    symConstraints2 vars constraint
+        case rebuildModel vars (getModel result) of
+            Nothing -> do
+                verbosePut verbosity 2 "- unsat"
+                return Nothing
+            Just rawModel -> do
+                verbosePut verbosity 2 "- sat"
+                let fm x = rawModel M.! x
+                let model = interpretation fm
+                verbosePut verbosity 3 $ "- " ++ resultName ++ ": " ++ show model
+                return $ Just model
+

src/Solver/Formula.hs

@@ -7,24 +7,13 @@ import Data.SBV
 import Property
 import Solver
 
-evaluateTerm :: (Ord a) => Term a -> VarMap a -> ModelReader SInteger SInteger
+evaluateTerm :: (Ord a) => Term a -> SIMap a -> SInteger
 evaluateTerm (Var x) m = val m x
-evaluateTerm (Const c) _ = return $ literal c
-evaluateTerm (Minus t) m = do
-        tVal <- evaluateTerm t m
-        return (- tVal)
-evaluateTerm (t :+: u) m = do
-        tVal <- evaluateTerm t m
-        uVal <- evaluateTerm u m
-        return $ tVal + uVal
-evaluateTerm (t :-: u) m = do
-        tVal <- evaluateTerm t m
-        uVal <- evaluateTerm u m
-        return $ tVal - uVal
-evaluateTerm (t :*: u) m = do
-        tVal <- evaluateTerm t m
-        uVal <- evaluateTerm u m
-        return $ tVal * uVal
+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
 
 opToFunction :: Op -> SInteger -> SInteger -> SBool
 opToFunction Gt = (.>)
@@ -34,21 +23,11 @@ opToFunction Ne = (./=)
 opToFunction Le = (.<=)
 opToFunction Lt = (.<)
 
-evaluateFormula :: (Ord a) => Formula a -> VarMap a -> IntConstraint
-evaluateFormula FTrue _ = return true
-evaluateFormula FFalse _ = return false
-evaluateFormula (LinearInequation lhs op rhs) m = do
-        lhsVal <- evaluateTerm lhs m
-        rhsVal <- evaluateTerm rhs m
-        return $ opToFunction op lhsVal rhsVal
-evaluateFormula (Neg p) m = do
-        pVal <- evaluateFormula p m
-        return $ bnot pVal
-evaluateFormula (p :&: q) m = do
-        pVal <- evaluateFormula p m
-        qVal <- evaluateFormula q m
-        return $ pVal &&& qVal
-evaluateFormula (p :|: q) m = do
-        pVal <- evaluateFormula p m
-        qVal <- evaluateFormula q m
-        return $ pVal ||| qVal
+evaluateFormula :: (Ord a) => Formula a -> SIMap a -> SBool
+evaluateFormula FTrue _ = true
+evaluateFormula FFalse _ = false
+evaluateFormula (LinearInequation lhs op rhs) m =
+        opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs 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

src/Solver/StateEquation.hs

@@ -3,7 +3,6 @@ module Solver.StateEquation
 where
 
 import Data.SBV
-import Control.Monad
 
 import Util
 import PetriNet
@@ -11,56 +10,46 @@ import Property
 import Solver
 import Solver.Formula
 
-placeConstraints :: PetriNet -> VarMap Place -> VarMap Transition -> IntConstraint
+placeConstraints :: PetriNet -> SIMap Place -> SIMap Transition -> SBool
 placeConstraints net m x =
-            liftM bAnd $ mapM checkPlaceEquation $ places net
-        where checkPlaceEquation p = do
-                mp <- val m p
-                incoming <- mapM addTransition $ lpre net p
-                outgoing <- mapM addTransition $ lpost net p
-                let pinit = literal $ initial net p
-                return $ pinit + sum incoming - sum outgoing .== mp
-              addTransition (t,w) = liftM (literal w *) (val x t)
-
-nonNegativityConstraints :: PetriNet -> VarMap Place -> VarMap Transition ->
-        IntConstraint
-nonNegativityConstraints net m x = do
-            mnn <- mapM (checkVal m) (places net)
-            xnn <- mapM (checkVal x) (transitions net)
-            return $ bAnd mnn &&& bAnd xnn
-        where checkVal mapping n = do
-                mn <- val mapping n
-                return $ mn .>= 0
-
-checkTraps :: [Trap] -> VarMap Place -> IntConstraint
-checkTraps traps m = do
-            tc <- mapM checkTrapDelta traps
-            return $ bAnd tc
-        where checkTrapDelta trap = do
-                mts <- mapM (val m) trap
-                return $ sum mts .>= 1
+            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 .== val m p
+              addTransition (t,w) = literal w * val x t
+
+nonNegativityConstraints :: PetriNet -> SIMap Place -> SIMap Transition -> SBool
+nonNegativityConstraints net m x =
+            let mnn = map (checkVal m) $ places net
+                xnn = map (checkVal x) $ transitions net
+            in  bAnd mnn &&& bAnd xnn
+        where checkVal mapping n = val mapping n .>= 0
+
+checkTraps :: [Trap] -> SIMap Place -> SBool
+checkTraps traps m =
+            bAnd $ map checkTrapDelta traps
+        where checkTrapDelta trap = sum (map (val m) trap) .>= 1
 
 checkStateEquation :: PetriNet -> Formula Place ->
-        VarMap Place -> VarMap Transition -> [Trap] ->
-        IntConstraint
-checkStateEquation net f m x traps = do
-        c1 <- placeConstraints net m x
-        c2 <- nonNegativityConstraints net m x
-        c3 <- checkTraps traps m
-        c4 <- evaluateFormula f m
-        return $ c1 &&& c2 &&& c3 &&& c4
+        SIMap Place -> SIMap Transition -> [Trap] -> SBool
+checkStateEquation net f m x traps =
+        placeConstraints net m x &&&
+        nonNegativityConstraints net m x &&&
+        checkTraps traps m &&&
+        evaluateFormula f m
 
 checkStateEquationSat :: PetriNet -> Formula Place -> [Trap] ->
-        ConstraintProblem Integer Marking
+        ConstraintProblem2 Integer Marking
 checkStateEquationSat net f traps =
         let m = makeVarMap $ places net
             x = makeVarMap $ transitions net
         in  ("state equation", "marking",
              getNames m ++ getNames x,
-             checkStateEquation net f m x traps,
-             markingFromAssignment m)
+             \fm -> checkStateEquation net f (fmap fm m) (fmap fm x) traps,
+             \fm -> markingFromAssignment (fmap fm m))
 
-markingFromAssignment :: VarMap Place -> IntResult Marking
-markingFromAssignment m =
-        liftM makeVector $ valMap m
+markingFromAssignment :: IMap Place -> Marking
+markingFromAssignment = makeVector