{-# LANGUAGE FlexibleContexts #-} module Solver.StrongConsensus (checkStrongConsensusSat, StrongConsensusCounterExample, findTrapConstraintsSat, findUTrapConstraintsSat, findUSiphonConstraintsSat, checkGeneralizedCoTrapSat, StableInequality) where import Data.SBV import qualified Data.Map as M import Data.List ((\\)) import Util import PopulationProtocol import Property import Solver type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector) type StableInequality = (IMap State, Integer) 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 (states pp \\ initialStates pp)) .== 0 differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SBool differentConsensusConstraints pp m1 m2 = (sum (mval m1 (trueStates pp)) .> 0 &&& sum (mval m2 (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 State -> SIMap Transition -> SIMap Transition -> Trap -> SBool checkUTrap pp m0 m1 m2 x1 x2 utrap = (((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByConfiguration utrap m1)) &&& (((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByConfiguration utrap m2)) where upost = mpost pp utrap upre = mpre pp utrap uunmark = upost \\ upre checkUTrapConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool checkUTrapConstraints pp m0 m1 m2 x1 x2 traps = bAnd $ map (checkUTrap pp m0 m1 m2 x1 x2) traps checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Siphon -> SBool checkUSiphon pp m0 m1 m2 x1 x2 usiphon = (((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByConfiguration usiphon m0)) &&& (((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByConfiguration usiphon m0)) where upost = mpost pp usiphon upre = mpre pp usiphon umark = upre \\ upost checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons = bAnd $ map (checkUSiphon pp m0 m1 m2 x1 x2) siphons checkInequalityConstraint :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> StableInequality -> SBool checkInequalityConstraint pp m0 m1 m2 (k, c) = (checkInequality m0) ==> (checkInequality m1 &&& checkInequality m2) where checkInequality m = sum [ literal (val k q) * (val m q) | q <- states pp ] .>= literal c checkInequalityConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> [StableInequality] -> SBool checkInequalityConstraints pp m0 m1 m2 inequalities = bAnd [ checkInequalityConstraint pp m0 m1 m2 i | i <- inequalities ] checkStrongConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Trap] -> [Siphon] -> [StableInequality] -> SBool checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalities = stateEquationConstraints pp m0 m1 x1 &&& stateEquationConstraints pp m0 m2 x2 &&& initialConfiguration pp m0 &&& nonNegativityConstraints m0 &&& nonNegativityConstraints m1 &&& nonNegativityConstraints m2 &&& nonNegativityConstraints x1 &&& nonNegativityConstraints x2 &&& terminalConstraints pp m1 &&& terminalConstraints pp m2 &&& differentConsensusConstraints pp m1 m2 &&& checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&& checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons &&& checkInequalityConstraints pp m0 m1 m2 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 x1 = makeVarMap $ transitions pp 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 inequalities, \fm -> configurationsFromAssignment (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 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2) -- 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 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" findTrap :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> Maybe (Int, Integer) -> SBool findTrap pp m0 m1 m2 x1 x2 b sizeLimit = checkSizeLimit b sizeLimit &&& checkBinary b &&& trapConstraints pp b &&& ( (statesPostsetOfSequence pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) ||| (statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b) ) findTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> MinConstraintProblem Integer Trap Integer findTrapConstraintsSat pp m0 m1 m2 x1 x2 = let b = makeVarMap $ states pp in (minimizeMethod, \sizeLimit -> ("trap marked by x1 or x2 and not marked in m1 or m2", "trap", getNames b, \fm -> findTrap pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit, \fm -> statesFromAssignment (fmap fm b))) findUTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> Maybe (Int, Integer) -> SBool findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit = checkSizeLimit b sizeLimit &&& checkBinary b &&& ( (statesPostsetOfSequence pp x1 b &&& uTrapConstraints pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) ||| (statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByConfiguration pp m2 b) ) findUTrapConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> MinConstraintProblem Integer Trap Integer findUTrapConstraintsSat pp m0 m1 m2 x1 x2 = let b = makeVarMap $ states pp in (minimizeMethod, \sizeLimit -> ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap", getNames b, \fm -> findUTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit, \fm -> statesFromAssignment (fmap fm b))) findUSiphonConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> Maybe (Int, Integer) -> SBool findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit = checkSizeLimit b sizeLimit &&& checkBinary b &&& statesUnmarkedByConfiguration pp m0 b &&& ( (statesPresetOfSequence pp x1 b &&& uSiphonConstraints pp x1 b) ||| (statesPresetOfSequence pp x2 b &&& uSiphonConstraints pp x2 b) ) findUSiphonConstraintsSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> MinConstraintProblem Integer Siphon Integer findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 = let b = makeVarMap $ states pp in (minimizeMethod, \sizeLimit -> ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon", getNames b, \fm -> findUSiphonConstraints pp m0 m1 m2 x1 x2 (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)) -- stable linear inequalities checkStableInequalityForConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SInteger -> SBool checkStableInequalityForConfiguration pp m k c = sum [ (val k q) * literal (val m q) | q <- states pp ] .>= c checkSemiPositiveConstraints :: (Ord a, Show a) => SIMap a -> SBool checkSemiPositiveConstraints k = bAnd [ x .>= 0 | x <- vals k ] checkSemiNegativeConstraints :: (Ord a, Show a) => SIMap a -> SBool checkSemiNegativeConstraints k = bAnd [ x .<= 0 | x <- vals k ] checkGeneralizedTCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> Transition -> SBool checkGeneralizedTCoTrap pp k c t = checkTSurInvariant ||| checkTDisabled where checkTSurInvariant = sum output - sum input .>= c checkTDisabled = sum input .< c input = map addState $ lpre pp t output = map addState $ lpost pp t addState (q, w) = literal w * val k q checkGeneralizedCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> SBool checkGeneralizedCoTrap pp k c = bAnd [ checkGeneralizedTCoTrap pp k c t | t <- transitions pp ] checkGeneralizedCoTrapConstraints :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> SIMap State -> SInteger -> SBool checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 k c = checkSemiNegativeConstraints k &&& checkGeneralizedCoTrap pp k c &&& checkStableInequalityForConfiguration pp m0 k c &&& ((bnot (checkStableInequalityForConfiguration pp m1 k c)) ||| (bnot (checkStableInequalityForConfiguration pp m2 k c))) checkGeneralizedCoTrapSat :: PopulationProtocol -> Configuration -> Configuration -> Configuration -> FlowVector -> FlowVector -> ConstraintProblem Integer StableInequality checkGeneralizedCoTrapSat pp m0 m1 m2 x1 x2 = let k = makeVarMap $ states pp c = "'c" in ("generalized co-trap (stable inequality) holding m but not in m1 or m2", "stable inequality", c : getNames k, \fm -> checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm k) (fm c), \fm -> stableInequalityFromAssignment (fmap fm k) (fm c)) stableInequalityFromAssignment :: IMap State -> Integer -> StableInequality stableInequalityFromAssignment k c = (k, c)