Skip to content

GitLab

Commit d3fec96f authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Correctly use modulo predicates for checking correctness

parent d8aebc73
Hide whitespace changes
Inline Side-by-side
src/Property.hs
View file @ d3fec96f
......@@ -6,6 +6,8 @@ module Property
QuantFormula(..),
quantifiedVariables,
innerFormula,
negationNormalForm,
eliminateModulo,
Op(..),
Term(..),
PropResult(..),
......@@ -89,8 +91,33 @@ negationNormalForm (Neg (FFalse)) = FTrue
negationNormalForm (Neg (g :&: h)) = (negationNormalForm (Neg g)) :|: (negationNormalForm (Neg h))
negationNormalForm (Neg (g :|: h)) = (negationNormalForm (Neg g)) :&: (negationNormalForm (Neg h))
negationNormalForm (Neg (LinearInequation u op t)) = LinearInequation u (negateOp op) t
negationNormalForm (g :&: h) = (negationNormalForm g) :&: (negationNormalForm h)
negationNormalForm (g :|: h) = (negationNormalForm g) :|: (negationNormalForm h)
negationNormalForm f = f
eliminateModulo :: (Int -> a) -> Formula a -> (Formula a, [a])
eliminateModulo = eliminateModulo' 0
eliminateModulo' :: Int -> (Int -> a) -> Formula a -> (Formula a, [a])
eliminateModulo' _ _ (Neg g) = error "Formula not in negation normal form: cannot eliminate modulo"
eliminateModulo' n makeVar (LinearInequation lhs (ModEq m) rhs) =
let k = makeVar n
in (LinearInequation lhs Eq (rhs :+: ((Const m) :*: (Var k))), [k])
eliminateModulo' n makeVar (LinearInequation lhs (ModNe m) rhs) =
let j = makeVar (n + 1)
k = makeVar n
in ((LinearInequation lhs Eq (rhs :+: ((Var j) :+: ((Const m) :*: (Var k))))) :&:
(LinearInequation (Const 0) Lt (Var j)) :&: (LinearInequation (Var j) Lt (Const m)), [k, j])
eliminateModulo' n makeVar (g :|: h) =
let (g', ag) = eliminateModulo' n makeVar g
(h', ah) = eliminateModulo' (n + length ag) makeVar h
in (g' :|: h', ag ++ ah)
eliminateModulo' n makeVar (g :&: h) =
let (g', ag) = eliminateModulo' n makeVar g
(h', ah) = eliminateModulo' (n + length ag) makeVar h
in (g' :&: h', ag ++ ah)
eliminateModulo' _ _ f = (f, [])
quantifiedVariables :: QuantFormula a -> [a]
quantifiedVariables (ExQuantFormula xs _) = xs
......
src/Solver/StrongConsensus.hs
View file @ d3fec96f
......@@ -21,6 +21,8 @@ import Property
import Solver
import Solver.Formula
import Debug.Trace
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration)
type RefinementObjects = ([Trap], [Siphon])
......@@ -51,8 +53,9 @@ initialConfiguration pp m0 =
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&&
(evaluateFormula (precondition pp) m0)
differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
differentConsensusConstraints :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 qe qa =
(oT &&& oF) |||
(if checkCorrectness then correctnessConstraints else false)
where
......@@ -60,8 +63,9 @@ differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
oF = sum (mval m2 (falseStates pp)) .> 0
correctnessConstraints =
if null (quantifiedVariables (predicate pp)) then
let oP = evaluateFormula (innerFormula (predicate pp)) m0
in (oP &&& oF) ||| (bnot oP &&& oT)
let oPT = evaluateFormula pT (M.union m0 qe)
oPF = evaluateFormula pF (M.union m0 qe)
in (oPT &&& oF) ||| (oPF &&& oT)
else
let oPT = evaluateFormula (innerFormula (predicate pp)) (M.union m0 qe)
oPF = evaluateFormula (Neg (innerFormula (predicate pp))) (M.union m0 qa)
......@@ -103,9 +107,10 @@ 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
checkStrongConsensus :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
SIMap State -> SIMap State ->RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons) =
checkStrongConsensus :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
SIMap State -> SIMap State -> RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp pT pF m0 m1 m2 x1 x2 qe qa (utraps, usiphons) =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -116,10 +121,19 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons)
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 qe qa &&&
checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
makePredicates :: PopulationProtocol -> (Formula State, Formula State, [State])
makePredicates pp =
let elim s f = eliminateModulo (State . (s++) . show) f
fT = negationNormalForm $ innerFormula $ predicate pp
fF = negationNormalForm (Neg fT)
(pT, varsT) = elim "mpt'" fT
(pF, varsF) = elim "mpf'" fF
in (pT, pF, varsT ++ varsF)
checkStrongConsensusSat :: Bool -> PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat checkCorrectness pp refinements =
let m0 = makeVarMapWith ("m0'"++) $ states pp
......@@ -127,11 +141,12 @@ checkStrongConsensusSat checkCorrectness pp refinements =
m2 = makeVarMapWith ("m2'"++) $ states pp
x1 = makeVarMapWith ("x1'"++) $ transitions pp
x2 = makeVarMapWith ("x2'"++) $ transitions pp
qe = makeVarMapWith ("e'"++) $ quantifiedVariables (predicate pp)
(pT, pF, modVars) = makePredicates pp
qe = makeVarMapWith ("e'"++) $ modVars
qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
in ("strong consensus", "(c0, c1, c2, x1, x2)",
getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2, getNames qe, getNames qa,
\fm -> checkStrongConsensus checkCorrectness pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) (fmap fm qe) (fmap fm qa) refinements,
\fm -> checkStrongConsensus checkCorrectness pp pT pF (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) (fmap fm qe) (fmap fm qa) refinements,
\fm -> counterExampleFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
counterExampleFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
......@@ -306,9 +321,10 @@ unusedBySequence pp max siphon x =
checkBounds :: Integer -> SIMap State -> SBool
checkBounds max = bAnd . map (\x -> x .>= 0 &&& x .<= literal max) . vals
checkStrongConsensusComplete :: Bool -> PopulationProtocol -> Integer -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
checkStrongConsensusComplete :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
Integer -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 qe qa =
checkStrongConsensusComplete checkCorrectness pp pT pF max m0 m1 m2 x1 x2 r1 r2 s1 s2 qe qa =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -319,7 +335,7 @@ checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 qe qa &&&
checkBounds max r1 &&&
checkBounds max r2 &&&
checkBounds max s1 &&&
......@@ -345,11 +361,12 @@ checkStrongConsensusCompleteSat checkCorrectness pp =
r2 = makeVarMapWith ("r2'"++) $ states pp
s1 = makeVarMapWith ("s1'"++) $ states pp
s2 = makeVarMapWith ("s2'"++) $ states pp
qe = makeVarMapWith ("e'"++) $ quantifiedVariables (predicate pp)
(pT, pF, modVars) = makePredicates pp
qe = makeVarMapWith ("e'"++) $ modVars
qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
in ("strong consensus", "(m0, m1, m2, x1, x2, r1, r2, s1, s2)",
concatMap getNames [m0, m1, m2, r1, r2, s1, s2] ++ concatMap getNames [x1, x2], getNames qe, getNames qa,
\fm -> checkStrongConsensusComplete checkCorrectness pp max (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2)
\fm -> checkStrongConsensusComplete checkCorrectness pp pT pF max (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2)
(fmap fm r1) (fmap fm r2) (fmap fm s1) (fmap fm s2) (fmap fm qe) (fmap fm qa),
\fm -> completeCounterExampleFromAssignment max (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) (fmap fm r1) (fmap fm r2) (fmap fm s1) (fmap fm s2))
......
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