StateEquation.hs 1.47 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
nonnegativityConstraints ::  ModelSI -> SBool
23
nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
24
25

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

checkStateEquation :: PetriNet -> Formula -> [[String]] -> ModelSI -> SBool
checkStateEquation net f traps m =
        placeConstraints net m &&&
32
        nonnegativityConstraints m &&&
33
34
35
36
37
38
39
40
41
        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]
42
markedPlacesFromAssignment net a = filter (cElem a) $ places net