Skip to content

GitLab

Commit 2deed1ec authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Remove quantified formula and additional existential/forall quantifiers

parent 280b25b4
Hide whitespace changes
Inline Side-by-side
Showing with 42 additions and 90 deletions
src/Parser/PP.hs
View file @ 2deed1ec
......@@ -131,18 +131,6 @@ formAtom = try linIneq
formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
quantFormula :: Parser (QuantFormula String)
quantFormula =
(do
reserved "EXISTS"
xs <- optionalCommaSep ident
reservedOp ":"
p <- formula
return (ExQuantFormula xs p)
)
<|>
(ExQuantFormula [] <$> formula)
instance FromJSON (Formula String) where
parseJSON (String v) = do
let f = parse formula "" (T.unpack v)
......@@ -154,17 +142,6 @@ instance FromJSON (Formula String) where
instance ToJSON (Formula String) where
toJSON x = String ""
instance FromJSON (QuantFormula String) where
parseJSON (String v) = do
let formula = parse quantFormula "" (T.unpack v)
case formula of
Left e -> fail "Predicate formula not well-formed."
Right r -> return r
parseJSON _ = fail "Expect string for predicate."
instance ToJSON (QuantFormula String) where
toJSON x = String ""
data RecordTransition = RecordTransition {
name :: String,
pre :: [String],
......@@ -178,7 +155,7 @@ data RecordPP = RecordPP {
initialStates :: [String],
trueStates :: [String],
precondition :: Maybe (Formula String),
predicate :: Maybe (QuantFormula String),
predicate :: Maybe (Formula String),
description :: Maybe String
} deriving (Show)
......@@ -191,7 +168,7 @@ recordPP2PopulationProtocol r =
falseStates = [q | q <- states r, not (S.member q (S.fromList (trueStates r)))]
arcs = [(q, name t, 1) | t <- transitions r, q <- pre t] ++
[(name t, q, 1) | t <- transitions r, q <- post t]
p = case predicate r of Nothing -> ExQuantFormula [] FTrue
p = case predicate r of Nothing -> FTrue
(Just p') -> p'
precond = case precondition r of Nothing -> FTrue
(Just p') -> p'
......
src/PopulationProtocol.hs
View file @ 2deed1ec
......@@ -77,7 +77,7 @@ data PopulationProtocol = PopulationProtocol {
initialStates :: [State],
trueStates :: [State],
falseStates :: [State],
predicate :: QuantFormula State,
predicate :: Formula State,
precondition :: Formula State,
adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]),
adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)])
......@@ -154,7 +154,7 @@ invertPopulationProtocol pp =
makePopulationProtocol :: String -> [State] -> [Transition] ->
[State] -> [State] -> [State] -> QuantFormula State -> Formula State ->
[State] -> [State] -> [State] -> Formula State -> Formula State ->
[Either (Transition, State, Integer) (State, Transition, Integer)] ->
PopulationProtocol
makePopulationProtocol name states transitions initialStates trueStates falseStates predicate precondition arcs =
......@@ -189,7 +189,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] ->
QuantFormula String -> Formula String -> [(String, String, Integer)] -> PopulationProtocol
Formula String -> Formula String -> [(String, String, Integer)] -> PopulationProtocol
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate precondition arcs =
makePopulationProtocol
name
......@@ -224,7 +224,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
error $ l ++ " and " ++ r ++ " both transitions"
makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] ->
QuantFormula State -> Formula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
Formula State -> Formula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
PopulationProtocol
makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate precondition ts =
makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate precondition arcs
......@@ -233,7 +233,7 @@ makePopulationProtocolWithTrans name states initialStates trueStates falseStates
[ Left (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ]
makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] ->
QuantFormula String -> Formula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
Formula String -> Formula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
PopulationProtocol
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate precondition arcs =
makePopulationProtocolWithTrans
......
src/Property.hs
View file @ 2deed1ec
......@@ -3,9 +3,6 @@
module Property
(Property(..),
Formula(..),
QuantFormula(..),
quantifiedVariables,
innerFormula,
negationNormalForm,
eliminateModulo,
Op(..),
......@@ -71,9 +68,6 @@ negateOp Lt = Ge
negateOp (ModEq m) = (ModNe m)
negateOp (ModNe m) = (ModEq m)
data QuantFormula a = ExQuantFormula [a] (Formula a)
deriving (Eq)
data Formula a =
FTrue | FFalse
| LinearInequation (Term a) Op (Term a)
......@@ -91,9 +85,12 @@ 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 (Neg (Neg g)) = negationNormalForm g
negationNormalForm (g :&: h) = (negationNormalForm g) :&: (negationNormalForm h)
negationNormalForm (g :|: h) = (negationNormalForm g) :|: (negationNormalForm h)
negationNormalForm f = f
negationNormalForm f@(LinearInequation _ _ _) = f
negationNormalForm FTrue = FTrue
negationNormalForm FFalse = FFalse
eliminateModulo :: (Int -> a) -> Formula a -> (Formula a, [a])
eliminateModulo = eliminateModulo' 0
......@@ -118,16 +115,6 @@ eliminateModulo' n makeVar (g :&: h) =
in (g' :&: h', ag ++ ah)
eliminateModulo' _ _ f = (f, [])
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
show FTrue = "true"
show FFalse = "false"
......@@ -137,9 +124,6 @@ instance (Show a) => Show (Formula a) where
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
fmap _ FTrue = FTrue
fmap _ FFalse = FFalse
......
src/Solver.hs
View file @ 2deed1ec
......@@ -14,7 +14,7 @@ import Control.Monad.IO.Class
import Control.Applicative
type ConstraintProblem a b =
(String, String, [String], [String], [String], (String -> SBV a) -> SBool, (String -> a) -> b)
(String, String, [String], (String -> SBV a) -> SBool, (String -> a) -> b)
type MinConstraintProblem a b c =
(Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c))
......@@ -24,13 +24,11 @@ rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m
symConstraints :: SymWord a => [String] -> [String] -> [String] -> ((String -> SBV a) -> SBool) ->
symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
Symbolic SBool
symConstraints vars exVars allVars constraint = do
symConstraints vars constraint = do
syms <- mapM exists vars
exSyms <- mapM exists exVars
allSyms <- mapM forall allVars
return $ constraint $ val $ M.fromList $ (vars `zip` syms) ++ (exVars `zip` exSyms) ++ (allVars `zip` allSyms)
return $ constraint $ val $ M.fromList $ (vars `zip` syms)
getSolverConfig :: BackendSolver -> Bool -> SMTConfig
getSolverConfig Options.Z3 verbose = z3 { verbose=verbose }
......@@ -43,12 +41,12 @@ getSolverConfig Options.CVC4 verbose =
checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
ConstraintProblem a b -> OptIO (Maybe b)
checkSat (problemName, resultName, vars, exVars, allVars, constraint, interpretation) = do
checkSat (problemName, resultName, vars, constraint, interpretation) = do
verbosePut 2 $ "Checking SAT of " ++ problemName
verbosity <- opt optVerbosity
solver <- opt optSolver
result <- liftIO (satWith (getSolverConfig solver (verbosity >= 4))
(symConstraints vars exVars allVars constraint))
(symConstraints vars constraint))
case rebuildModel vars (getModelAssignment result) of
Nothing -> do
verbosePut 2 "- unsat"
......
src/Solver/LayeredTermination.hs
View file @ 2deed1ec
......@@ -76,7 +76,7 @@ checkLayeredTerminationSat pp triplets k =
b = makeVarMap $ transitions pp
in (minimizeMethod, \sizeLimit ->
("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 -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys)))
......
src/Solver/StrongConsensus.hs
View file @ 2deed1ec
......@@ -54,22 +54,17 @@ initialConfiguration pp m0 =
(evaluateFormula (precondition pp) m0)
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 =
SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 pVars =
(oT &&& oF) |||
(if checkCorrectness then correctnessConstraints else false)
where
oT = sum (mval m1 (trueStates pp)) .> 0
oF = sum (mval m2 (falseStates pp)) .> 0
correctnessConstraints =
if null (quantifiedVariables (predicate pp)) then
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)
in (oPT &&& oF) ||| (oPF &&& oT)
let oPT = evaluateFormula pT (M.union m0 pVars)
oPF = evaluateFormula pF (M.union m0 pVars)
in (oPT &&& oF) ||| (oPF &&& oT)
unmarkedByConfiguration :: [State] -> SIMap State -> SBool
unmarkedByConfiguration r m = sum (mval m r) .== 0
......@@ -109,8 +104,8 @@ checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons =
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) =
SIMap State -> RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp pT pF m0 m1 m2 x1 x2 pVars (utraps, usiphons) =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -121,14 +116,14 @@ checkStrongConsensus checkCorrectness pp pT pF m0 m1 m2 x1 x2 qe qa (utraps, usi
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 qe qa &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 pVars &&&
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
fT = negationNormalForm $ predicate pp
fF = negationNormalForm (Neg fT)
(pT, varsT) = elim "mpt'" fT
(pF, varsF) = elim "mpf'" fF
......@@ -141,12 +136,11 @@ checkStrongConsensusSat checkCorrectness pp refinements =
m2 = makeVarMapWith ("m2'"++) $ states pp
x1 = makeVarMapWith ("x1'"++) $ transitions pp
x2 = makeVarMapWith ("x2'"++) $ transitions pp
(pT, pF, modVars) = makePredicates pp
qe = makeVarMapWith ("e'"++) $ modVars
qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
(pT, pF, modVarNames) = makePredicates pp
modVars = makeVarMapWith ("e'"++) $ modVarNames
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 pT pF (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) (fmap fm qe) (fmap fm qa) refinements,
concatMap getNames [m0, m1, m2, modVars] ++ concatMap getNames [x1, x2],
\fm -> checkStrongConsensus checkCorrectness pp pT pF (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) (fmap fm modVars) 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
......@@ -231,7 +225,7 @@ findTrapConstraintsSat pp c =
let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit ->
("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 -> statesFromAssignment (fmap fm b)))
......@@ -249,7 +243,7 @@ findUTrapConstraintsSat pp c =
let b = makeVarMap $ states pp
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",
getNames b, [], [],
getNames b,
\fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b)))
......@@ -266,7 +260,7 @@ findSiphonConstraintsSat pp c =
let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit ->
("siphon used by x1 or x2 and unmarked in m0", "siphon",
getNames b, [], [],
getNames b,
\fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit,
\fm -> statesFromAssignment (fmap fm b)))
......@@ -286,7 +280,7 @@ findUSiphonConstraintsSat pp c =
let b = makeVarMap $ states pp
in (minimizeMethod, \sizeLimit ->
("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 -> statesFromAssignment (fmap fm b)))
......@@ -323,8 +317,8 @@ checkBounds max = bAnd . map (\x -> x .>= 0 &&& x .<= literal max) . vals
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 pT pF max m0 m1 m2 x1 x2 r1 r2 s1 s2 qe qa =
SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
checkStrongConsensusComplete checkCorrectness pp pT pF max m0 m1 m2 x1 x2 r1 r2 s1 s2 pVars =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -335,7 +329,7 @@ checkStrongConsensusComplete checkCorrectness pp pT pF max m0 m1 m2 x1 x2 r1 r2
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 qe qa &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 pVars &&&
checkBounds max r1 &&&
checkBounds max r2 &&&
checkBounds max s1 &&&
......@@ -361,13 +355,12 @@ checkStrongConsensusCompleteSat checkCorrectness pp =
r2 = makeVarMapWith ("r2'"++) $ states pp
s1 = makeVarMapWith ("s1'"++) $ states pp
s2 = makeVarMapWith ("s2'"++) $ states pp
(pT, pF, modVars) = makePredicates pp
qe = makeVarMapWith ("e'"++) $ modVars
qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
(pT, pF, modVarNames) = makePredicates pp
modVars = makeVarMapWith ("e'"++) $ modVarNames
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, modVars] ++ concatMap getNames [x1, 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 modVars),
\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 ->
......
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