Commit b0578845 authored by Philipp Meyer's avatar Philipp Meyer

Add support for quantified predicates

parent ad99d8de
population protocol "Flock of birds protocol with c = 10" {
states { _0 _1 _2 _3 _4 _5 _6 _7 _8 _9 _10}
transitions { x__0__10 x__1__1 x__1__2 x__1__3 x__1__4 x__1__5 x__1__6 x__1__7 x__1__8 x__1__9 x__1__10 x__2__2 x__2__3 x__2__4 x__2__5 x__2__6 x__2__7 x__2__8 x__2__9 x__2__10 x__3__3 x__3__4 x__3__5 x__3__6 x__3__7 x__3__8 x__3__9 x__3__10 x__4__4 x__4__5 x__4__6 x__4__7 x__4__8 x__4__9 x__4__10 x__5__5 x__5__6 x__5__7 x__5__8 x__5__9 x__5__10 x__6__6 x__6__7 x__6__8 x__6__9 x__6__10 x__7__7 x__7__8 x__7__9 x__7__10 x__8__8 x__8__9 x__8__10 x__9__9 x__9__10 }
arcs {
{ _0, _10 } -> x__0__10 -> { _10, _10 }
{ _1, _1 } -> x__1__1 -> { _2, _0 }
{ _1, _2 } -> x__1__2 -> { _3, _0 }
{ _1, _3 } -> x__1__3 -> { _4, _0 }
{ _1, _4 } -> x__1__4 -> { _5, _0 }
{ _1, _5 } -> x__1__5 -> { _6, _0 }
{ _1, _6 } -> x__1__6 -> { _7, _0 }
{ _1, _7 } -> x__1__7 -> { _8, _0 }
{ _1, _8 } -> x__1__8 -> { _9, _0 }
{ _1, _9 } -> x__1__9 -> { _10, _10 }
{ _1, _10 } -> x__1__10 -> { _10, _10 }
{ _2, _2 } -> x__2__2 -> { _4, _0 }
{ _2, _3 } -> x__2__3 -> { _5, _0 }
{ _2, _4 } -> x__2__4 -> { _6, _0 }
{ _2, _5 } -> x__2__5 -> { _7, _0 }
{ _2, _6 } -> x__2__6 -> { _8, _0 }
{ _2, _7 } -> x__2__7 -> { _9, _0 }
{ _2, _8 } -> x__2__8 -> { _10, _10 }
{ _2, _9 } -> x__2__9 -> { _10, _10 }
{ _2, _10 } -> x__2__10 -> { _10, _10 }
{ _3, _3 } -> x__3__3 -> { _6, _0 }
{ _3, _4 } -> x__3__4 -> { _7, _0 }
{ _3, _5 } -> x__3__5 -> { _8, _0 }
{ _3, _6 } -> x__3__6 -> { _9, _0 }
{ _3, _7 } -> x__3__7 -> { _10, _10 }
{ _3, _8 } -> x__3__8 -> { _10, _10 }
{ _3, _9 } -> x__3__9 -> { _10, _10 }
{ _3, _10 } -> x__3__10 -> { _10, _10 }
{ _4, _4 } -> x__4__4 -> { _8, _0 }
{ _4, _5 } -> x__4__5 -> { _9, _0 }
{ _4, _6 } -> x__4__6 -> { _10, _10 }
{ _4, _7 } -> x__4__7 -> { _10, _10 }
{ _4, _8 } -> x__4__8 -> { _10, _10 }
{ _4, _9 } -> x__4__9 -> { _10, _10 }
{ _4, _10 } -> x__4__10 -> { _10, _10 }
{ _5, _5 } -> x__5__5 -> { _10, _10 }
{ _5, _6 } -> x__5__6 -> { _10, _10 }
{ _5, _7 } -> x__5__7 -> { _10, _10 }
{ _5, _8 } -> x__5__8 -> { _10, _10 }
{ _5, _9 } -> x__5__9 -> { _10, _10 }
{ _5, _10 } -> x__5__10 -> { _10, _10 }
{ _6, _6 } -> x__6__6 -> { _10, _10 }
{ _6, _7 } -> x__6__7 -> { _10, _10 }
{ _6, _8 } -> x__6__8 -> { _10, _10 }
{ _6, _9 } -> x__6__9 -> { _10, _10 }
{ _6, _10 } -> x__6__10 -> { _10, _10 }
{ _7, _7 } -> x__7__7 -> { _10, _10 }
{ _7, _8 } -> x__7__8 -> { _10, _10 }
{ _7, _9 } -> x__7__9 -> { _10, _10 }
{ _7, _10 } -> x__7__10 -> { _10, _10 }
{ _8, _8 } -> x__8__8 -> { _10, _10 }
{ _8, _9 } -> x__8__9 -> { _10, _10 }
{ _8, _10 } -> x__8__10 -> { _10, _10 }
{ _9, _9 } -> x__9__9 -> { _10, _10 }
{ _9, _10 } -> x__9__10 -> { _10, _10 }
}
initial {_0 _1}
true {_10}
false {_0 _1 _2 _3 _4 _5 _6 _7 _8 _9}
predicate { _1 >= 10 }
}
population protocol "New birds protocol with c = 10" {
states { _0 _1 _2 _3 _4 _5 _6 _7 _8 _9 _10}
transitions { x__0__10 x__1__1 x__1__10 x__2__2 x__2__10 x__3__3 x__3__10 x__4__4 x__4__10 x__5__5 x__5__10 x__6__6 x__6__10 x__7__7 x__7__10 x__8__8 x__8__10 x__9__9 x__9__10 }
arcs {
{ _0, _10 } -> x__0__10 -> { _10, _10 }
{ _1, _1 } -> x__1__1 -> { _1, _2 }
{ _1, _10 } -> x__1__10 -> { _10, _10 }
{ _2, _2 } -> x__2__2 -> { _2, _3 }
{ _2, _10 } -> x__2__10 -> { _10, _10 }
{ _3, _3 } -> x__3__3 -> { _3, _4 }
{ _3, _10 } -> x__3__10 -> { _10, _10 }
{ _4, _4 } -> x__4__4 -> { _4, _5 }
{ _4, _10 } -> x__4__10 -> { _10, _10 }
{ _5, _5 } -> x__5__5 -> { _5, _6 }
{ _5, _10 } -> x__5__10 -> { _10, _10 }
{ _6, _6 } -> x__6__6 -> { _6, _7 }
{ _6, _10 } -> x__6__10 -> { _10, _10 }
{ _7, _7 } -> x__7__7 -> { _7, _8 }
{ _7, _10 } -> x__7__10 -> { _10, _10 }
{ _8, _8 } -> x__8__8 -> { _8, _9 }
{ _8, _10 } -> x__8__10 -> { _10, _10 }
{ _9, _9 } -> x__9__9 -> { _9, _10 }
{ _9, _10 } -> x__9__10 -> { _10, _10 }
}
initial {_0 _1}
true {_10}
false {_0 _1 _2 _3 _4 _5 _6 _7 _8 _9}
predicate { _1 >= 10 }
}
population protocol "Modulo Protocol with m = 3 and c = 1" {
states { _mod0 _mod1 _mod2 _modpassivetrue _modpassivefalse}
transitions { x__mod0__mod0 x__mod0__mod1 x__mod0__mod2 x__mod0__modpassivetrue x__mod1__mod1 x__mod1__mod2 x__mod1__modpassivefalse x__mod2__mod2 x__mod2__modpassivetrue }
arcs {
{ _mod0, _mod0 } -> x__mod0__mod0 -> { _mod0, _modpassivefalse }
{ _mod0, _mod1 } -> x__mod0__mod1 -> { _mod1, _modpassivetrue }
{ _mod0, _mod2 } -> x__mod0__mod2 -> { _mod2, _modpassivefalse }
{ _mod0, _modpassivetrue } -> x__mod0__modpassivetrue -> { _mod0, _modpassivefalse }
{ _mod1, _mod1 } -> x__mod1__mod1 -> { _mod2, _modpassivefalse }
{ _mod1, _mod2 } -> x__mod1__mod2 -> { _mod0, _modpassivefalse }
{ _mod1, _modpassivefalse } -> x__mod1__modpassivefalse -> { _mod1, _modpassivetrue }
{ _mod2, _mod2 } -> x__mod2__mod2 -> { _mod1, _modpassivetrue }
{ _mod2, _modpassivetrue } -> x__mod2__modpassivetrue -> { _mod2, _modpassivefalse }
}
initial {_mod0 _mod1 _mod2}
true {_mod1 _modpassivetrue}
false {_mod0 _mod2 _modpassivefalse}
predicate {
EXISTS k : (_mod1 + 2 * _mod2 = 1 + 3*k)
}
}
...@@ -21,9 +21,9 @@ languageDef = ...@@ -21,9 +21,9 @@ languageDef =
Token.commentLine = "//", Token.commentLine = "//",
Token.identStart = letter <|> char '_', Token.identStart = letter <|> char '_',
Token.identLetter = alphaNum <|> char '_', Token.identLetter = alphaNum <|> char '_',
Token.reservedNames = ["true", "false"], Token.reservedNames = ["true", "false", "EXISTS", "FORALL"],
Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">", Token.reservedOpNames = ["->", "<", "<=", "=", "!=", ">=", ">",
"+", "-", "*", "&&", "||", "!"] "+", "-", "*", "&&", "||", "!", ":"]
} }
lexer :: Token.TokenParser () lexer :: Token.TokenParser ()
...@@ -107,7 +107,7 @@ data Statement = States [String] ...@@ -107,7 +107,7 @@ data Statement = States [String]
| Initial [String] | Initial [String]
| TrueStatement [String] | TrueStatement [String]
| FalseStatement [String] | FalseStatement [String]
| PredicateStatement (Formula String) | PredicateStatement (QuantFormula String)
| Arcs [(String,String,Integer)] | Arcs [(String,String,Integer)]
statement :: Parser Statement statement :: Parser Statement
...@@ -125,10 +125,10 @@ populationProtocol = do ...@@ -125,10 +125,10 @@ populationProtocol = do
reserved "protocol" reserved "protocol"
name <- option "" ident name <- option "" ident
statements <- braces (many statement) statements <- braces (many statement)
let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],[],[]) statements let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],Nothing,[]) statements
let predicate = case ps of let predicate = case ps of
[] -> FTrue Nothing -> ExQuantFormula [] FTrue
(p:ps) -> foldl (:&:) p ps Just p -> p
return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as
where where
splitStatement (qs,ts,qinitial,qtrue,qfalse,ps,as) stmnt = case stmnt of splitStatement (qs,ts,qinitial,qtrue,qfalse,ps,as) stmnt = case stmnt of
...@@ -137,7 +137,7 @@ populationProtocol = do ...@@ -137,7 +137,7 @@ populationProtocol = do
Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,ps,as) Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,ps,as)
TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,ps,as) TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,ps,as)
FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,ps,as) FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,ps,as)
PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,p : ps,as) PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,Just p,as)
Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as) Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as)
binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
...@@ -193,10 +193,22 @@ formAtom = try linIneq ...@@ -193,10 +193,22 @@ formAtom = try linIneq
formula :: Parser (Formula String) formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula" formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
predicate :: Parser (Formula String) quantFormula :: Parser (QuantFormula String)
quantFormula =
(do
reserved "EXISTS"
xs <- optionalCommaSep ident
reservedOp ":"
p <- formula
return (ExQuantFormula xs p)
)
<|>
(ExQuantFormula [] <$> formula)
predicate :: Parser (QuantFormula String)
predicate = do predicate = do
reserved "predicate" reserved "predicate"
form <- braces formula form <- braces quantFormula
return form return form
parseContent :: Parser PopulationProtocol parseContent :: Parser PopulationProtocol
......
...@@ -77,7 +77,7 @@ data PopulationProtocol = PopulationProtocol { ...@@ -77,7 +77,7 @@ data PopulationProtocol = PopulationProtocol {
initialStates :: [State], initialStates :: [State],
trueStates :: [State], trueStates :: [State],
falseStates :: [State], falseStates :: [State],
predicate :: Formula State, predicate :: QuantFormula State,
adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]), adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]),
adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)]) adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)])
} }
...@@ -149,7 +149,7 @@ invertPopulationProtocol pp = ...@@ -149,7 +149,7 @@ invertPopulationProtocol pp =
makePopulationProtocol :: String -> [State] -> [Transition] -> makePopulationProtocol :: String -> [State] -> [Transition] ->
[State] -> [State] -> [State] -> Formula State -> [State] -> [State] -> [State] -> QuantFormula State ->
[Either (Transition, State, Integer) (State, Transition, Integer)] -> [Either (Transition, State, Integer) (State, Transition, Integer)] ->
PopulationProtocol PopulationProtocol
makePopulationProtocol name states transitions initialStates trueStates falseStates predicate arcs = makePopulationProtocol name states transitions initialStates trueStates falseStates predicate arcs =
...@@ -183,7 +183,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta ...@@ -183,7 +183,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld) addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] -> makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] ->
Formula String -> [(String, String, Integer)] -> PopulationProtocol QuantFormula String -> [(String, String, Integer)] -> PopulationProtocol
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate arcs = makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate arcs =
makePopulationProtocol makePopulationProtocol
name name
...@@ -217,7 +217,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat ...@@ -217,7 +217,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
error $ l ++ " and " ++ r ++ " both transitions" error $ l ++ " and " ++ r ++ " both transitions"
makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] -> makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] ->
Formula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] -> QuantFormula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
PopulationProtocol PopulationProtocol
makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate ts = makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate ts =
makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate arcs makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate arcs
...@@ -226,7 +226,7 @@ makePopulationProtocolWithTrans name states initialStates trueStates falseStates ...@@ -226,7 +226,7 @@ makePopulationProtocolWithTrans name states initialStates trueStates falseStates
[ Left (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ] [ Left (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ]
makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] ->
Formula String -> [(String, ([(String, Integer)], [(String, Integer)]))] -> QuantFormula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
PopulationProtocol PopulationProtocol
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate arcs = makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate arcs =
makePopulationProtocolWithTrans makePopulationProtocolWithTrans
......
...@@ -3,6 +3,9 @@ ...@@ -3,6 +3,9 @@
module Property module Property
(Property(..), (Property(..),
Formula(..), Formula(..),
QuantFormula(..),
quantifiedVariables,
innerFormula,
Op(..), Op(..),
Term(..), Term(..),
PropResult(..), PropResult(..),
...@@ -48,6 +51,9 @@ instance Show Op where ...@@ -48,6 +51,9 @@ instance Show Op where
show Le = "≤" show Le = "≤"
show Lt = "<" show Lt = "<"
data QuantFormula a = ExQuantFormula [a] (Formula a)
deriving (Eq)
data Formula a = data Formula a =
FTrue | FFalse FTrue | FFalse
| LinearInequation (Term a) Op (Term a) | LinearInequation (Term a) Op (Term a)
...@@ -59,6 +65,16 @@ data Formula a = ...@@ -59,6 +65,16 @@ data Formula a =
infixr 3 :&: infixr 3 :&:
infixr 2 :|: infixr 2 :|:
quantifiedVariables :: QuantFormula a -> [a]
quantifiedVariables (ExQuantFormula xs _) = xs
innerFormula :: QuantFormula a -> Formula a
innerFormula (ExQuantFormula _ p) = p
instance (Show a) => Show (QuantFormula a) where
show (ExQuantFormula [] p) = show p
show (ExQuantFormula ps p) = "∃" ++ unwords (map show ps) ++ ": " ++ show p
instance (Show a) => Show (Formula a) where instance (Show a) => Show (Formula a) where
show FTrue = "true" show FTrue = "true"
show FFalse = "false" show FFalse = "false"
...@@ -68,6 +84,9 @@ instance (Show a) => Show (Formula a) where ...@@ -68,6 +84,9 @@ instance (Show a) => Show (Formula a) where
show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")" show (p :&: q) = "(" ++ show p ++ " ∧ " ++ show q ++ ")"
show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")" show (p :|: q) = "(" ++ show p ++ " ∨ " ++ show q ++ ")"
instance Functor QuantFormula where
fmap f (ExQuantFormula xs p) = ExQuantFormula (fmap f xs) (fmap f p)
instance Functor Formula where instance Functor Formula where
fmap _ FTrue = FTrue fmap _ FTrue = FTrue
fmap _ FFalse = FFalse fmap _ FFalse = FFalse
......
...@@ -14,7 +14,7 @@ import Control.Monad.IO.Class ...@@ -14,7 +14,7 @@ import Control.Monad.IO.Class
import Control.Applicative import Control.Applicative
type ConstraintProblem a b = type ConstraintProblem a b =
(String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b) (String, String, [String], [String], [String], (String -> SBV a) -> SBool, (String -> a) -> b)
type MinConstraintProblem a b c = type MinConstraintProblem a b c =
(Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c)) (Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c))
...@@ -24,11 +24,13 @@ rebuildModel _ (Left _) = Nothing ...@@ -24,11 +24,13 @@ rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown" rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m
symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) -> symConstraints :: SymWord a => [String] -> [String] -> [String] -> ((String -> SBV a) -> SBool) ->
Symbolic SBool Symbolic SBool
symConstraints vars constraint = do symConstraints vars exVars allVars constraint = do
syms <- mapM exists vars syms <- mapM exists vars
return $ constraint $ val $ M.fromList $ vars `zip` syms exSyms <- mapM exists exVars
allSyms <- mapM forall allVars
return $ constraint $ val $ M.fromList $ (vars `zip` syms) ++ (exVars `zip` exSyms) ++ (allVars `zip` allSyms)
getSolverConfig :: Bool -> Bool -> SMTConfig getSolverConfig :: Bool -> Bool -> SMTConfig
getSolverConfig verbose auto = getSolverConfig verbose auto =
...@@ -37,12 +39,12 @@ getSolverConfig verbose auto = ...@@ -37,12 +39,12 @@ getSolverConfig verbose auto =
checkSat :: (SatModel a, SymWord a, Show a, Show b) => checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
ConstraintProblem a b -> OptIO (Maybe b) ConstraintProblem a b -> OptIO (Maybe b)
checkSat (problemName, resultName, vars, constraint, interpretation) = do checkSat (problemName, resultName, vars, exVars, allVars, constraint, interpretation) = do
verbosePut 2 $ "Checking SAT of " ++ problemName verbosePut 2 $ "Checking SAT of " ++ problemName
verbosity <- opt optVerbosity verbosity <- opt optVerbosity
autoConf <- opt optSMTAuto autoConf <- opt optSMTAuto
result <- liftIO (satWith (getSolverConfig (verbosity >= 4) autoConf) result <- liftIO (satWith (getSolverConfig (verbosity >= 4) autoConf)
(symConstraints vars constraint)) (symConstraints vars exVars allVars constraint))
case rebuildModel vars (getModel result) of case rebuildModel vars (getModel result) of
Nothing -> do Nothing -> do
verbosePut 2 "- unsat" verbosePut 2 "- unsat"
......
...@@ -3,6 +3,7 @@ module Solver.Formula ...@@ -3,6 +3,7 @@ module Solver.Formula
where where
import Data.SBV import Data.SBV
import qualified Data.Map as M
import Util import Util
import Property import Property
......
...@@ -76,7 +76,7 @@ checkLayeredTerminationSat pp triplets k = ...@@ -76,7 +76,7 @@ checkLayeredTerminationSat pp triplets k =
b = makeVarMap $ transitions pp b = makeVarMap $ transitions pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
("layered termination", "invariant", ("layered termination", "invariant",
concat (map getNames ys) ++ getNames b, concat (map getNames ys) ++ getNames b, [], [],
\fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit, \fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit,
\fm -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys))) \fm -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys)))
......
...@@ -50,16 +50,21 @@ initialConfiguration pp m0 = ...@@ -50,16 +50,21 @@ initialConfiguration pp m0 =
(sum (mval m0 (initialStates pp)) .>= 2) &&& (sum (mval m0 (initialStates pp)) .>= 2) &&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) (sum (mval m0 (states pp \\ initialStates pp)) .== 0)
differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SBool differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp m0 m1 m2 = differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
(o1 &&& o2) ||| (oT &&& oF) |||
(if checkCorrectness then correctnessConstraints else false) (if checkCorrectness then correctnessConstraints else false)
where where
o1 = sum (mval m1 (trueStates pp)) .> 0 oT = sum (mval m1 (trueStates pp)) .> 0
o2 = sum (mval m2 (falseStates pp)) .> 0 oF = sum (mval m2 (falseStates pp)) .> 0
correctnessConstraints = correctnessConstraints =
let o0 = evaluateFormula (predicate pp) m0 if null (quantifiedVariables (predicate pp)) then
in (o0 &&& o2) ||| (bnot o0 &&& o1) let oP = evaluateFormula (innerFormula (predicate pp)) m0
in (oP &&& oF) ||| (bnot oP &&& oT)
else
let oPT = evaluateFormula (innerFormula (predicate pp)) (M.union m0 qe)
oPF = evaluateFormula (Neg (innerFormula (predicate pp))) (M.union m0 qa)
in (oPT &&& oF) ||| (oPF &&& oT)
unmarkedByConfiguration :: [State] -> SIMap State -> SBool unmarkedByConfiguration :: [State] -> SIMap State -> SBool
unmarkedByConfiguration r m = sum (mval m r) .== 0 unmarkedByConfiguration r m = sum (mval m r) .== 0
...@@ -98,8 +103,8 @@ checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons = ...@@ -98,8 +103,8 @@ 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 -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
RefinementObjects -> SBool SIMap State -> SIMap State ->RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 (utraps, usiphons) = checkStrongConsensus checkCorrectness pp 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 &&&
...@@ -110,7 +115,7 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 (utraps, usiphons) = ...@@ -110,7 +115,7 @@ checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 (utraps, usiphons) =
nonNegativityConstraints x2 &&& nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&& terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&& terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp m0 m1 m2 &&& differentConsensusConstraints checkCorrectness pp 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
...@@ -121,9 +126,11 @@ checkStrongConsensusSat checkCorrectness pp refinements = ...@@ -121,9 +126,11 @@ 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)
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 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) refinements, \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 -> 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
...@@ -208,7 +215,7 @@ findTrapConstraintsSat pp c = ...@@ -208,7 +215,7 @@ findTrapConstraintsSat pp c =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
("trap marked by x1 or x2 and not marked in m1 or m2", "trap", ("trap marked by x1 or x2 and not marked in m1 or m2", "trap",
getNames b, getNames b, [], [],
\fm -> findTrapConstraints pp c (fmap fm b) sizeLimit, \fm -> findTrapConstraints pp c (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b))) \fm -> statesFromAssignment (fmap fm b)))
...@@ -226,7 +233,7 @@ findUTrapConstraintsSat pp c = ...@@ -226,7 +233,7 @@ findUTrapConstraintsSat pp c =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> 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", ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap",
getNames b, getNames b, [], [],
\fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit, \fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b))) \fm -> statesFromAssignment (fmap fm b)))
...@@ -243,7 +250,7 @@ findSiphonConstraintsSat pp c = ...@@ -243,7 +250,7 @@ findSiphonConstraintsSat pp c =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
("siphon used by x1 or x2 and unmarked in m0", "siphon", ("siphon used by x1 or x2 and unmarked in m0", "siphon",
getNames b, getNames b, [], [],
\fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit, \fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b))) \fm -> statesFromAssignment (fmap fm b)))
...@@ -263,7 +270,7 @@ findUSiphonConstraintsSat pp c = ...@@ -263,7 +270,7 @@ findUSiphonConstraintsSat pp c =
let b = makeVarMap $ states pp let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit -> in (minimizeMethod, \sizeLimit ->
("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon", ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon",
getNames b, getNames b, [], [],
\fm -> findUSiphonConstraints pp c (fmap fm b) sizeLimit, \fm -> findUSiphonConstraints pp c (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b))) \fm -> statesFromAssignment (fmap fm b)))
...@@ -299,8 +306,8 @@ checkBounds :: Integer -> SIMap State -> SBool ...@@ -299,8 +306,8 @@ 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 -> Integer -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
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 = checkStrongConsensusComplete checkCorrectness pp 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 &&&
...@@ -311,7 +318,7 @@ checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 ...@@ -311,7 +318,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 &&& differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa &&&
checkBounds max r1 &&& checkBounds max r1 &&&
checkBounds max r2 &&& checkBounds max r2 &&&
checkBounds max s1 &&& checkBounds max s1 &&&
...@@ -337,9 +344,12 @@ checkStrongConsensusCompleteSat checkCorrectness pp = ...@@ -337,9 +344,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'"++)