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

TransitionInvariant.hs 1.39 KB
Newer Older
1
module Solver.TransitionInvariant
2
3
    (checkTransitionInvariant,checkTransitionInvariantSat,
     firedTransitionsFromAssignment)
4
5
6
7
8
9
10
11
12
13
14
15
16
17
where

import Data.SBV
import qualified Data.Map as M

import PetriNet
import Property
import Solver
import Solver.Formula

tInvariantConstraints :: PetriNet -> ModelSI -> SBool
tInvariantConstraints net m =
            bAnd $ map checkTransitionEquation $ places net
        where checkTransitionEquation p =
18
19
                let incoming = map addTransition $ lpre net p
                    outgoing = map addTransition $ lpost net p
20
                in  sum outgoing - sum incoming .>= 0
21
              addTransition (t,w) = literal w * (m M.! t)
22

23
24
25
26
27
finalInvariantConstraints :: ModelSI -> SBool
finalInvariantConstraints m = sum (M.elems m) .> 0

nonnegativityConstraints :: ModelSI -> SBool
nonnegativityConstraints m = bAnd $ map (.>= 0) $ M.elems m
28
29
30
31

checkTransitionInvariant :: PetriNet -> Formula -> ModelSI -> SBool
checkTransitionInvariant net f m =
        tInvariantConstraints net m &&&
32
33
        nonnegativityConstraints m &&&
        finalInvariantConstraints m &&&
34
35
36
37
38
        evaluateFormula f m

checkTransitionInvariantSat :: PetriNet -> Formula -> ([String], ModelSI -> SBool)
checkTransitionInvariantSat net f =
        (transitions net, checkTransitionInvariant net f)
39
40
41

firedTransitionsFromAssignment :: ModelI -> [String]
firedTransitionsFromAssignment a = M.keys $ M.filter ( > 0) a