LayeredTermination.hs 7.67 KB
Newer Older
1
2
{-# LANGUAGE FlexibleContexts #-}

Philipp Meyer's avatar
Philipp Meyer committed
3
4
5
module Solver.LayeredTermination
    (checkLayeredTerminationSat,
     LayeredTerminationInvariant)
6
7
8
where

import Data.SBV
9
import Data.List (intercalate,genericReplicate)
10
11
12
import qualified Data.Map as M

import Util
13
import PopulationProtocol
14
15
16
17
import Property
import Solver
import StructuralComputation

18
19
type InvariantSize = ([Int], [Integer], [Int])

Philipp Meyer's avatar
Philipp Meyer committed
20
21
22
type LayeredTerminationInvariant = [LayerInvariant]
data LayerInvariant =
            LayerInvariant (Integer, [Transition], IVector State)
23

Philipp Meyer's avatar
Philipp Meyer committed
24
25
instance Invariant LayerInvariant where
        invariantSize (LayerInvariant (_, ti, yi)) = if null ti then 0 else size yi
26

Philipp Meyer's avatar
Philipp Meyer committed
27
28
instance Show LayerInvariant where
        show (LayerInvariant (i, ti, yi)) =
29
30
                "T_" ++ show i ++ ":\n" ++ unlines (map show ti) ++
                    (if null ti then "" else "\nY_" ++ show i ++ ": " ++ intercalate " + " (map showWeighted (items yi)) ++ "\n")
31
32
33
34
35
36

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

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

Philipp Meyer's avatar
Philipp Meyer committed
41
42
layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool
layerTerminationConstraints pp i b y =
43
            bAnd $ map checkTransition $ transitions pp
44
        where checkTransition t =
45
46
                let incoming = map addState $ lpre pp t
                    outgoing = map addState $ lpost pp t
47
                in  (val b t .== literal i) ==> (sum outgoing - sum incoming .< 0)
48
              addState (q, w) = literal w * val y q
49

50
51
terminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> [SIMap State] -> SBool
terminationConstraints pp k b ys =
Philipp Meyer's avatar
Philipp Meyer committed
52
        bAnd $ [layerTerminationConstraints pp i b y | (i,y) <- zip [1..] ys]
53

Philipp Meyer's avatar
Philipp Meyer committed
54
55
56
57
layerConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SBool
layerConstraints pp k b =
            bAnd $ map checkLayer $ transitions pp
        where checkLayer t = literal 1 .<= val b t &&& val b t .<= literal k
58

Philipp Meyer's avatar
Philipp Meyer committed
59
60
layerOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool
layerOrderConstraints pp triplets k b =
61
62
63
            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)

Philipp Meyer's avatar
Philipp Meyer committed
64
65
66
checkLayeredTermination :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
checkLayeredTermination pp triplets k b ys sizeLimit =
        layerConstraints pp k b &&&
67
        terminationConstraints pp k b ys &&&
Philipp Meyer's avatar
Philipp Meyer committed
68
        layerOrderConstraints pp triplets k b &&&
69
70
        checkNonNegativityConstraints ys &&&
        checkSizeLimit k b ys sizeLimit
71

Philipp Meyer's avatar
Philipp Meyer committed
72
73
checkLayeredTerminationSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize
checkLayeredTerminationSat pp triplets k =
74
        let makeYName i = (++) (genericReplicate i '\'')
75
76
            ys = [makeVarMapWith (makeYName i) $ states pp | i <- [1..k]]
            b = makeVarMap $ transitions pp
77
        in  (minimizeMethod, \sizeLimit ->
78
            ("layered termination", "invariant",
79
             concat (map getNames ys) ++ getNames b,
Philipp Meyer's avatar
Philipp Meyer committed
80
             \fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit,
81
             \fm -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys)))
82

83
minimizeMethod :: Int -> InvariantSize -> String
84
minimizeMethod 1 (curYSize, _, _) = "number of states in y less than " ++ show (sum curYSize)
Philipp Meyer's avatar
Philipp Meyer committed
85
86
minimizeMethod 2 (_, _, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize)
minimizeMethod 3 (curYSize, _, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize) ++
87
                                        " or same number of transitions and number of states in y less than " ++ show curYSize
88
minimizeMethod 4 (_, curYMax, _) = "maximum coefficient in y is less than " ++ show (maximum curYMax)
89
90
minimizeMethod 5 (curYSize, curYMax, _) = "number of states in y less than " ++ show (sum curYSize) ++
                                        " or same number of states and maximum coefficient in y is less than " ++ show (maximum curYMax)
Philipp Meyer's avatar
Philipp Meyer committed
91
minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize) ++
92
93
                                        " or same number of transitions and number of states in y less than " ++ show (sum curYSize) ++
                                        " or same number of transitions and same number of states and maximum coefficient in y less than " ++ show (maximum curYMax)
94
95
minimizeMethod _ _ = error "minimization method not supported"

96
checkSizeLimit :: Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
97
checkSizeLimit _ _ _ Nothing = true
98
99
100
checkSizeLimit k b ys (Just (1, (curYSize, _, _))) = (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize)))
checkSizeLimit k b ys (Just (2, (_, _, curTSize))) = (sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))
checkSizeLimit k b ys (Just (3, (curYSize, _, curTSize))) =
101
102
        ((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))) ||| (
            ((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .== literal (fromIntegral (last curTSize))) &&&
103
            (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize)))
104
        )
105
106
107
108
109
110
111
112
113
114
115
checkSizeLimit k b ys (Just (4, (_, curYMax, _))) = ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax)))
checkSizeLimit k b ys (Just (5, (curYSize, curYMax, _))) =
        (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize))) ||| (
            (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .== literal (fromIntegral (sum curYSize))) &&&
            ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax))))
checkSizeLimit k b ys (Just (6, (curYSize, curYMax, curTSize))) =
        ((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .< literal (fromIntegral (last curTSize))) ||| (
            ((sum (map (\tb -> ite (tb .== (literal k)) (1::SInteger) 0) (vals b))) .== literal (fromIntegral (last curTSize))) &&&
            ((sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .< literal (fromIntegral (sum curYSize))) ||| (
                (sum (map (\y -> sum (map (\yi -> ite (yi .> 0) (1::SInteger) 0) (vals y))) ys) .== literal (fromIntegral (sum curYSize))) &&&
                ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax))))))
116
117
checkSizeLimit _ _ _ (Just (_, _)) = error "minimization method not supported"

Philipp Meyer's avatar
Philipp Meyer committed
118
invariantFromAssignment :: PopulationProtocol -> Integer -> IMap Transition -> [IMap State] -> (LayeredTerminationInvariant, InvariantSize)
119
invariantFromAssignment pp k b ys =
Philipp Meyer's avatar
Philipp Meyer committed
120
            (invariant, (map invariantLength invariant, map invariantMaxCoefficient invariant, map layerSize invariant))
121
        where
Philipp Meyer's avatar
Philipp Meyer committed
122
123
124
125
            invariant = [LayerInvariant (i, M.keys (M.filter (== i) b), makeVector y) | (i,y) <- zip [1..] ys]
            invariantMaxCoefficient (LayerInvariant (_, _, yi)) = maximum $ vals yi
            invariantLength (LayerInvariant (_, _, yi)) = size yi
            layerSize (LayerInvariant (_, ti, _)) = length ti