Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

Commit 30287c06 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Used Z3 API for trap constraints

parent 6a216738
...@@ -24,6 +24,9 @@ import qualified Printer.SARA as SARAPrinter ...@@ -24,6 +24,9 @@ import qualified Printer.SARA as SARAPrinter
import Property import Property
import Solver import Solver
import Solver.StateEquation import Solver.StateEquation
import Solver.TrapConstraints
--import Solver.TransitionInvariant
--import Solver.SComponent
data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read) data InputFormat = PNET | LOLA | TPN | MIST deriving (Show,Read)
...@@ -221,7 +224,7 @@ transformNet (net, props) TerminationByReachability = ...@@ -221,7 +224,7 @@ transformNet (net, props) TerminationByReachability =
ps = ["'sigma", "'m1", "'m2"] ++ ps = ["'sigma", "'m1", "'m2"] ++
places net ++ map prime (places net) places net ++ map prime (places net)
is = [("'m1", 1)] ++ is = [("'m1", 1)] ++
initials net ++ map (first prime) (initials net) linitials net ++ map (first prime) (linitials net)
transformTransition t = transformTransition t =
let (preT, postT) = context net t let (preT, postT) = context net t
pre' = [("'m1",1)] ++ preT ++ map (first prime) preT pre' = [("'m1",1)] ++ preT ++ map (first prime) preT
...@@ -245,7 +248,7 @@ transformNet (net, props) TerminationByReachability = ...@@ -245,7 +248,7 @@ transformNet (net, props) TerminationByReachability =
transformNet (net, props) ValidateIdentifiers = transformNet (net, props) ValidateIdentifiers =
let ps = map validateId $ places net let ps = map validateId $ places net
ts = map validateId $ transitions net ts = map validateId $ transitions net
is = map (first validateId) $ initials net is = map (first validateId) $ linitials net
as = map (\(a,b,x) -> (validateId a, validateId b, x)) $ arcs net as = map (\(a,b,x) -> (validateId a, validateId b, x)) $ arcs net
gs = map validateId $ ghostTransitions net gs = map validateId $ ghostTransitions net
net' = makePetriNet (name net) ps ts as is gs net' = makePetriNet (name net) ps ts as is gs
...@@ -289,6 +292,7 @@ checkProperty verbosity net refine p = do ...@@ -289,6 +292,7 @@ checkProperty verbosity net refine p = do
verbosePut verbosity 3 $ show p verbosePut verbosity 3 $ show p
r <- case ptype p of r <- case ptype p of
Safety -> checkSafetyProperty verbosity net refine (pformula p) [] Safety -> checkSafetyProperty verbosity net refine (pformula p) []
Liveness -> checkLivenessProperty verbosity net refine (pformula p) []
verbosePut verbosity 0 $ showPropertyName p ++ verbosePut verbosity 0 $ showPropertyName p ++
if r then " is satisfied." if r then " is satisfied."
else " may not be satisfied." else " may not be satisfied."
...@@ -305,7 +309,51 @@ checkSafetyProperty verbosity net refine f traps = do ...@@ -305,7 +309,51 @@ checkSafetyProperty verbosity net refine f traps = do
verbosePut verbosity 1 "Assignment found" verbosePut verbosity 1 "Assignment found"
verbosePut verbosity 2 $ "Places marked: " ++ show assigned verbosePut verbosity 2 $ "Places marked: " ++ show assigned
verbosePut verbosity 3 $ "Assignment: " ++ show a verbosePut verbosity 3 $ "Assignment: " ++ show a
return False if refine then do
rt <- checkSatBool $ checkTrapSat net assigned
case rt of
Nothing -> do
verbosePut verbosity 1 "No trap found."
return False
Just at -> do
let trap = trapFromAssignment at
verbosePut verbosity 1 "Trap found"
verbosePut verbosity 2 $ "Places in trap: " ++
show trap
verbosePut verbosity 3 $ "Trap assignment: " ++
show at
checkSafetyProperty verbosity net refine f
(trap:traps)
else
return False
checkLivenessProperty :: Int -> PetriNet -> Bool ->
Formula -> [([String],[String])] -> IO Bool
checkLivenessProperty verbosity net refine f strans = do
r <- return Nothing -- checkSatInt $ checkTransitionInvariantSat net f strans
case r of
Nothing -> return True
Just ax -> do
let fired = [] -- firedTransitionsFromAssignment ax
verbosePut verbosity 1 "Assignment found"
-- 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
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
checkLivenessProperty verbosity net refine f
(sOutIn:strans)
else
return False
main :: IO () main :: IO ()
main = do main = do
......
...@@ -2,7 +2,7 @@ ...@@ -2,7 +2,7 @@
module PetriNet module PetriNet
(PetriNet,name,showNetName,places,transitions,initial, (PetriNet,name,showNetName,places,transitions,initial,
pre,lpre,post,lpost,initials,context,arcs,ghostTransitions, pre,lpre,post,lpost,initials,linitials,context,arcs,ghostTransitions,
makePetriNet,makePetriNetWithTrans) makePetriNet,makePetriNetWithTrans)
where where
...@@ -39,8 +39,11 @@ post net = map fst . snd . context net ...@@ -39,8 +39,11 @@ post net = map fst . snd . context net
lpost :: PetriNet -> String -> [(String, Integer)] lpost :: PetriNet -> String -> [(String, Integer)]
lpost net = snd . context net lpost net = snd . context net
initials :: PetriNet -> [(String,Integer)] initials :: PetriNet -> [String]
initials net = M.toList (initMap net) initials net = M.keys (initMap net)
linitials :: PetriNet -> [(String,Integer)]
linitials net = M.toList (initMap net)
showNetName :: PetriNet -> String showNetName :: PetriNet -> String
showNetName net = "Petri net" ++ showNetName net = "Petri net" ++
......
...@@ -18,7 +18,7 @@ renderNet net = ...@@ -18,7 +18,7 @@ renderNet net =
ps = "PLACE " <> intercalate "," ps = "PLACE " <> intercalate ","
(map stringUtf8 (places net)) <> ";\n" (map stringUtf8 (places net)) <> ";\n"
is = "MARKING " <> intercalate "," is = "MARKING " <> intercalate ","
(map showWeight (initials net)) <> ";\n" (map showWeight (linitials net)) <> ";\n"
makeTransition t = makeTransition t =
let (preT,postT) = context net t let (preT,postT) = context net t
preS = "CONSUME " <> intercalate "," preS = "CONSUME " <> intercalate ","
......
...@@ -50,7 +50,7 @@ renderProperty filename net (Property propname Safety f) = ...@@ -50,7 +50,7 @@ renderProperty filename net (Property propname Safety f) =
"FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename))) "FILE " <> stringUtf8 (reverse (takeWhile (/='/') (reverse filename)))
<> " TYPE LOLA;\n" <> <> " TYPE LOLA;\n" <>
"INITIAL " <> intercalate "," "INITIAL " <> intercalate ","
(map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (initials net)) (map (\(p,i) -> stringUtf8 p <> ":" <> integerDec i) (linitials net))
<> ";\n" <> <> ";\n" <>
"FINAL COVER;\n" <> "FINAL COVER;\n" <>
"CONSTRAINTS " <> renderFormula f <> ";" "CONSTRAINTS " <> renderFormula f <> ";"
......
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Solver module Solver
(checkSat,checkSatInt,MModelS,MModelI,MModelB, (checkSat,checkSatInt,checkSatBool,MModelS,MModelI,MModelB,
MModel(..),mVal,mValues,mElemsWith,mElemSum,CModel(..)) MModel(..),mVal,mValues,mElemsWith,mElemSum,CModel(..),
Z3Type(..),mkOr',mkAnd')
where where
import Z3.Monad import Z3.Monad
import qualified Data.Map as M
import Control.Monad import Control.Monad
import qualified Data.Map as M
newtype MModel a = MModel { getMap :: M.Map String a } newtype MModel a = MModel { getMap :: M.Map String a }
...@@ -16,15 +17,22 @@ instance Show a => Show (MModel a) where ...@@ -16,15 +17,22 @@ instance Show a => Show (MModel a) where
type MModelS = MModel AST type MModelS = MModel AST
type MModelI = MModel Integer type MModelI = MModel Integer
type MModelB = MModel Bool type MModelB = MModel (Maybe Bool)
class Z3Type a where class Z3Type a where
mkConcrete :: a -> Z3 AST mkVal :: a -> Z3 AST -- TODO: needed?
getConcrete :: AST -> Z3 a getVal :: AST -> Z3 a
instance Z3Type Integer where instance Z3Type Integer where
mkConcrete = mkInt mkVal = mkInt
getConcrete = getInt getVal = getInt
instance Z3Type (Maybe Bool) where
mkVal x = case x of
Nothing -> error "can not make undefined constant"
Just True -> mkTrue
Just False -> mkFalse
getVal = getBool
mVal :: MModel a -> String -> a mVal :: MModel a -> String -> a
mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x (getMap m) mVal m x = M.findWithDefault (error ("key not found: " ++ x)) x (getMap m)
...@@ -38,6 +46,14 @@ mElemsWith f m = M.keys $ M.filter f $ getMap m ...@@ -38,6 +46,14 @@ mElemsWith f m = M.keys $ M.filter f $ getMap m
mElemSum :: (Num a) => MModel a -> [String] -> a mElemSum :: (Num a) => MModel a -> [String] -> a
mElemSum m xs = sum $ map (mVal m) xs mElemSum m xs = sum $ map (mVal m) xs
mkOr' :: [AST] -> Z3 AST
mkOr' [] = mkFalse
mkOr' xs = mkOr xs
mkAnd' :: [AST] -> Z3 AST
mkAnd' [] = mkTrue
mkAnd' xs = mkAnd xs
--class SMModel a where --class SMModel a where
-- mElem :: MModel a -> String -> Z3 AST -- mElem :: MModel a -> String -> Z3 AST
-- mNotElem :: MModel a -> String -> Z3 AST -- mNotElem :: MModel a -> String -> Z3 AST
...@@ -74,7 +90,7 @@ checkSat mkSort (vars, constraint) = do ...@@ -74,7 +90,7 @@ checkSat mkSort (vars, constraint) = do
ms <- evalT m syms ms <- evalT m syms
case ms of case ms of
Just xs -> do Just xs -> do
vals <- mapM getConcrete xs vals <- mapM getVal xs
let cmodel = MModel $ M.fromList $ vars `zip` vals let cmodel = MModel $ M.fromList $ vars `zip` vals
return $ Just cmodel return $ Just cmodel
Nothing -> error "Prover returned incomplete model" Nothing -> error "Prover returned incomplete model"
...@@ -83,4 +99,7 @@ checkSat mkSort (vars, constraint) = do ...@@ -83,4 +99,7 @@ checkSat mkSort (vars, constraint) = do
(Sat, Nothing) -> error "Prover returned sat but no model" (Sat, Nothing) -> error "Prover returned sat but no model"
checkSatInt :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel Integer)) checkSatInt :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel Integer))
checkSatInt problem = evalZ3 $ checkSat mkIntSort problem checkSatInt = evalZ3 . checkSat mkIntSort
checkSatBool :: ([String], MModel AST -> Z3 ()) -> IO (Maybe (MModel (Maybe Bool)))
checkSatBool = evalZ3 . checkSat mkBoolSort
...@@ -9,7 +9,7 @@ import Solver ...@@ -9,7 +9,7 @@ import Solver
evaluateTerm :: Term -> MModelS -> Z3 AST evaluateTerm :: Term -> MModelS -> Z3 AST
evaluateTerm (Var x) m = return $ mVal m x evaluateTerm (Var x) m = return $ mVal m x
evaluateTerm (Const c) _ = mkInt c evaluateTerm (Const c) _ = mkVal c
evaluateTerm (Minus t) m = mkUnaryMinus =<< evaluateTerm t m evaluateTerm (Minus t) m = mkUnaryMinus =<< evaluateTerm t m
evaluateTerm (t :+: u) m = evalBinaryTerm m mkAdd t u evaluateTerm (t :+: u) m = evalBinaryTerm m mkAdd t u
evaluateTerm (t :-: u) m = evalBinaryTerm m mkSub t u evaluateTerm (t :-: u) m = evalBinaryTerm m mkSub t u
......
...@@ -16,20 +16,20 @@ placeConstraints net m = mapM_ (assertCnstr <=< checkPlaceEquation) $ places net ...@@ -16,20 +16,20 @@ placeConstraints net m = mapM_ (assertCnstr <=< checkPlaceEquation) $ places net
where checkPlaceEquation p = do where checkPlaceEquation p = do
incoming <- mapM (addTransition 1 ) $ lpre net p incoming <- mapM (addTransition 1 ) $ lpre net p
outgoing <- mapM (addTransition (-1)) $ lpost net p outgoing <- mapM (addTransition (-1)) $ lpost net p
pinit <- mkInt $ initial net p pinit <- mkVal $ initial net p
sums <- mkAdd (pinit:(incoming ++ outgoing)) sums <- mkAdd (pinit:(incoming ++ outgoing))
mkEq sums (mVal m p) mkEq sums (mVal m p)
addTransition fac (t,w) = addTransition fac (t,w) =
mkInt (fac*w) >>= \w' -> mkMul [w', mVal m t] mkVal (fac*w) >>= \w' -> mkMul [w', mVal m t]
nonnegativityConstraints :: MModelS -> Z3 () nonnegativityConstraints :: MModelS -> Z3 ()
nonnegativityConstraints m = mapM_ (assertCnstr <=< geZero) $ mValues m nonnegativityConstraints m = mapM_ (assertCnstr <=< geZero) $ mValues m
where geZero v = mkGe v =<< mkInt (0::Integer) where geZero v = mkGe v =<< mkVal (0::Integer)
checkTraps :: [[String]] -> MModelS -> Z3 () checkTraps :: [[String]] -> MModelS -> Z3 ()
checkTraps traps m = mapM_ (assertCnstr <=< checkTrap) traps checkTraps traps m = mapM_ (assertCnstr <=< checkTrap) traps
where checkTrap trap = mkAdd (map (mVal m) trap) >>= where checkTrap trap = mkAdd (map (mVal m) trap) >>=
(\v -> mkGe v =<< mkInt (1::Integer)) (\v -> mkGe v =<< mkVal (1::Integer))
checkStateEquation :: PetriNet -> Formula -> [[String]] -> MModelS -> Z3 () checkStateEquation :: PetriNet -> Formula -> [[String]] -> MModelS -> Z3 ()
checkStateEquation net f traps m = do checkStateEquation net f traps m = do
......
...@@ -4,35 +4,36 @@ module Solver.TrapConstraints ...@@ -4,35 +4,36 @@ module Solver.TrapConstraints
) )
where where
import Data.SBV import Z3.Monad
import Control.Monad
import PetriNet import PetriNet
import Solver import Solver
trapConstraints :: PetriNet -> ModelSB -> SBool trapConstraints :: PetriNet -> MModelS -> Z3 ()
trapConstraints net m = trapConstraints net m = mapM_ (assertCnstr <=< trapConstraint) $ transitions net
bAnd $ map trapConstraint $ transitions net where trapConstraint t = do
where trapConstraint t = lhs <- mkOr' (map (mVal m) $ pre net t)
bOr (map (mElem m) $ pre net t) ==> bOr (map (mElem m) $ post net t) rhs <- mkOr' (map (mVal m) $ post net t)
mkImplies lhs rhs
trapInitiallyMarked :: PetriNet -> ModelSB -> SBool trapInitiallyMarked :: PetriNet -> MModelS -> Z3 ()
trapInitiallyMarked net m = trapInitiallyMarked net m = assertCnstr =<< mkOr' (map (mVal m) (initials net))
let marked = map fst $ filter (( > 0) . snd) $ initials net
in bOr $ map (mElem m) marked
trapUnassigned :: [String] -> ModelSB -> SBool trapUnassigned :: [String] -> MModelS -> Z3 ()
trapUnassigned assigned m = bAnd $ map (mNotElem m) assigned trapUnassigned assigned m = mapM_ (assertCnstr <=< (mkNot . mVal m)) assigned
checkTrap :: PetriNet -> [String] -> ModelSB -> SBool checkTrap :: PetriNet -> [String] -> MModelS -> Z3 ()
checkTrap net assigned m = checkTrap net assigned m = do
trapConstraints net m &&& trapConstraints net m
trapInitiallyMarked net m &&& trapInitiallyMarked net m
trapUnassigned assigned m trapUnassigned assigned m
checkTrapSat :: PetriNet -> [String] -> ([String], ModelSB -> SBool) checkTrapSat :: PetriNet -> [String] -> ([String], MModelS -> Z3 ())
checkTrapSat net assigned = checkTrapSat net assigned =
(places net, checkTrap net assigned) (places net, checkTrap net assigned)
trapFromAssignment :: ModelB -> [String] trapFromAssignment :: MModelB -> [String]
trapFromAssignment = mElemsWith id trapFromAssignment = mElemsWith (\x -> case x of Just True -> True
_ -> False )
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment