StateEquation.hs 1.63 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
module Solver.StateEquation
    (checkStateEquation,checkStateEquationSat,
     markedPlacesFromAssignment)
where

import Data.SBV

import PetriNet
import Property
import Solver
import Solver.Formula

placeConstraints :: PetriNet -> ModelSI -> SBool
14
placeConstraints net m = bAnd $ map checkPlaceEquation $ places net
15
16
17
18
        where checkPlaceEquation p =
                let incoming = map addTransition $ lpre net p
                    outgoing = map addTransition $ lpost net p
                    pinit = literal $ initial net p
19
20
                in  pinit + sum incoming - sum outgoing .== mVal m p
              addTransition (t,w) = literal w * mVal m t
21

22
23
24
25
26
nonNegativityConstraints :: PetriNet -> ModelSI -> SBool
nonNegativityConstraints net m =
            bAnd (map checkNonNegativity (places net)) &&&
            bAnd (map checkNonNegativity (transitions net))
        where checkNonNegativity x = mVal m x .>= 0
27
28

checkTraps :: [[String]] -> ModelSI -> SBool
29
checkTraps traps m = bAnd $ map checkTrapDelta traps
30
        where checkTrapDelta trap = sum (map (mVal m) trap) .>= 1
31
32
33
34

checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
checkStateEquation net f traps m =
        placeConstraints net m &&&
35
        nonNegativityConstraints net m &&&
36
37
38
39
40
41
42
43
44
        checkTraps traps m &&&
        evaluateFormula f m

checkStateEquationSat :: PetriNet -> Formula -> [[String]] ->
        ([String], ModelSI -> SBool)
checkStateEquationSat net f traps =
        (places net ++ transitions net, checkStateEquation net f traps)

markedPlacesFromAssignment :: PetriNet -> ModelI -> [String]
45
markedPlacesFromAssignment net a = filter (cElem a) $ places net