The name of the initial branch for new projects is now "main" instead of "master". Existing projects remain unchanged. More information: https://doku.lrz.de/display/PUBLIC/GitLab

SComponent.hs 3.63 KB
Newer Older
1
module Solver.SComponent
2
    (checkSComponent,checkSComponentSat,
3
     getSComponentOutIn)
4 5
where

Philipp Meyer's avatar
Philipp Meyer committed
6 7
import Z3.Monad
import Control.Monad
8
import Data.List (partition)
9 10 11 12 13 14 15

import PetriNet
import Solver

prime :: String -> String
prime = ('\'':)

Philipp Meyer's avatar
Philipp Meyer committed
16
checkPrePostPlaces :: PetriNet -> MModelS -> Z3 ()
17
checkPrePostPlaces net m =
Philipp Meyer's avatar
Philipp Meyer committed
18 19 20 21 22 23 24
            mapM_ (assertCnstr <=< checkPrePostPlace) $ places net
        where checkPrePostPlace p = do
                incoming <- mapM (mElem m) $ pre net p
                outgoing <- mapM (mElem m) $ post net p
                lhs <- mElem m p
                rhs <- mkAnd' (incoming ++ outgoing)
                mkImplies lhs rhs
25

Philipp Meyer's avatar
Philipp Meyer committed
26
checkPrePostTransitions :: PetriNet -> MModelS -> Z3 ()
27
checkPrePostTransitions net m =
Philipp Meyer's avatar
Philipp Meyer committed
28 29 30 31 32 33 34 35 36
            mapM_ (assertCnstr <=< checkPrePostTransition) $ transitions net
        where checkPrePostTransition t = do
                incoming <- mElemSum m $ pre net t
                outgoing <- mElemSum m $ post net t
                in1 <- mkEq incoming =<< mkVal (1::Integer)
                out1 <- mkEq outgoing =<< mkVal (1::Integer)
                lhs <- mElem m t
                rhs <- mkAnd [in1, out1]
                mkImplies lhs rhs
37

Philipp Meyer's avatar
Philipp Meyer committed
38 39 40 41 42 43 44 45 46 47
checkSubsetTransitions :: [String] -> MModelS -> Z3 ()
checkSubsetTransitions fired m = do
            mapM_ (assertCnstr <=< checkTransition) fired
            fired'sum <- mElemSum m (map prime fired)
            firedsum <- mElemSum m fired
            assertCnstr =<< mkLt fired'sum firedsum
        where checkTransition t = do
                lhs <- mElem m (prime t)
                rhs <- mElem m t
                mkImplies lhs rhs
48

Philipp Meyer's avatar
Philipp Meyer committed
49 50 51 52
checkNotEmpty :: [String] -> MModelS -> Z3 ()
checkNotEmpty fired m = do
        lhs <- mElemSum m (map prime fired)
        assertCnstr =<< mkGt lhs =<< mkVal (0::Integer)
53

Philipp Meyer's avatar
Philipp Meyer committed
54
checkClosed :: PetriNet -> MModelI -> MModelS -> Z3 ()
55
checkClosed net ax m =
Philipp Meyer's avatar
Philipp Meyer committed
56 57 58 59
            mapM_ (assertCnstr <=< checkPlaceClosed) $ places net
        where checkPlaceClosed p = do
                lhs <- mElem m p
                rhs <- mkAnd' =<< mapM checkTransition
60
                             [(t,t') | t <- pre net p, t' <- post net p,
Philipp Meyer's avatar
Philipp Meyer committed
61 62 63 64 65 66
                                       cElem ax t, cElem ax t' ]
                mkImplies lhs rhs
              checkTransition (t,t') = do
                lhs <- mElem m (prime t)
                rhs <- mElem m (prime t')
                mkImplies lhs rhs
67

Philipp Meyer's avatar
Philipp Meyer committed
68 69 70 71 72 73 74
checkTokens :: PetriNet -> MModelS -> Z3 ()
checkTokens net m = do
            initS <- mapM addPlace (linitials net)
            sums <- mkAdd' initS
            assertCnstr =<< mkEq sums =<< mkVal (1::Integer)
        where addPlace (p,x) =
                mkVal x >>= \x' -> mkMul [x', mVal m p]
75

Philipp Meyer's avatar
Philipp Meyer committed
76 77 78 79 80 81 82
checkBinary :: MModelS -> Z3 ()
checkBinary m =
            mapM_ (assertCnstr <=< checkBinaryVal) $ mValues m
        where checkBinaryVal x = do
                x0 <- mkEq x =<< mkVal (0::Integer)
                x1 <- mkEq x =<< mkVal (1::Integer)
                mkOr [x0,x1]
83

Philipp Meyer's avatar
Philipp Meyer committed
84 85 86 87 88 89 90 91
checkSComponent :: PetriNet -> [String] -> MModelI -> MModelS -> Z3 ()
checkSComponent net fired ax m = do
        checkPrePostPlaces net m
        checkPrePostTransitions net m
        checkSubsetTransitions fired m
        checkNotEmpty fired m
        checkClosed net ax m
        checkTokens net m
92 93
        checkBinary m

Philipp Meyer's avatar
Philipp Meyer committed
94
checkSComponentSat :: PetriNet -> [String] -> MModelI -> ([String], MModelS -> Z3 ())
95 96 97
checkSComponentSat net fired ax =
        (places net ++ transitions net ++ map prime fired,
         checkSComponent net fired ax)
98

Philipp Meyer's avatar
Philipp Meyer committed
99
getSComponentOutIn :: PetriNet -> MModelI -> MModelI -> ([String], [String])
100
getSComponentOutIn net ax as =
101
        partition (cElem ax) $ filter (cElem as) (transitions net)
102