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

Added invariant generation for safety properties

parent 46c2f0be
......@@ -32,6 +32,7 @@ import Solver.TrapConstraints
import Solver.TransitionInvariant
import Solver.SubnetEmptyTrap
import Solver.LivenessInvariant
import Solver.SafetyInvariant
import Solver.SComponent
--import Solver.CommFreeReachability
......@@ -435,10 +436,17 @@ checkSafetyProperty :: Int -> PetriNet -> Bool -> Bool ->
checkSafetyProperty verbosity net refine invariant f = do
r <- checkSafetyProperty' verbosity net refine f []
case r of
(Nothing, _) ->
if invariant then
-- TODO: add invariant generation
error "Invariant generation for safety properties not yet supported"
(Nothing, traps) ->
if invariant then do
r' <- checkSat verbosity $ checkSafetyInvariantSat net f traps
case r' of
Nothing -> do
verbosePut verbosity 0 "No invariant found"
return Unknown
Just inv -> do
verbosePut verbosity 0 "Invariant found"
mapM_ print inv
return Satisfied
else
return Satisfied
(Just _, _) ->
......@@ -487,21 +495,6 @@ checkLivenessProperty verbosity net refine invariant f = do
(Just _, _) ->
return Unknown
{-
generateLivenessInvariant :: Int -> PetriNet ->
Formula -> [SCompCut] -> IO PropResult
generateLivenessInvariant verbosity net f comps = do
verbosePut verbosity 1 "Generating invariant"
let cuts = generateCuts f comps
r <- checkSat $ checkLivenessInvariantSat net cuts
case r of
Nothing -> return Unsatisfied
Just as -> do
let inv = getLivenessInvariant net cuts as
mapM_ print inv
return Satisfied
-}
checkLivenessProperty' :: Int -> PetriNet -> Bool ->
Formula Transition -> [Cut] -> IO (Maybe FiringVector, [Cut])
checkLivenessProperty' verbosity net refine f cuts = do
......@@ -523,9 +516,9 @@ checkLivenessProperty' verbosity net refine f cuts = do
findLivenessRefinement :: Int -> PetriNet -> FiringVector ->
IO (Maybe Cut)
findLivenessRefinement verbosity net x = do
--r1 <- findLivenessRefinementByEmptyTraps verbosity net
-- (initialMarking net) x []
r1 <- findLivenessRefinementBySComponent verbosity net x
r1 <- findLivenessRefinementByEmptyTraps verbosity net
(initialMarking net) x []
--r1 <- findLivenessRefinementBySComponent verbosity net x
case r1 of
Nothing -> findLivenessRefinementByEmptyTraps verbosity net
(initialMarking net) x []
......
......@@ -13,7 +13,7 @@ where
import qualified Data.Map as M
import Control.Arrow (first,(***))
import Data.List (sort)
import Data.List (sort,(\\))
import Util
......@@ -27,6 +27,7 @@ instance Show Transition where
type ContextMap a b = M.Map a ([(b, Integer)],[(b, Integer)])
-- TODO: Use Map/Set for pre/post
class (Ord a, Ord b) => Nodes a b | a -> b where
lpre :: PetriNet -> a -> [(b, Integer)]
lpre net = fst . context net
......@@ -118,18 +119,14 @@ renamePetriNetPlacesAndTransitions f 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: use strongly connected components and min cuts
constructCut' :: Cut -> Cut
constructCut' (ts, u) =
(nubOrd (map (sort *** sort) ts), nubOrd u)
-- TODO: better cuts, scc, min cut?
constructCut:: PetriNet -> FiringVector -> [Trap] -> Cut
constructCut net x traps =
constructCut' (map trapComponent traps, concatMap trapOutput traps)
constructCut net _ traps =
uniqueCut (map trapComponent traps, concatMap trapOutput traps)
where trapComponent trap =
(trap, filter (\t -> val x t > 0) (mpre net trap))
trapOutput trap =
filter (\t -> val x t == 0) (mpost net trap)
(trap, mpre net trap)
trapOutput trap = mpost net trap \\ mpre net trap
uniqueCut (ts, u) = (nubOrd (map (sort *** sort) ts), nubOrd u)
-- TODO: better constructors, only one main constructor
-- TODO: enforce sorted lists
......
......@@ -24,9 +24,7 @@ symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
Symbolic SBool
symConstraints vars constraint = do
syms <- mapM exists vars
let symMap = M.fromList $ vars `zip` syms
let fm x = symMap M.! x
return $ constraint fm
return $ constraint $ val $ M.fromList $ vars `zip` syms
checkSat :: (SatModel a, SymWord a, Show a, Show b) => Int ->
ConstraintProblem a b -> IO (Maybe b)
......@@ -40,8 +38,7 @@ checkSat verbosity (problemName, resultName, vars, constraint, interpretation) =
return Nothing
Just rawModel -> do
verbosePut verbosity 2 "- sat"
let fm x = rawModel M.! x
let model = interpretation fm
let model = interpretation $ val rawModel
verbosePut verbosity 3 $ "- " ++ resultName ++ ": " ++ show model
verbosePut verbosity 4 $ "- raw model: " ++ show rawModel
return $ Just model
......
......@@ -29,8 +29,7 @@ showSimpleCuts cs inv = intercalate " ∧ " (map showTrans cs)
instance Show LivenessInvariant where
show (RankingFunction (n, cs, xs)) = n ++
" [" ++ showSimpleCuts cs True ++ "]: " ++
intercalate " + " (map showPlace (items xs))
where showPlace (p, w) = show w ++ show p
intercalate " + " (map showWeighted (items xs))
show (ComponentCut (n, cs, ps)) = n ++
" [" ++ showSimpleCuts cs False ++ "]: " ++
show ps
......@@ -41,9 +40,6 @@ type NamedCut = (String, [(String, SimpleCut)])
placeName :: String -> Place -> String
placeName n p = n ++ "@p" ++ show p
numPref :: String -> [String]
numPref s = map (\i -> s ++ show i) [(1::Integer)..]
generateCuts :: Formula Transition -> [Cut] -> [NamedCut]
generateCuts f cuts =
zipWith nameCut
......@@ -112,6 +108,7 @@ checkLivenessInvariant :: PetriNet -> [NamedCut] -> SIMap String -> SBool
checkLivenessInvariant net cuts m =
bAnd (map (checkCut net m) cuts)
-- TODO: split up into many smaller sat problems
checkLivenessInvariantSat :: PetriNet -> Formula Transition -> [Cut] ->
ConstraintProblem Integer [LivenessInvariant]
checkLivenessInvariantSat net f cuts =
......
module Solver.SafetyInvariant (
checkSafetyInvariantSat
, SafetyInvariant
) where
import Data.SBV
import Data.List (intercalate)
import qualified Data.Map as M
import Control.Arrow (second)
import Util
import Solver
import Property
import PetriNet
type NamedTrap = (String, Trap)
type SimpleTerm = (Vector Place, Integer)
type NamedTerm = (String, SimpleTerm)
data SafetyInvariant =
SafetyPlaceInvariant NamedTerm
| SafetyTrapInvariant NamedTrap
instance Show SafetyInvariant where
show (SafetyPlaceInvariant (n, (ps, c))) = n ++ ": " ++
intercalate " + " (map showWeighted (items ps)) ++
" ≤ " ++ show c
show (SafetyTrapInvariant (n, ps)) = n ++ ": " ++
intercalate " + " (map show ps) ++
" ≥ 1"
formulaToSimpleTerms :: Formula Place -> [SimpleTerm]
formulaToSimpleTerms = transformF
where
transformF FTrue = []
transformF (p :&: q) = transformF p ++ transformF q
transformF (LinearInequation ps Gt (Const 0)) =
transformT 1 ps 1
transformF (LinearInequation ps Ge (Const 1)) =
transformT 1 ps 1
transformF (LinearInequation ps Eq (Const 0)) =
transformT (-1) ps 0
transformF (LinearInequation ps Le (Const 0)) =
transformT (-1) ps 0
transformF (LinearInequation ps Lt (Const 1)) =
transformT (-1) ps 0
transformF f =
error $ "formula not supported for invariant: " ++ show f
transformT fac ps w = [(buildVector (transformTerm fac ps), w)]
transformTerm fac (t :+: u) =
transformTerm fac t ++ transformTerm fac u
transformTerm fac (t :-: u) =
transformTerm fac t ++ transformTerm (- fac) u
transformTerm fac (Const c :*: t) = transformTerm (fac * c) t
transformTerm fac (t :*: Const c) = transformTerm (fac * c) t
transformTerm fac (Var x) = [(x, fac)]
transformTerm _ t =
error $ "term not supported for invariant: " ++ show t
trapToSimpleTerm :: Trap -> SimpleTerm
trapToSimpleTerm traps = (buildVector (map (\p -> (p, 1)) traps), 1)
checkInductivityConstraint :: PetriNet -> SIMap Place -> SBool
checkInductivityConstraint net lambda =
bAnd $ map checkInductivity $ transitions net
where checkInductivity t =
let incoming = map addPlace $ lpre net t
outgoing = map addPlace $ lpost net t
in sum outgoing - sum incoming .<= 0
addPlace (p,w) = literal w * val lambda p
checkSafetyConstraint :: PetriNet -> [NamedTerm] -> SIMap Place ->
SIMap String -> SBool
checkSafetyConstraint net terms lambda y =
sum (map addPlace (linitials net)) .< sum (map addTerm terms)
where addPlace (p,w) = literal w * val lambda p
addTerm (n,(_,c)) = literal c * val y n
checkPropertyConstraint :: PetriNet -> [NamedTerm] -> SIMap Place ->
SIMap String -> SBool
checkPropertyConstraint net terms lambda y =
bAnd $ map checkPlace $ places net
where checkPlace p =
val lambda p .>= sum (map (addTerm p) terms)
addTerm p (n,(ps,_)) = val y n * literal (val ps p)
checkNonNegativityConstraint :: [NamedTerm] -> SIMap String -> SBool
checkNonNegativityConstraint terms y =
bAnd $ map checkVal terms
where checkVal (n,_) = val y n .>= 0
checkSafetyInvariant :: PetriNet -> [NamedTerm] -> SIMap Place ->
SIMap String -> SBool
checkSafetyInvariant net terms lambda y =
checkInductivityConstraint net lambda &&&
checkSafetyConstraint net terms lambda y &&&
checkPropertyConstraint net terms lambda y &&&
checkNonNegativityConstraint terms y
-- TODO: split up into many smaller sat problems
checkSafetyInvariantSat :: PetriNet -> Formula Place -> [Trap] ->
ConstraintProblem Integer [SafetyInvariant]
checkSafetyInvariantSat net f traps =
let formTerms = formulaToSimpleTerms f
namedTraps = numPref "@trap" `zip` traps
namedTrapTerms = map (second trapToSimpleTerm) namedTraps
namedFormTerms = numPref "@term" `zip` formTerms
namedTerms = namedFormTerms ++ namedTrapTerms
lambda = makeVarMap $ places net
names = map fst namedTerms
myVarMap fvm = M.fromList $ names `zip` fmap fvm names
in ("safety invariant constraints", "safety invariant",
getNames lambda ++ names,
\fm -> checkSafetyInvariant net namedTerms
(fmap fm lambda) (myVarMap fm),
\fm -> getSafetyInvariant net namedTraps (fmap fm lambda))
getSafetyInvariant :: PetriNet -> [NamedTrap] -> IMap Place ->
[SafetyInvariant]
getSafetyInvariant net namedTraps lambda =
placeInv : map SafetyTrapInvariant namedTraps
where placeInv = SafetyPlaceInvariant
("@safe", (buildVector (items lambda),
sum (map (\(p,i) -> val lambda p * i) (linitials net))))
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}
module Util
(verbosePut,elems,items,emap,
nubOrd,nubOrdBy,prime,val,vals,mval,zeroVal,positiveVal,sumVal,
(verbosePut,elems,items,emap,prime,numPref,
nubOrd,nubOrdBy,val,vals,mval,zeroVal,positiveVal,sumVal,
makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
Vector,Model,VarMap,SIMap,SBMap,IMap,BMap)
Vector,Model,VarMap,SIMap,SBMap,IMap,BMap,showWeighted)
where
import Data.SBV
......@@ -99,7 +99,16 @@ verbosePut :: Int -> Int -> String -> IO ()
verbosePut verbosity level str =
when (verbosity >= level) (putStrLn str)
{-
- String functions
-}
prime :: String -> String
prime = ('\'':)
numPref :: String -> [String]
numPref s = map (\i -> s ++ show i) [(1::Integer)..]
showWeighted :: (Show a, Num b, Eq b, Show b) => (a, b) -> String
showWeighted (x, w) = (if w == 1 then "" else show w) ++ show x
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