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

3
4
5
module Solver.TerminalMarkingsUniqueConsensus
    (checkTerminalMarkingsUniqueConsensusSat,
     TerminalMarkingsUniqueConsensusCounterExample,
6
7
     checkUnmarkedTrapSat,
     checkUnmarkedSiphonSat)
8
9
10
where

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

import Util
import PetriNet
import Property
import Solver

19
type TerminalMarkingsUniqueConsensusCounterExample = (Marking, Marking, Marking, FiringVector, FiringVector)
20

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

30
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
31
32
33
nonNegativityConstraints m =
            bAnd $ map checkVal $ vals m
        where checkVal x = x .>= 0
34

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

41
42
43
44
45
46
47
48
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)
49

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

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

62
checkSiphon :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
63
64
checkSiphon net m0 m1 m2 x1 x2 siphon =
            unmarkedByMarking m0 ==> (unmarkedByMarking m1 &&& unmarkedByMarking m2 &&& notPresetOfSequence x1 &&& notPresetOfSequence x2)
65
66
        where unmarkedByMarking m = sum (mval m siphon) .== 0
              notPresetOfSequence x = sum (mval x (mpost net siphon)) .== 0
67

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

72
checkTerminalMarkingsUniqueConsensus :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition ->
73
        [Trap] -> [Siphon] -> SBool
74
75
76
checkTerminalMarkingsUniqueConsensus net m0 m1 m2 x1 x2 traps siphons =
        initialMarkingConstraints net m0 &&&
        differentConsensusConstraints net m1 m2 &&&
77
78
79
80
81
82
83
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
84
        terminalConstraints net m1 &&&
85
        terminalConstraints net m2 &&&
86
87
        checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
        checkSiphonConstraints net m0 m1 m2 x1 x2 siphons
88

89
90
checkTerminalMarkingsUniqueConsensusSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem Integer TerminalMarkingsUniqueConsensusCounterExample
checkTerminalMarkingsUniqueConsensusSat net traps siphons =
91
92
93
94
95
96
97
        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,
98
             \fm -> checkTerminalMarkingsUniqueConsensus net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons,
99
100
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

101
markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> TerminalMarkingsUniqueConsensusCounterExample
102
103
markingsFromAssignment m0 m1 m2 x1 x2 =
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
104

105
106
-- trap and siphon refinement constraints

107
siphonConstraints :: PetriNet -> SIMap Place -> SBool
108
109
110
siphonConstraints net b =
            bAnd $ map siphonConstraint $ transitions net
        where siphonConstraint t =
111
                  sum (mval b $ post net t) .> 0 ==> sum (mval b $ pre net t) .> 0
112

113
trapConstraints :: PetriNet -> SIMap Place -> SBool
114
115
116
trapConstraints net b =
            bAnd $ map trapConstraint $ transitions net
        where trapConstraint t =
117
                  sum (mval b $ pre net t) .> 0 ==> sum (mval b $ post net t) .> 0
118

119
placesMarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
120
placesMarkedByMarking net m b = sum (mval b $ elems m) .> 0
121

122
placesUnmarkedByMarking :: PetriNet -> Marking -> SIMap Place -> SBool
123
placesUnmarkedByMarking net m b = sum (mval b $ elems m) .== 0
124

125
placesPostsetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
126
placesPostsetOfSequence net x b = sum (mval b $ mpost net $ elems x) .> 0
127

128
placesPresetOfSequence :: PetriNet -> FiringVector -> SIMap Place -> SBool
129
placesPresetOfSequence net x b = sum (mval b $ mpre net $ elems x) .> 0
130

131
132
nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
133

134
135
136
137
138
139
140
141
142
143
144
145
146
147
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"

148
checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> SIMap Place -> Maybe (Int, Integer) -> SBool
149
checkUnmarkedTrap net m0 m1 m2 x1 x2 b sizeLimit =
150
151
        trapConstraints net b &&&
        nonemptySet b &&&
152
153
        checkSizeLimit b sizeLimit &&&
        checkBinary b &&&
154
155
156
157
158
159
        (
            (placesMarkedByMarking net m0 b &&& (placesUnmarkedByMarking net m1 b ||| placesUnmarkedByMarking net m2 b)) |||
            (placesPostsetOfSequence net x1 b &&& placesUnmarkedByMarking net m1 b) |||
            (placesPostsetOfSequence net x2 b &&& placesUnmarkedByMarking net m2 b)
        )

160
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Trap Integer
161
162
checkUnmarkedTrapSat net m0 m1 m2 x1 x2 =
        let b = makeVarMap $ places net
163
164
        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",
165
             getNames b,
166
167
             \fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
             \fm -> placesFromAssignment (fmap fm b)))
168

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

180
checkUnmarkedSiphonSat :: PetriNet -> Marking -> Marking -> Marking -> FiringVector -> FiringVector -> MinConstraintProblem Integer Siphon Integer
181
checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 =
182
        let b = makeVarMap $ places net
183
184
        in  (minimizeMethod, \sizeLimit ->
            ("siphon unmarked in m0 and marked in m1 or m2 or used as input in x1 or x2", "siphon",
185
             getNames b,
186
187
             \fm -> checkUnmarkedSiphon net m0 m1 m2 x1 x2 (fmap fm b) sizeLimit,
             \fm -> placesFromAssignment (fmap fm b)))
188

189
190
placesFromAssignment :: IMap Place -> ([Place], Integer)
placesFromAssignment b = (M.keys (M.filter (> 0) b), sum (M.elems b))