Starting from 2021-07-01, all LRZ GitLab users will be required to explicitly accept the GitLab Terms of Service. Please see the detailed information at https://doku.lrz.de/display/PUBLIC/GitLab and make sure that your projects conform to the requirements.

TransitionInvariant.hs 2.21 KB
Newer Older
1
module Solver.TransitionInvariant
2 3
    (checkTransitionInvariant,checkTransitionInvariantSat,
     firedTransitionsFromAssignment)
4 5
where

6 7
import Z3.Monad
import Control.Monad
8 9 10 11 12 13

import PetriNet
import Property
import Solver
import Solver.Formula

14
tInvariantConstraints :: PetriNet -> MModelS -> Z3 ()
15
tInvariantConstraints net m =
16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
            mapM_ (assertCnstr <=< checkTransitionEquation) $ places net
        where checkTransitionEquation p = do
                incoming <- mapM (addTransition   1 ) $ lpre net p
                outgoing <- mapM (addTransition (-1)) $ lpost net p
                sums <- mkAdd' (incoming ++ outgoing)
                mkGe sums =<< mkVal (0::Integer)
              addTransition fac (t,w) =
                  mkVal (fac*w) >>= \w' -> mkMul [w', mVal m t]

finalInvariantConstraints :: MModelS -> Z3 ()
finalInvariantConstraints m = do
        sums <- mkAdd' (mValues m)
        assertCnstr =<< mkGt sums =<< mkVal (0::Integer)

nonnegativityConstraints :: MModelS -> Z3 ()
nonnegativityConstraints m = mapM_ (assertCnstr <=< geZero) $ mValues m
        where geZero v = mkGe v =<< mkVal (0::Integer)

checkSComponentTransitions :: [([String],[String])] -> MModelS -> Z3 ()
checkSComponentTransitions strans m = mapM_ (assertCnstr <=< checkInOut) strans
        where checkInOut (sOut,sIn) = do
                lhs <- mkAnd' =<<
                        mapM (\t -> mkGt (mVal m t) =<< mkVal (0::Integer)) sOut
                rhs <- mkOr'  =<<
                        mapM (\t -> mkGt (mVal m t) =<< mkVal (0::Integer)) sIn
                mkImplies lhs rhs
42 43

checkTransitionInvariant :: PetriNet -> Formula -> [([String],[String])] ->
44 45 46 47 48 49 50
        MModelS -> Z3 ()
checkTransitionInvariant net f strans m = do
        tInvariantConstraints net m
        nonnegativityConstraints m
        finalInvariantConstraints m
        checkSComponentTransitions strans m
        assertCnstr =<< evaluateFormula f m
51

52
checkTransitionInvariantSat :: PetriNet -> Formula -> [([String],[String])] ->
53
        ([String], MModelS -> Z3 ())
54 55
checkTransitionInvariantSat net f strans =
        (transitions net, checkTransitionInvariant net f strans)
56

57
firedTransitionsFromAssignment :: MModelI -> [String]
58
firedTransitionsFromAssignment = mElemsWith (> 0)