Allow specification of refinements in different orders (650084a7) · Commits · i7 / peregrine

src/Main.hs

+37 −31

Original line number	Diff line number	Diff line
		@@ -92,42 +92,48 @@ printInvariant inv = do

		checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
		checkStrongConsensus pp = do
		r <- checkStrongConsensus' pp [] []
		r <- checkStrongConsensus' pp ([], [])
		case r of
		(Nothing, _, _) -> return Satisfied
		(Just _, _, _) -> return Unknown
		(Nothing, _) -> return Satisfied
		(Just _, _) -> return Unknown

		checkStrongConsensus' :: PopulationProtocol -> [Trap] -> [Siphon] ->
		OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon])
		checkStrongConsensus' pp utraps usiphons = do
		r <- checkSat $ checkStrongConsensusSat pp utraps usiphons
		checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
		OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
		checkStrongConsensus' pp refinements = do
		r <- checkSat $ checkStrongConsensusSat pp refinements
		case r of
		Nothing -> return (Nothing, utraps, usiphons)
		Nothing -> return (Nothing, refinements)
		Just c -> do
		refine <- opt optRefinementType
		if isJust refine then
		refineStrongConsensus pp utraps usiphons c
		else
		return (Just c, utraps, usiphons)

		refineStrongConsensus :: PopulationProtocol -> [Trap] -> [Siphon] -> StrongConsensusCounterExample ->
		OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon])
		refineStrongConsensus pp utraps usiphons c = do
		r1 <- checkSatMin $ Solver.StrongConsensus.findTrapConstraintsSat pp c
		case r1 of
		Nothing -> do
		r2 <- checkSatMin $ Solver.StrongConsensus.findUSiphonConstraintsSat pp c
		case r2 of
		optRefine <- opt optRefinementType
		let refinementMethods = case optRefine of
		RefDefault -> [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
		RefList rs -> rs
		RefAll -> error "not yet implemented"
		refineStrongConsensus pp refinementMethods refinements c


		refineStrongConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
		StrongConsensusCounterExample ->
		OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
		refineStrongConsensus pp [] refinements c = return (Just c, refinements)
		refineStrongConsensus pp (ref:refs) refinements c = do
		let refinementMethod = case ref of
		TrapRefinement -> Solver.StrongConsensus.findTrapConstraintsSat
		SiphonRefinement -> Solver.StrongConsensus.findSiphonConstraintsSat
		UTrapRefinement -> Solver.StrongConsensus.findUTrapConstraintsSat
		USiphonRefinement -> Solver.StrongConsensus.findUSiphonConstraintsSat
		r <- checkSatMin $ refinementMethod pp c
		case r of
		Nothing -> do
		r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp c
		case r3 of
		Nothing -> return (Just c, utraps, usiphons)
		Just utrap ->
		checkStrongConsensus' pp (utrap:utraps) usiphons
		Just usiphon ->
		checkStrongConsensus' pp utraps (usiphon:usiphons)
		Just trap ->
		checkStrongConsensus' pp (trap:utraps) usiphons
		refineStrongConsensus pp refs refinements c
		Just refinement -> do
		let (utraps, usiphons) = refinements
		let refinements' = case ref of
		TrapRefinement -> (refinement:utraps, usiphons)
		SiphonRefinement -> (utraps, refinement:usiphons)
		UTrapRefinement -> (refinement:utraps, usiphons)
		USiphonRefinement -> (utraps, refinement:usiphons)
		checkStrongConsensus' pp refinements'

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

src/Options.hs

+18 −14

Original line number	Diff line number	Diff line
		{-# LANGUAGE TupleSections #-}

		module Options
		(InputFormat(..),OutputFormat(..),RefinementType(..),
		(InputFormat(..),OutputFormat(..),RefinementType(..),RefinementOption(..),
		Options(..),startOptions,options,parseArgs,
		usageInformation)
		where
		@@ -26,12 +26,16 @@ data RefinementType = TrapRefinement
		\| USiphonRefinement
		deriving (Show,Read)

		data RefinementOption = RefDefault
		\| RefList [RefinementType]
		\| RefAll

		data Options = Options { inputFormat :: InputFormat
		, optVerbosity :: Int
		, optShowHelp :: Bool
		, optShowVersion :: Bool
		, optProperties :: [Property]
		, optRefinementType :: Maybe [RefinementType]
		, optRefinementType :: RefinementOption
		, optMinimizeRefinement :: Int
		, optSMTAuto :: Bool
		, optInvariant :: Bool
		@@ -47,7 +51,7 @@ startOptions = Options { inputFormat = InPP
		, optShowHelp = False
		, optShowVersion = False
		, optProperties = []
		, optRefinementType = Just [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
		, optRefinementType = RefDefault
		, optMinimizeRefinement = 0
		, optSMTAuto = True
		, optInvariant = False
		@@ -78,21 +82,21 @@ options =
		, Option "r" ["refinement"]
		(ReqArg (\arg opt ->
		let addRef ref =
		Right opt { optRefinementType =
		case optRefinementType opt of
		Nothing -> Just [ref]
		Just(refs) -> Just (refs ++ [ref])

		}
		RefDefault -> RefList [ref]
		(RefList refs) -> RefList (refs ++ [ref])
		RefAll -> RefAll
		in case arg of
		"trap" -> addRef TrapRefinement
		"siphon" -> addRef SiphonRefinement
		"utrap" -> addRef UTrapRefinement
		"usiphon" -> addRef USiphonRefinement
		"none" -> Right opt { optRefinementType = RefList [] }
		"trap" -> Right opt { optRefinementType = addRef TrapRefinement }
		"siphon" -> Right opt { optRefinementType = addRef SiphonRefinement }
		"utrap" -> Right opt { optRefinementType = addRef UTrapRefinement }
		"usiphon" -> Right opt { optRefinementType = addRef USiphonRefinement }
		"all" -> Right opt { optRefinementType = RefAll }
		_ -> Left ("invalid argument for refinement method: " ++ arg)
		)
		"METHOD")
		("Refine with METHOD (trap, siphon, utrap, usiphon)")
		("Refine with METHOD (trap, siphon, utrap, usiphon, none, all)")

		, Option "s" ["structure"]
		(NoArg (\opt -> Right opt { optPrintStructure = True }))

src/Solver/StrongConsensus.hs

+33 −8

Original line number	Diff line number	Diff line
		@@ -3,7 +3,9 @@
		module Solver.StrongConsensus
		(checkStrongConsensusSat,
		StrongConsensusCounterExample,
		RefinementObjects,
		findTrapConstraintsSat,
		findSiphonConstraintsSat,
		findUTrapConstraintsSat,
		findUSiphonConstraintsSat)
		where
		@@ -18,6 +20,7 @@ import Property
		import Solver

		type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
		type RefinementObjects = ([Trap], [Siphon])

		stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
		stateEquationConstraints pp m0 m x =
		@@ -84,8 +87,8 @@ checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons =
		bAnd $ map (checkUSiphon pp m0 m1 m2 x1 x2) siphons

		checkStrongConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
		[Trap] -> [Siphon] -> SBool
		checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons =
		RefinementObjects -> SBool
		checkStrongConsensus pp m0 m1 m2 x1 x2 (utraps, usiphons) =
		stateEquationConstraints pp m0 m1 x1 &&&
		stateEquationConstraints pp m0 m2 x2 &&&
		initialConfiguration pp m0 &&&
		@@ -100,8 +103,8 @@ checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons =
		checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
		checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons

		checkStrongConsensusSat :: PopulationProtocol -> [Trap] -> [Siphon] -> ConstraintProblem Integer StrongConsensusCounterExample
		checkStrongConsensusSat pp utraps usiphons =
		checkStrongConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
		checkStrongConsensusSat pp refinements =
		let m0 = makeVarMap $ states pp
		m1 = makeVarMapWith prime $ states pp
		m2 = makeVarMapWith (prime . prime) $ states pp
		@@ -109,11 +112,11 @@ checkStrongConsensusSat pp utraps usiphons =
		x2 = makeVarMapWith prime $ transitions pp
		in ("strong consensus", "(c0, c1, c2, x1, x2)",
		getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
		\fm -> checkStrongConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) utraps usiphons,
		\fm -> configurationsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
		\fm -> checkStrongConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) refinements,
		\fm -> counterExampleFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

		configurationsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
		configurationsFromAssignment m0 m1 m2 x1 x2 =
		counterExampleFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
		counterExampleFromAssignment m0 m1 m2 x1 x2 =
		(makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)

		-- trap and siphon refinement constraints
		@@ -130,6 +133,10 @@ trapConstraints :: PopulationProtocol -> SIMap State -> SBool
		trapConstraints pp b =
		bAnd $ map (trapConstraint pp b) $ transitions pp

		siphonConstraints :: PopulationProtocol -> SIMap State -> SBool
		siphonConstraints pp b =
		bAnd $ map (siphonConstraint pp b) $ transitions pp

		uTrapConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
		uTrapConstraints pp x b =
		bAnd $ map (trapConstraint pp b) $ elems x
		@@ -212,6 +219,24 @@ findUTrapConstraintsSat pp c =
		\fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit,
		\fm -> statesFromAssignment (fmap fm b)))

		findSiphonConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
		findSiphonConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
		checkSizeLimit b sizeLimit &&&
		checkBinary b &&&
		siphonConstraints pp b &&&
		statesUnmarkedByConfiguration pp m0 b &&&
		(statesPresetOfSequence pp x1 b \|\|\| statesPresetOfSequence pp x2 b)

		findSiphonConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
		findSiphonConstraintsSat pp c =
		let b = makeVarMap $ states pp
		in (minimizeMethod, \sizeLimit ->
		("siphon used by x1 or x2 and unmarked in m0", "siphon",
		getNames b,
		\fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit,
		\fm -> statesFromAssignment (fmap fm b)))


		findUSiphonConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
		findUSiphonConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
		checkSizeLimit b sizeLimit &&&