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