TerminalMarkingReachable.hs 3.57 KB
Newer Older
1
2
3
4
5
6
7
8
{-# LANGUAGE FlexibleContexts #-}

module Solver.TerminalMarkingReachable
    (checkTerminalMarkingReachableSat,
     TerminalMarkingReachableInvariant)
where

import Data.SBV
9
import Data.List (intercalate,genericReplicate)
10
11
12
13
14
15
16
17
18
19
import qualified Data.Map as M

import Util
import PetriNet
import Property
import Solver
import StructuralComputation

type TerminalMarkingReachableInvariant = [BlockInvariant]
data BlockInvariant =
20
            BlockInvariant (Integer, [Transition], IVector Place)
21
22

instance Invariant BlockInvariant where
23
        invariantSize (BlockInvariant (_, ti, yi)) = if null ti then 0 else size yi
24
25
26

instance Show BlockInvariant where
        show (BlockInvariant (i, ti, yi)) =
27
28
                "T_" ++ show i ++ ":\n" ++ unlines (map show ti) ++
                    (if null ti then "" else "\nY_" ++ show i ++ ": " ++ intercalate " + " (map showWeighted (items yi)) ++ "\n")
29
30
31
32
33
34

nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints m =
            bAnd $ map checkVal $ vals m
        where checkVal x = x .>= 0

35
36
37
checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool
checkNonNegativityConstraints xs =
            bAnd $ map nonNegativityConstraints xs
38

39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
blockTerminationConstraints :: PetriNet -> Integer -> SIMap Transition -> SIMap Place -> SBool
blockTerminationConstraints net i b y =
            bAnd $ map checkTransition $ transitions net
        where checkTransition t =
                let incoming = map addPlace $ lpre net t
                    outgoing = map addPlace $ lpost net t
                in  (val b t .== literal i) ==> (sum outgoing - sum incoming .< 0)
              addPlace (p, w) = literal w * val y p

terminationConstraints :: PetriNet -> Integer -> SIMap Transition -> [SIMap Place] -> SBool
terminationConstraints net k b ys =
        bAnd $ [blockTerminationConstraints net i b y | (i,y) <- zip [1..] ys]

blockConstraints :: PetriNet -> Integer -> SIMap Transition -> SBool
blockConstraints net k b =
            bAnd $ map checkBlock $ transitions net
        where checkBlock t = literal 1 .<= val b t &&& val b t .<= literal k

blockOrderConstraints :: PetriNet -> [Triplet] -> Integer -> SIMap Transition -> SBool
blockOrderConstraints net triplets k b =
            bAnd $ map checkTriplet triplets
        where checkTriplet (s,t,ts) = (val b s .> val b t) ==> bOr (map (\t' -> val b t' .== val b t) ts)

checkTerminalMarkingReachable :: PetriNet -> [Triplet] -> Integer -> SIMap Transition -> [SIMap Place] -> SBool
checkTerminalMarkingReachable net triplets k b ys =
        blockConstraints net k b &&&
        terminationConstraints net k b ys &&&
        blockOrderConstraints net triplets k b &&&
        checkNonNegativityConstraints ys

checkTerminalMarkingReachableSat :: PetriNet -> [Triplet] -> Integer -> ConstraintProblem Integer TerminalMarkingReachableInvariant
70
checkTerminalMarkingReachableSat net triplets k =
71
        let makeYName i = (++) (genericReplicate i '\'')
72
73
74
75
            ys = [makeVarMapWith (makeYName i) $ places net | i <- [1..k]]
            b = makeVarMap $ transitions net
        in  ("terminal marking reachable", "invariant",
             concat (map getNames ys) ++ getNames b,
76
77
             \fm -> checkTerminalMarkingReachable net triplets k (fmap fm b) (map (fmap fm) ys),
             \fm -> invariantFromAssignment net k (fmap fm b) (map (fmap fm) ys))
78

79
80
81
invariantFromAssignment :: PetriNet -> Integer -> IMap Transition -> [IMap Place] -> TerminalMarkingReachableInvariant
invariantFromAssignment net k b ys =
        [BlockInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys]