{-# LANGUAGE FlexibleContexts #-} module Solver.LayeredTermination (checkLayeredTerminationSat, LayeredTerminationInvariant) where import Data.SBV import Data.List (intercalate,genericReplicate) import qualified Data.Map as M import Util import PopulationProtocol import Property import Solver import StructuralComputation type InvariantSize = ([Int], [Integer], [Int]) type LayeredTerminationInvariant = [LayerInvariant] data LayerInvariant = LayerInvariant (Integer, [Transition], IVector State) instance Invariant LayerInvariant where invariantSize (LayerInvariant (_, ti, yi)) = if null ti then 0 else size yi instance Show LayerInvariant where show (LayerInvariant (i, ti, yi)) = "T_" ++ show i ++ ":\n" ++ unlines (map show ti) ++ (if null ti then "" else "\nY_" ++ show i ++ ": " ++ intercalate " + " (map showWeighted (items yi)) ++ "\n") nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool nonNegativityConstraints m = bAnd \$ map checkVal \$ vals m where checkVal x = x .>= 0 checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool checkNonNegativityConstraints xs = bAnd \$ map nonNegativityConstraints xs layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool layerTerminationConstraints pp i b y = bAnd \$ map checkTransition \$ transitions pp where checkTransition t = let incoming = map addState \$ lpre pp t outgoing = map addState \$ lpost pp t in (val b t .== literal i) ==> (sum outgoing - sum incoming .< 0) addState (q, w) = literal w * val y q terminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> [SIMap State] -> SBool terminationConstraints pp k b ys = bAnd \$ [layerTerminationConstraints pp i b y | (i,y) <- zip [1..] ys] 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 layerOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool layerOrderConstraints pp 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) checkLayeredTermination :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool checkLayeredTermination pp triplets k b ys sizeLimit = layerConstraints pp k b &&& terminationConstraints pp k b ys &&& layerOrderConstraints pp triplets k b &&& checkNonNegativityConstraints ys &&& checkSizeLimit k b ys sizeLimit checkLayeredTerminationSat :: PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize checkLayeredTerminationSat pp triplets k = let makeYName i = (++) (genericReplicate i '\'') ys = [makeVarMapWith (makeYName i) \$ states pp | i <- [1..k]] b = makeVarMap \$ transitions pp in (minimizeMethod, \sizeLimit -> ("layered termination", "invariant", concat (map getNames ys) ++ getNames b, [], [], \fm -> checkLayeredTermination pp triplets k (fmap fm b) (map (fmap fm) ys) sizeLimit, \fm -> invariantFromAssignment pp k (fmap fm b) (map (fmap fm) ys))) minimizeMethod :: Int -> InvariantSize -> String minimizeMethod 1 (curYSize, _, _) = "number of states in y less than " ++ show (sum curYSize) 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) ++ " or same number of transitions and number of states in y less than " ++ show curYSize minimizeMethod 4 (_, curYMax, _) = "maximum coefficient in y is less than " ++ show (maximum curYMax) 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) minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last layer less than " ++ show (last curTSize) ++ " 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) minimizeMethod _ _ = error "minimization method not supported" checkSizeLimit :: Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool checkSizeLimit _ _ _ Nothing = true 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))) = ((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))) ) 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)))))) checkSizeLimit _ _ _ (Just (_, _)) = error "minimization method not supported" invariantFromAssignment :: PopulationProtocol -> Integer -> IMap Transition -> [IMap State] -> (LayeredTerminationInvariant, InvariantSize) invariantFromAssignment pp k b ys = (invariant, (map invariantLength invariant, map invariantMaxCoefficient invariant, map layerSize invariant)) where 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