Commit 7aa92317 authored by Philipp Meyer's avatar Philipp Meyer

Update for newer SBV and Aeson versions

parent 1488bd45
......@@ -6,7 +6,7 @@ module Parser.PP
(parseContent)
where
import Data.Aeson
import Data.Aeson (FromJSON, ToJSON, toJSON, parseJSON, Value(String), eitherDecode)
import Data.Aeson.TH (deriveJSON, defaultOptions)
import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity
......
......@@ -18,13 +18,13 @@ type ConstraintProblem a b =
type MinConstraintProblem a b c =
(Int -> c -> String, Maybe (Int, c) -> ConstraintProblem a (b, c))
rebuildModel :: SymWord a => [String] -> Either String (Bool, [a]) ->
rebuildModel :: SymVal a => [String] -> Either String (Bool, [a]) ->
Maybe (Model a)
rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m
symConstraints :: SymWord a => [String] -> ((String -> SBV a) -> SBool) ->
symConstraints :: SymVal a => [String] -> ((String -> SBV a) -> SBool) ->
Symbolic SBool
symConstraints vars constraint = do
syms <- mapM exists vars
......@@ -39,7 +39,7 @@ getSolverConfig Options.CVC4 verbose =
solver = (solver cvc4) { Data.SBV.options = const ["--lang", "smt", "--incremental", "--no-interactive-prompt"] }
}
checkSat :: (SatModel a, SymWord a, Show a, Show b) =>
checkSat :: (SatModel a, SymVal a, Show a, Show b) =>
ConstraintProblem a b -> OptIO (Maybe b)
checkSat (problemName, resultName, vars, constraint, interpretation) = do
verbosePut 2 $ "Checking SAT of " ++ problemName
......@@ -58,7 +58,7 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do
verbosePut 4 $ "- raw model: " ++ show rawModel
return $ Just model
checkSatMin :: (SatModel a, SymWord a, Show a, Show b, Show c) =>
checkSatMin :: (SatModel a, SymVal a, Show a, Show b, Show c) =>
MinConstraintProblem a b c -> OptIO (Maybe b)
checkSatMin (minMethod, minProblem) = do
optMin <- opt optMinimizeRefinement
......
......@@ -27,10 +27,10 @@ opToFunction (ModEq _) = error "symbolic modulo not supported"
opToFunction (ModNe _) = error "symbolic modulo not supported"
evaluateFormula :: (Ord a, Show a) => Formula a -> SIMap a -> SBool
evaluateFormula FTrue _ = true
evaluateFormula FFalse _ = false
evaluateFormula FTrue _ = sTrue
evaluateFormula FFalse _ = sFalse
evaluateFormula (Equation lhs op rhs) m =
opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m)
evaluateFormula (Neg p) m = bnot $ evaluateFormula p m
evaluateFormula (p :&: q) m = evaluateFormula p m &&& evaluateFormula q m
evaluateFormula (p :|: q) m = evaluateFormula p m ||| evaluateFormula q m
evaluateFormula (Neg p) m = sNot $ evaluateFormula p m
evaluateFormula (p :&: q) m = evaluateFormula p m .&& evaluateFormula q m
evaluateFormula (p :|: q) m = evaluateFormula p m .|| evaluateFormula q m
......@@ -31,49 +31,49 @@ instance Show LayerInvariant where
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints m =
bAnd $ map checkVal $ vals m
sAnd $ map checkVal $ vals m
where checkVal x = x .>= 0
checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool
checkNonNegativityConstraints xs =
bAnd $ map nonNegativityConstraints xs
sAnd $ map nonNegativityConstraints xs
layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool
layerTerminationConstraints pp i b y =
bAnd $ map checkTransition $ transitions pp
sAnd $ 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)
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]
sAnd $ [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
sAnd $ map checkLayer $ transitions pp
where checkLayer t = literal 1 .<= val b t .&& val b t .<= literal k
deterministicLayerConstraints :: PopulationProtocol -> SIMap Transition -> SBool
deterministicLayerConstraints pp b =
bAnd $ map checkTransition [ (t1,t2) | t1 <- transitions pp, t2 <- transitions pp, t1 /= t2, samePreset (t1,t2) ]
sAnd $ map checkTransition [ (t1,t2) | t1 <- transitions pp, t2 <- transitions pp, t1 /= t2, samePreset (t1,t2) ]
where checkTransition (t1,t2) = (val b t1 .== val b t2)
samePreset (t1,t2) = (lpre pp t1 == lpre pp t2)
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)
sAnd $ map checkTriplet triplets
where checkTriplet (s,t,ts) = (val b s .> val b t) .=> sOr (map (\t' -> val b t' .== val b t) ts)
checkLayeredTermination :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
checkLayeredTermination deterministic pp triplets k b ys sizeLimit =
layerConstraints pp k b &&&
(if deterministic then deterministicLayerConstraints pp b else true) &&&
terminationConstraints pp k b ys &&&
layerOrderConstraints pp triplets k b &&&
checkNonNegativityConstraints ys &&&
layerConstraints pp k b .&&
(if deterministic then deterministicLayerConstraints pp b else sTrue) .&&
terminationConstraints pp k b ys .&&
layerOrderConstraints pp triplets k b .&&
checkNonNegativityConstraints ys .&&
checkSizeLimit k b ys sizeLimit
checkLayeredTerminationSat :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize
......@@ -101,24 +101,24 @@ minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last
minimizeMethod _ _ = error "minimization method not supported"
checkSizeLimit :: Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
checkSizeLimit _ _ _ Nothing = true
checkSizeLimit _ _ _ Nothing = sTrue
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 (\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))) &&&
(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))) &&&
((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"
......
This diff is collapsed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment