StrongConsensus.hs 18.5 KB
Newer Older
1
2
{-# LANGUAGE FlexibleContexts #-}

Philipp Meyer's avatar
Philipp Meyer committed
3
4
module Solver.StrongConsensus
    (checkStrongConsensusSat,
5
     checkStrongConsensusCompleteSat,
Philipp Meyer's avatar
Philipp Meyer committed
6
     StrongConsensusCounterExample,
7
     RefinementObjects,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
8
     findTrapConstraintsSat,
9
     findSiphonConstraintsSat,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
10
     findUTrapConstraintsSat,
11
     findUSiphonConstraintsSat)
12
13
14
where

import Data.SBV
15
import qualified Data.Map as M
16
import Data.List ((\\),genericLength)
17
18

import Util
19
import PopulationProtocol
20
21
import Property
import Solver
22
import Solver.Formula
23

24
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
25
type StrongConsensusCompleteCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector, Configuration, Configuration, Configuration, Configuration)
26
type RefinementObjects = ([Trap], [Siphon])
27

28
29
30
31
32
33
34
stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
stateEquationConstraints pp m0 m x =
            bAnd $ map checkStateEquation $ states pp
        where checkStateEquation q =
                let incoming = map addTransition $ lpre pp q
                    outgoing = map addTransition $ lpost pp q
                in  val m0 q + sum incoming - sum outgoing .== val m q
35
              addTransition (t,w) = literal w * val x t
36

37
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
38
39
40
nonNegativityConstraints m =
            bAnd $ map checkVal $ vals m
        where checkVal x = x .>= 0
41

42
43
44
45
46
terminalConstraints :: PopulationProtocol -> SIMap State -> SBool
terminalConstraints pp m =
            bAnd $ map checkTransition $ transitions pp
        where checkTransition t = bOr $ map checkState $ lpre pp t
              checkState (q,w) = val m q .<= literal (fromInteger (w - 1))
47

48
49
initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
initialConfiguration pp m0 =
50
51
        (sum (mval m0 (initialStates pp)) .>= 2) &&&
        (sum (mval m0 (states pp \\ initialStates pp)) .== 0)
52

53
54
55
differentConsensusConstraints :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa =
            (oT &&& oF) |||
56
57
            (if checkCorrectness then correctnessConstraints else false)
        where
58
59
            oT = sum (mval m1 (trueStates pp)) .> 0
            oF = sum (mval m2 (falseStates pp)) .> 0
60
            correctnessConstraints =
61
62
63
64
65
66
67
                if null (quantifiedVariables (predicate pp)) then
                    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)
68

69
70
unmarkedByConfiguration :: [State] -> SIMap State -> SBool
unmarkedByConfiguration r m = sum (mval m r) .== 0
Philipp J. Meyer's avatar
Philipp J. Meyer committed
71

72
73
markedByConfiguration :: [State] -> SIMap State -> SBool
markedByConfiguration r m = sum (mval m r) .> 0
Philipp J. Meyer's avatar
Philipp J. Meyer committed
74
75
76
77
78
79
80

sequenceNotIn :: [Transition] -> SIMap Transition -> SBool
sequenceNotIn u x = sum (mval x u) .== 0

sequenceIn :: [Transition] -> SIMap Transition -> SBool
sequenceIn u x = sum (mval x u) .> 0

81
82
checkUTrap :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkUTrap pp m0 m1 m2 x1 x2 utrap =
83
84
            (((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByConfiguration utrap m1)) &&&
            (((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByConfiguration utrap m2))
85
86
        where upost = mpost pp utrap
              upre = mpre pp utrap
87
              uunmark = upost \\ upre
Philipp J. Meyer's avatar
Philipp J. Meyer committed
88

89
90
91
checkUTrapConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkUTrapConstraints pp m0 m1 m2 x1 x2 traps =
        bAnd $ map (checkUTrap pp m0 m1 m2 x1 x2) traps
Philipp J. Meyer's avatar
Philipp J. Meyer committed
92

93
94
checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkUSiphon pp m0 m1 m2 x1 x2 usiphon =
95
96
            (((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByConfiguration usiphon m0)) &&&
            (((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByConfiguration usiphon m0))
97
98
        where upost = mpost pp usiphon
              upre = mpre pp usiphon
99
              umark = upre \\ upost
Philipp J. Meyer's avatar
Philipp J. Meyer committed
100

101
102
103
checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons =
        bAnd $ map (checkUSiphon pp m0 m1 m2 x1 x2) siphons
104

105
checkStrongConsensus :: Bool -> PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
106
107
        SIMap State -> SIMap State ->RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp m0 m1 m2 x1 x2 qe qa (utraps, usiphons) =
108
109
        stateEquationConstraints pp m0 m1 x1 &&&
        stateEquationConstraints pp m0 m2 x2 &&&
110
        initialConfiguration pp m0 &&&
111
112
113
114
115
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
116
117
        terminalConstraints pp m1 &&&
        terminalConstraints pp m2 &&&
118
        differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa &&&
119
        checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
120
        checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
121

122
123
checkStrongConsensusSat :: Bool -> PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat checkCorrectness pp refinements =
124
125
126
127
128
        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
129
130
            qe = makeVarMapWith ("e'"++) $ quantifiedVariables (predicate pp)
            qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
131
        in  ("strong consensus", "(c0, c1, c2, x1, x2)",
132
133
             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,
134
             \fm -> counterExampleFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))
135

136
137
counterExampleFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
counterExampleFromAssignment m0 m1 m2 x1 x2 =
138
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
139

140
141
-- trap and siphon refinement constraints

142
143
144
trapConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
trapConstraint pp b t =
        sum (mval b $ pre pp t) .> 0 ==> sum (mval b $ post pp t) .> 0
Philipp J. Meyer's avatar
Philipp J. Meyer committed
145

146
147
148
siphonConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
siphonConstraint pp b t =
        sum (mval b $ post pp t) .> 0 ==> sum (mval b $ pre pp t) .> 0
149

150
151
152
trapConstraints :: PopulationProtocol -> SIMap State -> SBool
trapConstraints pp b =
        bAnd $ map (trapConstraint pp b) $ transitions pp
Philipp J. Meyer's avatar
Philipp J. Meyer committed
153

154
155
156
157
siphonConstraints :: PopulationProtocol -> SIMap State -> SBool
siphonConstraints pp b =
        bAnd $ map (siphonConstraint pp b) $ transitions pp

158
uTrapConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
159
160
uTrapConstraints pp x b =
        bAnd $ map (trapConstraint pp b) $ elems x
Philipp J. Meyer's avatar
Philipp J. Meyer committed
161

162
uSiphonConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
163
164
uSiphonConstraints pp x b =
        bAnd $ map (siphonConstraint pp b) $ elems x
165

166
167
statesMarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
168

169
170
statesUnmarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesUnmarkedByConfiguration pp m b = sum (mval b $ elems m) .== 0
171

172
statesPostsetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
173
statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
174

175
statesPresetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
176
statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
177

178
noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
179
180
noOutputTransitionEnabled pp m b =
            bAnd $ map outputTransitionNotEnabled $ transitions pp
181
182
        where
            outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
183
184
            outputTransitionOfB t = sum [val b q | (q, w) <- lpre pp t, val m q >= w] .> 0
            transitionNotEnabledInB t = sum [val b q | (q, w) <- lpre pp t, val m q < w] .> 0
185

186
187
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
188

189
checkBinary :: SIMap State -> SBool
190
191
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals

192
checkSizeLimit :: SIMap State -> Maybe (Int, Integer) -> SBool
193
194
195
196
197
198
199
200
201
202
checkSizeLimit _ Nothing = true
checkSizeLimit b (Just (1, curSize)) = (.< literal curSize) $ sumVal b
checkSizeLimit b (Just (2, curSize)) = (.> literal curSize) $ sumVal b
checkSizeLimit _ (Just (_, _)) = error "minimization method not supported"

minimizeMethod :: Int -> Integer -> String
minimizeMethod 1 curSize = "size smaller than " ++ show curSize
minimizeMethod 2 curSize = "size larger than " ++ show curSize
minimizeMethod _ _ = error "minimization method not supported"

203
204
findTrapConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrapConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
205
206
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
207
        trapConstraints pp b &&&
208
        (
209
210
            (statesPostsetOfSequence pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) |||
            (statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
211
        )
212

213
214
findTrapConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat pp c =
215
        let b = makeVarMap $ states pp
Philipp J. Meyer's avatar
Philipp J. Meyer committed
216
        in  (minimizeMethod, \sizeLimit ->
217
            ("trap marked by x1 or x2 and not marked in m1 or m2", "trap",
218
             getNames b, [],  [],
219
             \fm -> findTrapConstraints pp c (fmap fm b) sizeLimit,
220
             \fm -> statesFromAssignment (fmap fm b)))
Philipp J. Meyer's avatar
Philipp J. Meyer committed
221

222
223
findUTrapConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
Philipp J. Meyer's avatar
Philipp J. Meyer committed
224
225
226
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
        (
227
228
            (statesPostsetOfSequence pp x1 b &&& uTrapConstraints pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) |||
            (statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
Philipp J. Meyer's avatar
Philipp J. Meyer committed
229
230
        )

231
232
findUTrapConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat pp c =
233
        let b = makeVarMap $ states pp
234
        in  (minimizeMethod, \sizeLimit ->
235
            ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap",
236
             getNames b, [],  [],
237
             \fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit,
238
             \fm -> statesFromAssignment (fmap fm b)))
239

240
241
242
243
244
245
246
247
248
249
250
251
252
findSiphonConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findSiphonConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
        siphonConstraints pp b &&&
        statesUnmarkedByConfiguration pp m0 b &&&
        (statesPresetOfSequence pp x1 b ||| statesPresetOfSequence pp x2 b)

findSiphonConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
findSiphonConstraintsSat pp c =
        let b = makeVarMap $ states pp
        in  (minimizeMethod, \sizeLimit ->
            ("siphon used by x1 or x2 and unmarked in m0", "siphon",
253
             getNames b, [],  [],
254
255
256
257
             \fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit,
             \fm -> statesFromAssignment (fmap fm b)))


258
259
findUSiphonConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
260
261
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
262
        statesUnmarkedByConfiguration pp m0 b &&&
263
        (
264
265
            (statesPresetOfSequence pp x1 b &&& uSiphonConstraints pp x1 b) |||
            (statesPresetOfSequence pp x2 b &&& uSiphonConstraints pp x2 b)
266
        )
267

268
269
findUSiphonConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat pp c =
270
        let b = makeVarMap $ states pp
271
        in  (minimizeMethod, \sizeLimit ->
272
            ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon",
273
             getNames b, [],  [],
274
             \fm -> findUSiphonConstraints pp c (fmap fm b) sizeLimit,
275
             \fm -> statesFromAssignment (fmap fm b)))
276

277
278
statesFromAssignment :: IMap State -> ([State], Integer)
statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307

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

308
checkStrongConsensusComplete :: Bool -> PopulationProtocol -> Integer -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
309
310
        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 =
311
312
313
314
315
316
317
318
319
320
        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 &&&
321
        differentConsensusConstraints checkCorrectness pp m0 m1 m2 qe qa &&&
322
323
324
325
326
327
328
329
330
331
332
333
334
        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

335
336
checkStrongConsensusCompleteSat :: Bool -> PopulationProtocol -> ConstraintProblem Integer StrongConsensusCompleteCounterExample
checkStrongConsensusCompleteSat checkCorrectness pp =
337
338
339
340
341
342
343
344
345
346
        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
347
348
            qe = makeVarMapWith ("e'"++) $ quantifiedVariables (predicate pp)
            qa = makeVarMapWith ("a'"++) $ quantifiedVariables (predicate pp)
349
        in  ("strong consensus", "(m0, m1, m2, x1, x2, r1, r2, s1, s2)",
350
351
352
             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)
                        (fmap fm r1) (fmap fm r2) (fmap fm s1) (fmap fm s2) (fmap fm qe) (fmap fm qa),
353
354
355
356
357
358
359
             \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