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
        initialMarkingConstraints net m0 &&&
        differentConsensusConstraints net m1 m2 &&&
89
90
91
92
93
94
95
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
96
        terminalConstraints net m1 &&&
97
        terminalConstraints net m2 &&&
98
        checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
99
100
        checkSiphonConstraints net m0 m1 m2 x1 x2 siphons &&&
        checkInequalityConstraints net m0 m1 m2 inequalities
101

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

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

118
119
-- trap and siphon refinement constraints

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

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

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

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

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

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

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

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

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

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

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

188
189
190
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 &&&
191
        nonemptySet b &&&
192
193
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
194
195
        noOutputTransitionEnabled net m0 b &&&
        (placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b)
196

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

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

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