Add options to verify abstract population protocols

src/Main.hs

@@ -79,7 +79,8 @@ checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
 checkProperty pp prop = do
         verbosePut 1 $ "\nChecking " ++ show prop
         r <- case prop of
-                LayeredTermination -> checkLayeredTermination pp
+                LayeredTermination -> checkLayeredTermination False pp
+                DeterministicLayeredTermination -> checkLayeredTermination True pp
                 StrongConsensus -> checkStrongConsensus False pp
                 StrongConsensusWithCorrectness -> checkStrongConsensus True pp
                 ReachableTermConfigInConsensus -> checkReachableTermConfigInConsensus pp
@@ -115,7 +116,7 @@ checkReachableTermConfigInConsensus' pp refinements = do
                             in refineReachableTermConfigInConsensus pp refinementMethods refinements c
                         RefList refinementMethods ->
                             refineReachableTermConfigInConsensus pp refinementMethods refinements c
-                        RefAll -> return (Nothing, refinements)
+                        RefAll -> error "All refinement method not supported for checking reachable term config in consensus"
 
 refineReachableTermConfigInConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
         ReachableTermConfigInConsensusCounterExample ->
@@ -194,19 +195,19 @@ refineStrongConsensus checkCorrectness pp (ref:refs) refinements c = do
                          USiphonRefinement -> (utraps, refinement:usiphons)
                 checkStrongConsensus' checkCorrectness pp refinements'
 
-checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
-checkLayeredTermination pp = do
+checkLayeredTermination :: Bool -> PopulationProtocol -> OptIO PropResult
+checkLayeredTermination deterministic pp = do
         let nonTrivialTriplets = filter (not . trivialTriplet) $ generateTriplets pp
-        checkLayeredTermination' pp nonTrivialTriplets 1 $ genericLength $ transitions pp
+        checkLayeredTermination' deterministic pp nonTrivialTriplets 1 $ genericLength $ transitions pp
 
-checkLayeredTermination' :: PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
-checkLayeredTermination' pp triplets k kmax = do
+checkLayeredTermination' :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> Integer -> OptIO PropResult
+checkLayeredTermination' deterministic pp triplets k kmax = do
         verbosePut 1 $ "Checking layered termination with at most " ++ show k ++ " layers"
-        r <- checkSatMin $ checkLayeredTerminationSat pp triplets k
+        r <- checkSatMin $ checkLayeredTerminationSat deterministic pp triplets k
         case r of
             Nothing ->
                 if k < kmax then
-                    checkLayeredTermination' pp triplets (k + 1) kmax
+                    checkLayeredTermination' deterministic pp triplets (k + 1) kmax
                 else
                     return Unknown
             Just inv -> do

src/Options.hs

@@ -81,6 +81,10 @@ options =
         (NoArg (addProperty LayeredTermination))
         "Prove that the protocol satisfies layered termination"
 
+        , Option "" ["deterministic-layered-termination"]
+        (NoArg (addProperty DeterministicLayeredTermination))
+        "Prove that the protocol satisfies deterministic layered termination"
+
         , Option "" ["strong-consensus"]
         (NoArg (addProperty StrongConsensus))
         "Prove that the protocol satisfies strong consensus"

src/Property.hs

@@ -128,12 +128,14 @@ instance Functor Formula where
         fmap f (p :|: q) = fmap f p :|: fmap f q
 
 data Property = LayeredTermination
+              | DeterministicLayeredTermination
               | StrongConsensus
               | StrongConsensusWithCorrectness
               | ReachableTermConfigInConsensus
 
 instance Show Property where
         show LayeredTermination = "layered termination"
+        show DeterministicLayeredTermination = "deterministic layered termination"
         show StrongConsensus = "strong consensus"
         show StrongConsensusWithCorrectness = "strong consensus with correctness"
         show ReachableTermConfigInConsensus = "terminal configurations are in consensus"

src/Solver/LayeredTermination.hs

@@ -56,28 +56,35 @@ layerConstraints pp k b =
             bAnd $ map checkLayer $ transitions pp
         where checkLayer t = literal 1 .<= val b t &&& val b t .<= literal k
 
+deterministicLayerConstraints :: PopulationProtocol -> SIMap Transition -> SBool
+deterministicLayerConstraints pp b =
+            bAnd $ map checkTransition [ (t1,t2) | t1 <- transitions pp, t2 <- transitions pp, t1 /= t2, samePreset (t1,t2) ]
+        where checkTransition (t1,t2) = (val b t1 .== val b t2)
+              samePreset (t1,t2) = (lpre pp t1 == lpre pp t2)
+
 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)
 
-checkLayeredTermination :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
-checkLayeredTermination pp triplets k b ys sizeLimit =
+checkLayeredTermination :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
+checkLayeredTermination deterministic pp triplets k b ys sizeLimit =
         layerConstraints pp k b &&&
+        (if deterministic then deterministicLayerConstraints pp b else true) &&&
         terminationConstraints pp k b ys &&&
         layerOrderConstraints pp triplets k b &&&
         checkNonNegativityConstraints ys &&&
         checkSizeLimit k b ys sizeLimit
 
-checkLayeredTerminationSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize
-checkLayeredTerminationSat pp triplets k =
+checkLayeredTerminationSat :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize
+checkLayeredTerminationSat deterministic pp triplets k =
         let makeYName i = (++) (genericReplicate i '\'')
             ys = [makeVarMapWith (makeYName i) $ states pp | i <- [1..k]]
             b = makeVarMap $ transitions pp
         in  (minimizeMethod, \sizeLimit ->
             ("layered termination", "invariant",
              concat (map getNames ys) ++ getNames b,
-             \fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit,
+             \fm -> checkLayeredTermination deterministic 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