TerminalMarkingsUniqueConsensus.hs 14.2 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
            (((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByMarking utrap m1)) &&&
            (((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByMarking utrap m2))
70
71
72
        where upost = mpost net utrap
              upre = mpre net utrap
              uunmark = upost \\ upre
Philipp J. Meyer's avatar
Philipp J. Meyer committed
73
74
75
76
77
78
79

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 =
80
81
            (((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByMarking usiphon m0)) &&&
            (((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByMarking usiphon m0))
82
83
84
        where upost = mpost net usiphon
              upre = mpre net usiphon
              umark = upre \\ upost
Philipp J. Meyer's avatar
Philipp J. Meyer committed
85
86
87
88

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
89

90
91
92
93
94
95
96
97
98
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 ]

99
checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
100
101
        [Trap] -> [Siphon] -> [StableInequality] -> SBool
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 utraps usiphons inequalities =
102
103
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
104
        initialMarkingConstraints net m0 &&&
105
106
107
108
109
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
110
        terminalConstraints net m1 &&&
111
        terminalConstraints net m2 &&&
112
        differentConsensusConstraints net m1 m2 &&&
Philipp J. Meyer's avatar
Philipp J. Meyer committed
113
114
        checkUTrapConstraints net m0 m1 m2 x1 x2 utraps &&&
        checkUSiphonConstraints net m0 m1 m2 x1 x2 usiphons &&&
115
        checkInequalityConstraints net m0 m1 m2 inequalities
116

117
118
checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
checkTerminalMarkingsUniqueConsensusSat net utraps usiphons inequalities =
119
120
121
122
123
124
125
        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,
126
             \fm -> checkTerminalMarkingsUniqueConsensus net (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 Place -> IMap Place -> IMap Place -> 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

Philipp J. Meyer's avatar
Philipp J. Meyer committed
135
136
137
138
139
140
141
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
142

143
trapConstraints :: PetriNet -> SIMap Place -> SBool
144
trapConstraints net b =
Philipp J. Meyer's avatar
Philipp J. Meyer committed
145
146
147
148
149
150
151
152
153
        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
154

155
placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
156
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
157

158
placesUnmarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
159
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0
160

161
placesPostsetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
162
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
163

164
placesPresetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
165
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
166

167
168
169
170
171
172
173
174
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

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

178
179
180
181
182
183
184
185
186
187
188
189
190
191
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"

192
193
findTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findTrap net m0 m1 m2 x1 x2 b sizeLimit =
194
195
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
196
        trapConstraints net b &&&
197
198
199
200
        (
            (placesPostsetOfSequence net x1 b &&& placesUnmarkedByMarking net m1 b) |||
            (placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b)
        )
201

202
203
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
204
205
        let b = makeVarMap $ places net
        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
             \fm -> findTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
209
210
211
212
213
214
215
             \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 &&&
        (
216
217
            (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
218
219
220
221
        )

findUTrapConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUTrapConstraintsSat net m0 m1 m2 x1 x2 =
222
        let b = makeVarMap $ places net
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,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
226
             \fm -> findUTrapConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
227
             \fm -> placesFromAssignment (fmap fm b)))
228

Philipp J. Meyer's avatar
Philipp J. Meyer committed
229
230
findUSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
231
232
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
233
        placesUnmarkedByMarking net m0 b &&&
234
        (
235
236
            (placesPresetOfSequence net x1 b &&& uSiphonConstraints net x1 b) |||
            (placesPresetOfSequence net x2 b &&& uSiphonConstraints net x2 b)
237
        )
238

Philipp J. Meyer's avatar
Philipp J. Meyer committed
239
240
findUSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findUSiphonConstraintsSat net m0 m1 m2 x1 x2 =
241
        let b = makeVarMap $ places net
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,
Philipp J. Meyer's avatar
Philipp J. Meyer committed
245
             \fm -> findUSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
246
             \fm -> placesFromAssignment (fmap fm b)))
247

248
249
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
250
251
252
253
254
255
256
257
258
259
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

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