Added option for minimization of refinement structures

src/Main.hs

@@ -271,20 +271,20 @@ refineSafetyProperty net f traps m = do
 checkLivenessProperty :: PetriNet ->
         Formula Transition -> OptIO PropResult
 checkLivenessProperty net f = do
-        r <- checkLivenessProperty' net f []
+        (r, cuts) <- checkLivenessProperty' net f []
+        verbosePut 2 $ "Number of refinements: " ++ show (length cuts)
         case r of
-            (Nothing, cuts) -> do
+            Nothing -> do
                 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 net f cuts = do
-        verbosePut 2 $ "Number of cuts: " ++ show (length cuts)
         simp <- opt optSimpFormula
         let dnfCuts = generateCuts f cuts
         verbosePut 2 $ "Number of disjuncts: " ++ show (length dnfCuts)
@@ -329,12 +329,12 @@ findLivenessRefinement net x = do
 findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
         OptIO (Maybe Cut)
 findLivenessRefinementBySComponent net x =
-        checkSat $ checkSComponentSat net x
+        checkSatMin $ checkSComponentSat net x
 
 findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
         [Trap] -> OptIO (Maybe Cut)
 findLivenessRefinementByEmptyTraps net m x traps = do
-        r <- checkSat $ checkSubnetEmptyTrapSat net m x
+        r <- checkSatMin $ checkSubnetEmptyTrapSat net m x
         case r of
             Nothing -> do
                 rm <- refineSafetyProperty net FTrue traps m

src/Options.hs

@@ -45,6 +45,7 @@ data Options = Options { inputFormat :: InputFormat
                        , optRefine :: Bool
                        , optSimpFormula :: Bool
                        , optRefinementType :: RefinementType
+                       , optMinimizeRefinement :: Bool
                        , optInvariant :: Bool
                        , optOutput :: Maybe String
                        , outputFormat :: OutputFormat
@@ -62,6 +63,7 @@ startOptions = Options { inputFormat = PNET
                        , optRefine = True
                        , optSimpFormula = True
                        , optRefinementType = SComponentRefinement
+                       , optMinimizeRefinement = False
                        , optInvariant = False
                        , optOutput = Nothing
                        , outputFormat = OutLOLA
@@ -224,6 +226,12 @@ options =
                }))
         "Do not simplify formula for invariant generation"
 
+        , Option "" ["minimize-refinement"]
+        (NoArg (\opt -> Right opt {
+                   optMinimizeRefinement = True
+               }))
+        "Minimize size of refinement structure (trap/s-component)"
+
         , Option "v" ["verbose"]
         (NoArg (\opt -> Right opt { optVerbosity = optVerbosity opt + 1 }))
         "Increase verbosity (may be specified more than once)"

src/Solver.hs

 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 
 module Solver
-    (prime,checkSat,val,vals,positiveVal,zeroVal,
+    (prime,checkSat,checkSatMin,val,vals,positiveVal,zeroVal,
      getNames,
      ConstraintProblem)
 where
@@ -12,6 +12,7 @@ import qualified Data.Map as M
 import Util
 import Options
 import Control.Monad.IO.Class
+import Control.Applicative
 
 type ConstraintProblem a b =
         (String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
@@ -46,3 +47,22 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do
                 verbosePut 4 $ "- raw model: " ++ show rawModel
                 return $ Just model
 
+checkSatMin :: (SatModel a, SymWord a, Show a, Show b) =>
+        (Maybe Integer -> ConstraintProblem a (b, Integer)) -> OptIO (Maybe b)
+checkSatMin minProblem = do
+        optMin <- opt optMinimizeRefinement
+        r0 <- checkSat $ minProblem Nothing
+        case r0 of
+            Nothing -> return Nothing
+            Just (result, size) ->
+                if optMin then
+                    Just <$> findSmaller result size
+                else
+                    return $ Just result
+    where findSmaller result size = do
+            verbosePut 2 $ "Checking for size smaller than " ++ show size
+            r1 <- checkSat $ minProblem (Just size)
+            case r1 of
+                Nothing -> return result
+                Just (result', size') -> findSmaller result' size'
+

src/Solver/LivenessInvariant.hs

@@ -20,13 +20,13 @@ data LivenessInvariant =
             RankingFunction (SimpleCut, Vector Place)
           | ComponentCut (SimpleCut, [Trap])
 
-showSimpleCuts :: SimpleCut -> Bool -> String
-showSimpleCuts cs inv = intercalate " ∧ " (showSimpleCut cs)
+showSimpleCuts :: SimpleCut -> String
+showSimpleCuts cs = intercalate " ∧ " (showSimpleCut cs)
         where showSimpleCut (ts0, cs1) =
                 if S.null ts0 then
-                    map (showTrans inv) cs1
+                    map (showTrans True) cs1
                 else
-                    showTrans (not inv) ts0 : map (showTrans inv) cs1
+                    showTrans False ts0 : map (showTrans True) cs1
               showTrans pos ts =
                   if pos then
                        let d = intercalate " ∨ "
@@ -37,10 +37,10 @@ showSimpleCuts cs inv = intercalate " ∧ " (showSimpleCut cs)
 
 instance Show LivenessInvariant where
         show (RankingFunction (cs, xs)) =
-                    "[" ++ showSimpleCuts cs True ++ "]: " ++
+                    "[" ++ showSimpleCuts cs ++ "]: " ++
                     intercalate " + " (map showWeighted (items xs))
         show (ComponentCut (cs, ps)) =
-                    "[" ++ showSimpleCuts cs False ++ "]: " ++
+                    "[" ++ showSimpleCuts cs ++ "]: " ++
                     show ps
 
 type SimpleCut = (S.Set Transition, [S.Set Transition])

src/Solver/SComponent.hs

@@ -65,35 +65,41 @@ checkBinary p' t' y =
             checkBins y
         where checkBins xs = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ vals xs
 
-checkSComponent :: PetriNet -> FiringVector -> SIMap Place ->
+checkSizeLimit :: SIMap Place -> SIMap Transition -> Maybe Integer -> SBool
+checkSizeLimit _ _ Nothing = true
+checkSizeLimit p' _ (Just size) = (.< literal size) $ sumVal p'
+
+checkSComponent :: PetriNet -> FiringVector -> Maybe Integer -> SIMap Place ->
         SIMap Transition -> SIMap Transition -> SBool
-checkSComponent net x p' t' y =
+checkSComponent net x sizeLimit p' t' y =
         checkPrePostPlaces net p' t' &&&
         checkPrePostTransitions net p' t' &&&
         checkSubsetTransitions x t' y &&&
         checkNotEmpty y &&&
+        checkSizeLimit p' t' sizeLimit &&&
         checkClosed net x p' y &&&
         checkTokens net p' &&&
         checkBinary p' t' y
 
-checkSComponentSat :: PetriNet -> FiringVector ->
-        ConstraintProblem Integer Cut
-checkSComponentSat net x =
+checkSComponentSat :: PetriNet -> FiringVector -> Maybe Integer ->
+        ConstraintProblem Integer (Cut, Integer)
+checkSComponentSat net x sizeLimit =
         let fired = elems x
             p' = makeVarMap $ places net
             t' = makeVarMap $ transitions net
             y = makeVarMapWith prime fired
         in  ("S-component constraints", "cut",
             getNames p' ++ getNames t' ++ getNames y,
-            \fm -> checkSComponent net x (fmap fm p') (fmap fm t') (fmap fm y),
+            \fm -> checkSComponent net x sizeLimit (fmap fm p') (fmap fm t') (fmap fm y),
             \fm -> cutFromAssignment net x (fmap fm p') (fmap fm t') (fmap fm y))
 
 cutFromAssignment :: PetriNet -> FiringVector -> IMap Place ->
-        IMap Transition -> IMap Transition -> Cut
+        IMap Transition -> IMap Transition -> (Cut, Integer)
 cutFromAssignment net x p' t' y =
         let ts = filter (\t -> val x t > 0) $ elems $ M.filter (> 0) t'
             (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
-        in  constructCut net x [s1,s2]
+            size = fromIntegral $ M.size $ M.filter (> 0) p'
+        in  (constructCut net x [s1,s2], size)
 

src/Solver/SubnetEmptyTrap.hs

@@ -10,32 +10,40 @@ import PetriNet
 import Solver
 
 subnetTrapConstraints :: PetriNet -> Marking -> FiringVector ->
-        SBMap Place -> SBool
+        SIMap Place -> SBool
 subnetTrapConstraints net m x b =
             bAnd $ map trapConstraint $ elems x
-        where placeConstraints = mval b . filter (\p -> val m p == 0)
+        where placeConstraints = (.> 0) . sum . mval b . filter (\p -> val m p == 0)
               trapConstraint t =
-                  bOr (placeConstraints (pre net t)) ==>
-                  bOr (placeConstraints (post net t))
+                  placeConstraints (pre net t) ==> placeConstraints (post net t)
 
-properTrap :: SBMap Place -> SBool
-properTrap b = bOr $ vals b
+properTrap :: SIMap Place -> SBool
+properTrap b = sum (vals b) .> 0
+
+checkSizeLimit :: SIMap Place -> Maybe Integer -> SBool
+checkSizeLimit _ Nothing = true
+checkSizeLimit b (Just size) = (.< literal size) $ sumVal b
+
+checkBinary :: SIMap Place -> SBool
+checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
 
 checkSubnetEmptyTrap :: PetriNet -> Marking -> FiringVector ->
-        SBMap Place -> SBool
-checkSubnetEmptyTrap net m x b =
+        SIMap Place -> Maybe Integer -> SBool
+checkSubnetEmptyTrap net m x b sizeLimit =
         subnetTrapConstraints net m x b &&&
+        checkSizeLimit b sizeLimit &&&
+        checkBinary b &&&
         properTrap b
 
-checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector ->
-        ConstraintProblem Bool Trap
-checkSubnetEmptyTrapSat net m x =
+checkSubnetEmptyTrapSat :: PetriNet -> Marking -> FiringVector -> Maybe Integer ->
+        ConstraintProblem Integer (Trap, Integer)
+checkSubnetEmptyTrapSat net m x sizeLimit =
         let b = makeVarMap $ filter (\p -> val m p == 0) $ mpost net $ elems x
         in  ("subnet empty trap constraints", "trap",
             getNames b,
-            \fm -> checkSubnetEmptyTrap net m x (fmap fm b),
+            \fm -> checkSubnetEmptyTrap net m x (fmap fm b) sizeLimit,
             \fm -> trapFromAssignment (fmap fm b))
 
-trapFromAssignment :: BMap Place -> Trap
-trapFromAssignment b = M.keys $ M.filter id b
+trapFromAssignment :: IMap Place -> (Trap, Integer)
+trapFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))