TerminalMarkingsUniqueConsensus.hs 14.3 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

checkUTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkUTrap net m0 m1 m2 x1 x2 utrap =
68
69
70
71
72
73
74
75
            (
                ((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
76
77
78
79
80
81
82

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 =
83
84
85
86
87
88
89
90
91
92
93
94
            (
                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
95
96
97
98

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
99

100
101
102
103
104
105
106
107
108
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 ]

109
checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
110
111
        [Trap] -> [Siphon] -> [StableInequality] -> SBool
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 utraps usiphons inequalities =
112
113
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
114
        initialMarkingConstraints net m0 &&&
115
116
117
118
119
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
120
        terminalConstraints net m1 &&&
121
        terminalConstraints net m2 &&&
122
        differentConsensusConstraints net m1 m2 &&&
Philipp J. Meyer's avatar
Philipp J. Meyer committed
123
124
        checkUTrapConstraints net m0 m1 m2 x1 x2 utraps &&&
        checkUSiphonConstraints net m0 m1 m2 x1 x2 usiphons &&&
125
        checkInequalityConstraints net m0 m1 m2 inequalities
126

127
128
checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
checkTerminalMarkingsUniqueConsensusSat net utraps usiphons inequalities =
129
130
131
132
133
134
135
        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,
136
             \fm -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) utraps usiphons inequalities,
137
138
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

139
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample
140
141
markingsFromAssignment m0 m1 m2 x1 x2 =
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
142

143
144
-- trap and siphon refinement constraints

Philipp J. Meyer's avatar
Philipp J. Meyer committed
145
146
147
148
149
150
151
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
152

153
trapConstraints :: PetriNet -> SIMap Place -> SBool
154
trapConstraints net b =
Philipp J. Meyer's avatar
Philipp J. Meyer committed
155
156
157
158
159
160
161
162
163
        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
164

165
placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
166
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
167

168
placesUnmarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
169
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0
170

171
placesPostsetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
172
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
173

174
placesPresetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
175
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
176

177
178
179
180
181
182
183
184
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

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

188
189
190
191
192
193
194
195
196
197
198
199
200
201
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"

202
203
findTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findTrap net m0 m1 m2 x1 x2 b sizeLimit =
204
205
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
206
        trapConstraints net b &&&
207
208
209
210
        (
            (placesPostsetOfSequence net x1 b &&& placesUnmarkedByMarking net m1 b) |||
            (placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b)
        )
211

212
213
findTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findTrapConstraintsSat net m0 m1 m2 x1 x2 =
Philipp J. Meyer's avatar
Philipp J. Meyer committed
214
215
        let b = makeVarMap $ places net
        in  (minimizeMethod, \sizeLimit ->
216
            ("trap marked by x1 or x2 and not marked in m1 or m2", "trap",
Philipp J. Meyer's avatar
Philipp J. Meyer committed
217
             getNames b,
218
             \fm -> findTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
219
220
221
222
223
224
225
             \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 &&&
        (
226
227
            (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
228
229
230
231
        )

findUTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat net m0 m1 m2 x1 x2 =
232
        let b = makeVarMap $ places net
233
        in  (minimizeMethod, \sizeLimit ->
234
            ("u-trap (w.r.t. x1 or x2) marked by x1 or x2 and not marked in m1 or m2", "u-trap",
235
             getNames b,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
236
             \fm -> findUTrapConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
237
             \fm -> placesFromAssignment (fmap fm b)))
238

Philipp J. Meyer's avatar
Philipp J. Meyer committed
239
240
findUSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
241
242
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
243
        placesUnmarkedByMarking net m0 b &&&
244
        (
245
246
            (placesPresetOfSequence net x1 b &&& uSiphonConstraints net x1 b) |||
            (placesPresetOfSequence net x2 b &&& uSiphonConstraints net x2 b)
247
        )
248

Philipp J. Meyer's avatar
Philipp J. Meyer committed
249
250
findUSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat net m0 m1 m2 x1 x2 =
251
        let b = makeVarMap $ places net
252
        in  (minimizeMethod, \sizeLimit ->
253
            ("u-siphon (w.r.t. x1 or x2) used by x1 or x2 and unmarked in m0", "u-siphon",
254
             getNames b,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
255
             \fm -> findUSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
256
             \fm -> placesFromAssignment (fmap fm b)))
257

258
259
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
260
261
262
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

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