TerminalMarkingsUniqueConsensus.hs 14.4 KB
Newer Older
1
2
{-# LANGUAGE FlexibleContexts #-}

3
4
5
module Solver.TerminalMarkingsUniqueConsensus
    (checkTerminalMarkingsUniqueConsensusSat,
     TerminalMarkingsUniqueConsensusCounterExample,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
6
7
8
     findTrapConstraintsSat,
     findUTrapConstraintsSat,
     findUSiphonConstraintsSat,
9
10
     checkGeneralizedCoTrapSat,
     StableInequality)
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 TerminalMarkingsUniqueConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector)
23

24
type StableInequality = (IMap State, Integer)
25

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

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

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

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

50
51
52
differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints pp m1 m2 =
        (sum (mval m1 (yesStates pp)) .> 0 &&& sum (mval m2 (noStates pp)) .> 0)
53

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

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

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

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

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

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

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

90
91
checkInequalityConstraint :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> StableInequality -> SBool
checkInequalityConstraint pp m0 m1 m2 (k, c) =
92
            (checkInequality m0) ==> (checkInequality m1 &&& checkInequality m2)
93
        where checkInequality m = sum [ literal (val k q) * (val m q) | q <- states pp ] .>= literal c
94

95
96
97
checkInequalityConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> [StableInequality] -> SBool
checkInequalityConstraints pp m0 m1 m2 inequalities =
        bAnd [ checkInequalityConstraint pp m0 m1 m2 i | i <- inequalities ]
98

99
checkTerminalMarkingsUniqueConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
100
        [Trap] -> [Siphon] -> [StableInequality] -> SBool
101
102
103
104
checkTerminalMarkingsUniqueConsensus pp m0 m1 m2 x1 x2 utraps usiphons inequalities =
        stateEquationConstraints pp m0 m1 x1 &&&
        stateEquationConstraints pp m0 m2 x2 &&&
        initialMarkingConstraints pp m0 &&&
105
106
107
108
109
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
110
111
112
113
114
115
116
117
118
119
120
121
122
123
        terminalConstraints pp m1 &&&
        terminalConstraints pp m2 &&&
        differentConsensusConstraints pp m1 m2 &&&
        checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
        checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons &&&
        checkInequalityConstraints pp m0 m1 m2 inequalities

checkTerminalMarkingsUniqueConsensusSat :: PopulationProtocol -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
checkTerminalMarkingsUniqueConsensusSat pp utraps usiphons inequalities =
        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
124
125
        in  ("unique terminal marking", "(m0, m1, m2, x1, x2)",
             getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
126
             \fm -> checkTerminalMarkingsUniqueConsensus pp (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) utraps usiphons inequalities,
127
128
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

129
markingsFromAssignment :: IMap State -> IMap State -> IMap State -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample
130
131
markingsFromAssignment m0 m1 m2 x1 x2 =
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
132

133
134
-- trap and siphon refinement constraints

135
136
137
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
138

139
140
141
siphonConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
siphonConstraint pp b t =
        sum (mval b $ post pp t) .> 0 ==> sum (mval b $ pre pp t) .> 0
142

143
144
145
trapConstraints :: PopulationProtocol -> SIMap State -> SBool
trapConstraints pp b =
        bAnd $ map (trapConstraint pp b) $ transitions pp
Philipp J. Meyer's avatar
Philipp J. Meyer committed
146

147
148
149
uTrapConstraints :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
uTrapConstraints pp x b =
        bAnd $ map (trapConstraint pp b) $ elems x
Philipp J. Meyer's avatar
Philipp J. Meyer committed
150

151
152
153
uSiphonConstraints :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
uSiphonConstraints pp x b =
        bAnd $ map (siphonConstraint pp b) $ elems x
154

155
156
statesMarkedByMarking :: PopulationProtocol -> Marking -> SIMap State -> SBool
statesMarkedByMarking pp m b = sum (mval b $ elems m) .> 0
157

158
159
statesUnmarkedByMarking :: PopulationProtocol -> Marking -> SIMap State -> SBool
statesUnmarkedByMarking pp m b = sum (mval b $ elems m) .== 0
160

161
162
statesPostsetOfSequence :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
statesPostsetOfSequence pp x b = sum (mval b $ mpost pp $ elems x) .> 0
163

164
165
statesPresetOfSequence :: PopulationProtocol -> FiringVector -> SIMap State -> SBool
statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
166

167
168
169
noOutputTransitionEnabled :: PopulationProtocol -> Marking -> SIMap State -> SBool
noOutputTransitionEnabled pp m b =
            bAnd $ map outputTransitionNotEnabled $ transitions pp
170
171
        where
            outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
172
173
            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
174

175
176
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
177

178
checkBinary :: SIMap State -> SBool
179
180
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals

181
checkSizeLimit :: SIMap State -> Maybe (Int, Integer) -> SBool
182
183
184
185
186
187
188
189
190
191
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"

192
193
findTrap :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrap pp m0 m1 m2 x1 x2 b sizeLimit =
194
195
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
196
        trapConstraints pp b &&&
197
        (
198
199
            (statesPostsetOfSequence pp x1 b &&& statesUnmarkedByMarking pp m1 b) |||
            (statesPostsetOfSequence pp x2 b &&& statesUnmarkedByMarking pp m2 b)
200
        )
201

202
203
204
findTrapConstraintsSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat pp m0 m1 m2 x1 x2 =
        let b = makeVarMap $ states pp
Philipp J. Meyer's avatar
Philipp J. Meyer committed
205
        in  (minimizeMethod, \sizeLimit ->
206
            ("trap marked by x1 or x2 and not marked in m1 or m2", "trap",
Philipp J. Meyer's avatar
Philipp J. Meyer committed
207
             getNames b,
208
209
             \fm -> findTrap pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
             \fm -> statesFromAssignment (fmap fm b)))
Philipp J. Meyer's avatar
Philipp J. Meyer committed
210

211
212
findUTrapConstraints :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
Philipp J. Meyer's avatar
Philipp J. Meyer committed
213
214
215
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
        (
216
217
            (statesPostsetOfSequence pp x1 b &&& uTrapConstraints pp x1 b &&& statesUnmarkedByMarking pp m1 b) |||
            (statesPostsetOfSequence pp x2 b &&& uTrapConstraints pp x2 b &&& statesUnmarkedByMarking pp m2 b)
Philipp J. Meyer's avatar
Philipp J. Meyer committed
218
219
        )

220
221
222
findUTrapConstraintsSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat pp m0 m1 m2 x1 x2 =
        let b = makeVarMap $ states pp
223
        in  (minimizeMethod, \sizeLimit ->
224
            ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap",
225
             getNames b,
226
227
             \fm -> findUTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
             \fm -> statesFromAssignment (fmap fm b)))
228

229
230
findUSiphonConstraints :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints pp m0 m1 m2 x1 x2 b sizeLimit =
231
232
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
233
        statesUnmarkedByMarking pp m0 b &&&
234
        (
235
236
            (statesPresetOfSequence pp x1 b &&& uSiphonConstraints pp x1 b) |||
            (statesPresetOfSequence pp x2 b &&& uSiphonConstraints pp x2 b)
237
        )
238

239
240
241
findUSiphonConstraintsSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat pp m0 m1 m2 x1 x2 =
        let b = makeVarMap $ states pp
242
        in  (minimizeMethod, \sizeLimit ->
243
            ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon",
244
             getNames b,
245
246
             \fm -> findUSiphonConstraints pp m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
             \fm -> statesFromAssignment (fmap fm b)))
247

248
249
statesFromAssignment :: IMap State -> ([State], Integer)
statesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
250
251
252

-- stable linear inequalities

253
254
255
checkStableInequalityForMarking :: PopulationProtocol -> Marking -> SIMap State -> SInteger -> SBool
checkStableInequalityForMarking pp m k c =
        sum [ (val k q) * literal (val m q) | q <- states pp ] .>= c
256
257
258
259
260
261
262
263
264

checkSemiPositiveConstraints :: (Ord a, Show a) => SIMap a -> SBool
checkSemiPositiveConstraints k =
            bAnd [ x .>= 0 | x <- vals k ]

checkSemiNegativeConstraints :: (Ord a, Show a) => SIMap a -> SBool
checkSemiNegativeConstraints k =
            bAnd [ x .<= 0 | x <- vals k ]

265
266
checkGeneralizedTCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> Transition -> SBool
checkGeneralizedTCoTrap pp k c t =
267
268
269
            checkTSurInvariant ||| checkTDisabled
        where checkTSurInvariant = sum output - sum input .>= c
              checkTDisabled = sum input .< c
270
271
272
              input = map addState $ lpre pp t
              output = map addState $ lpost pp t
              addState (q, w) = literal w * val k q
273

274
275
276
checkGeneralizedCoTrap :: PopulationProtocol -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrap pp k c =
        bAnd [ checkGeneralizedTCoTrap pp k c t | t <- transitions pp ]
277

278
279
checkGeneralizedCoTrapConstraints :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap State -> SInteger -> SBool
checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 k c =
280
        checkSemiNegativeConstraints k &&&
281
282
283
        checkGeneralizedCoTrap pp k c &&&
        checkStableInequalityForMarking pp m0 k c &&&
        ((bnot (checkStableInequalityForMarking pp m1 k c)) ||| (bnot (checkStableInequalityForMarking pp m2 k c)))
284

285
286
287
checkGeneralizedCoTrapSat :: PopulationProtocol -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Integer StableInequality
checkGeneralizedCoTrapSat pp m0 m1 m2 x1 x2 =
        let k = makeVarMap $ states pp
288
289
290
            c = "'c"
        in  ("generalized co-trap (stable inequality) holding m but not in m1 or m2", "stable inequality",
             c : getNames k,
291
             \fm -> checkGeneralizedCoTrapConstraints pp m0 m1 m2 x1 x2 (fmap fm k) (fm c),
292
293
             \fm -> stableInequalityFromAssignment (fmap fm k) (fm c))

294
stableInequalityFromAssignment :: IMap State -> Integer -> StableInequality
295
296
stableInequalityFromAssignment k c = (k, c)