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

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

import Data.SBV
14
import qualified Data.Map as M
15
import Data.List ((\\))
16
17

import Util
18
import PopulationProtocol
19
20
21
import Property
import Solver

22
type StrongConsensusCounterExample = (Configuration, Configuration, Configuration, FlowVector, FlowVector)
23
type RefinementObjects = ([Trap], [Siphon])
24

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

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

39
40
41
42
43
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))
44

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

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

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

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

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

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

73
74
75
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
76

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

85
86
87
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
88

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

106
107
checkStrongConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer StrongConsensusCounterExample
checkStrongConsensusSat pp refinements =
108
109
110
111
112
        let m0 = makeVarMap $ states pp
            m1 = makeVarMapWith prime $ states pp
            m2 = makeVarMapWith (prime . prime) $ states pp
            x1 = makeVarMap $ transitions pp
            x2 = makeVarMapWith prime $ transitions pp
113
        in  ("strong consensus", "(c0, c1, c2, x1, x2)",
114
             getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
115
116
             \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))
117

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

122
123
-- trap and siphon refinement constraints

124
125
126
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
127

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
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)))


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

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

259
260
statesFromAssignment :: IMap State -> ([State], Integer)
statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))