...
 
Commits (3)
...@@ -112,7 +112,7 @@ ...@@ -112,7 +112,7 @@
"_mod1", "_mod1",
"_mod2" "_mod2"
], ],
"predicate": "( 0 * _mod0 + 1 * _mod1 + 2 * _mod2 ) % 3 = 1", "predicate": "0 * _mod0 + 1 * _mod1 + 2 * _mod2 =%3 1",
"trueStates": [ "trueStates": [
"_mod1", "_mod1",
"_modpassivetrue" "_modpassivetrue"
......
...@@ -103,6 +103,7 @@ parseOp = (reservedOp "<" *> return Lt) <|> ...@@ -103,6 +103,7 @@ parseOp = (reservedOp "<" *> return Lt) <|>
(reservedOp "=" *> return Eq) <|> (reservedOp "=" *> return Eq) <|>
(reservedOp "!=" *> return Ne) <|> (reservedOp "!=" *> return Ne) <|>
(reservedOp ">" *> return Gt) <|> (reservedOp ">" *> return Gt) <|>
(reservedOp ">=" *> return Ge) <|>
(reservedOp "=%" *> (ModEq <$> integer)) <|> (reservedOp "=%" *> (ModEq <$> integer)) <|>
(reservedOp "!=%" *> (ModNe <$> integer)) (reservedOp "!=%" *> (ModNe <$> integer))
......
...@@ -6,6 +6,8 @@ module Property ...@@ -6,6 +6,8 @@ module Property
QuantFormula(..), QuantFormula(..),
quantifiedVariables, quantifiedVariables,
innerFormula, innerFormula,
negationNormalForm,
eliminateModulo,
Op(..), Op(..),
Term(..), Term(..),
PropResult(..), PropResult(..),
...@@ -89,8 +91,33 @@ negationNormalForm (Neg (FFalse)) = FTrue ...@@ -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 (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 (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 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 :: QuantFormula a -> [a]
quantifiedVariables (ExQuantFormula xs _) = xs quantifiedVariables (ExQuantFormula xs _) = xs
......
...@@ -21,6 +21,8 @@ import Property ...@@ -21,6 +21,8 @@ import Property
import Solver import Solver
import Solver.Formula import Solver.Formula
import Debug.Trace
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector) type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration) type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration)
type RefinementObjects = ([Trap], [Siphon]) type RefinementObjects = ([Trap], [Siphon])
...@@ -51,8 +53,9 @@ initialConfiguration pp m0 = ...@@ -51,8 +53,9 @@ initialConfiguration pp m0 =
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&& (sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&&
(evaluateFormula (precondition pp) m0) (evaluateFormula (precondition pp) m0)
differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool differentConsensusConstraints :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa = SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 qe qa =
(oT &&& oF) ||| (oT &&& oF) |||
(if checkCorrectness then correctnessConstraints else false) (if checkCorrectness then correctnessConstraints else false)
where where
...@@ -60,8 +63,9 @@ differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa = ...@@ -60,8 +63,9 @@ differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
oF = sum (mval m2 (falseStates pp)) .> 0 oF = sum (mval m2 (falseStates pp)) .> 0
correctnessConstraints = correctnessConstraints =
if null (quantifiedVariables (predicate pp)) then if null (quantifiedVariables (predicate pp)) then
let oP = evaluateFormula (innerFormula (predicate pp)) m0 let oPT = evaluateFormula pT (M.union m0 qe)
in (oP &&& oF) ||| (bnot oP &&& oT) oPF = evaluateFormula pF (M.union m0 qe)
in (oPT &&& oF) ||| (oPF &&& oT)
else else
let oPT = evaluateFormula (innerFormula (predicate pp)) (M.union m0 qe) let oPT = evaluateFormula (innerFormula (predicate pp)) (M.union m0 qe)
oPF = evaluateFormula (Neg (innerFormula (predicate pp))) (M.union m0 qa) oPF = evaluateFormula (Neg (innerFormula (predicate pp))) (M.union m0 qa)
...@@ -103,9 +107,10 @@ checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> S ...@@ -103,9 +107,10 @@ checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> S
checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons = checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons =
bAnd $ map (checkUSiphon 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 -> checkStrongConsensus :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
SIMap State -> SIMap State ->RefinementObjects -> SBool SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons) = 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 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&& stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&& initialConfiguration pp m0 &&&
...@@ -116,10 +121,19 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons) ...@@ -116,10 +121,19 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons)
nonNegativityConstraints x2 &&& nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&& terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&& 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 &&& checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons 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 :: Bool -> PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat checkCorrectness pp refinements = checkStrongConsensusSat checkCorrectness pp refinements =
let m0 = makeVarMapWith ("m0'"++) $ states pp let m0 = makeVarMapWith ("m0'"++) $ states pp
...@@ -127,11 +141,12 @@ checkStrongConsensusSat checkCorrectness pp refinements = ...@@ -127,11 +141,12 @@ checkStrongConsensusSat checkCorrectness pp refinements =
m2 = makeVarMapWith ("m2'"++) $ states pp m2 = makeVarMapWith ("m2'"++) $ states pp
x1 = makeVarMapWith ("x1'"++) $ transitions pp x1 = makeVarMapWith ("x1'"++) $ transitions pp
x2 = makeVarMapWith ("x2'"++) $ 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) qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
in ("strong consensus", "(c0, c1, c2, x1, x2)", in ("strong consensus", "(c0, c1, c2, x1, x2)",
getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2, getNames qe, getNames qa, 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)) \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 counterExampleFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
...@@ -306,9 +321,10 @@ unusedBySequence pp max siphon x = ...@@ -306,9 +321,10 @@ unusedBySequence pp max siphon x =
checkBounds :: Integer -> SIMap State -> SBool checkBounds :: Integer -> SIMap State -> SBool
checkBounds max = bAnd . map (\x -> x .>= 0 &&& x .<= literal max) . vals 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 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 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&& stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&& initialConfiguration pp m0 &&&
...@@ -319,7 +335,7 @@ checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 ...@@ -319,7 +335,7 @@ checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2
nonNegativityConstraints x2 &&& nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&& terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&& 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 r1 &&&
checkBounds max r2 &&& checkBounds max r2 &&&
checkBounds max s1 &&& checkBounds max s1 &&&
...@@ -345,11 +361,12 @@ checkStrongConsensusCompleteSat checkCorrectness pp = ...@@ -345,11 +361,12 @@ checkStrongConsensusCompleteSat checkCorrectness pp =
r2 = makeVarMapWith ("r2'"++) $ states pp r2 = makeVarMapWith ("r2'"++) $ states pp
s1 = makeVarMapWith ("s1'"++) $ states pp s1 = makeVarMapWith ("s1'"++) $ states pp
s2 = makeVarMapWith ("s2'"++) $ 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) qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
in ("strong consensus", "(m0, m1, m2, x1, x2, r1, r2, s1, s2)", 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, 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), (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)) \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))
......