From c9113b43b8e45f84fae803f846b0ad36e31e0ea1 Mon Sep 17 00:00:00 2001 From: Philipp Meyer Date: Tue, 2 May 2017 15:34:15 +0200 Subject: [PATCH] Rename options and properties --- src/Main.hs | 106 +++++++----------- src/Options.hs | 47 ++++---- src/Parser/PP.hs | 30 ++--- src/Property.hs | 68 ++--------- ...kingReachable.hs => LayeredTermination.hs} | 70 ++++++------ ...sUniqueConsensus.hs => StrongConsensus.hs} | 20 ++-- 6 files changed, 129 insertions(+), 212 deletions(-) rename src/Solver/{TerminalMarkingReachable.hs => LayeredTermination.hs} (73%) rename src/Solver/{TerminalMarkingsUniqueConsensus.hs => StrongConsensus.hs} (93%) diff --git a/src/Main.hs b/src/Main.hs index 86e899d5..cc9b621f 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -21,8 +21,8 @@ import qualified Printer.DOT as DOTPrinter import Property import StructuralComputation import Solver -import Solver.TerminalMarkingsUniqueConsensus -import Solver.TerminalMarkingReachable +import Solver.LayeredTermination +import Solver.StrongConsensus writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO () writeFiles basename pp props = do @@ -47,9 +47,8 @@ checkFile file = do format <- opt inputFormat let parser = case format of InPP -> PPParser.parseContent - (pp,props) <- liftIO $ parseFile parser file - implicitProperties <- opt optProperties - let props' = props ++ map (makeImplicitProperty pp) implicitProperties + pp <- liftIO $ parseFile parser file + props <- opt optProperties verbosePut 1 $ "Analyzing " ++ showNetName pp verbosePut 2 $ "Number of states: " ++ show (length (states pp)) @@ -65,33 +64,22 @@ checkFile file = do output <- opt optOutput case output of Just outputfile -> - writeFiles outputfile pp props' + writeFiles outputfile pp props Nothing -> return () -- TODO: short-circuit? parallel? - rs <- mapM (checkProperty pp) props' + rs <- mapM (checkProperty pp) props verbosePut 0 "" return $ resultsAnd rs -makeImplicitProperty :: PopulationProtocol -> ImplicitProperty -> Property -makeImplicitProperty _ TerminalMarkingsUniqueConsensus = - Property "reachable terminal markings have a unique consensus" $ Constraint TerminalMarkingsUniqueConsensusConstraint -makeImplicitProperty _ TerminalMarkingReachable = - Property "terminal marking reachable" $ Constraint TerminalMarkingReachableConstraint - checkProperty :: PopulationProtocol -> Property -> OptIO PropResult -checkProperty pp p = do - verbosePut 1 $ "\nChecking " ++ showPropertyName p - verbosePut 3 $ show p - r <- case pcont p of --- (Safety pf) -> checkSafetyProperty pp pf --- (Liveness pf) -> checkLivenessProperty pp pf - (Constraint pc) -> checkConstraintProperty pp pc - verbosePut 0 $ showPropertyName p ++ " " ++ - case r of - Satisfied -> "is satisfied." - Unsatisfied -> "is not satisfied." - Unknown-> "may not be satisfied." +checkProperty pp prop = do + verbosePut 1 $ "\nChecking " ++ show prop + r <- case prop of + Correctness -> error "not yet implemented" + LayeredTermination -> checkLayeredTermination pp + StrongConsensus -> checkStrongConsensus pp + verbosePut 0 $ show prop ++ " " ++ show r return r printInvariant :: (Show a, Invariant a) => (Maybe [a], [a]) -> OptIO PropResult @@ -112,66 +100,60 @@ printInvariant (baseInvResult, addedInv) = mapM_ (putLine . show) addedInv return Satisfied -checkConstraintProperty :: PopulationProtocol -> ConstraintProperty -> OptIO PropResult -checkConstraintProperty pp cp = - case cp of - TerminalMarkingsUniqueConsensusConstraint -> checkTerminalMarkingsUniqueConsensusProperty pp - TerminalMarkingReachableConstraint -> checkTerminalMarkingReachableProperty pp - -checkTerminalMarkingsUniqueConsensusProperty :: PopulationProtocol -> OptIO PropResult -checkTerminalMarkingsUniqueConsensusProperty pp = do - r <- checkTerminalMarkingsUniqueConsensusProperty' pp [] [] [] +checkStrongConsensus :: PopulationProtocol -> OptIO PropResult +checkStrongConsensus pp = do + r <- checkStrongConsensus' pp [] [] [] case r of (Nothing, _, _, _) -> return Satisfied (Just _, _, _, _) -> return Unknown -checkTerminalMarkingsUniqueConsensusProperty' :: PopulationProtocol -> +checkStrongConsensus' :: PopulationProtocol -> [Trap] -> [Siphon] -> [StableInequality] -> - OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality]) -checkTerminalMarkingsUniqueConsensusProperty' pp utraps usiphons inequalities = do - r <- checkSat $ checkTerminalMarkingsUniqueConsensusSat pp utraps usiphons inequalities + OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality]) +checkStrongConsensus' pp utraps usiphons inequalities = do + r <- checkSat $ checkStrongConsensusSat pp utraps usiphons inequalities case r of Nothing -> return (Nothing, utraps, usiphons, inequalities) Just c -> do refine <- opt optRefinementType if isJust refine then - refineTerminalMarkingsUniqueConsensusProperty pp utraps usiphons inequalities c + refineStrongConsensus pp utraps usiphons inequalities c else return (Just c, utraps, usiphons, inequalities) -refineTerminalMarkingsUniqueConsensusProperty :: PopulationProtocol -> - [Trap] -> [Siphon] -> [StableInequality] -> TerminalMarkingsUniqueConsensusCounterExample -> - OptIO (Maybe TerminalMarkingsUniqueConsensusCounterExample, [Trap], [Siphon], [StableInequality]) -refineTerminalMarkingsUniqueConsensusProperty pp utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do - r1 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findTrapConstraintsSat pp m0 m1 m2 x1 x2 +refineStrongConsensus :: PopulationProtocol -> + [Trap] -> [Siphon] -> [StableInequality] -> StrongConsensusCounterExample -> + OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality]) +refineStrongConsensus pp utraps usiphons inequalities c@(m0, m1, m2, x1, x2) = do + r1 <- checkSatMin $ Solver.StrongConsensus.findTrapConstraintsSat pp m0 m1 m2 x1 x2 case r1 of Nothing -> do - r2 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 + r2 <- checkSatMin $ Solver.StrongConsensus.findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 case r2 of Nothing -> do - r3 <- checkSatMin $ Solver.TerminalMarkingsUniqueConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2 + r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2 case r3 of Nothing -> return (Just c, utraps, usiphons, inequalities) Just utrap -> - checkTerminalMarkingsUniqueConsensusProperty' pp (utrap:utraps) usiphons inequalities + checkStrongConsensus' pp (utrap:utraps) usiphons inequalities Just usiphon -> - checkTerminalMarkingsUniqueConsensusProperty' pp utraps (usiphon:usiphons) inequalities + checkStrongConsensus' pp utraps (usiphon:usiphons) inequalities Just trap -> - checkTerminalMarkingsUniqueConsensusProperty' pp (trap:utraps) usiphons inequalities + checkStrongConsensus' pp (trap:utraps) usiphons inequalities -checkTerminalMarkingReachableProperty :: PopulationProtocol -> OptIO PropResult -checkTerminalMarkingReachableProperty pp = do +checkLayeredTermination :: PopulationProtocol -> OptIO PropResult +checkLayeredTermination pp = do let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp - checkTerminalMarkingReachableProperty' pp nonTrivialTriplets 1 $ genericLength $ transitions pp + checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp -checkTerminalMarkingReachableProperty' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult -checkTerminalMarkingReachableProperty' pp triplets k kmax = do +checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult +checkLayeredTermination' pp triplets k kmax = do verbosePut 1 $ "Checking terminal marking reachable with at most " ++ show k ++ " partitions" - r <- checkSatMin $ checkTerminalMarkingReachableSat pp triplets k + r <- checkSatMin $ checkLayeredTerminationSat pp triplets k case r of Nothing -> if k < kmax then - checkTerminalMarkingReachableProperty' pp triplets (k + 1) kmax + checkLayeredTermination' pp triplets (k + 1) kmax else return Unknown Just inv -> do @@ -195,15 +177,13 @@ main = do rs <- runReaderT (mapM checkFile files) opts' -- TODO: short-circuit with Control.Monad.Loops? parallel -- execution? - case resultsAnd rs of + let r = resultsAnd rs + case r of Satisfied -> - exitSuccessWith "All properties satisfied." - Unsatisfied -> - exitFailureWith "Some properties are not satisfied" - Unknown -> - exitFailureWith "Some properties may not be satisfied." + exitSuccessWith $ "All properties " ++ show r + _ -> + exitFailureWith $ "Some properties " ++ show r --- TODO: Always exit with exit code 0 unless an error occured exitSuccessWith :: String -> IO () exitSuccessWith msg = do putStrLn msg diff --git a/src/Options.hs b/src/Options.hs index f6a08718..592b3279 100644 --- a/src/Options.hs +++ b/src/Options.hs @@ -2,7 +2,7 @@ module Options (InputFormat(..),OutputFormat(..),RefinementType(..), - ImplicitProperty(..),Options(..),startOptions,options,parseArgs, + Options(..),startOptions,options,parseArgs, usageInformation) where @@ -10,6 +10,8 @@ import Control.Applicative ((<$>)) import System.Console.GetOpt import System.Environment (getArgs) +import Property (Property(..)) + data InputFormat = InPP deriving (Read) data OutputFormat = OutDOT deriving (Read) @@ -18,10 +20,6 @@ instance Show InputFormat where instance Show OutputFormat where show OutDOT = "DOT" -data ImplicitProperty = TerminalMarkingsUniqueConsensus - | TerminalMarkingReachable - deriving (Show,Read) - data RefinementType = TrapRefinement | SiphonRefinement | UTrapRefinement @@ -32,12 +30,11 @@ data Options = Options { inputFormat :: InputFormat , optVerbosity :: Int , optShowHelp :: Bool , optShowVersion :: Bool - , optProperties :: [ImplicitProperty] + , optProperties :: [Property] , optRefinementType :: Maybe [RefinementType] , optMinimizeRefinement :: Int , optSMTAuto :: Bool , optInvariant :: Bool - , optBoolConst :: Bool , optOutput :: Maybe String , outputFormat :: OutputFormat , optUseProperties :: Bool @@ -54,7 +51,6 @@ startOptions = Options { inputFormat = InPP , optMinimizeRefinement = 0 , optSMTAuto = True , optInvariant = False - , optBoolConst = False , optOutput = Nothing , outputFormat = OutDOT , optUseProperties = True @@ -63,35 +59,22 @@ startOptions = Options { inputFormat = InPP options :: [ OptDescr (Options -> Either String Options) ] options = - [ Option "" ["pp"] - (NoArg (\opt -> Right opt { inputFormat = InPP })) - "Use the population protocol input format" - - , Option "" ["structure"] - (NoArg (\opt -> Right opt { optPrintStructure = True })) - "Print structural information" - - , Option "" ["terminal-markings-unique-consensus"] + [ Option "" ["layered-termination"] (NoArg (\opt -> Right opt { - optProperties = optProperties opt ++ [TerminalMarkingsUniqueConsensus] + optProperties = optProperties opt ++ [LayeredTermination] })) - "Prove that terminal markings have a unique consensus" + "Prove that the protocol satisfies layered termination" - , Option "" ["terminal-marking-reachable"] + , Option "" ["strong-consensus"] (NoArg (\opt -> Right opt { - optProperties = optProperties opt ++ [TerminalMarkingReachable] + optProperties = optProperties opt ++ [StrongConsensus] })) - "Prove that a terminal marking is reachable" + "Prove that the protocol satisfies strong consensus" , Option "i" ["invariant"] (NoArg (\opt -> Right opt { optInvariant = True })) "Generate an invariant" - , Option "" ["bool-const"] - (NoArg (\opt -> Right opt { optBoolConst = True })) - ("Use boolean constraints instead of integer ones\n" ++ - " for transition invariant") - , Option "r" ["refinement"] (ReqArg (\arg opt -> let addRef ref = @@ -111,6 +94,16 @@ options = "METHOD") ("Refine with METHOD (trap, siphon, utrap, usiphon)") + , Option "s" ["structure"] + (NoArg (\opt -> Right opt { optPrintStructure = True })) + "Print structural information" + + + , Option "" ["in-pp"] + (NoArg (\opt -> Right opt { inputFormat = InPP })) + "Use the population protocol input format" + + , Option "o" ["output"] (ReqArg (\arg opt -> Right opt { optOutput = Just arg diff --git a/src/Parser/PP.hs b/src/Parser/PP.hs index bd2c3887..3587d87b 100644 --- a/src/Parser/PP.hs +++ b/src/Parser/PP.hs @@ -187,29 +187,17 @@ formAtom = try linIneq formula :: Parser (Formula String) formula = buildExpressionParser formOperatorTable formAtom "formula" -propertyType :: Parser PropertyType -propertyType = - (reserved "safety" *> return SafetyType) <|> - (reserved "liveness" *> return LivenessType) - -property :: Parser Property -property = do - pt <- propertyType - reserved "property" +predicate :: Parser (Formula PopulationProtocol.State) +predicate = do + reserved "predicate" name <- option "" ident - case pt of - SafetyType -> do - form <- braces formula - return Property - { pname=name, pcont=Safety (fmap PopulationProtocol.State form) } - LivenessType -> do - form <- braces formula - return Property { pname=name, pcont=Liveness (fmap Transition form) } - -parseContent :: Parser (PopulationProtocol,[Property]) + form <- braces formula + return (fmap PopulationProtocol.State form) + +parseContent :: Parser PopulationProtocol parseContent = do whiteSpace pp <- populationProtocol - properties <- many property +-- properties <- many predicate eof - return (pp, properties) + return pp diff --git a/src/Property.hs b/src/Property.hs index f16df313..ffcc0d18 100644 --- a/src/Property.hs +++ b/src/Property.hs @@ -2,11 +2,6 @@ module Property (Property(..), - showPropertyName, - renameProperty, - PropertyType(..), - PropertyContent(..), - ConstraintProperty(..), Formula(..), Op(..), Term(..), @@ -18,8 +13,6 @@ module Property resultsOr) where -import PopulationProtocol - data Term a = Var a | Const Integer @@ -84,58 +77,21 @@ instance Functor Formula where fmap f (p :&: q) = fmap f p :&: fmap f q fmap f (p :|: q) = fmap f p :|: fmap f q --- TODO: add functions to transform formula to CNF/DNF - -data PropertyType = SafetyType - | LivenessType - | ConstraintType - -data ConstraintProperty = TerminalMarkingsUniqueConsensusConstraint - | TerminalMarkingReachableConstraint - -instance Show ConstraintProperty where - show TerminalMarkingsUniqueConsensusConstraint = "reachable terminal markings have a unique consensus" - show TerminalMarkingReachableConstraint = "terminal marking reachable" - -data PropertyContent = Safety (Formula State) - | Liveness (Formula Transition) - | Constraint ConstraintProperty +data Property = Correctness + | LayeredTermination + | StrongConsensus -showPropertyType :: PropertyContent -> String -showPropertyType (Safety _) = "safety" -showPropertyType (Liveness _) = "liveness" -showPropertyType (Constraint _) = "constraint" - -showPropertyContent :: PropertyContent -> String -showPropertyContent (Safety f) = show f -showPropertyContent (Liveness f) = show f -showPropertyContent (Constraint c) = show c - -instance Show PropertyContent where - show pc = showPropertyType pc ++ " (" ++ showPropertyContent pc ++ ")" +instance Show Property where + show Correctness = "correctness" + show LayeredTermination = "layered termination" + show StrongConsensus = "strong consensus" -data Property = Property { - pname :: String, - pcont :: PropertyContent -} +data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq) -instance Show Property where - show p = - showPropertyName p ++ - " { " ++ showPropertyContent (pcont p) ++ " }" - -renameProperty :: (String -> String) -> Property -> Property -renameProperty f (Property pn (Safety pf)) = - Property pn (Safety (fmap (renameState f) pf)) -renameProperty f (Property pn (Liveness pf)) = - Property pn (Liveness (fmap (renameTransition f) pf)) -renameProperty _ p = p - -showPropertyName :: Property -> String -showPropertyName p = showPropertyType (pcont p) ++ " property" ++ - (if null (pname p) then "" else " " ++ show (pname p)) - -data PropResult = Satisfied | Unsatisfied | Unknown deriving (Show,Read,Eq) +instance Show PropResult where + show Satisfied = "satisfied" + show Unsatisfied = "not satisfied" + show Unknown = "may not be satisfied" resultAnd :: PropResult -> PropResult -> PropResult resultAnd Satisfied x = x diff --git a/src/Solver/TerminalMarkingReachable.hs b/src/Solver/LayeredTermination.hs similarity index 73% rename from src/Solver/TerminalMarkingReachable.hs rename to src/Solver/LayeredTermination.hs index e615ab6b..2e52247f 100644 --- a/src/Solver/TerminalMarkingReachable.hs +++ b/src/Solver/LayeredTermination.hs @@ -1,8 +1,8 @@ {-# LANGUAGE FlexibleContexts #-} -module Solver.TerminalMarkingReachable - (checkTerminalMarkingReachableSat, - TerminalMarkingReachableInvariant) +module Solver.LayeredTermination + (checkLayeredTerminationSat, + LayeredTerminationInvariant) where import Data.SBV @@ -17,15 +17,15 @@ import StructuralComputation type InvariantSize = ([Int], [Integer], [Int]) -type TerminalMarkingReachableInvariant = [BlockInvariant] -data BlockInvariant = - BlockInvariant (Integer, [Transition], IVector State) +type LayeredTerminationInvariant = [LayerInvariant] +data LayerInvariant = + LayerInvariant (Integer, [Transition], IVector State) -instance Invariant BlockInvariant where - invariantSize (BlockInvariant (_, ti, yi)) = if null ti then 0 else size yi +instance Invariant LayerInvariant where + invariantSize (LayerInvariant (_, ti, yi)) = if null ti then 0 else size yi -instance Show BlockInvariant where - show (BlockInvariant (i, ti, yi)) = +instance Show LayerInvariant where + show (LayerInvariant (i, ti, yi)) = "T_" ++ show i ++ ":\n" ++ unlines (map show ti) ++ (if null ti then "" else "\nY_" ++ show i ++ ": " ++ intercalate " + " (map showWeighted (items yi)) ++ "\n") @@ -38,8 +38,8 @@ checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool checkNonNegativityConstraints xs = bAnd $ map nonNegativityConstraints xs -blockTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool -blockTerminationConstraints pp i b y = +layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool +layerTerminationConstraints pp i b y = bAnd $ map checkTransition $ transitions pp where checkTransition t = let incoming = map addState $ lpre pp t @@ -49,46 +49,46 @@ blockTerminationConstraints pp i b y = terminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> [SIMap State] -> SBool terminationConstraints pp k b ys = - bAnd $ [blockTerminationConstraints pp i b y | (i,y) <- zip [1..] ys] + bAnd $ [layerTerminationConstraints pp i b y | (i,y) <- zip [1..] ys] -blockConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SBool -blockConstraints pp k b = - bAnd $ map checkBlock $ transitions pp - where checkBlock t = literal 1 .<= val b t &&& val b t .<= literal k +layerConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SBool +layerConstraints pp k b = + bAnd $ map checkLayer $ transitions pp + where checkLayer t = literal 1 .<= val b t &&& val b t .<= literal k -blockOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool -blockOrderConstraints pp triplets k b = +layerOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool +layerOrderConstraints pp triplets k b = bAnd $ map checkTriplet triplets where checkTriplet (s,t,ts) = (val b s .> val b t) ==> bOr (map (\t' -> val b t' .== val b t) ts) -checkTerminalMarkingReachable :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool -checkTerminalMarkingReachable pp triplets k b ys sizeLimit = - blockConstraints pp k b &&& +checkLayeredTermination :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool +checkLayeredTermination pp triplets k b ys sizeLimit = + layerConstraints pp k b &&& terminationConstraints pp k b ys &&& - blockOrderConstraints pp triplets k b &&& + layerOrderConstraints pp triplets k b &&& checkNonNegativityConstraints ys &&& checkSizeLimit k b ys sizeLimit -checkTerminalMarkingReachableSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer TerminalMarkingReachableInvariant InvariantSize -checkTerminalMarkingReachableSat pp triplets k = +checkLayeredTerminationSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize +checkLayeredTerminationSat pp triplets k = let makeYName i = (++) (genericReplicate i '\'') ys = [makeVarMapWith (makeYName i) $ states pp | i <- [1..k]] b = makeVarMap $ transitions pp in (minimizeMethod, \sizeLimit -> ("terminal marking reachable", "invariant", concat (map getNames ys) ++ getNames b, - \fm -> checkTerminalMarkingReachable pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit, + \fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit, \fm -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys))) minimizeMethod :: Int -> InvariantSize -> String minimizeMethod 1 (curYSize, _, _) = "number of states in y less than " ++ show (sum curYSize) -minimizeMethod 2 (_, _, curTSize) = "number of transitions in last block less than " ++ show (last curTSize) -minimizeMethod 3 (curYSize, _, curTSize) = "number of transitions in last block less than " ++ show (last curTSize) ++ +minimizeMethod 2 (_, _, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize) +minimizeMethod 3 (curYSize, _, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize) ++ " or same number of transitions and number of states in y less than " ++ show curYSize minimizeMethod 4 (_, curYMax, _) = "maximum coefficient in y is less than " ++ show (maximum curYMax) minimizeMethod 5 (curYSize, curYMax, _) = "number of states in y less than " ++ show (sum curYSize) ++ " or same number of states and maximum coefficient in y is less than " ++ show (maximum curYMax) -minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last block less than " ++ show (last curTSize) ++ +minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize) ++ " or same number of transitions and number of states in y less than " ++ show (sum curYSize) ++ " or same number of transitions and same number of states and maximum coefficient in y less than " ++ show (maximum curYMax) minimizeMethod _ _ = error "minimization method not supported" @@ -115,11 +115,11 @@ checkSizeLimit k b ys (Just (6, (curYSize, curYMax, curTSize))) = ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax)))))) checkSizeLimit _ _ _ (Just (_, _)) = error "minimization method not supported" -invariantFromAssignment :: PopulationProtocol -> Integer -> IMap Transition -> [IMap State] -> (TerminalMarkingReachableInvariant, InvariantSize) +invariantFromAssignment :: PopulationProtocol -> Integer -> IMap Transition -> [IMap State] -> (LayeredTerminationInvariant, InvariantSize) invariantFromAssignment pp k b ys = - (invariant, (map invariantLength invariant, map invariantMaxCoefficient invariant, map blockSize invariant)) + (invariant, (map invariantLength invariant, map invariantMaxCoefficient invariant, map layerSize invariant)) where - invariant = [BlockInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys] - invariantMaxCoefficient (BlockInvariant (_, _, yi)) = maximum $ vals yi - invariantLength (BlockInvariant (_, _, yi)) = size yi - blockSize (BlockInvariant (_, ti, _)) = length ti + invariant = [LayerInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys] + invariantMaxCoefficient (LayerInvariant (_, _, yi)) = maximum $ vals yi + invariantLength (LayerInvariant (_, _, yi)) = size yi + layerSize (LayerInvariant (_, ti, _)) = length ti diff --git a/src/Solver/TerminalMarkingsUniqueConsensus.hs b/src/Solver/StrongConsensus.hs similarity index 93% rename from src/Solver/TerminalMarkingsUniqueConsensus.hs rename to src/Solver/StrongConsensus.hs index f2a39dfc..955736c2 100644 --- a/src/Solver/TerminalMarkingsUniqueConsensus.hs +++ b/src/Solver/StrongConsensus.hs @@ -1,8 +1,8 @@ {-# LANGUAGE FlexibleContexts #-} -module Solver.TerminalMarkingsUniqueConsensus - (checkTerminalMarkingsUniqueConsensusSat, - TerminalMarkingsUniqueConsensusCounterExample, +module Solver.StrongConsensus + (checkStrongConsensusSat, + StrongConsensusCounterExample, findTrapConstraintsSat, findUTrapConstraintsSat, findUSiphonConstraintsSat, @@ -19,7 +19,7 @@ import PopulationProtocol import Property import Solver -type TerminalMarkingsUniqueConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector) +type StrongConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector) type StableInequality = (IMap State, Integer) @@ -96,9 +96,9 @@ checkInequalityConstraints :: PopulationProtocol -> SIMap State -> SIMap State - checkInequalityConstraints pp m0 m1 m2 inequalities = bAnd [ checkInequalityConstraint pp m0 m1 m2 i | i <- inequalities ] -checkTerminalMarkingsUniqueConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> +checkStrongConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Trap] -> [Siphon] -> [StableInequality] -> SBool -checkTerminalMarkingsUniqueConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalities = +checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalities = stateEquationConstraints pp m0 m1 x1 &&& stateEquationConstraints pp m0 m2 x2 &&& initialMarkingConstraints pp m0 &&& @@ -114,8 +114,8 @@ checkTerminalMarkingsUniqueConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalit checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons &&& checkInequalityConstraints pp m0 m1 m2 inequalities -checkTerminalMarkingsUniqueConsensusSat :: PopulationProtocol -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample -checkTerminalMarkingsUniqueConsensusSat pp utraps usiphons inequalities = +checkStrongConsensusSat :: PopulationProtocol -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer StrongConsensusCounterExample +checkStrongConsensusSat pp utraps usiphons inequalities = let m0 = makeVarMap $ states pp m1 = makeVarMapWith prime $ states pp m2 = makeVarMapWith (prime . prime) $ states pp @@ -123,10 +123,10 @@ checkTerminalMarkingsUniqueConsensusSat pp utraps usiphons inequalities = x2 = makeVarMapWith prime $ transitions pp in ("unique terminal marking", "(m0, m1, m2, x1, x2)", getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2, - \fm -> checkTerminalMarkingsUniqueConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) utraps usiphons inequalities, + \fm -> checkStrongConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) utraps usiphons inequalities, \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2)) -markingsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample +markingsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample markingsFromAssignment m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2) -- GitLab