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

Added auto option for refinement and more informative for invariants

parent 72840d1d
......@@ -5,7 +5,8 @@ import System.IO
import Control.Monad
import Control.Concurrent.ParallelIO
import Control.Arrow (first)
import Data.List (partition)
import Data.List (partition,minimumBy)
import Data.Ord (comparing)
import Data.Maybe
import qualified Data.ByteString.Lazy as L
import Control.Monad.Reader
......@@ -231,22 +232,35 @@ checkSafetyProperty net f = do
(Nothing, traps) -> do
invariant <- opt optInvariant
if invariant then
checkSat (checkSafetyInvariantSat net f traps) >>= printInvariant
getSafetyInvariant net f traps >>= printInvariant
else
return Satisfied
(Just _, _) ->
return Unknown
printInvariant :: (Show a, Invariant a) => Maybe [a] -> OptIO PropResult
printInvariant invResult =
case invResult of
getSafetyInvariant :: PetriNet -> Formula Place -> [Trap] ->
OptIO (Maybe [SafetyInvariant], [SafetyInvariant])
getSafetyInvariant net f traps = do
r <- checkSat $ checkSafetyInvariantSat net f traps
let trapInvs = map trapToSafetyInvariant traps
return (sequence [r], trapInvs)
printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult
printInvariant (baseInvResult, addedInv) =
case baseInvResult of
Nothing -> do
verbosePut 0 "No invariant found"
return Unknown
Just inv -> do
Just baseInv -> do
verbosePut 0 "Invariant found"
verbosePut 2 $ "Number of atoms in invariants: " ++ show (map invariantSize inv)
mapM_ (putLine . show) inv
let baseSize = map invariantSize baseInv
let addedSize = map invariantSize addedInv
verbosePut 2 $ "Number of atoms in base invariants: " ++ show baseSize ++
" (total of " ++ show (sum baseSize)
verbosePut 2 $ "Number of atoms in added invariants: " ++ show addedSize ++
" (total of " ++ show (sum addedSize)
mapM_ (putLine . show) baseInv
mapM_ (putLine . show) addedInv
return Satisfied
checkSafetyProperty' :: PetriNet ->
......@@ -272,28 +286,58 @@ refineSafetyProperty net f traps m = do
Just trap ->
checkSafetyProperty' net f (trap:traps)
applyRefinementMethod :: RefinementMethod -> Options -> Options
applyRefinementMethod (rtype, mtype) opts =
opts { optRefinementType = rtype, optMinimizeRefinement = mtype }
type RefinementMethod = (Maybe RefinementType, Int)
refinementMethods :: [RefinementMethod]
refinementMethods =
[(Just SComponentRefinement, 0)
,(Just SComponentRefinement, 1)
,(Just SComponentWithCutRefinement, 1)
,(Just SComponentWithCutRefinement, 2)
,(Just SComponentWithCutRefinement, 3)
,(Just SComponentWithCutRefinement, 4)
]
checkLivenessProperty :: PetriNet ->
Formula Transition -> OptIO PropResult
checkLivenessProperty net f = do
(r, cuts) <- checkLivenessProperty' net f []
verbosePut 2 $ "Number of refinements: " ++ show (length cuts)
let methods = map (local . applyRefinementMethod) refinementMethods
auto <- opt optAuto
r <-
if auto then do
rAll <- mapM ($ checkLivenessProperty' net f []) methods
verbosePut 2 $
"Number of refinements in tested methods: " ++ show (map (length . snd) rAll)
let rSucc = filter (isNothing . fst) rAll
if null rSucc then
return (Nothing, [])
else
return $ minimumBy (comparing (length . snd)) rSucc
else
checkLivenessProperty' net f []
case r of
Nothing -> do
(Nothing, cuts) -> do
verbosePut 2 $ "Number of refinements: " ++ show (length cuts)
invariant <- opt optInvariant
if invariant then
getLivenessInvariant net f cuts >>= printInvariant
else
return Satisfied
Just _ ->
(Just _, _) ->
return Unknown
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe [LivenessInvariant])
getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] ->
OptIO (Maybe [LivenessInvariant], [LivenessInvariant])
getLivenessInvariant net f cuts = do
dnfCuts <- generateCuts net f cuts
verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
invs <- parallelIO (map (checkSat . checkLivenessInvariantSat net f) dnfCuts)
let cutInvs = map (Just . cutToLivenessInvariant) cuts
return $ sequence (invs ++ cutInvs)
let cutInvs = map cutToLivenessInvariant cuts
return (sequence invs, cutInvs)
checkLivenessProperty' :: PetriNet ->
Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
......
......@@ -42,9 +42,10 @@ data Options = Options { inputFormat :: InputFormat
, optShowVersion :: Bool
, optProperties :: [ImplicitProperty]
, optTransformations :: [NetTransformation]
, optSimpFormula :: Int
, optSimpMethod :: Int
, optRefinementType :: Maybe RefinementType
, optMinimizeRefinement :: Int
, optAuto :: Bool
, optInvariant :: Bool
, optOutput :: Maybe String
, outputFormat :: OutputFormat
......@@ -59,9 +60,10 @@ startOptions = Options { inputFormat = PNET
, optShowVersion = False
, optProperties = []
, optTransformations = []
, optSimpFormula = -1
, optSimpMethod = 1
, optRefinementType = Just SComponentWithCutRefinement
, optMinimizeRefinement = 0
, optAuto = False
, optInvariant = False
, optOutput = Nothing
, outputFormat = OutLOLA
......@@ -219,23 +221,22 @@ options =
"Do not use the properties given in the input file"
, Option "s" ["simp"]
(ReqArg (\arg opt -> case (arg, reads arg) of
("auto", _) -> Right opt { optSimpFormula = -1 }
(_, [(i, "")]) -> Right opt { optSimpFormula = i }
_ -> Left ("invalid argument for simplification level: " ++ arg)
(ReqArg (\arg opt -> case reads arg of
[(i, "")] -> Right opt { optSimpMethod = i }
_ -> Left ("invalid argument for simplification method: " ++ arg)
)
"METHOD")
"Simply formula with method METHOD (0-2 or auto)"
"Simply formula with method METHOD (0-2)"
, Option "" ["simp-1"]
(NoArg (\opt -> Right opt {
optSimpFormula = 1
optSimpMethod = 1
}))
"Use simplification level 1 for invariant generation"
, Option "" ["simp-2"]
(NoArg (\opt -> Right opt {
optSimpFormula = 2
optSimpMethod = 2
}))
"Use simplification level 2 for invariant generation"
......@@ -247,7 +248,11 @@ options =
_ -> Left ("invalid argument for minimization method: " ++ is)
)
"METHOD")
"Minimize size of refinement structure by method METHOD"
"Minimize size of refinement structure by method METHOD (1-4)"
, Option "" ["auto"]
(NoArg (\opt -> Right opt { optAuto = True }))
"Automatically find best refinement, minimization and simplification method"
, Option "v" ["verbose"]
(NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
......
module Solver.SafetyInvariant (
checkSafetyInvariantSat
, SafetyInvariant
, trapToSafetyInvariant
) where
import Data.SBV
......@@ -13,25 +14,24 @@ 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
SafetyPlaceInvariant SimpleTerm
| SafetyTrapInvariant Trap
instance Show SafetyInvariant where
show (SafetyPlaceInvariant (n, (ps, c))) = n ++ ": " ++
show (SafetyPlaceInvariant (ps, c)) =
intercalate " + " (map showWeighted (items ps)) ++
" ≤ " ++ show c
show (SafetyTrapInvariant (n, ps)) = n ++ ": " ++
show (SafetyTrapInvariant ps) =
intercalate " + " (map show ps) ++
" ≥ 1"
instance Invariant SafetyInvariant where
invariantSize (SafetyPlaceInvariant (_, (ps, _))) = size ps
invariantSize (SafetyTrapInvariant (_, ps)) = length ps
invariantSize (SafetyPlaceInvariant (ps, _)) = size ps
invariantSize (SafetyTrapInvariant ps) = length ps
formulaToSimpleTerms :: Formula Place -> [SimpleTerm]
formulaToSimpleTerms = transformF
......@@ -103,7 +103,7 @@ checkSafetyInvariant net terms lambda y =
-- TODO: split up into many smaller sat problems
checkSafetyInvariantSat :: PetriNet -> Formula Place -> [Trap] ->
ConstraintProblem Integer [SafetyInvariant]
ConstraintProblem Integer SafetyInvariant
checkSafetyInvariantSat net f traps =
let formTerms = formulaToSimpleTerms f
namedTraps = numPref "@trap" `zip` traps
......@@ -117,12 +117,14 @@ checkSafetyInvariantSat net f traps =
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))))
\fm -> getSafetyInvariant net (fmap fm lambda))
trapToSafetyInvariant :: Trap -> SafetyInvariant
trapToSafetyInvariant = SafetyTrapInvariant
getSafetyInvariant :: PetriNet -> IMap Place ->
SafetyInvariant
getSafetyInvariant net lambda =
SafetyPlaceInvariant
(buildVector (items lambda),
sum (map (\(p,i) -> val lambda p * i) (linitials net)))
......@@ -103,13 +103,16 @@ applySimpConfig (simpFunctions, initialCut, otfIndex) cuts = do
generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
generateCuts net f cuts = do
let configs = [noSimp, simpWithFormula, simpWithoutFormula]
simp <- opt optSimpFormula
let simpConfig | simp < 0 = drop 1 configs
| simp >= length configs = error ("Invalid simplification: " ++ show simp)
| otherwise = [configs !! simp]
auto <- opt optAuto
simp <- opt optSimpMethod
let simpConfig | auto = drop 1 configs
| simp >= 0 && simp < length configs = [configs !! simp]
| otherwise =
error ("Invalid simplification: " ++ show simp)
let tasks = map (\c -> applySimpConfig (c net f) cuts) simpConfig
rs <- parallelIO tasks
verbosePut 2 $ "Number of disjuncts in simplified versions: " ++ show (map length rs)
when auto $ verbosePut 2 $
"Number of disjuncts in tested simplifications: " ++ show (map length rs)
return $ minimumBy (comparing length) rs
combineCuts :: [SimpleCut] -> [SimpleCut]
......
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