From 29184fb1e030934ed649483771daf208c3a967a4 Mon Sep 17 00:00:00 2001 From: Philipp Meyer Date: Fri, 25 Jul 2014 15:43:54 +0200 Subject: [PATCH] Used Z3 API for transition invariants --- src/Main.hs | 10 ++--- src/Solver.hs | 16 +++++++- src/Solver/TransitionInvariant.hs | 67 ++++++++++++++++++------------- 3 files changed, 57 insertions(+), 36 deletions(-) diff --git a/src/Main.hs b/src/Main.hs index 89ff1578..04f78e39 100644 --- a/src/Main.hs +++ b/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 diff --git a/src/Solver.hs b/src/Solver.hs index 908097c7..8dfe39ef 100644 --- a/src/Solver.hs +++ b/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 diff --git a/src/Solver/TransitionInvariant.hs b/src/Solver/TransitionInvariant.hs index 143d5a9b..825a7827 100644 --- a/src/Solver/TransitionInvariant.hs +++ b/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) -- GitLab