Changed processing of option to check correctness (ad99d8de) · Commits · i7 / peregrine

src/Main.hs

+14 −16

Original line number	Diff line number	Diff line
		@@ -80,7 +80,8 @@ checkProperty pp prop = do
		verbosePut 1 $ "\nChecking " ++ show prop
		r <- case prop of
		LayeredTermination -> checkLayeredTermination pp
		StrongConsensus -> checkStrongConsensus pp
		StrongConsensus -> checkStrongConsensus False pp
		StrongConsensusWithCorrectness -> checkStrongConsensus True pp
		verbosePut 0 $ show prop ++ " " ++ show r
		return r

		@@ -92,20 +93,17 @@ printInvariant inv = do
		" (total of " ++ show (sum invSize) ++ ")"
		mapM_ (putLine . show) inv

		checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
		checkStrongConsensus pp = do
		checkCorrectness <- opt optCorrectness
		when checkCorrectness $ verbosePut 1 "- additionally checking correctness"
		r <- checkStrongConsensus' pp ([], [])
		checkStrongConsensus :: Bool -> PopulationProtocol -> OptIO PropResult
		checkStrongConsensus checkCorrectness pp = do
		r <- checkStrongConsensus' checkCorrectness pp ([], [])
		case r of
		(Nothing, _) -> return Satisfied
		(Just _, _) -> return Unknown

		checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
		checkStrongConsensus' :: Bool -> PopulationProtocol -> RefinementObjects ->
		OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
		checkStrongConsensus' pp refinements = do
		checkStrongConsensus' checkCorrectness pp refinements = do
		optRefine <- opt optRefinementType
		checkCorrectness <- opt optCorrectness
		case optRefine of
		RefAll -> do
		r <- checkSat $ checkStrongConsensusCompleteSat checkCorrectness pp
		@@ -121,16 +119,16 @@ checkStrongConsensus' pp refinements = do
		case optRefine of
		RefDefault ->
		let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
		in refineStrongConsensus pp refinementMethods refinements c
		in refineStrongConsensus checkCorrectness pp refinementMethods refinements c
		RefList refinementMethods ->
		refineStrongConsensus pp refinementMethods refinements c
		refineStrongConsensus checkCorrectness pp refinementMethods refinements c
		RefAll -> return (Nothing, refinements)

		refineStrongConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
		refineStrongConsensus :: Bool -> PopulationProtocol -> [RefinementType] -> RefinementObjects ->
		StrongConsensusCounterExample ->
		OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
		refineStrongConsensus pp [] refinements c = return (Just c, refinements)
		refineStrongConsensus pp (ref:refs) refinements c = do
		refineStrongConsensus _ _ [] refinements c = return (Just c, refinements)
		refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do
		let refinementMethod = case ref of
		TrapRefinement -> Solver.StrongConsensus.findTrapConstraintsSat
		SiphonRefinement -> Solver.StrongConsensus.findSiphonConstraintsSat
		@@ -139,7 +137,7 @@ refineStrongConsensus pp (ref:refs) refinements c = do
		r <- checkSatMin $ refinementMethod pp c
		case r of
		Nothing -> do
		refineStrongConsensus pp refs refinements c
		refineStrongConsensus checkCorrectness pp refs refinements c
		Just refinement -> do
		let (utraps, usiphons) = refinements
		let refinements' = case ref of
		@@ -147,7 +145,7 @@ refineStrongConsensus pp (ref:refs) refinements c = do
		SiphonRefinement -> (utraps, refinement:usiphons)
		UTrapRefinement -> (refinement:utraps, usiphons)
		USiphonRefinement -> (utraps, refinement:usiphons)
		checkStrongConsensus' pp refinements'
		checkStrongConsensus' checkCorrectness pp refinements'

		checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
		checkLayeredTermination pp = do

src/Options.hs

+11 −13

Original line number	Diff line number	Diff line
		@@ -38,7 +38,6 @@ data Options = Options { inputFormat :: InputFormat
		, optShowHelp :: Bool
		, optShowVersion :: Bool
		, optProperties :: PropertyOption
		, optCorrectness :: Bool
		, optRefinementType :: RefinementOption
		, optMinimizeRefinement :: Int
		, optSMTAuto :: Bool
		@@ -55,7 +54,6 @@ startOptions = Options { inputFormat = InPP
		, optShowHelp = False
		, optShowVersion = False
		, optProperties = PropDefault
		, optCorrectness = False
		, optRefinementType = RefDefault
		, optMinimizeRefinement = 0
		, optSMTAuto = True
		@@ -66,26 +64,26 @@ startOptions = Options { inputFormat = InPP
		, optPrintStructure = False
		}

		addProperty :: Property -> Options -> Either String Options
		addProperty prop opt =
		Right opt {
		optProperties = case optProperties opt of
		PropDefault -> PropList [prop]
		(PropList props) -> PropList (props ++ [prop])
		}

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

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

		, Option "" ["correctness"]
		(NoArg (\opt -> Right opt { optCorrectness = True }))
		(NoArg (addProperty StrongConsensusWithCorrectness))
		"Prove that the protocol correctly satisfies the given predicate"

		, Option "i" ["invariant"]

src/Property.hs

+3 −2

Original line number	Diff line number	Diff line
		@@ -77,13 +77,14 @@ instance Functor Formula where
		fmap f (p :&: q) = fmap f p :&: fmap f q
		fmap f (p :\|: q) = fmap f p :\|: fmap f q

		data Property = Correctness
		\| LayeredTermination
		data Property = LayeredTermination
		\| StrongConsensus
		\| StrongConsensusWithCorrectness

		instance Show Property where
		show LayeredTermination = "layered termination"
		show StrongConsensus = "strong consensus"
		show StrongConsensusWithCorrectness = "strong consensus with correctness"

		data PropResult = Satisfied \| Unsatisfied \| Unknown deriving (Eq)