2.12.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

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

import Data.SBV
import qualified Data.Map as M

import PetriNet
import Property
import Solver
import Solver.Formula

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

23
24
nonnegativityConstraints ::  ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m
25
26

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

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