LayeredTermination.hs

{-# 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 ->
            ("terminal marking reachable", "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