StrongConsensus.hs 17 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
22
import Property
import Solver

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

27
28
29
30
31
32
33
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
34
              addTransition (t,w) = literal w * val x t
35

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

41
42
43
44
45
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))
46

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

51
52
differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints pp m1 m2 =
53
        (sum (mval m1 (trueStates pp)) .> 0 &&& sum (mval m2 (falseStates pp)) .> 0)
54

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

58
59
markedByConfiguration :: [State] -> SIMap State -> SBool
markedByConfiguration r m = sum (mval m r) .> 0
Philipp J. Meyer's avatar
Philipp J. Meyer committed
60
61
62
63
64
65
66

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

67
68
checkUTrap :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkUTrap pp m0 m1 m2 x1 x2 utrap =
69
70
            (((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByConfiguration utrap m1)) &&&
            (((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByConfiguration utrap m2))
71
72
        where upost = mpost pp utrap
              upre = mpre pp utrap
73
              uunmark = upost \\ upre
Philipp J. Meyer's avatar
Philipp J. Meyer committed
74

75
76
77
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
78

79
80
checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkUSiphon pp m0 m1 m2 x1 x2 usiphon =
81
82
            (((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByConfiguration usiphon m0)) &&&
            (((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByConfiguration usiphon m0))
83
84
        where upost = mpost pp usiphon
              upre = mpre pp usiphon
85
              umark = upre \\ upost
Philipp J. Meyer's avatar
Philipp J. Meyer committed
86

87
88
89
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
90

Philipp Meyer's avatar
Philipp Meyer committed
91
checkStrongConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
92
93
        RefinementObjects -> SBool
checkStrongConsensus pp m0 m1 m2 x1 x2 (utraps, usiphons) =
94
95
        stateEquationConstraints pp m0 m1 x1 &&&
        stateEquationConstraints pp m0 m2 x2 &&&
96
        initialConfiguration pp m0 &&&
97
98
99
100
101
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
102
103
104
105
        terminalConstraints pp m1 &&&
        terminalConstraints pp m2 &&&
        differentConsensusConstraints pp m1 m2 &&&
        checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
106
        checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
107

108
109
checkStrongConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat pp refinements =
110
111
112
113
114
        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
115
        in  ("strong consensus", "(c0, c1, c2, x1, x2)",
116
             getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
117
118
             \fm -> checkStrongConsensus 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))
119

120
121
counterExampleFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> StrongConsensusCounterExample
counterExampleFromAssignment m0 m1 m2 x1 x2 =
122
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
123

124
125
-- trap and siphon refinement constraints

126
127
128
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
129

130
131
132
siphonConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
siphonConstraint pp b t =
        sum (mval b $ post pp t) .> 0 ==> sum (mval b $ pre pp t) .> 0
133

134
135
136
trapConstraints :: PopulationProtocol -> SIMap State -> SBool
trapConstraints pp b =
        bAnd $ map (trapConstraint pp b) $ transitions pp
Philipp J. Meyer's avatar
Philipp J. Meyer committed
137

138
139
140
141
siphonConstraints :: PopulationProtocol -> SIMap State -> SBool
siphonConstraints pp b =
        bAnd $ map (siphonConstraint pp b) $ transitions pp

142
uTrapConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
143
144
uTrapConstraints pp x b =
        bAnd $ map (trapConstraint pp b) $ elems x
Philipp J. Meyer's avatar
Philipp J. Meyer committed
145

146
uSiphonConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
147
148
uSiphonConstraints pp x b =
        bAnd $ map (siphonConstraint pp b) $ elems x
149

150
151
statesMarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
152

153
154
statesUnmarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesUnmarkedByConfiguration pp m b = sum (mval b $ elems m) .== 0
155

156
statesPostsetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
157
statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
158

159
statesPresetOfSequence :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
160
statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
161

162
noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
163
164
noOutputTransitionEnabled pp m b =
            bAnd $ map outputTransitionNotEnabled $ transitions pp
165
166
        where
            outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
167
168
            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
169

170
171
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
172

173
checkBinary :: SIMap State -> SBool
174
175
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals

176
checkSizeLimit :: SIMap State -> Maybe (Int, Integer) -> SBool
177
178
179
180
181
182
183
184
185
186
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"

187
188
findTrapConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrapConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
189
190
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
191
        trapConstraints pp b &&&
192
        (
193
194
            (statesPostsetOfSequence pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) |||
            (statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
195
        )
196

197
198
findTrapConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat pp c =
199
        let b = makeVarMap $ states pp
Philipp J. Meyer's avatar
Philipp J. Meyer committed
200
        in  (minimizeMethod, \sizeLimit ->
201
            ("trap marked by x1 or x2 and not marked in m1 or m2", "trap",
Philipp J. Meyer's avatar
Philipp J. Meyer committed
202
             getNames b,
203
             \fm -> findTrapConstraints pp c (fmap fm b) sizeLimit,
204
             \fm -> statesFromAssignment (fmap fm b)))
Philipp J. Meyer's avatar
Philipp J. Meyer committed
205

206
207
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
208
209
210
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
        (
211
212
            (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
213
214
        )

215
216
findUTrapConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat pp c =
217
        let b = makeVarMap $ states pp
218
        in  (minimizeMethod, \sizeLimit ->
219
            ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap",
220
             getNames b,
221
             \fm -> findUTrapConstraints pp c (fmap fm b) sizeLimit,
222
             \fm -> statesFromAssignment (fmap fm b)))
223

224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
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",
             getNames b,
             \fm -> findSiphonConstraints pp c (fmap fm b) sizeLimit,
             \fm -> statesFromAssignment (fmap fm b)))


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

252
253
findUSiphonConstraintsSat :: PopulationProtocol -> StrongConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat pp c =
254
        let b = makeVarMap $ states pp
255
        in  (minimizeMethod, \sizeLimit ->
256
            ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon",
257
             getNames b,
258
             \fm -> findUSiphonConstraints pp c (fmap fm b) sizeLimit,
259
             \fm -> statesFromAssignment (fmap fm b)))
260

261
262
statesFromAssignment :: IMap State -> ([State], Integer)
statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
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
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340

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