TransitionInvariant.hs 1.8 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 incoming - sum outgoing .>= 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
32
33
34
35
36
37
checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool
checkSComponentTransitions strans m = bAnd $ map checkInOut strans
        where checkInOut (sOut,sIn) =
                bAnd (map (\t -> m M.! t .> 0) sOut) ==>
                bOr (map (\t -> m M.! t .> 0) sIn)

checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] ->
        ModelSI -> SBool
checkTransitionInvariant net f strans m =
38
        tInvariantConstraints net m &&&
39
40
        nonnegativityConstraints m &&&
        finalInvariantConstraints m &&&
41
        checkSComponentTransitions strans m &&&
42
43
        evaluateFormula f m

44
45
46
47
checkTransitionInvariantSat :: PetriNet -> Formula -> [([String],[String])] ->
        ([String], ModelSI -> SBool)
checkTransitionInvariantSat net f strans =
        (transitions net, checkTransitionInvariant net f strans)
48
49
50

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