Skip to content

GitLab

Commit 9676c8c2 authored by Philipp Meyer's avatar Philipp Meyer
Browse files
Options

Remove stable inequality; simplify refinement argument passing

parent 430f9c2e
Hide whitespace changes
Inline Side-by-side
Showing with 43 additions and 106 deletions
src/Main.hs
View file @ 9676c8c2
......@@ -92,44 +92,42 @@ 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
checkStrongConsensus' :: PopulationProtocol ->
[Trap] -> [Siphon] -> [StableInequality] ->
OptIO (Maybe StrongConsensusCounterExample, [Trap], [Siphon], [StableInequality])
checkStrongConsensus' pp utraps usiphons inequalities = do
r <- checkSat $ checkStrongConsensusSat pp utraps usiphons inequalities
(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
case r of
Nothing -> return (Nothing, utraps, usiphons, inequalities)
Nothing -> return (Nothing, utraps, usiphons)
Just c -> do
refine <- opt optRefinementType
if isJust refine then
refineStrongConsensus pp utraps usiphons inequalities c
refineStrongConsensus pp utraps usiphons c
else
return (Just c, utraps, usiphons, inequalities)
return (Just c, utraps, usiphons)
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
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 m0 m1 m2 x1 x2
r2 <- checkSatMin $ Solver.StrongConsensus.findUSiphonConstraintsSat pp c
case r2 of
Nothing -> do
r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp m0 m1 m2 x1 x2
r3 <- checkSatMin $ Solver.StrongConsensus.findUTrapConstraintsSat pp c
case r3 of
Nothing -> return (Just c, utraps, usiphons, inequalities)
Nothing -> return (Just c, utraps, usiphons)
Just utrap ->
checkStrongConsensus' pp (utrap:utraps) usiphons inequalities
checkStrongConsensus' pp (utrap:utraps) usiphons
Just usiphon ->
checkStrongConsensus' pp utraps (usiphon:usiphons) inequalities
checkStrongConsensus' pp utraps (usiphon:usiphons)
Just trap ->
checkStrongConsensus' pp (trap:utraps) usiphons inequalities
checkStrongConsensus' pp (trap:utraps) usiphons
checkLayeredTermination :: PopulationProtocol -> OptIO PropResult
checkLayeredTermination pp = do
......
src/Solver/StrongConsensus.hs
View file @ 9676c8c2
......@@ -5,9 +5,7 @@ module Solver.StrongConsensus
StrongConsensusCounterExample,
findTrapConstraintsSat,
findUTrapConstraintsSat,
findUSiphonConstraintsSat,
checkGeneralizedCoTrapSat,
StableInequality)
findUSiphonConstraintsSat)
where
import Data.SBV
......@@ -21,8 +19,6 @@ 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
......@@ -87,18 +83,9 @@ checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> S
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 =
[Trap] -> [Siphon] -> SBool
checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -111,11 +98,10 @@ checkStrongConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalities =
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
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
checkStrongConsensusSat :: PopulationProtocol -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat pp utraps usiphons inequalities =
checkStrongConsensusSat :: PopulationProtocol -> [Trap] -> [Siphon] -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat pp utraps usiphons =
let m0 = makeVarMap $ states pp
m1 = makeVarMapWith prime $ states pp
m2 = makeVarMapWith (prime . prime) $ states pp
......@@ -123,7 +109,7 @@ checkStrongConsensusSat pp utraps usiphons inequalities =
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 -> 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))
configurationsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
......@@ -189,8 +175,8 @@ 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 =
findTrapConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrapConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
trapConstraints pp b &&&
......@@ -199,17 +185,17 @@ findTrap pp m0 m1 m2 x1 x2 b sizeLimit =
(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 =
findTrapConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat pp c =
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 -> findTrapConstraints pp c (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 =
findUTrapConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
(
......@@ -217,17 +203,17 @@ findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
(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 =
findUTrapConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat pp c =
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 -> findUTrapConstraints pp c (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 =
findUSiphonConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
statesUnmarkedByConfiguration pp m0 b &&&
......@@ -236,61 +222,14 @@ findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
(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 =
findUSiphonConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat pp c =
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 -> 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))
-- 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)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment