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

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

import Data.SBV
9
import qualified Data.Map as M
10
11
12
13
14
15

import Util
import PetriNet
import Property
import Solver

16
stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
17
stateEquationConstraints net m0 m x =
18
19
            bAnd $ map checkStateEquation $ places net
        where checkStateEquation p =
20
21
                let incoming = map addTransition $ lpre net p
                    outgoing = map addTransition $ lpost net p
22
                in  val m0 p + sum incoming - sum outgoing .== val m p
23
24
              addTransition (t,w) = literal w * val x t

25
26
27
28
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints m =
            bAnd $ map checkVal $ vals m
        where checkVal x = x .>= 0
29
30
31
32

terminalConstraints :: PetriNet -> SIMap Place -> SBool
terminalConstraints net m =
            bAnd $ map checkTransition $ transitions net
33
        where checkTransition t = bOr $ map checkPlace $ lpre net t
34
35
              checkPlace (p,w) = val m p .< literal w

36
nonEqualityConstraints :: (Ord a, Show a) => PetriNet -> SIMap a -> SIMap a -> SBool
37
nonEqualityConstraints net m1 m2 =
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
            if elemsSet m1 /= elemsSet m2 then
                false
            else
                bOr $ map checkNonEquality $ elems m1
        where checkNonEquality x = val m1 x ./= val m2 x

checkTrap :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkTrap net m0 m1 m2 x1 x2 trap =
            checkMarkingDelta m0 m1 &&&
            checkMarkingDelta m0 m2 &&&
            checkSequenceDelta x1 m1 &&&
            checkSequenceDelta x2 m2
        where checkMarkingDelta m0 m =
                sum (map (val m0) trap) .>= 1 ==> sum (map (val m) trap) .>= 1
              checkSequenceDelta x m =
                sum (map (val x) (mpre net trap)) .>= 1 ==> sum (map (val m) trap) .>= 1

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

59
60
checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkUniqueTerminalMarking net m0 m1 m2 x1 x2 traps =
61
        nonEqualityConstraints net m1 m2 &&&
62
63
64
65
66
67
68
        stateEquationConstraints net m0 m1 x1 &&&
        stateEquationConstraints net m0 m2 x2 &&&
        nonNegativityConstraints m0 &&&
        nonNegativityConstraints m1 &&&
        nonNegativityConstraints m2 &&&
        nonNegativityConstraints x1 &&&
        nonNegativityConstraints x2 &&&
69
        terminalConstraints net m1 &&&
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
        terminalConstraints net m2 &&&
        checkTrapConstraints net m0 m1 m2 x1 x2 traps

checkUniqueTerminalMarkingSat :: PetriNet -> [Trap] -> ConstraintProblem Integer (Marking, Marking, Marking, FiringVector, FiringVector)
checkUniqueTerminalMarkingSat net traps =
        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,
             \fm -> checkUniqueTerminalMarking net (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2) traps,
             \fm -> markingsFromAssignment (fmap fm m0) (fmap fm m1) (fmap fm m2) (fmap fm x1) (fmap fm x2))

markingsFromAssignment :: IMap Place -> IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> (Marking, Marking, Marking, FiringVector, FiringVector)
markingsFromAssignment m0 m1 m2 x1 x2 = (makeVector m0, makeVector m1, makeVector m2, makeVector x1, makeVector x2)

-- trap refinement constraints

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

trapMarkedByMarking :: PetriNet -> Marking -> SBMap Place -> SBool
trapMarkedByMarking net m b = bOr $ mval b $ elems m

trapMarkedBySequence :: PetriNet -> FiringVector -> SBMap Place -> SBool
trapMarkedBySequence net x b = bOr $ mval b $ mpost net $ elems x

trapUnassigned :: Marking -> SBMap Place -> SBool
trapUnassigned m b = bAnd $ map (bnot . val b) $ elems m

properTrap :: SBMap Place -> SBool
properTrap b = bOr $ vals b
107

108
109
110
111
112
113
checkUnmarkedTrap :: PetriNet -> Marking -> Marking -> FiringVector -> SBMap Place -> SBool
checkUnmarkedTrap net m0 m x b =
        trapConstraints net b &&&
        (trapMarkedByMarking net m0 b ||| trapMarkedBySequence net x b) &&&
        trapUnassigned m b &&&
        properTrap b
114

115
116
117
118
119
120
121
checkUnmarkedTrapSat :: PetriNet -> Marking -> Marking -> FiringVector -> ConstraintProblem Bool Trap
checkUnmarkedTrapSat net m0 m x =
        let b = makeVarMap $ places net
        in  ("unmarked trap marked by sequence or initial marking", "trap",
             getNames b,
             \fm -> checkUnmarkedTrap net m0 m x (fmap fm b),
             \fm -> trapFromAssignment (fmap fm b))
122

123
124
trapFromAssignment :: BMap Place -> Trap
trapFromAssignment b = M.keys $ M.filter id b