TerminalMarkingsUniqueConsensus.hs 14.5 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
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
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 =
            ((unmarkedByMarking utrap m0) ||| (
                ((sequenceIn u x1) ||| (markedByMarking utrap m1)) &&&
                ((sequenceIn u x2) ||| (markedByMarking utrap m2))
            ))
        where u = (mpost net utrap \\ mpre net utrap)

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 =
            ((markedByMarking usiphon m0) ||| (
                ((sequenceIn u x1) ||| (unmarkedByMarking usiphon m1)) &&&
                ((sequenceIn u x2) ||| (unmarkedByMarking usiphon m2))
            ))
        where u = (mpre net usiphon \\ mpost net usiphon)

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 ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
110
111
        [Trap] -> [Trap] -> [Siphon] -> [StableInequality] -> SBool
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps 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
125
        checkTrapConstraints net m0 m1 m2 traps &&&
        checkUTrapConstraints net m0 m1 m2 x1 x2 utraps &&&
        checkUSiphonConstraints net m0 m1 m2 x1 x2 usiphons &&&
126
        checkInequalityConstraints net m0 m1 m2 inequalities
127

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

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

144
145
-- trap and siphon refinement constraints

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

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

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

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

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

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

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

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

189
190
191
192
193
194
195
196
197
198
199
200
201
202
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
203
204
findTrap :: PetriNet -> Marking -> Marking -> Marking -> SIMap Place -> Maybe (Int, Integer) -> SBool
findTrap net m0 m1 m2 b sizeLimit =
205
        placesMarkedByMarking net m0 b &&&
206
207
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
208
209
        trapConstraints net b &&&
        ((placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b))
210

Philipp J. Meyer's avatar
Philipp J. Meyer committed
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
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 =
        placesMarkedByMarking net m0 b &&&
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
        (
            (uTrapConstraints net x1 b &&& placesUnmarkedByMarking net m1 b) |||
            (uTrapConstraints net x2 b &&& placesUnmarkedByMarking net m2 b)
        )

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 ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
234
            ("u-trap (w.r.t. x1 or x2) marked in m0 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
        placesUnmarkedByMarking net m0 b &&&
242
243
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
244
        (
Philipp J. Meyer's avatar
Philipp J. Meyer committed
245
246
            (uSiphonConstraints net x1 b &&& placesMarkedByMarking net m1 b) |||
            (uSiphonConstraints net x2 b &&& placesMarkedByMarking net m2 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 ->
Philipp J. Meyer's avatar
Philipp J. Meyer committed
253
            ("u-siphon (w.r.t. x1 or x2) not marked in m0 and marked in m1 or m2", "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)