24.09., 9:00 - 11:00: Due to updates GitLab will be unavailable for some minutes between 09:00 and 11:00.

...
 
Commits (4)
...@@ -22,8 +22,8 @@ executable peregrine ...@@ -22,8 +22,8 @@ executable peregrine
main-is: Main.hs main-is: Main.hs
other-modules: other-modules:
-- other-extensions: -- other-extensions:
build-depends: base >=4 && <5, sbv == 7.13, parsec >= 3.1, containers, transformers, build-depends: base >=4 && <5, sbv, parsec >= 3.1, containers, transformers,
bytestring, mtl, stm, async, text, aeson bytestring, mtl, stm, async, text, aeson
hs-source-dirs: src hs-source-dirs: src
default-language: Haskell2010 default-language: Haskell2010
ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N ghc-options: -fsimpl-tick-factor=1000 -threaded -rtsopts -with-rtsopts=-N -dynamic
...@@ -6,7 +6,7 @@ module Parser.PP ...@@ -6,7 +6,7 @@ module Parser.PP
(parseContent) (parseContent)
where where
import Data.Aeson import Data.Aeson (FromJSON, ToJSON, toJSON, parseJSON, Value(String), eitherDecode)
import Data.Aeson.TH (deriveJSON, defaultOptions) import Data.Aeson.TH (deriveJSON, defaultOptions)
import Control.Applicative ((<*),(*>),(<$>)) import Control.Applicative ((<*),(*>),(<$>))
import Data.Functor.Identity import Data.Functor.Identity
......
...@@ -18,13 +18,13 @@ type ConstraintProblem a b = ...@@ -18,13 +18,13 @@ type ConstraintProblem a b =
type MinConstraintProblem a b c = type MinConstraintProblem a b c =
(Int -> c -> String, Maybe (Int, c) -> ConstraintProblem 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) Maybe (Model a)
rebuildModel _ (Left _) = Nothing rebuildModel _ (Left _) = Nothing
rebuildModel _ (Right (True, _)) = error "Prover returned unknown" rebuildModel _ (Right (True, _)) = error "Prover returned unknown"
rebuildModel vars (Right (False, m)) = Just $ M.fromList $ vars `zip` m 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 Symbolic SBool
symConstraints vars constraint = do symConstraints vars constraint = do
syms <- mapM exists vars syms <- mapM exists vars
...@@ -39,7 +39,7 @@ getSolverConfig Options.CVC4 verbose = ...@@ -39,7 +39,7 @@ getSolverConfig Options.CVC4 verbose =
solver = (solver cvc4) { Data.SBV.options = const ["--lang", "smt", "--incremental", "--no-interactive-prompt"] } 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) ConstraintProblem a b -> OptIO (Maybe b)
checkSat (problemName, resultName, vars, constraint, interpretation) = do checkSat (problemName, resultName, vars, constraint, interpretation) = do
verbosePut 2 $ "Checking SAT of " ++ problemName verbosePut 2 $ "Checking SAT of " ++ problemName
...@@ -58,7 +58,7 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do ...@@ -58,7 +58,7 @@ checkSat (problemName, resultName, vars, constraint, interpretation) = do
verbosePut 4 $ "- raw model: " ++ show rawModel verbosePut 4 $ "- raw model: " ++ show rawModel
return $ Just model 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) MinConstraintProblem a b c -> OptIO (Maybe b)
checkSatMin (minMethod, minProblem) = do checkSatMin (minMethod, minProblem) = do
optMin <- opt optMinimizeRefinement optMin <- opt optMinimizeRefinement
......
...@@ -27,10 +27,10 @@ opToFunction (ModEq _) = error "symbolic modulo not supported" ...@@ -27,10 +27,10 @@ opToFunction (ModEq _) = error "symbolic modulo not supported"
opToFunction (ModNe _) = error "symbolic modulo not supported" opToFunction (ModNe _) = error "symbolic modulo not supported"
evaluateFormula :: (Ord a, Show a) => Formula a -> SIMap a -> SBool evaluateFormula :: (Ord a, Show a) => Formula a -> SIMap a -> SBool
evaluateFormula FTrue _ = true evaluateFormula FTrue _ = sTrue
evaluateFormula FFalse _ = false evaluateFormula FFalse _ = sFalse
evaluateFormula (Equation lhs op rhs) m = evaluateFormula (Equation lhs op rhs) m =
opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m) opToFunction op (evaluateTerm lhs m) (evaluateTerm rhs m)
evaluateFormula (Neg p) m = bnot $ evaluateFormula p 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
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 ...@@ -31,49 +31,49 @@ instance Show LayerInvariant where
nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool nonNegativityConstraints :: (Ord a, Show a) => SIMap a -> SBool
nonNegativityConstraints m = nonNegativityConstraints m =
bAnd $ map checkVal $ vals m sAnd $ map checkVal $ vals m
where checkVal x = x .>= 0 where checkVal x = x .>= 0
checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool checkNonNegativityConstraints :: (Ord a, Show a) => [SIMap a] -> SBool
checkNonNegativityConstraints xs = checkNonNegativityConstraints xs =
bAnd $ map nonNegativityConstraints xs sAnd $ map nonNegativityConstraints xs
layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool layerTerminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> SIMap State -> SBool
layerTerminationConstraints pp i b y = layerTerminationConstraints pp i b y =
bAnd $ map checkTransition $ transitions pp sAnd $ map checkTransition $ transitions pp
where checkTransition t = where checkTransition t =
let incoming = map addState $ lpre pp t let incoming = map addState $ lpre pp t
outgoing = map addState $ lpost 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 addState (q, w) = literal w * val y q
terminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> [SIMap State] -> SBool terminationConstraints :: PopulationProtocol -> Integer -> SIMap Transition -> [SIMap State] -> SBool
terminationConstraints pp k b ys = 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 :: PopulationProtocol -> Integer -> SIMap Transition -> SBool
layerConstraints pp k b = layerConstraints pp k b =
bAnd $ map checkLayer $ transitions pp sAnd $ map checkLayer $ transitions pp
where checkLayer t = literal 1 .<= val b t &&& val b t .<= literal k where checkLayer t = literal 1 .<= val b t .&& val b t .<= literal k
deterministicLayerConstraints :: PopulationProtocol -> SIMap Transition -> SBool deterministicLayerConstraints :: PopulationProtocol -> SIMap Transition -> SBool
deterministicLayerConstraints pp b = 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) where checkTransition (t1,t2) = (val b t1 .== val b t2)
samePreset (t1,t2) = (lpre pp t1 == lpre pp t2) samePreset (t1,t2) = (lpre pp t1 == lpre pp t2)
layerOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool layerOrderConstraints :: PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> SBool
layerOrderConstraints pp triplets k b = layerOrderConstraints pp triplets k b =
bAnd $ map checkTriplet triplets sAnd $ map checkTriplet triplets
where checkTriplet (s,t,ts) = (val b s .> val b t) ==> bOr (map (\t' -> val b t' .== val b t) ts) 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 :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool
checkLayeredTermination deterministic pp triplets k b ys sizeLimit = checkLayeredTermination deterministic pp triplets k b ys sizeLimit =
layerConstraints pp k b &&& layerConstraints pp k b .&&
(if deterministic then deterministicLayerConstraints pp b else true) &&& (if deterministic then deterministicLayerConstraints pp b else sTrue) .&&
terminationConstraints pp k b ys &&& terminationConstraints pp k b ys .&&
layerOrderConstraints pp triplets k b &&& layerOrderConstraints pp triplets k b .&&
checkNonNegativityConstraints ys &&& checkNonNegativityConstraints ys .&&
checkSizeLimit k b ys sizeLimit checkSizeLimit k b ys sizeLimit
checkLayeredTerminationSat :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize checkLayeredTerminationSat :: Bool -> PopulationProtocol -> [Triplet] -> Integer -> MinConstraintProblem Integer LayeredTerminationInvariant InvariantSize
...@@ -101,24 +101,24 @@ minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last ...@@ -101,24 +101,24 @@ minimizeMethod 6 (curYSize, curYMax, curTSize) = "number of transitions in last
minimizeMethod _ _ = error "minimization method not supported" minimizeMethod _ _ = error "minimization method not supported"
checkSizeLimit :: Integer -> SIMap Transition -> [SIMap State] -> Maybe (Int, InvariantSize) -> SBool 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 (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 (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))) = 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))) (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 (4, (_, curYMax, _))) = ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax)))
checkSizeLimit k b ys (Just (5, (curYSize, 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)))) ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax))))
checkSizeLimit k b ys (Just (6, (curYSize, curYMax, curTSize))) = 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 (\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 (\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)))))) ((foldl smax 0 (concatMap vals ys)) .< literal (fromIntegral (maximum curYMax))))))
checkSizeLimit _ _ _ (Just (_, _)) = error "minimization method not supported" checkSizeLimit _ _ _ (Just (_, _)) = error "minimization method not supported"
......
This diff is collapsed.