Change handling of default properties (612a3cfb) · Commits · i7 / peregrine

src/Main.hs

+4 −1

Original line number	Diff line number	Diff line
		@@ -48,7 +48,10 @@ checkFile file = do
		let parser = case format of
		InPP -> PPParser.parseContent
		pp <- liftIO $ parseFile parser file
		props <- opt optProperties
		propOpt <- opt optProperties
		let props = case propOpt of
		PropDefault -> [LayeredTermination, StrongConsensus]
		PropList ps -> ps
		verbosePut 1 $ "Analyzing " ++ showNetName pp
		verbosePut 2 $
		"Number of states: " ++ show (length (states pp))

src/Options.hs

+12 −10

Original line number	Diff line number	Diff line
		@@ -2,7 +2,7 @@

		module Options
		(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
		Options(..),startOptions,options,parseArgs,
		PropertyOption(..),Options(..),startOptions,options,parseArgs,
		usageInformation)
		where

		@@ -26,6 +26,9 @@ data RefinementType = TrapRefinement
		\| USiphonRefinement
		deriving (Show,Read)

		data PropertyOption = PropDefault
		\| PropList [Property]

		data RefinementOption = RefDefault
		\| RefList [RefinementType]
		\| RefAll
		@@ -34,7 +37,7 @@ data Options = Options { inputFormat :: InputFormat
		, optVerbosity :: Int
		, optShowHelp :: Bool
		, optShowVersion :: Bool
		, optProperties :: [Property]
		, optProperties :: PropertyOption
		, optRefinementType :: RefinementOption
		, optMinimizeRefinement :: Int
		, optSMTAuto :: Bool
		@@ -50,7 +53,7 @@ startOptions = Options { inputFormat = InPP
		, optVerbosity = 1
		, optShowHelp = False
		, optShowVersion = False
		, optProperties = []
		, optProperties = PropDefault
		, optRefinementType = RefDefault
		, optMinimizeRefinement = 0
		, optSMTAuto = True
		@@ -61,20 +64,21 @@ startOptions = Options { inputFormat = InPP
		, optPrintStructure = False
		}

		defaultOptions :: Options
		defaultOptions = startOptions{ optProperties = [LayeredTermination, StrongConsensus] }

		options :: [ OptDescr (Options -> Either String Options) ]
		options =
		[ Option "" ["layered-termination"]
		(NoArg (\opt -> Right opt {
		optProperties = optProperties opt ++ [LayeredTermination]
		optProperties = case optProperties opt of
		PropDefault -> PropList [LayeredTermination]
		(PropList props) -> PropList ([LayeredTermination] ++ props)
		}))
		"Prove that the protocol satisfies layered termination"

		, Option "" ["strong-consensus"]
		(NoArg (\opt -> Right opt {
		optProperties = optProperties opt ++ [StrongConsensus]
		optProperties = case optProperties opt of
		PropDefault -> PropList [StrongConsensus]
		(PropList props) -> PropList ([StrongConsensus] ++ props)
		}))
		"Prove that the protocol satisfies strong consensus"

		@@ -155,8 +159,6 @@ parseArgs :: IO (Either String (Options, [String]))
		parseArgs = do
		args <- getArgs
		case getOpt Permute options args of
		([], files, []) ->
		return $ (,files) <$> (return defaultOptions)
		(actions, files, []) ->
		return $ (,files) <$> foldl (>>=) (return startOptions) actions
		(_, _, errs) -> return $ Left $ concat errs