Commit 72840d1d authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Print invariant size and changed option for simplification

parent 7198eef1
......@@ -9,7 +9,6 @@ import Data.List (partition)
import Data.Maybe
import qualified Data.ByteString.Lazy as L
import Control.Monad.Reader
import qualified Data.Set as S
import Util
import Options
......@@ -231,15 +230,14 @@ checkSafetyProperty net f = do
case r of
(Nothing, traps) -> do
invariant <- opt optInvariant
if invariant then do
r' <- checkSat $ checkSafetyInvariantSat net f traps
printInvariant r'
if invariant then
checkSat (checkSafetyInvariantSat net f traps) >>= printInvariant
else
return Satisfied
(Just _, _) ->
return Unknown
printInvariant :: (Show a) => Maybe [a] -> OptIO PropResult
printInvariant :: (Show a, Invariant a) => Maybe [a] -> OptIO PropResult
printInvariant invResult =
case invResult of
Nothing -> do
......@@ -247,6 +245,7 @@ printInvariant invResult =
return Unknown
Just inv -> do
verbosePut 0 "Invariant found"
verbosePut 2 $ "Number of atoms in invariants: " ++ show (map invariantSize inv)
mapM_ (putLine . show) inv
return Satisfied
......@@ -292,9 +291,9 @@ getLivenessInvariant :: PetriNet -> Formula Transition -> [Cut] -> OptIO (Maybe
getLivenessInvariant net f cuts = do
dnfCuts <- generateCuts net f cuts
verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
rs <- parallelIO (map (checkSat . checkLivenessInvariantSat net f) dnfCuts)
let added = map (Just . cutToLivenessInvariant) cuts
return $ sequence (rs ++ added)
invs <- parallelIO (map (checkSat . checkLivenessInvariantSat net f) dnfCuts)
let cutInvs = map (Just . cutToLivenessInvariant) cuts
return $ sequence (invs ++ cutInvs)
checkLivenessProperty' :: PetriNet ->
Formula Transition -> [Cut] -> OptIO (Maybe FiringVector, [Cut])
......
......@@ -59,7 +59,7 @@ startOptions = Options { inputFormat = PNET
, optShowVersion = False
, optProperties = []
, optTransformations = []
, optSimpFormula = 100
, optSimpFormula = -1
, optRefinementType = Just SComponentWithCutRefinement
, optMinimizeRefinement = 0
, optInvariant = False
......@@ -219,12 +219,13 @@ options =
"Do not use the properties given in the input file"
, Option "s" ["simp"]
(ReqArg (\arg opt -> case reads arg of
[(i, "")] -> Right opt { optSimpFormula = i }
(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)
)
"LEVEL")
"Simply formula with level LEVEL"
"METHOD")
"Simply formula with method METHOD (0-2 or auto)"
, Option "" ["simp-1"]
(NoArg (\opt -> Right opt {
......
......@@ -9,7 +9,7 @@ module PetriNet
pre,lpre,post,lpost,mpre,mpost,context,ghostTransitions,
makePetriNet,makePetriNetWithTrans,
makePetriNetFromStrings,makePetriNetWithTransFromStrings,Trap,Cut,
constructCut,SimpleCut)
constructCut,SimpleCut,Invariant(..))
where
import qualified Data.Map as M
......@@ -64,6 +64,9 @@ type Trap = [Place]
-- TODO: generalize cut type
type Cut = ([([Place], [Transition])], [Transition])
class Invariant a where
invariantSize :: a -> Int
data PetriNet = PetriNet {
name :: String,
places :: [Place],
......
......@@ -54,15 +54,15 @@ checkSatMin minProblem = do
r0 <- checkSat $ minProblem Nothing
case r0 of
Nothing -> return Nothing
Just (result, size) ->
Just (result, curSize) ->
if optMin > 0 then
Just <$> findSmaller optMin result size
Just <$> findSmaller optMin result curSize
else
return $ Just result
where findSmaller optMin result size = do
verbosePut 2 $ "Checking for size smaller than " ++ show size
r1 <- checkSat $ minProblem (Just (optMin, size))
where findSmaller optMin result curSize = do
verbosePut 2 $ "Checking for size smaller than " ++ show curSize
r1 <- checkSat $ minProblem (Just (optMin, curSize))
case r1 of
Nothing -> return result
Just (result', size') -> findSmaller optMin result' size'
Just (result', curSize') -> findSmaller optMin result' curSize'
module Solver.LivenessInvariant (
checkLivenessInvariantSat
, LivenessInvariant
, invariantSize
, cutToLivenessInvariant
, SimpleCut
) where
......@@ -20,6 +21,12 @@ data LivenessInvariant =
RankingFunction (SimpleCut, Vector Place)
| ComponentCut (SimpleCut, [Trap])
instance Invariant LivenessInvariant where
invariantSize (RankingFunction ((c0, cs), ps)) =
S.size c0 + sum (map S.size cs) + size ps
invariantSize (ComponentCut ((c0, cs), ps)) =
S.size c0 + sum (map S.size cs) + sum (map length ps)
showSimpleCuts :: SimpleCut -> String
showSimpleCuts cs = intercalate " ∧ " (showSimpleCut cs)
where showSimpleCut (ts0, cs1) =
......
......@@ -67,7 +67,7 @@ checkBinary p' t' y =
checkSizeLimit :: SIMap Place -> SIMap Transition -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ _ Nothing = true
checkSizeLimit p' _ (Just (_, size)) = (.< literal size) $ sumVal p'
checkSizeLimit p' _ (Just (_, curSize)) = (.< literal curSize) $ sumVal p'
checkSComponent :: PetriNet -> FiringVector -> Maybe (Int, Integer) -> SIMap Place ->
SIMap Transition -> SIMap Transition -> SBool
......@@ -100,6 +100,6 @@ cutFromAssignment net x p' t' y =
(t1, t2) = partition (\t -> val y t > 0) ts
s1 = filter (\p -> val p' p > 0) $ mpre net t1
s2 = filter (\p -> val p' p > 0) $ mpre net t2
size = fromIntegral $ M.size $ M.filter (> 0) p'
in (constructCut net x [s1,s2], size)
curSize = fromIntegral $ M.size $ M.filter (> 0) p'
in (constructCut net x [s1,s2], curSize)
......@@ -29,6 +29,10 @@ instance Show SafetyInvariant where
intercalate " + " (map show ps) ++
" ≥ 1"
instance Invariant SafetyInvariant where
invariantSize (SafetyPlaceInvariant (_, (ps, _))) = size ps
invariantSize (SafetyTrapInvariant (_, ps)) = length ps
formulaToSimpleTerms :: Formula Place -> [SimpleTerm]
formulaToSimpleTerms = transformF
where
......
......@@ -57,6 +57,9 @@ cutTransitions (c0, cs) = S.unions (c0:cs)
type SimpConfig = ([[SimpleCut] -> OptIO [SimpleCut]], SimpleCut, Int)
noSimp :: PetriNet -> Formula Transition -> SimpConfig
noSimp _ _ = ([], (S.empty, []), 0)
simpWithoutFormula :: PetriNet -> Formula Transition -> SimpConfig
simpWithoutFormula net f =
(
......@@ -86,8 +89,7 @@ simpWithFormula net f =
applySimpConfig :: SimpConfig -> [Cut] -> OptIO [SimpleCut]
applySimpConfig (simpFunctions, initialCut, otfIndex) cuts = do
simp <- opt optSimpFormula
let (otfSimps, afterSimps) = splitAt otfIndex $ take simp simpFunctions
let (otfSimps, afterSimps) = splitAt otfIndex simpFunctions
let simpFunction = foldl (>=>) return afterSimps
let otfFunction = foldl (>=>) return otfSimps
let cnfCuts = map cutToSimpleDNFCuts cuts
......@@ -100,9 +102,14 @@ applySimpConfig (simpFunctions, initialCut, otfIndex) cuts = do
generateCuts :: PetriNet -> Formula Transition -> [Cut] -> OptIO [SimpleCut]
generateCuts net f cuts = do
let configs = [simpWithFormula, simpWithoutFormula]
let tasks = map (\c -> applySimpConfig (c net f) cuts) configs
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]
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)
return $ minimumBy (comparing length) rs
combineCuts :: [SimpleCut] -> [SimpleCut]
......
......@@ -22,7 +22,7 @@ properTrap b = sum (vals b) .> 0
checkSizeLimit :: SIMap Place -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit b (Just (_, size)) = (.< literal size) $ sumVal b
checkSizeLimit b (Just (_, curSize)) = (.< literal curSize) $ sumVal b
checkBinary :: SIMap Place -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
......
{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FunctionalDependencies #-}
module Util
(elems,items,emap,prime,numPref,
(elems,items,size,emap,prime,numPref,
listSet,listMap,val,vals,mval,zeroVal,positiveVal,sumVal,
makeVarMap,makeVarMapWith,buildVector,makeVector,getNames,
Vector,Model,VarMap,SIMap,SBMap,IMap,BMap,showWeighted,
......@@ -37,6 +37,7 @@ class MapLike c a b | c -> a, c -> b where
vals :: c -> [b]
elems :: c -> [a]
items :: c -> [(a,b)]
size :: c -> Int
mval :: c -> [a] -> [b]
mval = map . val
......@@ -50,12 +51,14 @@ instance (Ord a, Show a, Show b) => MapLike (M.Map a b) a b where
vals = M.elems
items = M.toList
elems = M.keys
size = M.size
instance (Ord a, Show a) => MapLike (Vector a) a Integer where
val (Vector v) x = M.findWithDefault 0 x v
vals = vals . getVector
items = M.toList . getVector
elems = M.keys . getVector
size = M.size . getVector
instance (Show a) => Show (Vector a) where
show (Vector v) =
......
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