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)