Add option to check that all potentially reachable terminal

configurations are in consensus

src/Main.hs

@@ -22,6 +22,7 @@ import StructuralComputation
 import Solver
 import Solver.LayeredTermination
 import Solver.StrongConsensus
+import Solver.ReachableTermConfigInConsensus
 
 writeFiles :: String -> PopulationProtocol -> [Property] -> OptIO ()
 writeFiles basename pp props = do
@@ -81,6 +82,7 @@ checkProperty pp prop = do
                 LayeredTermination -> checkLayeredTermination pp
                 StrongConsensus -> checkStrongConsensus False pp
                 StrongConsensusWithCorrectness -> checkStrongConsensus True pp
+                ReachableTermConfigInConsensus -> checkReachableTermConfigInConsensus pp
         verbosePut 0 $ show prop ++ " " ++ show r
         return r
 
@@ -92,6 +94,52 @@ printInvariant inv = do
                 " (total of " ++ show (sum invSize) ++ ")"
         mapM_ (putLine . show) inv
 
+checkReachableTermConfigInConsensus :: PopulationProtocol -> OptIO PropResult
+checkReachableTermConfigInConsensus pp = do
+        r <- checkReachableTermConfigInConsensus' pp ([], [])
+        case r of
+            (Nothing, _) -> return Satisfied
+            (Just _, _) -> return Unknown
+
+checkReachableTermConfigInConsensus' :: PopulationProtocol -> RefinementObjects ->
+        OptIO (Maybe ReachableTermConfigInConsensusCounterExample, RefinementObjects)
+checkReachableTermConfigInConsensus' pp refinements = do
+        optRefine <- opt optRefinementType
+        r <- checkSat $ checkReachableTermConfigInConsensusSat pp refinements
+        case r of
+            Nothing -> return (Nothing, refinements)
+            Just c -> do
+                case optRefine of
+                        RefDefault ->
+                            let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
+                            in refineReachableTermConfigInConsensus pp refinementMethods refinements c
+                        RefList refinementMethods ->
+                            refineReachableTermConfigInConsensus pp refinementMethods refinements c
+                        RefAll -> return (Nothing, refinements)
+
+refineReachableTermConfigInConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
+        ReachableTermConfigInConsensusCounterExample ->
+        OptIO (Maybe ReachableTermConfigInConsensusCounterExample, RefinementObjects)
+refineReachableTermConfigInConsensus _ [] refinements c = return (Just c, refinements)
+refineReachableTermConfigInConsensus pp (ref:refs) refinements c = do
+        let refinementMethod = case ref of
+                         TrapRefinement -> Solver.ReachableTermConfigInConsensus.findTrapConstraintsSat
+                         SiphonRefinement -> Solver.ReachableTermConfigInConsensus.findSiphonConstraintsSat
+                         UTrapRefinement -> Solver.ReachableTermConfigInConsensus.findUTrapConstraintsSat
+                         USiphonRefinement -> Solver.ReachableTermConfigInConsensus.findUSiphonConstraintsSat
+        r <- checkSatMin $ refinementMethod pp c
+        case r of
+            Nothing -> do
+                refineReachableTermConfigInConsensus 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)
+                checkReachableTermConfigInConsensus' pp refinements'
+
 checkStrongConsensus :: Bool -> PopulationProtocol -> OptIO PropResult
 checkStrongConsensus checkCorrectness pp = do
         r <- checkStrongConsensus' checkCorrectness pp ([], [])

src/Options.hs

@@ -89,6 +89,10 @@ options =
         (NoArg (addProperty StrongConsensusWithCorrectness))
         "Prove that the protocol correctly satisfies the given predicate"
 
+        , Option "" ["terminal-consensus"]
+        (NoArg (addProperty ReachableTermConfigInConsensus))
+        "Prove that reachable terminal configurations are in consensus"
+
         , Option "i" ["invariant"]
         (NoArg (\opt -> Right opt { optInvariant = True }))
         "Generate an invariant"

src/Property.hs

@@ -130,11 +130,13 @@ instance Functor Formula where
 data Property = LayeredTermination
               | StrongConsensus
               | StrongConsensusWithCorrectness
+              | ReachableTermConfigInConsensus
 
 instance Show Property where
         show LayeredTermination = "layered termination"
         show StrongConsensus = "strong consensus"
         show StrongConsensusWithCorrectness = "strong consensus with correctness"
+        show ReachableTermConfigInConsensus = "terminal configurations are in consensus"
 
 data PropResult = Satisfied | Unsatisfied | Unknown deriving (Eq)
 

src/Solver/ReachableTermConfigInConsensus.hs

+{-# LANGUAGE FlexibleContexts #-}
+
+module Solver.ReachableTermConfigInConsensus
+    (checkReachableTermConfigInConsensusSat,
+     ReachableTermConfigInConsensusCounterExample,
+     findTrapConstraintsSat,
+     findSiphonConstraintsSat,
+     findUTrapConstraintsSat,
+     findUSiphonConstraintsSat)
+where
+
+import Data.SBV
+import qualified Data.Map as M
+import Data.List ((\\),genericLength)
+
+import Util
+import PopulationProtocol
+import Property
+import Solver
+import Solver.Formula
+import Solver.StrongConsensus (RefinementObjects)
+
+import Debug.Trace
+
+type ReachableTermConfigInConsensusCounterExample = (Configuration, Configuration, FlowVector)
+
+stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
+stateEquationConstraints pp m0 m x =
+            bAnd $ map checkStateEquation $ states pp
+        where checkStateEquation q =
+                let incoming = map addTransition $ lpre pp q
+                    outgoing = map addTransition $ lpost pp q
+                in  val m0 q + sum incoming - sum outgoing .== val m q
+              addTransition (t,w) = literal w * val x t
+
+nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
+nonNegativityConstraints m =
+            bAnd $ map checkVal $ vals m
+        where checkVal x = x .>= 0
+
+terminalConstraints :: PopulationProtocol -> SIMap State -> SBool
+terminalConstraints pp m =
+            bAnd $ map checkTransition $ transitions pp
+        where checkTransition t = bOr $ map checkState $ lpre pp t
+              checkState (q,w) = val m q .<= literal (fromInteger (w - 1))
+
+initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
+initialConfiguration pp m0 =
+        (sum (mval m0 (initialStates pp)) .>= 2) &&&
+        (sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&&
+        (evaluateFormula (precondition pp) m0)
+
+differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SBool
+differentConsensusConstraints pp m =
+            oT &&& oF
+        where
+            oT = sum (mval m (trueStates pp)) .> 0
+            oF = sum (mval m (falseStates pp)) .> 0
+
+unmarkedByConfiguration :: [State] -> SIMap State -> SBool
+unmarkedByConfiguration r m = sum (mval m r) .== 0
+
+markedByConfiguration :: [State] -> SIMap State -> SBool
+markedByConfiguration r m = sum (mval m r) .> 0
+
+sequenceNotIn :: [Transition] -> SIMap Transition -> SBool
+sequenceNotIn u x = sum (mval x u) .== 0
+
+sequenceIn :: [Transition] -> SIMap Transition -> SBool
+sequenceIn u x = sum (mval x u) .> 0
+
+checkUTrap :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> Trap -> SBool
+checkUTrap pp m0 m1 x utrap =
+            (((sequenceIn upre x) &&& (sequenceNotIn uunmark x)) ==> (markedByConfiguration utrap m1))
+        where upost = mpost pp utrap
+              upre = mpre pp utrap
+              uunmark = upost \\ upre
+
+checkUTrapConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> [Trap] -> SBool
+checkUTrapConstraints pp m0 m1 x traps =
+        bAnd $ map (checkUTrap pp m0 m1 x) traps
+
+checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> Siphon -> SBool
+checkUSiphon pp m0 m1 x usiphon =
+            (((sequenceIn upost x) &&& (sequenceNotIn umark x)) ==> (markedByConfiguration usiphon m0))
+        where upost = mpost pp usiphon
+              upre = mpre pp usiphon
+              umark = upre \\ upost
+
+checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> [Siphon] -> SBool
+checkUSiphonConstraints pp m0 m1 x siphons =
+        bAnd $ map (checkUSiphon pp m0 m1 x) siphons
+
+checkReachableTermConfigInConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> RefinementObjects -> SBool
+checkReachableTermConfigInConsensus pp m0 m1 x (utraps, usiphons) =
+        stateEquationConstraints pp m0 m1 x &&&
+        initialConfiguration pp m0 &&&
+        nonNegativityConstraints m0 &&&
+        nonNegativityConstraints m1 &&&
+        nonNegativityConstraints x &&&
+        terminalConstraints pp m1 &&&
+        differentConsensusConstraints pp m1 &&&
+        checkUTrapConstraints pp m0 m1 x utraps &&&
+        checkUSiphonConstraints pp m0 m1 x usiphons
+
+checkReachableTermConfigInConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer ReachableTermConfigInConsensusCounterExample
+checkReachableTermConfigInConsensusSat pp refinements =
+        let m0 = makeVarMapWith ("m0'"++) $ states pp
+            m1 = makeVarMapWith ("m1'"++) $ states pp
+            x = makeVarMapWith ("x'"++) $ transitions pp
+        in  ("strong consensus", "(c0, c1, x)",
+             concatMap getNames [m0, m1] ++ concatMap getNames [x],
+             \fm -> checkReachableTermConfigInConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm x) refinements,
+             \fm -> counterExampleFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm x))
+
+counterExampleFromAssignment :: IMap State -> IMap State -> IMap Transition -> ReachableTermConfigInConsensusCounterExample
+counterExampleFromAssignment m0 m1 x =
+        (makeVector m0, makeVector m1, makeVector x)
+
+-- trap and siphon refinement constraints
+
+trapConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
+trapConstraint pp b t =
+        sum (mval b $ pre pp t) .> 0 ==> sum (mval b $ post pp t) .> 0
+
+siphonConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
+siphonConstraint pp b t =
+        sum (mval b $ post pp t) .> 0 ==> sum (mval b $ pre pp t) .> 0
+
+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
+
+uSiphonConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
+uSiphonConstraints pp x b =
+        bAnd $ map (siphonConstraint pp b) $ elems x
+
+statesMarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
+statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
+
+statesUnmarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
+statesUnmarkedByConfiguration pp m b = sum (mval b $ elems m) .== 0
+
+statesPostsetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
+statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
+
+statesPresetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
+statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
+
+noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
+noOutputTransitionEnabled pp m b =
+            bAnd $ map outputTransitionNotEnabled $ transitions pp
+        where
+            outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
+            outputTransitionOfB t = sum [val b q | (q, w) <- lpre pp t, val m q >= w] .> 0
+            transitionNotEnabledInB t = sum [val b q | (q, w) <- lpre pp t, val m q < w] .> 0
+
+nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
+nonemptySet b = sum (vals b) .> 0
+
+checkBinary :: SIMap State -> SBool
+checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
+
+checkSizeLimit :: SIMap State -> Maybe (Int, Integer) -> SBool
+checkSizeLimit _ Nothing = true
+checkSizeLimit b (Just (1, curSize)) = (.< literal curSize) $ sumVal b
+checkSizeLimit b (Just (2, curSize)) = (.> literal curSize) $ sumVal b
+checkSizeLimit _ (Just (_, _)) = error "minimization method not supported"
+
+minimizeMethod :: Int -> Integer -> String
+minimizeMethod 1 curSize = "size smaller than " ++ show curSize
+minimizeMethod 2 curSize = "size larger than " ++ show curSize
+minimizeMethod _ _ = error "minimization method not supported"
+
+findTrapConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
+findTrapConstraints pp (m0, m1, x) b sizeLimit =
+        checkSizeLimit b sizeLimit &&&
+        checkBinary b &&&
+        trapConstraints pp b &&&
+        statesPostsetOfSequence pp x b &&&
+        statesUnmarkedByConfiguration pp m1 b
+
+findTrapConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
+findTrapConstraintsSat pp c =
+        let b = makeVarMap $ states pp
+        in  (minimizeMethod, \sizeLimit ->
+            ("trap marked by x and not marked in m1", "trap",
+             getNames b,
+             \fm -> findTrapConstraints pp c (fmap fm b) sizeLimit,
+             \fm -> statesFromAssignment (fmap fm b)))
+
+findUTrapConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
+findUTrapConstraints pp (m0, m1, x) b sizeLimit =
+        checkSizeLimit b sizeLimit &&&
+        checkBinary b &&&
+        statesPostsetOfSequence pp x b &&&
+        uTrapConstraints pp x b &&&
+        statesUnmarkedByConfiguration pp m1 b
+
+findUTrapConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
+findUTrapConstraintsSat pp c =
+        let b = makeVarMap $ states pp
+        in  (minimizeMethod, \sizeLimit ->
+            ("u-trap (w.r.t. x) marked by x and not marked in m", "u-trap",
+             getNames b,
+             \fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit,
+             \fm -> statesFromAssignment (fmap fm b)))
+
+findSiphonConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
+findSiphonConstraints pp (m0, m1, x) b sizeLimit =
+        checkSizeLimit b sizeLimit &&&
+        checkBinary b &&&
+        siphonConstraints pp b &&&
+        statesUnmarkedByConfiguration pp m0 b &&&
+        statesPresetOfSequence pp x b
+
+findSiphonConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
+findSiphonConstraintsSat pp c =
+        let b = makeVarMap $ states pp
+        in  (minimizeMethod, \sizeLimit ->
+            ("siphon used by x and unmarked in m0", "siphon",
+             getNames b,
+             \fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit,
+             \fm -> statesFromAssignment (fmap fm b)))
+
+
+findUSiphonConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
+findUSiphonConstraints pp (m0, m1, x) b sizeLimit =
+        checkSizeLimit b sizeLimit &&&
+        checkBinary b &&&
+        statesUnmarkedByConfiguration pp m0 b &&&
+        statesPresetOfSequence pp x b &&&
+        uSiphonConstraints pp x b
+
+findUSiphonConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
+findUSiphonConstraintsSat pp c =
+        let b = makeVarMap $ states pp
+        in  (minimizeMethod, \sizeLimit ->
+            ("u-siphon (w.r.t. x) used by x and unmarked in m0", "u-siphon",
+             getNames b,
+             \fm -> findUSiphonConstraints pp c (fmap fm b) sizeLimit,
+             \fm -> statesFromAssignment (fmap fm b)))
+
+statesFromAssignment :: IMap State -> ([State], Integer)
+statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))

src/Solver/StrongConsensus.hs

@@ -287,7 +287,7 @@ findUSiphonConstraintsSat pp c =
 statesFromAssignment :: IMap State -> ([State], Integer)
 statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
 
--- method with all refinements directly encoded into the SMT theoryüjw
+-- method with all refinements directly encoded into the SMT theory
 
 findMaximalUnmarkedTrap :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SIMap State -> SBool
 findMaximalUnmarkedTrap pp max x m rs =