Commit 3c4fd698 authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Rewrote trap constraints

parent 6456c0fb
...@@ -12,6 +12,7 @@ import Control.Arrow (first) ...@@ -12,6 +12,7 @@ import Control.Arrow (first)
import Data.List (partition) import Data.List (partition)
import qualified Data.ByteString.Lazy as L import qualified Data.ByteString.Lazy as L
import Util
import Parser import Parser
import qualified Parser.PNET as PNET import qualified Parser.PNET as PNET
import qualified Parser.LOLA as LOLA import qualified Parser.LOLA as LOLA
...@@ -27,7 +28,7 @@ import Property ...@@ -27,7 +28,7 @@ import Property
import Structure import Structure
import Solver import Solver
import Solver.StateEquation import Solver.StateEquation
--import Solver.TrapConstraints import Solver.TrapConstraints
--import Solver.TransitionInvariant --import Solver.TransitionInvariant
--import Solver.LivenessInvariant --import Solver.LivenessInvariant
--import Solver.SComponent --import Solver.SComponent
...@@ -243,10 +244,6 @@ options = ...@@ -243,10 +244,6 @@ options =
"Show help" "Show help"
] ]
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
parseArgs :: IO (Either String (Options, [String])) parseArgs :: IO (Either String (Options, [String]))
parseArgs = do parseArgs = do
args <- getArgs args <- getArgs
...@@ -461,26 +458,19 @@ checkSafetyPropertyByCommFree verbosity net f = do ...@@ -461,26 +458,19 @@ checkSafetyPropertyByCommFree verbosity net f = do
checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool -> checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
Formula Place -> [Trap] -> IO PropResult Formula Place -> [Trap] -> IO PropResult
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
r <- checkSat $ checkStateEquationSat net f traps r <- checkSat verbosity $ checkStateEquationSat net f traps
case r of case r of
Nothing -> return Satisfied Nothing -> return Satisfied
Just assigned -> do Just marking -> do
verbosePut verbosity 1 "Assignment found"
verbosePut verbosity 2 $ "Places marked: " ++ show assigned
if refine then do if refine then do
rt <- return Nothing -- checkSat $ checkTrapSat net assigned rt <- checkSat verbosity $ checkTrapSat net marking
case rt of case rt of
Nothing -> do Nothing -> do
verbosePut verbosity 1 "No trap found." verbosePut verbosity 1 "No trap found."
return Unknown return Unknown
Just trap -> do Just trap -> do
-- let trap = trapFromAssignment at checkSafetyPropertyBySafetyRef verbosity net
verbosePut verbosity 1 "Trap found" refine f (trap:traps)
--verbosePut verbosity 2 $ "Places in trap: " ++
-- show trap
return Unknown
--checkSafetyPropertyBySafetyRef verbosity net
-- refine f (trap:traps)
else else
return Unknown return Unknown
{- {-
......
...@@ -3,13 +3,15 @@ ...@@ -3,13 +3,15 @@
module PetriNet module PetriNet
(PetriNet,Place(..),Transition(..),Marking,tokens,buildMarking, (PetriNet,Place(..),Transition(..),Marking,tokens,buildMarking,
marked,lmarked,makeMarking,
renamePlace,renameTransition,renamePetriNetPlacesAndTransitions, renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
name,showNetName,places,transitions,initial,initialMarking, name,showNetName,places,transitions,initial,initialMarking,
pre,lpre,post,lpost,initials,context,ghostTransitions, pre,lpre,post,lpost,initials,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans,makePetriNetWith) makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap)
where where
import qualified Data.Map as M import qualified Data.Map as M
import Data.List (intercalate)
import Control.Arrow (first) import Control.Arrow (first)
newtype Place = Place String deriving (Ord,Eq) newtype Place = Place String deriving (Ord,Eq)
...@@ -43,15 +45,27 @@ instance Nodes Transition Place where ...@@ -43,15 +45,27 @@ instance Nodes Transition Place where
newtype Marking = Marking { getMarking :: M.Map Place Integer } newtype Marking = Marking { getMarking :: M.Map Place Integer }
instance Show Marking where instance Show Marking where
show (Marking m) = show $ map showPlaceMarking $ M.toList m show (Marking m) =
"[" ++ intercalate "," (map showPlaceMarking (M.toList m)) ++ "]"
where showPlaceMarking (n,i) = where showPlaceMarking (n,i) =
show n ++ (if i /= 1 then "(" ++ show i ++ ")" else "") show n ++ (if i /= 1 then "(" ++ show i ++ ")" else "")
tokens :: Marking -> Place -> Integer tokens :: Marking -> Place -> Integer
tokens m p = M.findWithDefault 0 p (getMarking m) tokens m p = M.findWithDefault 0 p (getMarking m)
buildMarking :: [(String, Integer)] -> Marking buildMarking :: [(Place, Integer)] -> Marking
buildMarking xs = Marking $ M.fromList $ map (first Place) $ filter ((/=0) . snd) xs buildMarking = makeMarking . M.fromList
makeMarking :: M.Map Place Integer -> Marking
makeMarking = Marking . M.filter (/=0)
marked :: Marking -> [Place]
marked = M.keys . getMarking
lmarked :: Marking -> [(Place,Integer)]
lmarked = M.toList . getMarking
type Trap = [Place]
data PetriNet = PetriNet { data PetriNet = PetriNet {
name :: String, name :: String,
...@@ -121,7 +135,7 @@ makePetriNet name places transitions arcs initial gs = ...@@ -121,7 +135,7 @@ makePetriNet name places transitions arcs initial gs =
transitions = map Transition transitions, transitions = map Transition transitions,
adjacencyP = adP, adjacencyP = adP,
adjacencyT = adT, adjacencyT = adT,
initialMarking = buildMarking initial, initialMarking = buildMarking (map (first Place) initial),
ghostTransitions = map Transition gs ghostTransitions = map Transition gs
} }
where where
...@@ -159,7 +173,7 @@ makePetriNetWith name places ts initial gs = ...@@ -159,7 +173,7 @@ makePetriNetWith name places ts initial gs =
transitions = transitions, transitions = transitions,
adjacencyP = placeMap, adjacencyP = placeMap,
adjacencyT = M.fromList ts, adjacencyT = M.fromList ts,
initialMarking = Marking (M.fromList initial), initialMarking = buildMarking initial,
ghostTransitions = gs ghostTransitions = gs
} }
......
{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module Solver module Solver
(prime,checkSat,ModelReader,val,VarMap, (prime,checkSat,ModelReader,val,vals,VarMap,
getNames,makeVarMap,makeVarMapWith,varMapNames, getNames,makeVarMap,makeVarMapWith,
IntConstraint,BoolConstraint,IntResult,BoolResult, IntConstraint,BoolConstraint,IntResult,BoolResult,
Model(..),mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..)) Model,ConstraintProblem)
--mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M import qualified Data.Map as M
import Control.Monad.Reader import Control.Monad.Reader
import Control.Applicative
newtype Model a = Model { getMap :: M.Map String a } import Util
newtype VarMap a = VarMap { getVarMap :: M.Map a String }
getNames :: VarMap a -> [String] type Model a = M.Map String a
getNames = M.elems . getVarMap type VarMap a = M.Map a String
instance Show a => Show (Model a) where getNames :: VarMap a -> [String]
show = show . M.toList . getMap getNames = M.elems
type ModelReader a b = Reader (Model a) b type ModelReader a b = Reader (Model a) b
type IntConstraint = ModelReader SInteger SBool type IntConstraint = ModelReader SInteger SBool
...@@ -27,31 +26,36 @@ type BoolConstraint = ModelReader SBool SBool ...@@ -27,31 +26,36 @@ type BoolConstraint = ModelReader SBool SBool
type IntResult a = ModelReader Integer a type IntResult a = ModelReader Integer a
type BoolResult a = ModelReader Bool a type BoolResult a = ModelReader Bool a
type ConstraintProblem a b =
(String, String, [String], ModelReader (SBV a) SBool, ModelReader a b)
val :: (Ord a) => VarMap a -> a -> ModelReader b b val :: (Ord a) => VarMap a -> a -> ModelReader b b
val ma x = do val ma x = do
mb <- ask mb <- ask
return $ getMap mb M.! (getVarMap ma M.! x) return $ mb M.! (ma M.! x)
vals :: (Ord a) => VarMap a -> ModelReader b (M.Map a b)
vals ma = do
mb <- ask
return $ fmap (mb M.!) ma
makeVarMap :: (Show a, Ord a) => [a] -> VarMap a makeVarMap :: (Show a, Ord a) => [a] -> VarMap a
makeVarMap = makeVarMapWith id makeVarMap = makeVarMapWith id
makeVarMapWith :: (Show a, Ord a) => (String -> String) -> [a] -> VarMap a makeVarMapWith :: (Show a, Ord a) => (String -> String) -> [a] -> VarMap a
makeVarMapWith f xs = VarMap $ M.fromList $ xs `zip` map (f . show) xs makeVarMapWith f xs = M.fromList $ xs `zip` map (f . show) xs
varMapNames :: VarMap a -> [String]
varMapNames = M.elems . getVarMap
prime :: String -> String prime :: String -> String
prime = ('\'':) prime = ('\'':)
{-
mVal :: Model a -> String -> a mVal :: Model 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 m
mValues :: Model a -> [a] mValues :: Model a -> [a]
mValues m = M.elems $ getMap m mValues = M.elems
mElemsWith :: (a -> Bool) -> Model a -> [String] mElemsWith :: (a -> Bool) -> Model a -> [String]
mElemsWith f m = M.keys $ M.filter f $ getMap m mElemsWith f m = M.keys $ M.filter f m
mElemSum :: (Num a) => Model a -> [String] -> a mElemSum :: (Num a) => Model a -> [String] -> a
mElemSum m xs = sum $ map (mVal m) xs mElemSum m xs = sum $ map (mVal m) xs
...@@ -77,23 +81,32 @@ instance CModel Integer where ...@@ -77,23 +81,32 @@ instance CModel Integer where
instance CModel Bool where instance CModel Bool where
cElem = mVal cElem = mVal
cNotElem m x = not $ mVal m x cNotElem m x = not $ mVal m x
-}
symConstraints :: SymWord a => [String] -> ModelReader (SBV a) SBool -> symConstraints :: SymWord a => [String] -> ModelReader (SBV a) SBool ->
Symbolic SBool Symbolic SBool
symConstraints vars constraint = do symConstraints vars constraint = do
syms <- mapM exists vars syms <- mapM exists vars
return $ runReader constraint $ Model $ M.fromList $ vars `zip` syms return $ runReader constraint $ M.fromList $ vars `zip` syms
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) -> rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
Maybe (Model a) Maybe (Model a)
rebuildModel _ (Left _) = Nothing rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown" rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ Model $ M.fromList $ vars `zip` m rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m
checkSat :: (SatModel a, SymWord a) => checkSat :: (SatModel a, SymWord a, Show a, Show b) => Int ->
([String], ModelReader (SBV a) SBool, ModelReader a b) -> ConstraintProblem a b -> IO (Maybe b)
IO (Maybe b) checkSat verbosity (problemName, resultName, vars, constraint, interpretation) = do
checkSat (vars, constraint, interpretation) = do verbosePut verbosity 1 $ "Checking SAT of " ++ problemName
result <- satWith z3{verbose=False} $ symConstraints vars constraint result <- satWith z3{verbose=verbosity >= 4} $
return $ runReader interpretation <$> rebuildModel vars (getModel result) 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
module Solver.StateEquation module Solver.StateEquation
(checkStateEquation,checkStateEquationSat, (checkStateEquationSat)
markedPlacesFromAssignment,Trap)
where where
import Data.SBV import Data.SBV
...@@ -11,8 +10,6 @@ import Property ...@@ -11,8 +10,6 @@ import Property
import Solver import Solver
import Solver.Formula import Solver.Formula
type Trap = [Place]
placeConstraints :: PetriNet -> VarMap Place -> VarMap Transition -> IntConstraint placeConstraints :: PetriNet -> VarMap Place -> VarMap Transition -> IntConstraint
placeConstraints net m x = placeConstraints net m x =
liftM bAnd $ mapM checkPlaceEquation $ places net liftM bAnd $ mapM checkPlaceEquation $ places net
...@@ -55,16 +52,16 @@ checkStateEquation net f m x traps = do ...@@ -55,16 +52,16 @@ checkStateEquation net f m x traps = do
return $ c1 &&& c2 &&& c3 &&& c4 return $ c1 &&& c2 &&& c3 &&& c4
checkStateEquationSat :: PetriNet -> Formula Place -> [Trap] -> checkStateEquationSat :: PetriNet -> Formula Place -> [Trap] ->
([String], IntConstraint, IntResult Trap) ConstraintProblem Integer Marking
checkStateEquationSat net f traps = checkStateEquationSat net f traps =
let m = makeVarMap $ places net let m = makeVarMap $ places net
x = makeVarMap $ transitions net x = makeVarMap $ transitions net
in (getNames m ++ getNames x, in ("state equation", "marking",
getNames m ++ getNames x,
checkStateEquation net f m x traps, checkStateEquation net f m x traps,
markedPlacesFromAssignment net m) markingFromAssignment m)
markedPlacesFromAssignment :: PetriNet -> markingFromAssignment :: VarMap Place -> IntResult Marking
VarMap Place -> IntResult [Place] markingFromAssignment m =
markedPlacesFromAssignment net m = liftM makeMarking (vals m)
filterM (liftM (> 0) . val m) $ places net
module Solver.TrapConstraints module Solver.TrapConstraints
(checkTrap,checkTrapSat, (checkTrapSat)
trapFromAssignment
)
where where
import Data.SBV import Data.SBV
import Control.Monad
import qualified Data.Map as M
import PetriNet import PetriNet
import Solver import Solver
trapConstraints :: PetriNet -> ModelSB -> SBool trapConstraints :: PetriNet -> VarMap Place -> BoolConstraint
trapConstraints net m = trapConstraints net b =
bAnd $ map trapConstraint $ transitions net liftM bAnd $ mapM trapConstraint $ transitions net
where trapConstraint t = where trapConstraint t = do
bOr (map (mElem m) $ pre net t) ==> bOr (map (mElem m) $ post net t) cPre <- mapM (val b) $ pre net t
cPost <- mapM (val b) $ post net t
trapInitiallyMarked :: PetriNet -> ModelSB -> SBool return $ bOr cPre ==> bOr cPost
trapInitiallyMarked net m =
let marked = map fst $ filter (( > 0) . snd) $ initials net trapInitiallyMarked :: PetriNet -> VarMap Place -> BoolConstraint
in bOr $ map (mElem m) marked trapInitiallyMarked net b =
liftM bOr $ mapM (val b) $ marked $ initialMarking net
trapUnassigned :: [String] -> ModelSB -> SBool
trapUnassigned assigned m = bAnd $ map (mNotElem m) assigned trapUnassigned :: Marking -> VarMap Place -> BoolConstraint
trapUnassigned m b =
checkTrap :: PetriNet -> [String] -> ModelSB -> SBool liftM bAnd $ mapM (liftM bnot . val b) $ marked m
checkTrap net assigned m =
trapConstraints net m &&& checkTrap :: PetriNet -> Marking -> VarMap Place -> BoolConstraint
trapInitiallyMarked net m &&& checkTrap net m b = do
trapUnassigned assigned m c1 <- trapConstraints net b
c2 <- trapInitiallyMarked net b
checkTrapSat :: PetriNet -> [String] -> ([String], ModelSB -> SBool) c3 <- trapUnassigned m b
checkTrapSat net assigned = return $ c1 &&& c2 &&& c3
(places net, checkTrap net assigned)
checkTrapSat :: PetriNet -> Marking -> ConstraintProblem Bool Trap
trapFromAssignment :: ModelB -> [String] checkTrapSat net m =
trapFromAssignment = mElemsWith id let b = makeVarMap $ places net
in ("trap constraints", "trap",
getNames b,
checkTrap net m b,
trapFromAssignment b)
trapFromAssignment :: VarMap Place -> BoolResult Trap
trapFromAssignment b = do
ps <- vals b
return $ M.keys $ M.filter id ps
module Util
(verbosePut)
where
import Control.Monad
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
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