Extended option to choose refinement type

src/Main.hs

@@ -5,6 +5,7 @@ import System.IO
 import Control.Monad
 import Control.Arrow (first)
 import Data.List (partition)
+import Data.Maybe
 import qualified Data.ByteString.Lazy as L
 import Control.Monad.Reader
 
@@ -254,8 +255,8 @@ checkSafetyProperty' net f traps = do
         case r of
             Nothing -> return (Nothing, traps)
             Just m -> do
-                refine <- opt optRefine
-                if refine then
+                refine <- opt optRefinementType
+                if isJust refine then
                     refineSafetyProperty net f traps m
                 else
                     return (Just m, traps)
@@ -307,34 +308,42 @@ checkLivenessProperty' net f cuts = do
         case r of
             Nothing -> return (Nothing, cuts)
             Just x -> do
-                refine <- opt optRefine
-                if refine then do
-                    rt <- findLivenessRefinement net x
-                    case rt of
-                        Nothing ->
-                            return (Just x, cuts)
-                        Just cut ->
-                            checkLivenessProperty' net f (cut:cuts)
-                else
-                    return (Just x, cuts)
+                rt <- findLivenessRefinement net x
+                case rt of
+                    Nothing ->
+                        return (Just x, cuts)
+                    Just cut ->
+                        checkLivenessProperty' net f (cut:cuts)
 
 findLivenessRefinement :: PetriNet -> FiringVector ->
         OptIO (Maybe Cut)
 findLivenessRefinement net x = do
         refinementType <- opt optRefinementType
         case refinementType of
-            TrapRefinement ->
+            Just TrapRefinement ->
                 findLivenessRefinementByEmptyTraps net (initialMarking net) x []
-            SComponentRefinement -> do
+            Just SComponentRefinement -> do
                 r1 <- findLivenessRefinementBySComponent net x
                 case r1 of
                     Nothing -> findLivenessRefinementByEmptyTraps net
                                                       (initialMarking net) x []
                     Just _ -> return r1
+            Just SComponentWithCutRefinement -> do
+                r1 <- findLivenessRefinementBySComponentWithCut net x
+                case r1 of
+                    Nothing -> findLivenessRefinementByEmptyTraps net
+                                                      (initialMarking net) x []
+                    Just _ -> return r1
+            Nothing -> return Nothing
 
 findLivenessRefinementBySComponent :: PetriNet -> FiringVector ->
         OptIO (Maybe Cut)
 findLivenessRefinementBySComponent net x =
+        checkSatMin $ checkSComponentSat net x
+
+findLivenessRefinementBySComponentWithCut :: PetriNet -> FiringVector ->
+        OptIO (Maybe Cut)
+findLivenessRefinementBySComponentWithCut net x =
         checkSatMin $ checkSComponentWithCutSat net x
 
 findLivenessRefinementByEmptyTraps :: PetriNet -> Marking -> FiringVector ->
@@ -352,7 +361,7 @@ findLivenessRefinementByEmptyTraps net m x traps = do
                         return Nothing
             Just trap -> do
                 let traps' = trap:traps
-                rm <- local (\opts -> opts { optRefine = False }) $
+                rm <- local (\opts -> opts { optRefinementType = Nothing }) $
                             checkSafetyProperty' net FTrue traps'
                 case rm of
                     (Nothing, _) -> do

src/Options.hs

@@ -33,7 +33,7 @@ data ImplicitProperty = Termination
                       | StructCommunicationFree
                       deriving (Show,Read)
 
-data RefinementType = TrapRefinement | SComponentRefinement
+data RefinementType = TrapRefinement | SComponentRefinement | SComponentWithCutRefinement
                     deriving (Show,Read)
 
 data Options = Options { inputFormat :: InputFormat
@@ -42,9 +42,8 @@ data Options = Options { inputFormat :: InputFormat
                        , optShowVersion :: Bool
                        , optProperties :: [ImplicitProperty]
                        , optTransformations :: [NetTransformation]
-                       , optRefine :: Bool
                        , optSimpFormula :: Int
-                       , optRefinementType :: RefinementType
+                       , optRefinementType :: Maybe RefinementType
                        , optMinimizeRefinement :: Int
                        , optInvariant :: Bool
                        , optOutput :: Maybe String
@@ -60,9 +59,8 @@ startOptions = Options { inputFormat = PNET
                        , optShowVersion = False
                        , optProperties = []
                        , optTransformations = []
-                       , optRefine = True
                        , optSimpFormula = 2
-                       , optRefinementType = SComponentRefinement
+                       , optRefinementType = Just SComponentWithCutRefinement
                        , optMinimizeRefinement = 0
                        , optInvariant = False
                        , optOutput = Nothing
@@ -128,7 +126,7 @@ options =
                    optProperties = DeadlockFreeUnlessFinal : optProperties opt
                }))
         ("Prove that the net is deadlock-free\n" ++
-         "unless it is in the final marking")
+         "  unless it is in the final marking")
 
         , Option "" ["final-state-unreachable"]
         (NoArg (\opt -> Right opt {
@@ -179,17 +177,17 @@ options =
         (NoArg (\opt -> Right opt { optInvariant = True }))
         "Generate an invariant"
 
-        , Option "n" ["no-refinement"]
-        (NoArg (\opt -> Right opt { optRefine = False }))
-        "Don't use refinement"
-
-        , Option "" ["trap-refinement"]
-        (NoArg (\opt -> Right opt { optRefinementType = TrapRefinement }))
-        "Only use empty trap refinement for liveness properties"
-
-        , Option "" ["scomponent-refinement"]
-        (NoArg (\opt -> Right opt { optRefinementType = SComponentRefinement }))
-        "Use S-component refinement before trap refinement"
+        , Option "r" ["refinement"]
+        (ReqArg (\arg opt -> case reads arg :: [(Int, String)] of
+                    [(0, "")] -> Right opt { optRefinementType = Nothing }
+                    [(1, "")] -> Right opt { optRefinementType = Just SComponentWithCutRefinement }
+                    [(2, "")] -> Right opt { optRefinementType = Just SComponentRefinement }
+                    [(3, "")] -> Right opt { optRefinementType = Just TrapRefinement }
+                    _ -> Left ("invalid argument for refinement method: " ++ arg)
+                )
+                "METHOD")
+        ("Refine with METHOD (0=none, 1=SCompCut+Traps,\n" ++
+         "  2=SComp+Traps, 3=Traps)")
 
         , Option "o" ["output"]
         (ReqArg (\arg opt -> Right opt {