TerminalMarkingsUniqueConsensus.hs 14.8 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
18
19
20
21

import Util
import PetriNet
import Property
import Solver

22
type TerminalMarkingsUniqueConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector)
23

24
25
type StableInequality = (IMap Place, Integer)

26
stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
27
stateEquationConstraints net m0 m x =
28
29
            bAnd $ map checkStateEquation $ places net
        where checkStateEquation p =
30
31
                let incoming = map addTransition $ lpre net p
                    outgoing = map addTransition $ lpost net p
32
                in  val m0 p + sum incoming - sum outgoing .== val m p
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
terminalConstraints :: PetriNet -> SIMap Place -> SBool
41
42
terminalConstraints net m =
            bAnd $ map checkTransition $ transitions net
43
        where checkTransition t = bOr $ map checkPlace $ lpre net t
44
              checkPlace (p,w) = val m p .<= literal (fromInteger (w - 1))
45

46
47
48
49
50
51
initialMarkingConstraints :: PetriNet -> SIMap Place -> SBool
initialMarkingConstraints net m0 =
        sum (mval m0 (places net \\ initials net)) .== 0

differentConsensusConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
differentConsensusConstraints net m1 m2 =
52
        (sum (mval m1 (yesStates net)) .> 0 &&& sum (mval m2 (noStates net)) .> 0)
53

Philipp J. Meyer's avatar
Philipp J. Meyer committed
54
55
56
57
58
59
60
61
62
63
64
65
66
67
unmarkedByMarking :: [Place] -> SIMap Place -> SBool
unmarkedByMarking r m = sum (mval m r) .== 0

markedByMarking :: [Place] -> SIMap Place -> SBool
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

checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> Trap -> SBool
checkTrap net m0 m1 m2 trap =
68
            (markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2))
69
70
        where markedByMarking m = sum (mval m trap) .> 0
              markedBySequence x = sum (mval x (mpre net trap)) .> 0
71

Philipp J. Meyer's avatar
Philipp J. Meyer committed
72
73
74
75
76
77
checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> [Trap] -> SBool
checkTrapConstraints net m0 m1 m2 traps =
        bAnd $ map (checkTrap net m0 m1 m2) traps

checkUTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkUTrap net m0 m1 m2 x1 x2 utrap =
78
79
80
81
82
83
84
85
            (
                ((sequenceNotIn upre x1) ||| (sequenceIn uunmark x1) ||| (markedByMarking utrap m1))
            &&&
                ((sequenceNotIn upre x2) ||| (sequenceIn uunmark x2) ||| (markedByMarking utrap m2))
            )
        where upost = mpost net utrap
              upre = mpre net utrap
              uunmark = upost \\ upre
Philipp J. Meyer's avatar
Philipp J. Meyer committed
86
87
88
89
90
91
92

checkUTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkUTrapConstraints net m0 m1 m2 x1 x2 traps =
        bAnd $ map (checkUTrap net m0 m1 m2 x1 x2) traps

checkUSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkUSiphon net m0 m1 m2 x1 x2 usiphon =
93
94
95
96
97
98
99
100
101
102
103
104
            (
                markedByMarking usiphon m0
            |||
                (
                    ((sequenceNotIn upost x1) ||| (sequenceIn umark x1))
                &&&
                    ((sequenceNotIn upost x2) ||| (sequenceIn umark x2))
                )
            )
        where upost = mpost net usiphon
              upre = mpre net usiphon
              umark = upre \\ upost
Philipp J. Meyer's avatar
Philipp J. Meyer committed
105
106
107
108

checkUSiphonConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
checkUSiphonConstraints net m0 m1 m2 x1 x2 siphons =
        bAnd $ map (checkUSiphon net m0 m1 m2 x1 x2) siphons
109

110
111
112
113
114
115
116
117
118
checkInequalityConstraint :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> StableInequality -> SBool
checkInequalityConstraint net m0 m1 m2 (k, c) =
            (checkInequality m0) ==> (checkInequality m1 &&& checkInequality m2)
        where checkInequality m = sum [ literal (val k p) * (val m p) | p <- places net ] .>= literal c

checkInequalityConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> [StableInequality] -> SBool
checkInequalityConstraints net m0 m1 m2 inequalities =
        bAnd [ checkInequalityConstraint net m0 m1 m2 i | i <- inequalities ]

119
checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
120
121
        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> SBool
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps utraps usiphons inequalities =
122
123
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
124
        initialMarkingConstraints net m0 &&&
125
126
127
128
129
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
130
        terminalConstraints net m1 &&&
131
        terminalConstraints net m2 &&&
132
        differentConsensusConstraints net m1 m2 &&&
Philipp J. Meyer's avatar
Philipp J. Meyer committed
133
134
135
        checkTrapConstraints net m0 m1 m2 traps &&&
        checkUTrapConstraints net m0 m1 m2 x1 x2 utraps &&&
        checkUSiphonConstraints net m0 m1 m2 x1 x2 usiphons &&&
136
        checkInequalityConstraints net m0 m1 m2 inequalities
137

Philipp J. Meyer's avatar
Philipp J. Meyer committed
138
139
checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
checkTerminalMarkingsUniqueConsensusSat net traps utraps usiphons inequalities =
140
141
142
143
144
145
146
        let m0 = makeVarMap $ places net
            m1 = makeVarMapWith prime $ places net
            m2 = makeVarMapWith (prime . prime) $ places net
            x1 = makeVarMap $ transitions net
            x2 = makeVarMapWith prime $ transitions net
        in  ("unique terminal marking", "(m0, m1, m2, x1, x2)",
             getNames m0 ++ getNames m1 ++ getNames m2 ++ getNames x1 ++ getNames x2,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
147
             \fm -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps utraps usiphons inequalities,
148
149
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

150
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample
151
152
markingsFromAssignment m0 m1 m2 x1 x2 =
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
153

154
155
-- trap and siphon refinement constraints

Philipp J. Meyer's avatar
Philipp J. Meyer committed
156
157
158
159
160
161
162
trapConstraint :: PetriNet -> SIMap Place -> Transition -> SBool
trapConstraint net b t =
        sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0

siphonConstraint :: PetriNet -> SIMap Place -> Transition -> SBool
siphonConstraint net b t =
        sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
163

164
trapConstraints :: PetriNet -> SIMap Place -> SBool
165
trapConstraints net b =
Philipp J. Meyer's avatar
Philipp J. Meyer committed
166
167
168
169
170
171
172
173
174
        bAnd $ map (trapConstraint net b) $ transitions net

uTrapConstraints :: PetriNet -> FiringVector -> SIMap Place -> SBool
uTrapConstraints net x b =
        bAnd $ map (trapConstraint net b) $ elems x

uSiphonConstraints :: PetriNet -> FiringVector -> SIMap Place -> SBool
uSiphonConstraints net x b =
        bAnd $ map (siphonConstraint net b) $ elems x
175

176
placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
177
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
178

179
placesUnmarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
180
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0
181

182
placesPostsetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
183
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
184

185
placesPresetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
186
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
187

188
189
190
191
192
193
194
195
noOutputTransitionEnabled :: PetriNet -> Marking -> SIMap Place -> SBool
noOutputTransitionEnabled net m b =
            bAnd $ map outputTransitionNotEnabled $ transitions net
        where
            outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
            outputTransitionOfB t = sum [val b p | (p, w) <- lpre net t, val m p >= w] .> 0
            transitionNotEnabledInB t = sum [val b p | (p, w) <- lpre net t, val m p < w] .> 0

196
197
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
198

199
200
201
202
203
204
205
206
207
208
209
210
211
212
checkBinary :: SIMap Place -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals

checkSizeLimit :: SIMap Place -> Maybe (Int, Integer) -> SBool
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"

Philipp J. Meyer's avatar
Philipp J. Meyer committed
213
214
findTrap :: PetriNet -> Marking -> Marking -> Marking -> SIMap Place -> Maybe (Int, Integer) -> SBool
findTrap net m0 m1 m2 b sizeLimit =
215
        placesMarkedByMarking net m0 b &&&
216
217
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
218
219
        trapConstraints net b &&&
        ((placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b))
220

Philipp J. Meyer's avatar
Philipp J. Meyer committed
221
222
223
224
225
226
227
228
229
230
231
232
233
234
findTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat net m0 m1 m2 =
        let b = makeVarMap $ places net
        in  (minimizeMethod, \sizeLimit ->
            ("trap marked in m0 and unmarked in m1 or m2", "trap",
             getNames b,
             \fm -> findTrap net m0 m1 m2 (fmap fm b) sizeLimit,
             \fm -> placesFromAssignment (fmap fm b)))

findUTrapConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findUTrapConstraints net m0 m1 m2 x1 x2 b sizeLimit =
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
        (
235
236
            (placesPostsetOfSequence net x1 b &&& uTrapConstraints net x1 b &&& placesUnmarkedByMarking net m1 b) |||
            (placesPostsetOfSequence net x2 b &&& uTrapConstraints net x2 b &&& placesUnmarkedByMarking net m2 b)
Philipp J. Meyer's avatar
Philipp J. Meyer committed
237
238
239
240
        )

findUTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat net m0 m1 m2 x1 x2 =
241
        let b = makeVarMap $ places net
242
        in  (minimizeMethod, \sizeLimit ->
243
            ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap",
244
             getNames b,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
245
             \fm -> findUTrapConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
246
             \fm -> placesFromAssignment (fmap fm b)))
247

Philipp J. Meyer's avatar
Philipp J. Meyer committed
248
249
findUSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
250
251
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
252
        placesUnmarkedByMarking net m0 b &&&
253
        (
254
255
            (placesPresetOfSequence net x1 b &&& uSiphonConstraints net x1 b) |||
            (placesPresetOfSequence net x2 b &&& uSiphonConstraints net x2 b)
256
        )
257

Philipp J. Meyer's avatar
Philipp J. Meyer committed
258
259
findUSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat net m0 m1 m2 x1 x2 =
260
        let b = makeVarMap $ places net
261
        in  (minimizeMethod, \sizeLimit ->
262
            ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon",
263
             getNames b,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
264
             \fm -> findUSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
265
             \fm -> placesFromAssignment (fmap fm b)))
266

267
268
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
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

-- stable linear inequalities

checkStableInequalityForMarking :: PetriNet -> Marking -> SIMap Place -> SInteger -> SBool
checkStableInequalityForMarking net m k c =
        sum [ (val k p) * literal (val m p) | p <- places net ] .>= c

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 ]

checkGeneralizedTCoTrap :: PetriNet -> SIMap Place -> SInteger -> Transition -> SBool
checkGeneralizedTCoTrap net k c t =
            checkTSurInvariant ||| checkTDisabled
        where checkTSurInvariant = sum output - sum input .>= c
              checkTDisabled = sum input .< c
              input = map addPlace $ lpre net t
              output = map addPlace $ lpost net t
              addPlace (p, w) = literal w * val k p

checkGeneralizedCoTrap :: PetriNet -> SIMap Place -> SInteger -> SBool
checkGeneralizedCoTrap net k c =
        bAnd [ checkGeneralizedTCoTrap net k c t | t <- transitions net ]

checkGeneralizedCoTrapConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> SInteger -> SBool
checkGeneralizedCoTrapConstraints net m0 m1 m2 x1 x2 k c =
        checkSemiNegativeConstraints k &&&
        checkGeneralizedCoTrap net k c &&&
        checkStableInequalityForMarking net m0 k c &&&
        ((bnot (checkStableInequalityForMarking net m1 k c)) ||| (bnot (checkStableInequalityForMarking net m2 k c)))

checkGeneralizedCoTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> ConstraintProblem Integer StableInequality
checkGeneralizedCoTrapSat net m0 m1 m2 x1 x2 =
        let k = makeVarMap $ places net
            c = "'c"
        in  ("generalized co-trap (stable inequality) holding m but not in m1 or m2", "stable inequality",
             c : getNames k,
             \fm -> checkGeneralizedCoTrapConstraints net m0 m1 m2 x1 x2 (fmap fm k) (fm c),
             \fm -> stableInequalityFromAssignment (fmap fm k) (fm c))

stableInequalityFromAssignment :: IMap Place -> Integer -> StableInequality
stableInequalityFromAssignment k c = (k, c)