SComponentWithCut.hs 6.63 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
module Solver.SComponentWithCut
    (checkSComponentWithCutSat)
where

import Data.SBV
import Data.List (genericLength)
import qualified Data.Map as M

import Util
import PetriNet
import Solver

type SizeIndicator = (Integer, Integer, Integer, Integer, Integer)

checkPrePostPlaces :: PetriNet -> SIMap Place -> SIMap Place ->
        SIMap Transition -> SIMap Transition -> SIMap Transition ->
        SBool
checkPrePostPlaces net p1 p2 t0 t1 t2 =
            bAnd (map (checkPrePostPlace p1 [t0,t1]) (places net)) &&&
            bAnd (map (checkPrePostPlace p2 [t0,t2]) (places net))
        where checkPrePostPlace ps ts p =
                  let incoming = map (checkIn ts) $ pre net p
                      outgoing = map (checkIn ts) $ post net p
                  in  val ps p .== 1 ==> bAnd incoming &&& bAnd outgoing
              checkIn xs x = sum (map (`val` x) xs) .== 1

checkPrePostTransitions :: PetriNet -> SIMap Place -> SIMap Place ->
        SIMap Transition -> SIMap Transition -> SIMap Transition ->
        SBool
checkPrePostTransitions net p1 p2 t0 t1 t2 =
            bAnd (map (checkPrePostTransition t0 [p1,p2]) (transitions net)) &&&
            bAnd (map (checkPrePostTransition t1 [p1]) (transitions net)) &&&
            bAnd (map (checkPrePostTransition t2 [p2]) (transitions net))
        where checkPrePostTransition ts ps t =
                  let incoming = checkInOne ps $ pre net t
                      outgoing = checkInOne ps $ post net t
                  in  val ts t .== 1 ==> incoming &&& outgoing
              checkInOne xs x = sum (concatMap (`mval` x) xs) .== 1

checkComponents :: FiringVector -> SIMap Transition -> SIMap Transition -> SBool
checkComponents x t1 t2 = checkComponent t1 &&& checkComponent t2
        where checkTransition ts t = val ts t .== 1
              checkComponent ts = bOr $ map (checkTransition ts) $ elems x

checkZeroUnused :: FiringVector -> SIMap Transition -> SBool
checkZeroUnused x t0 = bAnd (map checkTransition (elems x))
        where checkTransition t = val t0 t .== 0

checkTokens :: PetriNet -> SIMap Place -> SIMap Place -> SBool
checkTokens net p1 p2 =
            sum (map addPlace $ linitials net) .== 1
        where addPlace (p,i) = literal i * (val p1 p + val p2 p)

checkDisjunct :: PetriNet ->
        SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
        SBool
checkDisjunct net p1 p2 t0 t1 t2 =
            bAnd (map checkPlace (places net)) &&&
            bAnd (map checkTransition (transitions net))
        where checkPlace p = val p1 p + val p2 p .<= 1
              checkTransition t = val t0 t + val t1 t + val t2 t .<= 1

checkBinary :: SIMap Place -> SIMap Place -> SIMap Transition ->
        SIMap Transition -> SIMap Transition -> SBool
checkBinary p1 p2 t0 t1 t2 =
            checkBins p1 &&& checkBins p2 &&& checkBins t0 &&& checkBins t1 &&& checkBins t2
        where checkBins xs = bAnd $ map (\x -> x .== 0 ||| x .== 1) $ vals xs

checkSizeLimit ::
        SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
71
        Maybe (Int, SizeIndicator) -> SBool
72
checkSizeLimit _ _ _ _ _ Nothing = true
73
checkSizeLimit p1 p2 t0 t1 t2 (Just (minMethod, (p1Size, p2Size, t0Size, t1Size, t2Size))) =
74
75
76
77
78
79
80
81
82
83
        let p1SizeNext = sumVal p1
            p2SizeNext = sumVal p2
            t0SizeNext = sumVal t0
            t1SizeNext = sumVal t1
            t2SizeNext = sumVal t2
            p1SizeNow = literal p1Size
            p2SizeNow = literal p2Size
            t0SizeNow = literal t0Size
            t1SizeNow = literal t1Size
            t2SizeNow = literal t2Size
84
        in  case minMethod of
85
                1 -> (t0SizeNext .< t0SizeNow) |||
86
87
88
89
                    (t0SizeNext .== t0SizeNow &&&
                        t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
                    (t0SizeNext .== t0SizeNow &&&
                        t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow)
90
                2 -> (t1SizeNext .> t1SizeNow &&& t2SizeNext .>= t2SizeNow) |||
91
92
93
                    (t1SizeNext .>= t1SizeNow &&& t2SizeNext .> t2SizeNow) |||
                    (t1SizeNext .== t1SizeNow &&& t2SizeNext .== t2SizeNow &&&
                        t0SizeNext .< t0SizeNow)
94
95
96
97
98
99
                3 -> (p1SizeNext + p2SizeNext .< p1SizeNow + p2SizeNow) |||
                    (p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&&
                        t0SizeNext .< t0SizeNow)
                4 -> (p1SizeNext + p2SizeNext .> p1SizeNow + p2SizeNow) |||
                    (p1SizeNext + p2SizeNext .== p1SizeNow + p2SizeNow &&&
                        t0SizeNext .< t0SizeNow)
100
                _ -> error $ "minimization method " ++ show minMethod ++ " not supported"
101

102
checkSComponent :: PetriNet -> FiringVector -> Maybe (Int, SizeIndicator) ->
103
104
105
106
107
108
109
110
111
112
113
114
        SIMap Place -> SIMap Place -> SIMap Transition -> SIMap Transition -> SIMap Transition ->
        SBool
checkSComponent net x sizeLimit p1 p2 t0 t1 t2 =
        checkPrePostPlaces net p1 p2 t0 t1 t2 &&&
        checkPrePostTransitions net p1 p2 t0 t1 t2 &&&
        checkZeroUnused x t0 &&&
        checkComponents x t1 t2 &&&
        checkSizeLimit p1 p2 t0 t1 t2 sizeLimit &&&
        checkTokens net p1 p2 &&&
        checkBinary p1 p2 t0 t1 t2 &&&
        checkDisjunct net p1 p2 t0 t1 t2

115
checkSComponentWithCutSat :: PetriNet -> FiringVector -> Maybe (Int, SizeIndicator) ->
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
        ConstraintProblem Integer (Cut, SizeIndicator)
checkSComponentWithCutSat net x sizeLimit =
        let p1 = makeVarMapWith ("P1@"++) $ places net
            p2 = makeVarMapWith ("P2@"++) $ places net
            t0 = makeVarMapWith ("T0@"++) $ transitions net
            t1 = makeVarMapWith ("T1@"++) $ transitions net
            t2 = makeVarMapWith ("T2@"++) $ transitions net
        in  ("general S-component constraints", "cut",
            getNames p1 ++ getNames p2 ++ getNames t0 ++ getNames t1 ++ getNames t2,
            \fm -> checkSComponent net x sizeLimit
                    (fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2),
            \fm -> cutFromAssignment
                    (fmap fm p1) (fmap fm p2) (fmap fm t0) (fmap fm t1) (fmap fm t2))

cutFromAssignment ::
        IMap Place -> IMap Place -> IMap Transition -> IMap Transition -> IMap Transition ->
        (Cut, SizeIndicator)
cutFromAssignment p1m p2m t0m t1m t2m =
        let p1 = M.keys $ M.filter (> 0) p1m
            p2 = M.keys $ M.filter (> 0) p2m
            t0 = M.keys $ M.filter (> 0) t0m
            t1 = M.keys $ M.filter (> 0) t1m
            t2 = M.keys $ M.filter (> 0) t2m
        in  (([(p1,t1),(p2,t2)], t0), (genericLength p1, genericLength p2,
                genericLength t0, genericLength t1, genericLength t2))