TransitionInvariant.hs 1.76 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
where

import Data.SBV

import PetriNet
import Property
import Solver
import Solver.Formula

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

22
finalInvariantConstraints :: ModelSI -> SBool
23
finalInvariantConstraints m = sum (mValues m) .> 0
24
25

nonnegativityConstraints :: ModelSI -> SBool
26
nonnegativityConstraints m = bAnd $ map (.>= 0) $ mValues m
27

28
29
30
checkSComponentTransitions :: [([String],[String])] -> ModelSI -> SBool
checkSComponentTransitions strans m = bAnd $ map checkInOut strans
        where checkInOut (sOut,sIn) =
31
32
                bAnd (map (\t -> mVal m t .> 0) sOut) ==>
                bOr (map (\t -> mVal m t .> 0) sIn)
33
34
35
36

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

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

firedTransitionsFromAssignment :: ModelI -> [String]
49
firedTransitionsFromAssignment = mElemsWith (> 0)