UniqueTerminalMarking.hs 8.01 KB
Newer Older
1
2
{-# LANGUAGE FlexibleContexts #-}

3
module Solver.UniqueTerminalMarking
4
    (checkUniqueTerminalMarkingSat,
5
     UniqueTerminalMarkingCounterExample,
6
7
     checkUnmarkedTrapSat,
     checkUnmarkedSiphonSat)
8
9
10
where

import Data.SBV
11
import qualified Data.Map as M
12
13
14
15
16
17

import Util
import PetriNet
import Property
import Solver

18
19
20
type UniqueTerminalMarkingCounterExample = (RMarking, RMarking, RMarking, RFiringVector, RFiringVector)

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

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

34
terminalConstraints :: PetriNet -> SRMap Place -> SBool
35
36
terminalConstraints net m =
            bAnd $ map checkTransition $ transitions net
37
        where checkTransition t = bOr $ map checkPlace $ lpre net t
38
              checkPlace (p,w) = val m p .== 0
39

40
nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SRMap a -> SRMap a -> SBool
41
nonEqualityConstraints net m1 m2 =
42
43
44
45
46
47
            if elemsSet m1 /= elemsSet m2 then
                false
            else
                bOr $ map checkNonEquality $ elems m1
        where checkNonEquality x = val m1 x ./= val m2 x

48
checkTrap :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> Trap -> SBool
49
checkTrap net m0 m1 m2 x1 x2 trap =
50
51
52
            (markedByMarking m0 ==> (markedByMarking m1 &&& markedByMarking m2)) &&&
            (markedBySequence x1 ==> markedByMarking m1) &&&
            (markedBySequence x2 ==> markedByMarking m2)
53
54
        where markedByMarking m = sum (map (val m) trap) .> 0
              markedBySequence x = sum (map (val x) (mpre net trap)) .> 0
55

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

60
checkSiphon :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition -> Siphon -> SBool
61
62
63
64
65
checkSiphon net m0 m1 m2 x1 x2 siphon =
            unmarkedByMarking m0 ==> (unmarkedByMarking m1 &&& unmarkedByMarking m2 &&& notPresetOfSequence x1 &&& notPresetOfSequence x2)
        where unmarkedByMarking m = sum (map (val m) siphon) .== 0
              notPresetOfSequence x = sum (map (val x) (mpost net siphon)) .== 0

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

70
checkUniqueTerminalMarking :: PetriNet -> SRMap Place -> SRMap Place -> SRMap Place -> SRMap Transition -> SRMap Transition ->
71
72
        [Trap] -> [Siphon] -> SBool
checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps siphons =
73
        nonEqualityConstraints net m1 m2 &&&
74
75
76
77
78
79
80
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
81
        terminalConstraints net m1 &&&
82
        terminalConstraints net m2 &&&
83
84
        checkTrapConstraints net m0 m1 m2 x1 x2 traps &&&
        checkSiphonConstraints net m0 m1 m2 x1 x2 siphons
85

86
checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> [Siphon] -> ConstraintProblem AlgReal UniqueTerminalMarkingCounterExample
87
checkUniqueTerminalMarkingSat net traps siphons =
88
89
90
91
92
93
94
        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,
95
             \fm -> checkUniqueTerminalMarking net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps siphons,
96
97
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

98
99
100
markingsFromAssignment :: RMap Place -> RMap Place -> RMap Place -> RMap Transition -> RMap Transition -> UniqueTerminalMarkingCounterExample
markingsFromAssignment m0 m1 m2 x1 x2 =
        (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)
101

102
103
104
105
106
107
108
-- trap and siphon refinement constraints

siphonConstraints :: PetriNet -> SBMap Place -> SBool
siphonConstraints net b =
            bAnd $ map siphonConstraint $ transitions net
        where siphonConstraint t =
                  bOr (mval b (post net t)) ==> bOr (mval b (pre net t))
109
110
111
112
113
114
115

trapConstraints :: PetriNet -> SBMap Place -> SBool
trapConstraints net b =
            bAnd $ map trapConstraint $ transitions net
        where trapConstraint t =
                  bOr (mval b (pre net t)) ==> bOr (mval b (post net t))

116
placesMarkedByMarking :: PetriNet -> RMarking -> SBMap Place -> SBool
117
placesMarkedByMarking net m b = bOr $ mval b $ elems m
118

119
placesUnmarkedByMarking :: PetriNet -> RMarking -> SBMap Place -> SBool
120
placesUnmarkedByMarking net m b = bAnd $ map (bnot . val b) $ elems m
121

122
placesPostsetOfSequence :: PetriNet -> RFiringVector -> SBMap Place -> SBool
123
placesPostsetOfSequence net x b = bOr $ mval b $ mpost net $ elems x
124

125
placesPresetOfSequence :: PetriNet -> RFiringVector -> SBMap Place -> SBool
126
placesPresetOfSequence net x b = bOr $ mval b $ mpre net $ elems x
127

128
129
nonemptySet :: (Ord a, Show a) => SBMap a -> SBool
nonemptySet b = bOr $ vals b
130

131
checkUnmarkedTrap :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SBMap Place -> SBool
132
133
134
135
136
137
138
139
140
checkUnmarkedTrap net m0 m1 m2 x1 x2 b =
        trapConstraints net b &&&
        nonemptySet b &&&
        (
            (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)
        )

141
checkUnmarkedTrapSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> ConstraintProblem Bool Trap
142
143
144
145
146
147
148
checkUnmarkedTrapSat net m0 m1 m2 x1 x2 =
        let b = makeVarMap $ places net
        in  ("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",
             getNames b,
             \fm -> checkUnmarkedTrap net m0 m1 m2 x1 x2 (fmap fm b),
             \fm -> placesFromAssignment (fmap fm b))

149
checkUnmarkedSiphon :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> SBMap Place -> SBool
150
151
152
153
154
155
156
157
checkUnmarkedSiphon net m0 m1 m2 x1 x2 b =
        siphonConstraints net b &&&
        nonemptySet b &&&
        (placesUnmarkedByMarking net m0 b &&&
            (placesMarkedByMarking net m1 b ||| placesMarkedByMarking net m2 b |||
             placesPresetOfSequence net x1 b ||| placesPresetOfSequence net x2 b)
        )

158
checkUnmarkedSiphonSat :: PetriNet -> RMarking -> RMarking -> RMarking -> RFiringVector -> RFiringVector -> ConstraintProblem Bool Siphon
159
checkUnmarkedSiphonSat net m0 m1 m2 x1 x2 =
160
        let b = makeVarMap $ places net
161
        in  ("siphon unmarked in m0 and marked in m1 or m2 or used as input in x1 or x2", "siphon",
162
             getNames b,
163
164
             \fm -> checkUnmarkedSiphon net m0 m1 m2 x1 x2 (fmap fm b),
             \fm -> placesFromAssignment (fmap fm b))
165

166
167
placesFromAssignment :: BMap Place -> Trap
placesFromAssignment b = M.keys $ M.filter id b