Add direct checking of strong consensus with a single SMT formula

src/Main.hs

@@ -97,20 +97,48 @@ checkStrongConsensus pp = do
             (Nothing, _) -> return Satisfied
             (Just _, _) -> return Unknown
 
+--checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
+--        OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
+--checkStrongConsensus' pp refinements = do
+--        optRefine <- opt optRefinementType
+--        let method = case optRefine of
+--                        RefAll -> checkStrongConsensusCompleteSat pp
+--                        _ -> checkStrongConsensusSat pp refinements
+--        r <- checkSat $ method
+--        case r of
+--            Nothing -> return (Nothing, refinements)
+--            Just c -> do
+--                case optRefine of
+--                        RefDefault ->
+--                            let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
+--                            in refineStrongConsensus pp refinementMethods refinements c
+--                        RefList refinementMethods ->
+--                            refineStrongConsensus pp refinementMethods refinements c
+--                        RefAll -> return (Nothing, refinements)
+
 checkStrongConsensus' :: PopulationProtocol -> RefinementObjects ->
         OptIO (Maybe StrongConsensusCounterExample, RefinementObjects)
 checkStrongConsensus' pp refinements = do
-        r <- checkSat $ checkStrongConsensusSat pp refinements
-        case r of
-            Nothing -> return (Nothing, refinements)
-            Just c -> do
-                optRefine <- opt optRefinementType
-                let refinementMethods = case optRefine of
-                        RefDefault -> [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
-                        RefList rs -> rs
-                        RefAll -> error "not yet implemented"
-                refineStrongConsensus pp refinementMethods refinements c
-
+        optRefine <- opt optRefinementType
+        case optRefine of
+            RefAll -> do
+                r <- checkSat $ checkStrongConsensusCompleteSat pp
+                case r of
+                    -- TODO unify counter example
+                    Nothing -> return (Nothing, refinements)
+                    Just (m0,m1,m2,x1,x2,_,_,_,_) -> return (Just (m0,m1,m2,x1,x2), refinements)
+            _ -> do
+                r <- checkSat $ checkStrongConsensusSat pp refinements
+                case r of
+                    Nothing -> return (Nothing, refinements)
+                    Just c -> do
+                        case optRefine of
+                                RefDefault ->
+                                    let refinementMethods = [TrapRefinement, SiphonRefinement, UTrapRefinement, USiphonRefinement]
+                                    in refineStrongConsensus pp refinementMethods refinements c
+                                RefList refinementMethods ->
+                                    refineStrongConsensus pp refinementMethods refinements c
+                                RefAll -> return (Nothing, refinements)
 
 refineStrongConsensus :: PopulationProtocol -> [RefinementType] -> RefinementObjects ->
         StrongConsensusCounterExample ->
@@ -165,8 +193,7 @@ main = do
                 when (optShowVersion opts) (exitSuccessWith "Version 0.01")
                 when (optShowHelp opts) (exitSuccessWith usageInformation)
                 when (null files) (exitErrorWith "No input file given")
-                let opts' = opts { optProperties = reverse (optProperties opts) }
-                rs <- runReaderT (mapM checkFile files) opts'
+                rs <- runReaderT (mapM checkFile files) opts
                 -- TODO: short-circuit with Control.Monad.Loops? parallel
                 -- execution?
                 let r = resultsAnd rs

src/PopulationProtocol.hs

@@ -5,6 +5,7 @@ module PopulationProtocol
     (PopulationProtocol,State(..),Transition(..),
      Configuration,FlowVector,RConfiguration,RFlowVector,
      renameState,renameTransition,renameStatesAndTransitions,
+     invertPopulationProtocol,
      name,showNetName,states,transitions,initialStates,trueStates,falseStates,
      pre,lpre,post,lpost,mpre,mpost,context,
      makePopulationProtocol,makePopulationProtocolWithTrans,
@@ -16,6 +17,7 @@ import qualified Data.Map as M
 import qualified Data.Set as S
 import Control.Arrow (first,(***))
 import Data.List (sort,(\\))
+import Data.Tuple (swap)
 
 import Util
 
@@ -125,6 +127,21 @@ renameStatesAndTransitions f pp =
               mapContext f (pre, post) =
                   (listMap (map (first f) pre), listMap (map (first f) post))
 
+invertPopulationProtocol :: PopulationProtocol -> PopulationProtocol
+invertPopulationProtocol pp =
+            PopulationProtocol {
+                name             = name pp,
+                states           = states pp,
+                transitions      = transitions pp,
+                initialStates    = initialStates pp,
+                trueStates       = trueStates pp,
+                falseStates      = falseStates pp,
+                adjacencyQ       = M.map swap $ adjacencyQ pp,
+                adjacencyT       = M.map swap $ adjacencyT pp
+            }
+
+
+
 makePopulationProtocol :: String -> [State] -> [Transition] ->
         [State] -> [State] -> [State] ->
         [Either (Transition, State, Integer) (State, Transition, Integer)] ->

src/Solver/StrongConsensus.hs

@@ -2,6 +2,7 @@
 
 module Solver.StrongConsensus
     (checkStrongConsensusSat,
+     checkStrongConsensusCompleteSat,
      StrongConsensusCounterExample,
      RefinementObjects,
      findTrapConstraintsSat,
@@ -12,7 +13,7 @@ where
 
 import Data.SBV
 import qualified Data.Map as M
-import Data.List ((\\))
+import Data.List ((\\),genericLength)
 
 import Util
 import PopulationProtocol
@@ -20,6 +21,7 @@ import Property
 import Solver
 
 type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
+type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration)
 type RefinementObjects = ([Trap], [Siphon])
 
 stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
@@ -105,11 +107,11 @@ checkStrongConsensus pp m0 m1 m2 x1 x2 (utraps, usiphons) =
 
 checkStrongConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
 checkStrongConsensusSat pp refinements =
-        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
+        let m0 = makeVarMapWith ("m0'"++) $ states pp
+            m1 = makeVarMapWith ("m1'"++) $ states pp
+            m2 = makeVarMapWith ("m2'"++) $ states pp
+            x1 = makeVarMapWith ("x1'"++) $ transitions pp
+            x2 = makeVarMapWith ("x2'"++) $ 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) refinements,
@@ -258,3 +260,81 @@ findUSiphonConstraintsSat pp c =
 
 statesFromAssignment :: IMap State -> ([State], Integer)
 statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
+
+-- method with all refinements directly encoded into the SMT theoryüjw
+
+findMaximalUnmarkedTrap :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SIMap State -> SBool
+findMaximalUnmarkedTrap pp max x m rs =
+        let stateConstraints q = unmarkedConstraints q &&& trapConstraints q
+            unmarkedConstraints q = (val m q .> 0) .== (val rs q .== 0)
+            trapConstraints q = (val rs q .< literal max) .== ((val rs q .== 0) ||| (successorConstraints q))
+            successorConstraints q = bOr [ transitionConstraints q t | t <- post pp q ]
+            transitionConstraints q t = (val x t .> 0) &&& bAnd [ val rs q' .< val rs q | q' <- post pp t ]
+        in  bAnd [ stateConstraints q | q <- states pp ]
+
+findMaximalUnmarkedSiphon :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SIMap State -> SBool
+findMaximalUnmarkedSiphon pp max x m s =
+        findMaximalUnmarkedTrap (invertPopulationProtocol pp) max x m s
+
+unmarkedBySequence :: PopulationProtocol -> Integer -> SIMap State -> SIMap Transition -> SBool
+unmarkedBySequence pp max trap x =
+            bAnd [ stateUnmarkedBySequence q | q <- states pp ]
+        where stateUnmarkedBySequence q = (val trap q .== literal max) ==> sum (mval x $ pre pp q) .== 0
+
+unusedBySequence :: PopulationProtocol -> Integer -> SIMap State -> SIMap Transition -> SBool
+unusedBySequence pp max siphon x =
+            bAnd [ stateUnusedBySequence q | q <- states pp ]
+        where stateUnusedBySequence q = (val siphon q .== literal max) ==> sum (mval x $ post pp q) .== 0
+
+checkBounds :: Integer -> SIMap State -> SBool
+checkBounds max = bAnd . map (\x -> x .>= 0 &&& x .<= literal max) . vals
+
+checkStrongConsensusComplete :: PopulationProtocol -> Integer -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
+        SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
+checkStrongConsensusComplete pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 =
+        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 &&&
+        checkBounds max r1 &&&
+        checkBounds max r2 &&&
+        checkBounds max s1 &&&
+        checkBounds max s2 &&&
+        findMaximalUnmarkedTrap pp max x1 m1 r1 &&&
+        findMaximalUnmarkedTrap pp max x2 m2 r2 &&&
+        findMaximalUnmarkedSiphon pp max x1 m0 s1 &&&
+        findMaximalUnmarkedSiphon pp max x2 m0 s2 &&&
+        unmarkedBySequence pp max r1 x1 &&&
+        unmarkedBySequence pp max r2 x2 &&&
+        unusedBySequence pp max s1 x1 &&&
+        unusedBySequence pp max s2 x2
+
+checkStrongConsensusCompleteSat :: PopulationProtocol -> ConstraintProblem Integer StrongConsensusCompleteCounterExample
+checkStrongConsensusCompleteSat pp =
+        let max = genericLength (states pp) + 1
+            m0 = makeVarMapWith ("m0'"++) $ states pp
+            m1 = makeVarMapWith ("m1'"++) $ states pp
+            m2 = makeVarMapWith ("m2'"++) $ states pp
+            x1 = makeVarMapWith ("x1'"++) $ transitions pp
+            x2 = makeVarMapWith ("x2'"++) $ transitions pp
+            r1 = makeVarMapWith ("r1'"++) $ states pp
+            r2 = makeVarMapWith ("r2'"++) $ states pp
+            s1 = makeVarMapWith ("s1'"++) $ states pp
+            s2 = makeVarMapWith ("s2'"++) $ states 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],
+             \fm -> checkStrongConsensusComplete pp 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))
+
+completeCounterExampleFromAssignment :: Integer -> IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition ->
+        IMap State -> IMap State -> IMap State -> IMap State -> StrongConsensusCompleteCounterExample
+completeCounterExampleFromAssignment max m0 m1 m2 x1 x2 r1 r2 s1 s2 =
+            (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2, makeVector r1, makeVector r2, makeVector s1, makeVector s2)
+        where maximalSet q = M.keys $ M.filter (== max) q