examples/remainder_m3_c1.pp

@@ -112,7 +112,7 @@
         "_mod1",
         "_mod2"
     ],
-    "predicate": "( 0 * _mod0 + 1 * _mod1 + 2 * _mod2 ) % 3 = 1",
+    "predicate": "0 * _mod0 + 1 * _mod1 + 2 * _mod2 =%3 1",
     "trueStates": [
         "_mod1",
         "_modpassivetrue"

src/Parser/PP.hs

@@ -103,6 +103,7 @@ parseOp = (reservedOp "<" *> return Lt) <|>
           (reservedOp "=" *> return Eq) <|>
           (reservedOp "!=" *> return Ne) <|>
           (reservedOp ">" *> return Gt) <|>
+          (reservedOp ">=" *> return Ge) <|>
           (reservedOp "=%" *> (ModEq <$> integer)) <|>
           (reservedOp "!=%" *> (ModNe <$> integer))
 

src/Property.hs

@@ -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

@@ -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))