Skip to content

GitLab

peregrine
peregrine
Commit 07a1543e authored by Philipp Meyer's avatar Philipp Meyer
Browse files
Options

Add support for checking correctness of protocols

parent d3719a77
Hide whitespace changes
Inline Side-by-side
Showing with 79 additions and 62 deletions
examples/broadcast.pp
View file @ 07a1543e
......@@ -7,4 +7,5 @@ population protocol "Broadcast Protocol" {
initial { _true _false }
true { _true }
false { _false }
predicate { _true >= 1 }
}
examples/majority.pp
View file @ 07a1543e
......@@ -10,4 +10,5 @@ population protocol "Majority Protocol" {
initial { good bad }
true { good neutral }
false { bad mildlybad }
predicate { good > bad }
}
examples/threshold_l3_c1.pp
View file @ 07a1543e
......@@ -294,4 +294,9 @@ population protocol "Old Threshold Protocol with l = 3 and c = 1" {
initial {_l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3}
true {_l_true_m3 _l_true_m2 _l_true_m1 _l_true_0 _l_true_p1 _l_true_p2 _l_true_p3 _nl_true_m3 _nl_true_m2 _nl_true_m1 _nl_true_0 _nl_true_p1 _nl_true_p2 _nl_true_p3}
false {_l_false_m3 _l_false_m2 _l_false_m1 _l_false_0 _l_false_p1 _l_false_p2 _l_false_p3 _nl_false_m3 _nl_false_m2 _nl_false_m1 _nl_false_0 _nl_false_p1 _nl_false_p2 _nl_false_p3}
predicate {
(-3) * _l_true_m3 + (-2) * _l_true_m2 + (-1) * _l_true_m1 + _l_true_p1 + 2 * _l_true_p2 + 3 * _l_true_p3 +
(-3) * _l_false_m3 + (-2) * _l_false_m2 + (-1) * _l_false_m1 + _l_false_p1 + 2 * _l_false_p2 + 3 * _l_false_p3
< 1
}
}
src/Main.hs
View file @ 07a1543e
......@@ -79,7 +79,6 @@ checkProperty :: PopulationProtocol -> Property -> OptIO PropResult
checkProperty pp prop = do
verbosePut 1 $ "\nChecking " ++ show prop
r <- case prop of
Correctness -> error "not yet implemented"
LayeredTermination -> checkLayeredTermination pp
StrongConsensus -> checkStrongConsensus pp
verbosePut 0 $ show prop ++ " " ++ show r
......@@ -95,43 +94,27 @@ printInvariant inv = do
checkStrongConsensus :: PopulationProtocol -> OptIO PropResult
checkStrongConsensus pp = do
checkCorrectness <- opt optCorrectness
when checkCorrectness $ verbosePut 1 "- additionally checking correctness"
r <- checkStrongConsensus' pp ([], [])
case r of
(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
optRefine <- opt optRefinementType
checkCorrectness <- opt optCorrectness
case optRefine of
RefAll -> do
r <- checkSat $ checkStrongConsensusCompleteSat pp
r <- checkSat $ checkStrongConsensusCompleteSat checkCorrectness 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
r <- checkSat $ checkStrongConsensusSat checkCorrectness pp refinements
case r of
Nothing -> return (Nothing, refinements)
Just c -> do
......
src/Options.hs
View file @ 07a1543e
......@@ -38,6 +38,7 @@ data Options = Options { inputFormat :: InputFormat
, optShowHelp :: Bool
, optShowVersion :: Bool
, optProperties :: PropertyOption
, optCorrectness :: Bool
, optRefinementType :: RefinementOption
, optMinimizeRefinement :: Int
, optSMTAuto :: Bool
......@@ -54,6 +55,7 @@ startOptions = Options { inputFormat = InPP
, optShowHelp = False
, optShowVersion = False
, optProperties = PropDefault
, optCorrectness = False
, optRefinementType = RefDefault
, optMinimizeRefinement = 0
, optSMTAuto = True
......@@ -82,6 +84,10 @@ options =
}))
"Prove that the protocol satisfies strong consensus"
, Option "" ["correctness"]
(NoArg (\opt -> Right opt { optCorrectness = True }))
"Prove that the protocol correctly satisfies the given predicate"
, Option "i" ["invariant"]
(NoArg (\opt -> Right opt { optInvariant = True }))
"Generate an invariant"
......
src/Parser/PP.hs
View file @ 07a1543e
......@@ -107,6 +107,7 @@ data Statement = States [String]
| Initial [String]
| TrueStatement [String]
| FalseStatement [String]
| PredicateStatement (Formula String)
| Arcs [(String,String,Integer)]
statement :: Parser Statement
......@@ -115,7 +116,8 @@ statement = States <$> states <|>
Arcs <$> arcs <|>
Initial <$> initial <|>
TrueStatement <$> trueStates <|>
FalseStatement <$> falseStates
FalseStatement <$> falseStates <|>
PredicateStatement <$> predicate
populationProtocol :: Parser PopulationProtocol
populationProtocol = do
......@@ -123,16 +125,20 @@ populationProtocol = do
reserved "protocol"
name <- option "" ident
statements <- braces (many statement)
let (qs,ts,qinitial,qtrue,qfalse,as) = foldl splitStatement ([],[],[],[],[],[]) statements
return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse as
let (qs,ts,qinitial,qtrue,qfalse,ps,as) = foldl splitStatement ([],[],[],[],[],[],[]) statements
let predicate = case ps of
[] -> FTrue
(p:ps) -> foldl (:&:) p ps
return $ makePopulationProtocolFromStrings name qs ts qinitial qtrue qfalse predicate as
where
splitStatement (qs,ts,qinitial,qtrue,qfalse,as) stmnt = case stmnt of
States q -> (q ++ qs,ts,qinitial,qtrue,qfalse,as)
Transitions t -> (qs,t ++ ts,qinitial,qtrue,qfalse,as)
Initial q -> (qs,ts,q ++ qinitial,qtrue,qfalse,as)
TrueStatement q -> (qs,ts,qinitial,q ++ qtrue,qfalse,as)
FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,as)
Arcs a -> (qs,ts,qinitial,qtrue,qfalse,a ++ as)
splitStatement (qs,ts,qinitial,qtrue,qfalse,ps,as) stmnt = case stmnt of
States q -> (q ++ qs,ts,qinitial,qtrue,qfalse,ps,as)
Transitions t -> (qs,t ++ ts,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)
FalseStatement q -> (qs,ts,qinitial,qtrue,q ++ qfalse,ps,as)
PredicateStatement p -> (qs,ts,qinitial,qtrue,qfalse,p : ps,as)
Arcs a -> (qs,ts,qinitial,qtrue,qfalse,ps,a ++ as)
binary :: String -> (a -> a -> a) -> Assoc -> Operator String () Identity a
binary name fun = Infix ( reservedOp name *> return fun )
......@@ -187,17 +193,16 @@ formAtom = try linIneq
formula :: Parser (Formula String)
formula = buildExpressionParser formOperatorTable formAtom <?> "formula"
predicate :: Parser (Formula PopulationProtocol.State)
predicate :: Parser (Formula String)
predicate = do
reserved "predicate"
name <- option "" ident
form <- braces formula
return (fmap PopulationProtocol.State form)
return form
parseContent :: Parser PopulationProtocol
parseContent = do
whiteSpace
pp <- populationProtocol
-- properties <- many predicate
properties <- many predicate
eof
return pp
src/PopulationProtocol.hs
View file @ 07a1543e
......@@ -6,7 +6,7 @@ module PopulationProtocol
Configuration,FlowVector,RConfiguration,RFlowVector,
renameState,renameTransition,renameStatesAndTransitions,
invertPopulationProtocol,
name,showNetName,states,transitions,initialStates,trueStates,falseStates,
name,showNetName,states,transitions,initialStates,trueStates,falseStates,predicate,
pre,lpre,post,lpost,mpre,mpost,context,
makePopulationProtocol,makePopulationProtocolWithTrans,
makePopulationProtocolFromStrings,makePopulationProtocolWithTransFromStrings,
......@@ -20,6 +20,7 @@ import Data.List (sort,(\\))
import Data.Tuple (swap)
import Util
import Property
newtype State = State String deriving (Ord,Eq)
newtype Transition = Transition String deriving (Ord,Eq)
......@@ -76,6 +77,7 @@ data PopulationProtocol = PopulationProtocol {
initialStates :: [State],
trueStates :: [State],
falseStates :: [State],
predicate :: Formula State,
adjacencyQ :: M.Map State ([(Transition,Integer)], [(Transition,Integer)]),
adjacencyT :: M.Map Transition ([(State,Integer)], [(State,Integer)])
}
......@@ -91,6 +93,7 @@ instance Show PopulationProtocol where
"\nInitial states : " ++ show (initialStates pp) ++
"\nTrue states : " ++ show (trueStates pp) ++
"\nFalse states : " ++ show (falseStates pp) ++
"\nPredicate : " ++ show (predicate pp) ++
"\nState arcs :\n" ++ unlines
(map showContext (M.toList (adjacencyQ pp))) ++
"\nTransition arcs:\n" ++ unlines
......@@ -118,6 +121,8 @@ renameStatesAndTransitions f pp =
listSet $ map (renameState f) $ trueStates pp,
falseStates =
listSet $ map (renameState f) $ falseStates pp,
predicate =
fmap (renameState f) $ predicate pp,
adjacencyQ = mapAdjacency (renameState f) (renameTransition f) $
adjacencyQ pp,
adjacencyT = mapAdjacency (renameTransition f) (renameState f) $
......@@ -136,6 +141,7 @@ invertPopulationProtocol pp =
initialStates = initialStates pp,
trueStates = trueStates pp,
falseStates = falseStates pp,
predicate = predicate pp,
adjacencyQ = M.map swap $ adjacencyQ pp,
adjacencyT = M.map swap $ adjacencyT pp
}
......@@ -143,10 +149,10 @@ invertPopulationProtocol pp =
makePopulationProtocol :: String -> [State] -> [Transition] ->
[State] -> [State] -> [State] ->
[State] -> [State] -> [State] -> Formula State ->
[Either (Transition, State, Integer) (State, Transition, Integer)] ->
PopulationProtocol
makePopulationProtocol name states transitions initialStates trueStates falseStates arcs =
makePopulationProtocol name states transitions initialStates trueStates falseStates predicate arcs =
PopulationProtocol {
name = name,
states = listSet states,
......@@ -154,6 +160,7 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
initialStates = listSet initialStates,
trueStates = listSet trueStates,
falseStates = listSet falseStates,
predicate = predicate,
adjacencyQ = M.map (listMap *** listMap) adQ,
adjacencyT = M.map (listMap *** listMap) adT
}
......@@ -176,8 +183,8 @@ makePopulationProtocol name states transitions initialStates trueStates falseSta
addArc (lNew,rNew) (lOld,rOld) = (lNew ++ lOld,rNew ++ rOld)
makePopulationProtocolFromStrings :: String -> [String] -> [String] -> [String] -> [String] -> [String] ->
[(String, String, Integer)] -> PopulationProtocol
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates arcs =
Formula String -> [(String, String, Integer)] -> PopulationProtocol
makePopulationProtocolFromStrings name states transitions initialStates trueStates falseStates predicate arcs =
makePopulationProtocol
name
(map State (S.toAscList stateSet))
......@@ -185,6 +192,7 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
(map State initialStates)
(map State trueStates)
(map State falseStates)
(fmap State predicate)
(map toEitherArc arcs)
where
stateSet = S.fromList states
......@@ -209,24 +217,25 @@ makePopulationProtocolFromStrings name states transitions initialStates trueStat
error $ l ++ " and " ++ r ++ " both transitions"
makePopulationProtocolWithTrans :: String -> [State] -> [State] -> [State] -> [State] ->
[(Transition, ([(State, Integer)], [(State, Integer)]))] ->
Formula State -> [(Transition, ([(State, Integer)], [(State, Integer)]))] ->
PopulationProtocol
makePopulationProtocolWithTrans name states initialStates trueStates falseStates ts =
makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates arcs
makePopulationProtocolWithTrans name states initialStates trueStates falseStates predicate ts =
makePopulationProtocol name states (map fst ts) initialStates trueStates falseStates predicate arcs
where
arcs = [ Right (q,t,w) | (t,(is,_)) <- ts, (q,w) <- is ] ++
[ Left (t,q,w) | (t,(_,os)) <- ts, (q,w) <- os ]
makePopulationProtocolWithTransFromStrings :: String -> [String] -> [String] -> [String] -> [String] ->
[(String, ([(String, Integer)], [(String, Integer)]))] ->
Formula String -> [(String, ([(String, Integer)], [(String, Integer)]))] ->
PopulationProtocol
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates arcs =
makePopulationProtocolWithTransFromStrings name states initialStates trueStates falseStates predicate arcs =
makePopulationProtocolWithTrans
name
(map State states)
(map State initialStates)
(map State trueStates)
(map State falseStates)
(fmap State predicate)
(map toTArc arcs)
where
toTArc (t, (iq, oq)) =
......
src/Property.hs
View file @ 07a1543e
......@@ -82,7 +82,6 @@ data Property = Correctness
| StrongConsensus
instance Show Property where
show Correctness = "correctness"
show LayeredTermination = "layered termination"
show StrongConsensus = "strong consensus"
......
src/Solver/StrongConsensus.hs
View file @ 07a1543e
......@@ -19,6 +19,7 @@ import Util
import PopulationProtocol
import Property
import Solver
import Solver.Formula
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration)
......@@ -49,9 +50,16 @@ initialConfiguration pp m0 =
(sum (mval m0 (initialStates pp)) .>= 2) &&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0)
differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints pp m1 m2 =
(sum (mval m1 (trueStates pp)) .> 0 &&& sum (mval m2 (falseStates pp)) .> 0)
differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp m0 m1 m2 =
(o1 &&& o2) |||
(if checkCorrectness then correctnessConstraints else false)
where
o1 = sum (mval m1 (trueStates pp)) .> 0
o2 = sum (mval m2 (falseStates pp)) .> 0
correctnessConstraints =
let o0 = evaluateFormula (predicate pp) m0
in (o0 &&& o2) ||| (bnot o0 &&& o1)
unmarkedByConfiguration :: [State] -> SIMap State -> SBool
unmarkedByConfiguration r m = sum (mval m r) .== 0
......@@ -89,9 +97,9 @@ 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 :: 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
checkStrongConsensus pp m0 m1 m2 x1 x2 (utraps, usiphons) =
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 (utraps, usiphons) =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -102,12 +110,12 @@ checkStrongConsensus pp m0 m1 m2 x1 x2 (utraps, usiphons) =
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints pp m1 m2 &&&
differentConsensusConstraints checkCorrectness pp m0 m1 m2 &&&
checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
checkStrongConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat pp refinements =
checkStrongConsensusSat :: Bool -> PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat checkCorrectness pp refinements =
let m0 = makeVarMapWith ("m0'"++) $ states pp
m1 = makeVarMapWith ("m1'"++) $ states pp
m2 = makeVarMapWith ("m2'"++) $ states pp
......@@ -115,7 +123,7 @@ checkStrongConsensusSat pp refinements =
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,
\fm -> checkStrongConsensus checkCorrectness pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) 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
......@@ -290,9 +298,9 @@ unusedBySequence pp max siphon x =
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 ->
checkStrongConsensusComplete :: Bool -> 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 =
checkStrongConsensusComplete checkCorrectness pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
......@@ -303,7 +311,7 @@ checkStrongConsensusComplete pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 =
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints pp m1 m2 &&&
differentConsensusConstraints checkCorrectness pp m0 m1 m2 &&&
checkBounds max r1 &&&
checkBounds max r2 &&&
checkBounds max s1 &&&
......@@ -317,8 +325,8 @@ checkStrongConsensusComplete pp max m0 m1 m2 x1 x2 r1 r2 s1 s2 =
unusedBySequence pp max s1 x1 &&&
unusedBySequence pp max s2 x2
checkStrongConsensusCompleteSat :: PopulationProtocol -> ConstraintProblem Integer StrongConsensusCompleteCounterExample
checkStrongConsensusCompleteSat pp =
checkStrongConsensusCompleteSat :: Bool -> PopulationProtocol -> ConstraintProblem Integer StrongConsensusCompleteCounterExample
checkStrongConsensusCompleteSat checkCorrectness pp =
let max = genericLength (states pp) + 1
m0 = makeVarMapWith ("m0'"++) $ states pp
m1 = makeVarMapWith ("m1'"++) $ states pp
......@@ -331,7 +339,7 @@ checkStrongConsensusCompleteSat 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 -> checkStrongConsensusComplete checkCorrectness 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 ->
......
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