TrapConstraints.hs 1.39 KB
Newer Older
1
module Solver.TrapConstraints
Philipp Meyer's avatar
Philipp Meyer committed
2
    (checkTrapSat)
3
4
5
where

import Data.SBV
Philipp Meyer's avatar
Philipp Meyer committed
6
7
import Control.Monad
import qualified Data.Map as M
8

9
import Util
10
11
12
import PetriNet
import Solver

Philipp Meyer's avatar
Philipp Meyer committed
13
14
15
16
17
18
19
20
21
22
trapConstraints :: PetriNet -> VarMap Place -> BoolConstraint
trapConstraints net b =
            liftM bAnd $ mapM trapConstraint $ transitions net
        where trapConstraint t = do
                cPre <- mapM (val b) $ pre net t
                cPost <- mapM (val b) $ post net t
                return $ bOr cPre ==> bOr cPost

trapInitiallyMarked :: PetriNet -> VarMap Place -> BoolConstraint
trapInitiallyMarked net b =
23
        liftM bOr $ mapM (val b) $ initials net
Philipp Meyer's avatar
Philipp Meyer committed
24
25
26

trapUnassigned :: Marking -> VarMap Place -> BoolConstraint
trapUnassigned m b =
27
        liftM bAnd $ mapM (liftM bnot . val b) $ elems m
Philipp Meyer's avatar
Philipp Meyer committed
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

checkTrap :: PetriNet -> Marking -> VarMap Place -> BoolConstraint
checkTrap net m b = do
        c1 <- trapConstraints net b
        c2 <- trapInitiallyMarked net b
        c3 <- trapUnassigned m b
        return $ c1 &&& c2 &&& c3

checkTrapSat :: PetriNet -> Marking -> ConstraintProblem Bool Trap
checkTrapSat net m =
        let b = makeVarMap $ places net
        in  ("trap constraints", "trap",
             getNames b,
             checkTrap net m b,
             trapFromAssignment b)

trapFromAssignment :: VarMap Place -> BoolResult Trap
trapFromAssignment b = do
46
47
        bm <- valMap b
        return $ M.keys $ M.filter id bm
48