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

3
4
5
module Solver.TerminalMarkingsUniqueConsensus
    (checkTerminalMarkingsUniqueConsensusSat,
     TerminalMarkingsUniqueConsensusCounterExample,
6
     checkUnmarkedTrapSat,
7
8
9
     checkGeneralizedSiphonConstraintsSat,
     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
51
52
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 =
        (sum (mval m1 (yesStates net)) .> 0 &&& sum (mval m2 (noStates net)) .> 0) |||
        (sum (mval m1 (noStates net)) .> 0 &&& sum (mval m2 (yesStates net)) .> 0)
53

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

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

64
checkSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
65
checkSiphon net m0 m1 m2 x1 x2 siphon =
66
67
68
            noTransitionEnabledByMarking m0 ==> (notPresetOfSequence x1 &&& notPresetOfSequence x2)
        where noTransitionEnabledByMarking m = bAnd $ map (notEnabledByMarkingInSiphon m) $ mpost net siphon
              notEnabledByMarkingInSiphon m t = bOr $ [val m p .< literal w | (p, w) <- lpre net t, p `elem` siphon]
69
              notPresetOfSequence x = sum (mval x (mpost net siphon)) .== 0
70

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

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

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

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

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

119
120
-- trap and siphon refinement constraints

121
122
siphonConstraints :: PetriNet -> Marking -> SIMap Place -> SBool
siphonConstraints net m0 b =
123
124
            bAnd $ map siphonConstraint $ transitions net
        where siphonConstraint t =
125
                  sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
126

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

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

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

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

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

145
146
147
148
149
150
151
152
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

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

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

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

180
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
181
182
checkUnmarkedTrapSat net m0 m1 m2 x1 x2 =
        let b = makeVarMap $ places net
183
184
        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",
185
             getNames b,
186
187
             \fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
             \fm -> placesFromAssignment (fmap fm b)))
188

189
190
191
checkGeneralizedSiphonConstraints :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
checkGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 b sizeLimit =
        siphonConstraints net m0 b &&&
192
        nonemptySet b &&&
193
194
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
195
196
        noOutputTransitionEnabled net m0 b &&&
        (placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b)
197

198
199
checkGeneralizedSiphonConstraintsSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
checkGeneralizedSiphonConstraintsSat net m0 m1 m2 x1 x2 =
200
        let b = makeVarMap $ places net
201
        in  (minimizeMethod, \sizeLimit ->
202
            ("siphon not enabling any output transitions in m0 and used as input in x1 or x2", "siphon",
203
             getNames b,
204
             \fm -> checkGeneralizedSiphonConstraints net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
205
             \fm -> placesFromAssignment (fmap fm b)))
206

207
208
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))
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
253
254
255

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