Used Z3 API for transition invariants

src/Main.hs

@@ -25,7 +25,7 @@ import Property
 import Solver
 import Solver.StateEquation
 import Solver.TrapConstraints
---import Solver.TransitionInvariant
+import Solver.TransitionInvariant
 --import Solver.SComponent
 
 data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
@@ -330,14 +330,14 @@ checkSafetyProperty verbosity net refine f traps = do
 checkLivenessProperty :: Int -> PetriNet -> Bool ->
         Formula -> [([String],[String])] -> IO Bool
 checkLivenessProperty verbosity net refine f strans = do
-        r <- return Nothing -- checkSatInt $ checkTransitionInvariantSat net f strans
+        r <- checkSatInt $ checkTransitionInvariantSat net f strans
         case r of
             Nothing -> return True
             Just ax -> do
-                let fired = [] -- firedTransitionsFromAssignment ax
+                let fired = firedTransitionsFromAssignment ax
                 verbosePut verbosity 1 "Assignment found"
---                verbosePut verbosity 2 $ "Transitions fired: " ++ show fired
---                verbosePut verbosity 3 $ "Assignment: " ++ show ax
+                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
                     case rt of

src/Solver.hs

@@ -3,7 +3,7 @@
 module Solver
     (checkSat,checkSatInt,checkSatBool,MModelS,MModelI,MModelB,
      MModel(..),mVal,mValues,mElemsWith,mElemSum,CModel(..),
-     Z3Type(..),mkOr',mkAnd')
+     Z3Type(..),mkOr',mkAnd',mkAdd',mkSub',mkMul')
 where
 
 import Z3.Monad
@@ -20,7 +20,7 @@ type MModelI = MModel Integer
 type MModelB = MModel (Maybe Bool)
 
 class Z3Type a where
-        mkVal :: a -> Z3 AST -- TODO: needed?
+        mkVal :: a -> Z3 AST
         getVal :: AST -> Z3 a
 
 instance Z3Type Integer where
@@ -54,6 +54,18 @@ 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
+
 --class SMModel a where
 --        mElem :: MModel a -> String -> Z3 AST
 --        mNotElem :: MModel a -> String -> Z3 AST

src/Solver/TransitionInvariant.hs

@@ -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)