Commit ac5befda authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Added new refinement for liveness properties

parent 55841da8
......@@ -22,7 +22,7 @@ executable slapnet
other-modules:
-- other-extensions:
build-depends: base >=4 && <5, sbv, parsec, containers, transformers,
bytestring
bytestring, mtl
hs-source-dirs: src
default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000
......@@ -30,6 +30,7 @@ import Solver
import Solver.StateEquation
import Solver.TrapConstraints
import Solver.TransitionInvariant
import Solver.SubnetEmptyTrap
--import Solver.LivenessInvariant
--import Solver.SComponent
--import Solver.CommFreeReachability
......@@ -431,58 +432,53 @@ checkProperty verbosity net refine invariant p = do
checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
Formula Place -> IO PropResult
checkSafetyProperty verbosity net refine invariant f =
-- TODO: add flag for this kind of structural check
--if checkCommunicationFree net then do
-- verbosePut verbosity 1 "Net found to be communication-free"
-- checkSafetyPropertyByCommFree verbosity net f
--else
do
r <- checkSafetyPropertyBySafetyRef verbosity net refine f []
if r == Satisfied && invariant then
-- TODO: add invariant generation
error "Invariant generation for safety properties not yet supported"
else
return r
{-
checkSafetyPropertyByCommFree :: Int -> PetriNet -> Formula -> IO PropResult
checkSafetyPropertyByCommFree verbosity net f = do
r <- checkSat $ checkCommFreeReachabilitySat net f
checkSafetyProperty verbosity net refine invariant f = do
r <- checkSafetyProperty' verbosity net refine f []
case r of
Nothing -> return Satisfied
Just a -> do
verbosePut verbosity 1 "Assignment found"
verbosePut verbosity 3 $ "Assignment: " ++ show a
return Unsatisfied
-}
checkSafetyPropertyBySafetyRef :: Int -> PetriNet -> Bool ->
Formula Place -> [Trap] -> IO PropResult
checkSafetyPropertyBySafetyRef verbosity net refine f traps = do
(Nothing, _) ->
if invariant then
-- TODO: add invariant generation
error "Invariant generation for safety properties not yet supported"
else
return Satisfied
(Just _, _) ->
return Unknown
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
case r of
Nothing -> return Satisfied
Just marking -> do
if refine then do
rt <- checkSat verbosity $ checkTrapSat net marking
case rt of
Nothing -> do
verbosePut verbosity 1 "No trap found."
return Unknown
Just trap -> do
checkSafetyPropertyBySafetyRef verbosity net
refine f (trap:traps)
Nothing -> return (Nothing, traps)
Just m ->
if refine then
refineSafetyProperty verbosity net f traps m
else
return Unknown
return (Just m, traps)
refineSafetyProperty :: Int -> PetriNet ->
Formula Place -> [Trap] -> Marking -> IO (Maybe Marking, [Trap])
refineSafetyProperty verbosity net f traps m = do
r <- checkSat verbosity $ checkTrapSat net m
case r of
Nothing -> do
return $ (Just m, traps)
Just trap -> do
checkSafetyProperty' verbosity net True f (trap:traps)
checkLivenessProperty :: Int -> PetriNet -> Bool -> Bool ->
Formula Transition -> IO PropResult
checkLivenessProperty verbosity net refine invariant f = do
(r, comps) <- checkLivenessPropertyByRef verbosity net refine f []
return r
--if r == Satisfied && invariant then
-- generateLivenessInvariant verbosity net f comps
--else
-- return r
r <- checkLivenessProperty' verbosity net refine f []
case r of
(Nothing, _) ->
if invariant then
-- TODO: add invariant generation
error "Invariant generation for liveness properties not yet supported"
else
return Satisfied
(Just _, _) ->
return Unknown
{-
generateLivenessInvariant :: Int -> PetriNet ->
Formula -> [SCompCut] -> IO PropResult
......@@ -497,23 +493,51 @@ generateLivenessInvariant verbosity net f comps = do
mapM_ print inv
return Satisfied
-}
checkLivenessPropertyByRef :: Int -> PetriNet -> Bool ->
Formula Transition -> [Cut] -> IO (PropResult, [Cut])
checkLivenessPropertyByRef verbosity net refine f cuts = do
checkLivenessProperty' :: Int -> PetriNet -> Bool ->
Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
checkLivenessProperty' verbosity net refine f cuts = do
r <- checkSat verbosity $ checkTransitionInvariantSat net f cuts
case r of
Nothing -> return (Satisfied, cuts)
Nothing -> return (Nothing, cuts)
Just x -> do
if refine then do
rt <- return Nothing -- checkSat $ checkSComponentSat net x
rt <- findLivenessRefinement verbosity net
(initialMarking net) x []
case rt of
Nothing -> do
return (Unknown, cuts)
return (Just x, cuts)
Just cut -> do
checkLivenessPropertyByRef verbosity net refine f
(cut:cuts)
checkLivenessProperty' verbosity net refine f
(cut:cuts)
else
return (Unknown, cuts)
return (Just x, cuts)
findLivenessRefinement :: Int -> PetriNet -> Marking -> FiringVector ->
[Trap] -> IO (Maybe Cut)
findLivenessRefinement verbosity net m x traps = do
r <- checkSat verbosity $ checkSubnetEmptyTrapSat net m x
case r of
Nothing -> do
rm <- refineSafetyProperty verbosity net FTrue traps m
case rm of
(Nothing, _) ->
return $ Just $ generateLivenessRefinement
net x traps
(Just _, _) ->
return Nothing
Just trap -> do
rm <- checkSafetyProperty' verbosity net False FTrue (trap:traps)
case rm of
(Nothing, _) ->
return $ Just $ generateLivenessRefinement
net x (trap:traps)
(Just m', _) ->
findLivenessRefinement verbosity net m' x (trap:traps)
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 =
......
......@@ -2,18 +2,18 @@
{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
module PetriNet
(PetriNet,Place(..),Transition(..),Marking,buildVector,
value,elems,items,makeVector,FiringVector,
(PetriNet,Place(..),Transition(..),Marking,FiringVector,
renamePlace,renameTransition,renamePetriNetPlacesAndTransitions,
name,showNetName,places,transitions,initialMarking,initial,initials,linitials,
pre,lpre,post,lpost,context,ghostTransitions,
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans,makePetriNetWith,Trap,Cut)
where
import qualified Data.Map as M
import Data.List (intercalate)
import Control.Arrow (first)
import Util
newtype Place = Place String deriving (Ord,Eq)
newtype Transition = Transition String deriving (Ord,Eq)
......@@ -24,16 +24,24 @@ instance Show Transition where
type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])
class Nodes a b | a -> b where
pre :: (Ord a) => PetriNet -> a -> [b]
pre net = map fst . fst . context net
post :: (Ord a) => PetriNet -> a -> [b]
post net = map fst . snd . context net
lpre :: (Ord a) => PetriNet -> a -> [(b, Integer)]
class (Ord a, Ord b) => Nodes a b | a -> b where
lpre :: PetriNet -> a -> [(b, Integer)]
lpre net = fst . context net
lpost :: (Ord a) => PetriNet -> a -> [(b, Integer)]
lpost :: PetriNet -> a -> [(b, Integer)]
lpost net = snd . context net
context :: (Ord a) => PetriNet -> a -> ([(b, Integer)], [(b, Integer)])
pre :: PetriNet -> a -> [b]
pre net = map fst . lpre net
post :: PetriNet -> a -> [b]
post net = map fst . lpost net
lmpre :: PetriNet -> [a] -> [(b, Integer)]
lmpre net = nubOrdBy fst . concatMap (lpre net)
lmpost :: PetriNet -> [a] -> [(b, Integer)]
lmpost net = nubOrdBy fst . concatMap (lpost net)
mpre :: PetriNet -> [a] -> [b]
mpre net = map fst . lmpre net
mpost :: PetriNet -> [a] -> [b]
mpost net = map fst . lmpost net
context :: PetriNet -> a -> ([(b, Integer)], [(b, Integer)])
context net x = M.findWithDefault ([],[]) x (contextMap net)
contextMap :: PetriNet -> ContextMap a b
......@@ -42,32 +50,9 @@ instance Nodes Place Transition where
instance Nodes Transition Place where
contextMap = adjacencyT
newtype Vector a = Vector { getVector :: M.Map a Integer }
type Marking = Vector Place
type FiringVector = Vector Transition
instance (Show a) => Show (Vector a) where
show (Vector v) =
"[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
where showEntry (v,x) =
show v ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
value :: (Ord a) => Vector a -> a -> Integer
value v x = M.findWithDefault 0 x (getVector v)
elems :: (Ord a) => Vector a -> [a]
elems = M.keys . getVector
items :: Vector a -> [(a,Integer)]
items = M.toList . getVector
buildVector :: (Ord a) => [(a, Integer)] -> Vector a
buildVector = makeVector . M.fromList
makeVector :: (Ord a) => M.Map a Integer -> Vector a
makeVector = Vector . M.filter (/=0)
type Trap = [Place]
type Cut = ([[Transition]], [Transition])
......@@ -123,13 +108,14 @@ renamePetriNetPlacesAndTransitions f net =
adjacencyP net,
adjacencyT = mapAdjacency (renameTransition f) (renamePlace f) $
adjacencyT net,
initialMarking = Vector $
M.mapKeys (renamePlace f) $ getVector $ initialMarking net,
initialMarking = vmap (renamePlace f) $ initialMarking net,
ghostTransitions = map (renameTransition f) $ ghostTransitions net
}
where mapAdjacency f g m = M.mapKeys f (M.map (mapContext g) m)
mapContext f (pre, post) = (map (first f) pre, map (first f) post)
-- TODO: better constructors, only one main constructor
-- TODO: enforce sorted lists
makePetriNet :: String -> [String] -> [String] ->
[(String, String, Integer)] ->
[(String, Integer)] -> [String] -> PetriNet
......@@ -163,7 +149,6 @@ makePetriNet name places transitions arcs initial gs =
" both places or transitions"
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
-- TODO: better constructors
makePetriNetWith :: String -> [Place] ->
[(Transition, ([(Place, Integer)], [(Place, Integer)]))] ->
[(Place, Integer)] -> [Transition] -> PetriNet
......
......@@ -5,7 +5,6 @@ module Solver
getNames,makeVarMap,makeVarMapWith,
IntConstraint,BoolConstraint,IntResult,BoolResult,
Model,ConstraintProblem)
--mVal,mValues,mElemsWith,mElemSum,SModel(..),CModel(..))
where
import Data.SBV
......
......@@ -5,6 +5,7 @@ where
import Data.SBV
import Control.Monad
import Util
import PetriNet
import Property
import Solver
......
module Solver.SubnetEmptyTrap
(checkSubnetEmptyTrapSat)
where
import Data.SBV
import Control.Monad
import qualified Data.Map as M
import Util
import PetriNet
import Solver
subnetTrapConstraints :: PetriNet -> Marking -> FiringVector ->
VarMap Place -> BoolConstraint
subnetTrapConstraints net m x b =
liftM bAnd $ mapM trapConstraint $ elems x
where placeConstraints = mapM (val b) . filter (\p -> value m p == 0)
trapConstraint t = do
cPre <- placeConstraints $ pre net t
cPost <- placeConstraints $ post net t
return $ bOr cPre ==> bOr cPost
properTrap :: VarMap Place -> BoolConstraint
properTrap b = liftM bOr $ vals b
checkSubnetEmptyTrap :: PetriNet -> Marking -> FiringVector ->
VarMap Place -> BoolConstraint
checkSubnetEmptyTrap net m x b = do
c1 <- subnetTrapConstraints net m x b
c2 <- properTrap b
return $ c1 &&& c2
checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector ->
ConstraintProblem Bool Trap
checkSubnetEmptyTrapSat net m x =
let b = makeVarMap $ filter (\p -> value m p == 0) $ mpost net $ elems x
in ("subnet empty trap constraints", "trap",
getNames b,
checkSubnetEmptyTrap net m x b,
trapFromAssignment b)
trapFromAssignment :: VarMap Place -> BoolResult Trap
trapFromAssignment b = do
bm <- valMap b
return $ M.keys $ M.filter id bm
module Solver.TInvariantRefinement
(checkSComponent,checkSComponentSat,
getSComponentOutIn,
getSComponentCompsCut,
SCompCut)
where
import Data.SBV
import Data.List (partition)
import PetriNet
import Solver
checkEmptyPlaces :: PetriNet -> [String] -> ModelI -> ModelSI -> SBool
checkEmptyPlaces net fired ax m =
checkPrePostPlaces net m &&&
checkPrePostTransitions net m &&&
checkSubsetTransitions fired m &&&
checkNotEmpty fired m &&&
checkClosed net ax m &&&
checkTokens net m &&&
checkBinary m
checkEmptyPlacesSat :: PetriNet -> [String] -> [String] -> ModelI ->
([String], ModelSI -> SBool)
checkEmptyPlacesSat net ts' ps' ax =
(ps', checkEmptyPlaces net ts' ps' ax)
--getSComponentOutIn :: PetriNet -> ModelI -> ModelI -> ([String], [String])
--getSComponentOutIn net ax as =
-- partition (cElem ax) $ filter (cElem as) (transitions net)
-- TODO: use strongly connected components and min cuts
--getSComponentCompsCut :: PetriNet -> ModelI -> ModelI -> SCompCut
--getSComponentCompsCut net ax as =
-- let (t, u) = partition (cElem ax) $ filter (cElem as) (transitions net)
-- (t1, t2) = partition (cElem as . prime) t
-- in [(t1, True), (t2, True), (u, False)]
subnetPlaces :: PetriNet -> [String] -> [String]
subnetPlaces net ts' = filter checkPlace (places net)
where checkPlace p = any (`elem` ts') (pre net p ++ post net p)
......@@ -5,6 +5,7 @@ where
import Data.SBV
import Control.Monad
import Util
import PetriNet
import Property
import Solver
......@@ -52,8 +53,8 @@ checkTransitionInvariant net f cuts x = do
checkTransitionInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
ConstraintProblem Integer FiringVector
checkTransitionInvariantSat net f cuts =
let x = makeVarMap $ transitions net
in ("transition invariant constraints", "transition invariant",
let x = makeVarMap $ transitions net
in ("transition invariant constraints", "transition invariant",
getNames x,
checkTransitionInvariant net f cuts x,
firingVectorFromAssignment x)
......
......@@ -6,6 +6,7 @@ import Data.SBV
import Control.Monad
import qualified Data.Map as M
import Util
import PetriNet
import Solver
......
module Util
(verbosePut)
(verbosePut,Vector,value,elems,items,buildVector,makeVector,vmap,
nubOrd,nubOrdBy)
where
import qualified Data.Map as M
import Control.Monad
import Data.List
import Data.Ord
import Data.Function
verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
newtype Vector a = Vector { getVector :: M.Map a Integer }
instance (Show a) => Show (Vector a) where
show (Vector v) =
"[" ++ intercalate "," (map showEntry (M.toList v)) ++ "]"
where showEntry (i,x) =
show i ++ (if x /= 1 then "(" ++ show x ++ ")" else "")
vmap :: (Ord a, Ord b) => (a -> b) -> Vector a -> Vector b
vmap f (Vector m) = Vector $ M.mapKeys f m
value :: (Ord a) => Vector a -> a -> Integer
value v x = M.findWithDefault 0 x (getVector v)
elems :: (Ord a) => Vector a -> [a]
elems = M.keys . getVector
items :: Vector a -> [(a,Integer)]
items = M.toList . getVector
buildVector :: (Ord a) => [(a, Integer)] -> Vector a
buildVector = makeVector . M.fromList
makeVector :: (Ord a) => M.Map a Integer -> Vector a
makeVector = Vector . M.filter (/=0)
nubOrd :: (Ord a) => [a] -> [a]
nubOrd = nubOrdBy id
nubOrdBy :: (Ord b) => (a -> b) -> [a] -> [a]
nubOrdBy f = map head . groupBy ((==) `on` f) . sortBy (comparing f)
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