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

3
4
5
module Solver.TerminalMarkingsUniqueConsensus
    (checkTerminalMarkingsUniqueConsensusSat,
     TerminalMarkingsUniqueConsensusCounterExample,
6
7
     findUnmarkedTrapSat,
     findGeneralizedSiphonConstraintsSat,
8
9
     checkGeneralizedCoTrapSat,
     StableInequality)
10
11
12
where

import Data.SBV
13
import qualified Data.Map as M
14
import Data.List ((\\))
15
16
17
18
19
20

import Util
import PetriNet
import Property
import Solver

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

23
24
type StableInequality = (IMap Place, Integer)

25
stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
26
stateEquationConstraints net m0 m x =
27
28
            bAnd $ map checkStateEquation $ places net
        where checkStateEquation p =
29
30
                let incoming = map addTransition $ lpre net p
                    outgoing = map addTransition $ lpost net p
31
                in  val m0 p + sum incoming - sum outgoing .== val m p
32
              addTransition (t,w) = literal w * val x t
33

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

39
terminalConstraints :: PetriNet -> SIMap Place -> SBool
40
41
terminalConstraints net m =
            bAnd $ map checkTransition $ transitions net
42
        where checkTransition t = bOr $ map checkPlace $ lpre net t
43
              checkPlace (p,w) = val m p .<= literal (fromInteger (w - 1))
44

45
46
47
48
49
50
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 =
51
        (sum (mval m1 (yesStates net)) .> 0 &&& sum (mval m2 (noStates net)) .> 0)
52

53
checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
54
checkTrap net m0 m1 m2 x1 x2 trap =
55
            (markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2))
56
57
        where markedByMarking m = sum (mval m trap) .> 0
              markedBySequence x = sum (mval x (mpre net trap)) .> 0
58

59
checkTrapConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
60
61
checkTrapConstraints net m0 m1 m2 x1 x2 traps =
        bAnd $ map (checkTrap net m0 m1 m2 x1 x2) traps
62

63
64
65
66
67
68
checkGeneralizedSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkGeneralizedSiphon net m0 m1 m2 x1 x2 siphon =
            ((unmarkedByMarking m0 &&& unmarkedBySequence x1) ==> (unmarkedByMarking m1)) &&&
            ((unmarkedByMarking m0 &&& unmarkedBySequence x2) ==> (unmarkedByMarking m2))
        where unmarkedByMarking m = sum (mval m siphon) .== 0
              unmarkedBySequence x = sum [ val x t | t <- (mpre net siphon \\ mpost net siphon) ] .== 0
69

70
71
72
checkGeneralizedSiphonConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
checkGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 siphons =
        bAnd $ map (checkGeneralizedSiphon net m0 m1 m2 x1 x2) siphons
73

74
75
76
77
78
79
80
81
82
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 ]

83
checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
84
85
        [Trap] -> [Siphon] -> [StableInequality] -> SBool
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons inequalities =
86
87
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
88
        initialMarkingConstraints net m0 &&&
89
90
91
92
93
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
94
        terminalConstraints net m1 &&&
95
        terminalConstraints net m2 &&&
96
        differentConsensusConstraints net m1 m2 &&&
97
        checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
98
        checkGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 siphons &&&
99
        checkInequalityConstraints net m0 m1 m2 inequalities
100

101
102
checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> [StableInequality] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
checkTerminalMarkingsUniqueConsensusSat net traps siphons inequalities =
103
104
105
106
107
108
109
        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,
110
             \fm -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons inequalities,
111
112
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

113
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample
114
115
markingsFromAssignment m0 m1 m2 x1 x2 =
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
116

117
118
-- trap and siphon refinement constraints

119
120
121
generalizedSiphonConstraints :: PetriNet -> FiringVector -> SIMap Place -> SBool
generalizedSiphonConstraints net x b =
            bAnd [ siphonConstraint t | t <- elems x ]
122
        where siphonConstraint t =
123
                sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
124

125
trapConstraints :: PetriNet -> SIMap Place -> SBool
126
127
128
trapConstraints net b =
            bAnd $ map trapConstraint $ transitions net
        where trapConstraint t =
129
                  sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0
130

131
placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
132
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
133

134
placesUnmarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
135
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0
136

137
placesPostsetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
138
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
139

140
placesPresetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
141
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
142

143
144
145
146
147
148
149
150
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

151
152
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
153

154
155
156
157
158
159
160
161
162
163
164
165
166
167
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"

168
169
170
findUnmarkedTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findUnmarkedTrap net m0 m1 m2 x1 x2 b sizeLimit =
        placesMarkedByMarking net m0 b &&&
171
172
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
173
174
        trapConstraints net b &&&
        ((placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b))
175

176
177
findUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
findUnmarkedTrapSat net m0 m1 m2 x1 x2 =
178
        let b = makeVarMap $ places net
179
180
        in  (minimizeMethod, \sizeLimit ->
            ("trap marked in m and unmarked in m1 or m2, or marked by x1 and unmarked in m1, or marked by x2 and unmarked in m2", "trap",
181
             getNames b,
182
             \fm -> findUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
183
             \fm -> placesFromAssignment (fmap fm b)))
184

185
186
187
findGeneralizedSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
findGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
        placesUnmarkedByMarking net m0 b &&&
188
189
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
190
191
192
193
        (
            (generalizedSiphonConstraints net x1 b &&& placesMarkedByMarking net m1 b) |||
            (generalizedSiphonConstraints net x2 b &&& placesMarkedByMarking net m2 b)
        )
194

195
196
findGeneralizedSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
findGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2 =
197
        let b = makeVarMap $ places net
198
        in  (minimizeMethod, \sizeLimit ->
199
            ("siphon (w.r.t. x1 or x2) not marked in m0 and marked in m1 or m2", "siphon",
200
             getNames b,
201
             \fm -> findGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
202
             \fm -> placesFromAssignment (fmap fm b)))
203

204
205
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252

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