UniqueTerminalMarking.hs 2.37 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
module Solver.UniqueTerminalMarking
    (checkUniqueTerminalMarkingSat)
where

import Data.SBV

import Util
import PetriNet
import Property
import Solver

12
13
14
15
stateEquationConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
stateEquationConstraints net m1 m2 x =
            bAnd $ map checkStateEquation $ places net
        where checkStateEquation p =
16
17
18
19
20
                let incoming = map addTransition $ lpre net p
                    outgoing = map addTransition $ lpost net p
                in  val m1 p + sum incoming - sum outgoing .== val m2 p
              addTransition (t,w) = literal w * val x t

21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
nonNegativityConstraints :: PetriNet -> SIMap Place -> SBool
nonNegativityConstraints net m =
            bAnd $ map checkVal $ places net
        where checkVal p = val m p .>= 0

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

nonEqualityConstraints :: PetriNet -> SIMap Place -> SIMap Place -> SBool
nonEqualityConstraints net m1 m2 =
            bOr $ map checkNonEquality $ places net
        where checkNonEquality p = val m1 p ./= val m2 p
37
38
39

checkUniqueTerminalMarking :: PetriNet -> SIMap Place -> SIMap Place -> SIMap Transition -> SBool
checkUniqueTerminalMarking net m1 m2 x =
40
41
42
43
44
45
        nonEqualityConstraints net m1 m2 &&&
        stateEquationConstraints net m1 m2 x &&&
        nonNegativityConstraints net m1 &&&
        nonNegativityConstraints net m2 &&&
        terminalConstraints net m1 &&&
        terminalConstraints net m2
46
47
48
49
50
51
52
53
54
55
56
57
58
59

checkUniqueTerminalMarkingSat :: PetriNet -> ConstraintProblem Integer (Marking, Marking)
checkUniqueTerminalMarkingSat net =
        let m1 = makeVarMap $ places net
            m2 = makeVarMapWith prime $ places net
            x  = makeVarMap $ transitions net
        in  ("unique terminal marking", "pair of markings",
             getNames m1 ++ getNames m2 ++ getNames x,
             \fm -> checkUniqueTerminalMarking net (fmap fm m1) (fmap fm m2) (fmap fm x),
             \fm -> markingsFromAssignment (fmap fm m1) (fmap fm m2))

markingsFromAssignment :: IMap Place -> IMap Place -> (Marking, Marking)
markingsFromAssignment m1 m2 = (makeVector m1, makeVector m2)