Skip to content

GitLab

Commit 1e7250ba authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Merge branch 'update-sbv' into 'master' 

Update SBV

See merge request i7/peregrine!3
parents 6ca1dec4 dd8aab5e
Pipeline #202544 passed with stage
in 8 minutes and 29 seconds
Hide whitespace changes
Inline Side-by-side
Showing with 169 additions and 169 deletions
peregrine.cabal
View file @ 1e7250ba
......@@ -22,8 +22,8 @@ executable peregrine
main-is: Main.hs
other-modules:
-- 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
hs-source-dirs: src
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
src/Parser/PP.hs
View file @ 1e7250ba
......@@ -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
......
src/Solver.hs
View file @ 1e7250ba
......@@ -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
......
src/Solver/Formula.hs
View file @ 1e7250ba
......@@ -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
src/Solver/LayeredTermination.hs
View file @ 1e7250ba
......@@ -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"
......
src/Solver/ReachableTermConfigInConsensus.hs
View file @ 1e7250ba
......@@ -26,7 +26,7 @@ type ReachableTermConfigInConsensusCounterExample = (Configuration, Configuratio
stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
stateEquationConstraints pp m0 m x =
bAnd $ map checkStateEquation $ states pp
sAnd $ map checkStateEquation $ states pp
where checkStateEquation q =
let incoming = map addTransition $ lpre pp q
outgoing = map addTransition $ lpost pp q
......@@ -35,24 +35,24 @@ stateEquationConstraints pp m0 m x =
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
terminalConstraints :: PopulationProtocol -> SIMap State -> SBool
terminalConstraints pp m =
bAnd $ map checkTransition $ transitions pp
where checkTransition t = bOr $ map checkState $ lpre pp t
sAnd $ map checkTransition $ transitions pp
where checkTransition t = sOr $ map checkState $ lpre pp t
checkState (q,w) = val m q .<= literal (fromInteger (w - 1))
initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
initialConfiguration pp m0 =
(sum (mval m0 (initialStates pp)) .>= 2) &&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&&
(sum (mval m0 (initialStates pp)) .>= 2) .&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) .&&
(evaluateFormula (precondition pp) m0)
differentConsensusConstraints :: PopulationProtocol -> SIMap State -> SBool
differentConsensusConstraints pp m =
oT &&& oF
oT .&& oF
where
oT = sum (mval m (trueStates pp)) .> 0
oF = sum (mval m (falseStates pp)) .> 0
......@@ -71,36 +71,36 @@ sequenceIn u x = sum (mval x u) .> 0
checkUTrap :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> Trap -> SBool
checkUTrap pp m0 m1 x utrap =
(((sequenceIn upre x) &&& (sequenceNotIn uunmark x)) ==> (markedByConfiguration utrap m1))
(((sequenceIn upre x) .&& (sequenceNotIn uunmark x)) .=> (markedByConfiguration utrap m1))
where upost = mpost pp utrap
upre = mpre pp utrap
uunmark = upost \\ upre
checkUTrapConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> [Trap] -> SBool
checkUTrapConstraints pp m0 m1 x traps =
bAnd $ map (checkUTrap pp m0 m1 x) traps
sAnd $ map (checkUTrap pp m0 m1 x) traps
checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> Siphon -> SBool
checkUSiphon pp m0 m1 x usiphon =
(((sequenceIn upost x) &&& (sequenceNotIn umark x)) ==> (markedByConfiguration usiphon m0))
(((sequenceIn upost x) .&& (sequenceNotIn umark x)) .=> (markedByConfiguration usiphon m0))
where upost = mpost pp usiphon
upre = mpre pp usiphon
umark = upre \\ upost
checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> [Siphon] -> SBool
checkUSiphonConstraints pp m0 m1 x siphons =
bAnd $ map (checkUSiphon pp m0 m1 x) siphons
sAnd $ map (checkUSiphon pp m0 m1 x) siphons
checkReachableTermConfigInConsensus :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> RefinementObjects -> SBool
checkReachableTermConfigInConsensus pp m0 m1 x (utraps, usiphons) =
stateEquationConstraints pp m0 m1 x &&&
initialConfiguration pp m0 &&&
nonNegativityConstraints m0 &&&
nonNegativityConstraints m1 &&&
nonNegativityConstraints x &&&
terminalConstraints pp m1 &&&
differentConsensusConstraints pp m1 &&&
checkUTrapConstraints pp m0 m1 x utraps &&&
stateEquationConstraints pp m0 m1 x .&&
initialConfiguration pp m0 .&&
nonNegativityConstraints m0 .&&
nonNegativityConstraints m1 .&&
nonNegativityConstraints x .&&
terminalConstraints pp m1 .&&
differentConsensusConstraints pp m1 .&&
checkUTrapConstraints pp m0 m1 x utraps .&&
checkUSiphonConstraints pp m0 m1 x usiphons
checkReachableTermConfigInConsensusSat :: PopulationProtocol -> RefinementObjects -> ConstraintProblem Integer ReachableTermConfigInConsensusCounterExample
......@@ -121,27 +121,27 @@ counterExampleFromAssignment m0 m1 x =
trapConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
trapConstraint pp b t =
sum (mval b $ pre pp t) .> 0 ==> sum (mval b $ post pp t) .> 0
sum (mval b $ pre pp t) .> 0 .=> sum (mval b $ post pp t) .> 0
siphonConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
siphonConstraint pp b t =
sum (mval b $ post pp t) .> 0 ==> sum (mval b $ pre pp t) .> 0
sum (mval b $ post pp t) .> 0 .=> sum (mval b $ pre pp t) .> 0
trapConstraints :: PopulationProtocol -> SIMap State -> SBool
trapConstraints pp b =
bAnd $ map (trapConstraint pp b) $ transitions pp
sAnd $ map (trapConstraint pp b) $ transitions pp
siphonConstraints :: PopulationProtocol -> SIMap State -> SBool
siphonConstraints pp b =
bAnd $ map (siphonConstraint pp b) $ transitions pp
sAnd $ map (siphonConstraint pp b) $ transitions pp
uTrapConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
uTrapConstraints pp x b =
bAnd $ map (trapConstraint pp b) $ elems x
sAnd $ map (trapConstraint pp b) $ elems x
uSiphonConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
uSiphonConstraints pp x b =
bAnd $ map (siphonConstraint pp b) $ elems x
sAnd $ map (siphonConstraint pp b) $ elems x
statesMarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
......@@ -157,9 +157,9 @@ statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
noOutputTransitionEnabled pp m b =
bAnd $ map outputTransitionNotEnabled $ transitions pp
sAnd $ map outputTransitionNotEnabled $ transitions pp
where
outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
outputTransitionNotEnabled t = outputTransitionOfB t .=> transitionNotEnabledInB t
outputTransitionOfB t = sum [val b q | (q, w) <- lpre pp t, val m q >= w] .> 0
transitionNotEnabledInB t = sum [val b q | (q, w) <- lpre pp t, val m q < w] .> 0
......@@ -167,10 +167,10 @@ nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
checkBinary :: SIMap State -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
checkBinary = sAnd . map (\x -> x .== 0 .|| x .== 1) . vals
checkSizeLimit :: SIMap State -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit _ Nothing = sTrue
checkSizeLimit b (Just (1, curSize)) = (.< literal curSize) $ sumVal b
checkSizeLimit b (Just (2, curSize)) = (.> literal curSize) $ sumVal b
checkSizeLimit _ (Just (_, _)) = error "minimization method not supported"
......@@ -182,10 +182,10 @@ minimizeMethod _ _ = error "minimization method not supported"
findTrapConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrapConstraints pp (m0, m1, x) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
trapConstraints pp b &&&
statesPostsetOfSequence pp x b &&&
checkSizeLimit b sizeLimit .&&
checkBinary b .&&
trapConstraints pp b .&&
statesPostsetOfSequence pp x b .&&
statesUnmarkedByConfiguration pp m1 b
findTrapConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
......@@ -199,10 +199,10 @@ findTrapConstraintsSat pp c =
findUTrapConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findUTrapConstraints pp (m0, m1, x) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
statesPostsetOfSequence pp x b &&&
uTrapConstraints pp x b &&&
checkSizeLimit b sizeLimit .&&
checkBinary b .&&
statesPostsetOfSequence pp x b .&&
uTrapConstraints pp x b .&&
statesUnmarkedByConfiguration pp m1 b
findUTrapConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Trap Integer
......@@ -216,10 +216,10 @@ findUTrapConstraintsSat pp c =
findSiphonConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findSiphonConstraints pp (m0, m1, x) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
siphonConstraints pp b &&&
statesUnmarkedByConfiguration pp m0 b &&&
checkSizeLimit b sizeLimit .&&
checkBinary b .&&
siphonConstraints pp b .&&
statesUnmarkedByConfiguration pp m0 b .&&
statesPresetOfSequence pp x b
findSiphonConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
......@@ -234,10 +234,10 @@ findSiphonConstraintsSat pp c =
findUSiphonConstraints :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findUSiphonConstraints pp (m0, m1, x) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
statesUnmarkedByConfiguration pp m0 b &&&
statesPresetOfSequence pp x b &&&
checkSizeLimit b sizeLimit .&&
checkBinary b .&&
statesUnmarkedByConfiguration pp m0 b .&&
statesPresetOfSequence pp x b .&&
uSiphonConstraints pp x b
findUSiphonConstraintsSat :: PopulationProtocol -> ReachableTermConfigInConsensusCounterExample -> MinConstraintProblem Integer Siphon Integer
......
src/Solver/StrongConsensus.hs
View file @ 1e7250ba
......@@ -29,7 +29,7 @@ type RefinementObjects = ([Trap], [Siphon])
stateEquationConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap Transition -> SBool
stateEquationConstraints pp m0 m x =
bAnd $ map checkStateEquation $ states pp
sAnd $ map checkStateEquation $ states pp
where checkStateEquation q =
let incoming = map addTransition $ lpre pp q
outgoing = map addTransition $ lpost pp q
......@@ -38,33 +38,33 @@ stateEquationConstraints pp m0 m x =
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
terminalConstraints :: PopulationProtocol -> SIMap State -> SBool
terminalConstraints pp m =
bAnd $ map checkTransition $ transitions pp
where checkTransition t = bOr $ map checkState $ lpre pp t
sAnd $ map checkTransition $ transitions pp
where checkTransition t = sOr $ map checkState $ lpre pp t
checkState (q,w) = val m q .<= literal (fromInteger (w - 1))
initialConfiguration :: PopulationProtocol -> SIMap State -> SBool
initialConfiguration pp m0 =
(sum (mval m0 (initialStates pp)) .>= 2) &&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) &&&
(sum (mval m0 (initialStates pp)) .>= 2) .&&
(sum (mval m0 (states pp \\ initialStates pp)) .== 0) .&&
(evaluateFormula (precondition pp) m0)
differentConsensusConstraints :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
SIMap State -> SIMap State -> SIMap State -> SIMap State -> SBool
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 pVars =
(oT &&& oF) |||
(if checkCorrectness then correctnessConstraints else false)
(oT .&& oF) .||
(if checkCorrectness then correctnessConstraints else sFalse)
where
oT = sum (mval m1 (trueStates pp)) .> 0
oF = sum (mval m2 (falseStates pp)) .> 0
correctnessConstraints =
let oPT = evaluateFormula pT (M.union m0 pVars)
oPF = evaluateFormula pF (M.union m0 pVars)
in (oPT &&& oF) ||| (oPF &&& oT)
in (oPT .&& oF) .|| (oPF .&& oT)
unmarkedByConfiguration :: [State] -> SIMap State -> SBool
unmarkedByConfiguration r m = sum (mval m r) .== 0
......@@ -80,44 +80,44 @@ sequenceIn u x = sum (mval x u) .> 0
checkUTrap :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Trap -> SBool
checkUTrap pp m0 m1 m2 x1 x2 utrap =
(((sequenceIn upre x1) &&& (sequenceNotIn uunmark x1)) ==> (markedByConfiguration utrap m1)) &&&
(((sequenceIn upre x2) &&& (sequenceNotIn uunmark x2)) ==> (markedByConfiguration utrap m2))
(((sequenceIn upre x1) .&& (sequenceNotIn uunmark x1)) .=> (markedByConfiguration utrap m1)) .&&
(((sequenceIn upre x2) .&& (sequenceNotIn uunmark x2)) .=> (markedByConfiguration utrap m2))
where upost = mpost pp utrap
upre = mpre pp utrap
uunmark = upost \\ upre
checkUTrapConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Trap] -> SBool
checkUTrapConstraints pp m0 m1 m2 x1 x2 traps =
bAnd $ map (checkUTrap pp m0 m1 m2 x1 x2) traps
sAnd $ map (checkUTrap pp m0 m1 m2 x1 x2) traps
checkUSiphon :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> Siphon -> SBool
checkUSiphon pp m0 m1 m2 x1 x2 usiphon =
(((sequenceIn upost x1) &&& (sequenceNotIn umark x1)) ==> (markedByConfiguration usiphon m0)) &&&
(((sequenceIn upost x2) &&& (sequenceNotIn umark x2)) ==> (markedByConfiguration usiphon m0))
(((sequenceIn upost x1) .&& (sequenceNotIn umark x1)) .=> (markedByConfiguration usiphon m0)) .&&
(((sequenceIn upost x2) .&& (sequenceNotIn umark x2)) .=> (markedByConfiguration usiphon m0))
where upost = mpost pp usiphon
upre = mpre pp usiphon
umark = upre \\ upost
checkUSiphonConstraints :: PopulationProtocol -> SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition -> [Siphon] -> SBool
checkUSiphonConstraints pp m0 m1 m2 x1 x2 siphons =
bAnd $ map (checkUSiphon pp m0 m1 m2 x1 x2) siphons
sAnd $ map (checkUSiphon pp m0 m1 m2 x1 x2) siphons
checkStrongConsensus :: Bool -> PopulationProtocol -> Formula State -> Formula State ->
SIMap State -> SIMap State -> SIMap State -> SIMap Transition -> SIMap Transition ->
SIMap State -> RefinementObjects -> SBool
checkStrongConsensus checkCorrectness pp pT pF m0 m1 m2 x1 x2 pVars (utraps, usiphons) =
stateEquationConstraints pp m0 m1 x1 &&&
stateEquationConstraints pp m0 m2 x2 &&&
initialConfiguration pp m0 &&&
nonNegativityConstraints m0 &&&
nonNegativityConstraints m1 &&&
nonNegativityConstraints m2 &&&
nonNegativityConstraints x1 &&&
nonNegativityConstraints x2 &&&
terminalConstraints pp m1 &&&
terminalConstraints pp m2 &&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 pVars &&&
checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps &&&
stateEquationConstraints pp m0 m1 x1 .&&
stateEquationConstraints pp m0 m2 x2 .&&
initialConfiguration pp m0 .&&
nonNegativityConstraints m0 .&&
nonNegativityConstraints m1 .&&
nonNegativityConstraints m2 .&&
nonNegativityConstraints x1 .&&
nonNegativityConstraints x2 .&&
terminalConstraints pp m1 .&&
terminalConstraints pp m2 .&&
differentConsensusConstraints checkCorrectness pp pT pF m0 m1 m2 pVars .&&
checkUTrapConstraints pp m0 m1 m2 x1 x2 utraps .&&
checkUSiphonConstraints pp m0 m1 m2 x1 x2 usiphons
makePredicates :: PopulationProtocol -> (Formula State, Formula State, [State])
......@@ -151,27 +151,27 @@ counterExampleFromAssignment m0 m1 m2 x1 x2 =
trapConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
trapConstraint pp b t =
sum (mval b $ pre pp t) .> 0 ==> sum (mval b $ post pp t) .> 0
sum (mval b $ pre pp t) .> 0 .=> sum (mval b $ post pp t) .> 0
siphonConstraint :: PopulationProtocol -> SIMap State -> Transition -> SBool
siphonConstraint pp b t =
sum (mval b $ post pp t) .> 0 ==> sum (mval b $ pre pp t) .> 0
sum (mval b $ post pp t) .> 0 .=> sum (mval b $ pre pp t) .> 0
trapConstraints :: PopulationProtocol -> SIMap State -> SBool
trapConstraints pp b =
bAnd $ map (trapConstraint pp b) $ transitions pp
sAnd $ map (trapConstraint pp b) $ transitions pp
siphonConstraints :: PopulationProtocol -> SIMap State -> SBool
siphonConstraints pp b =
bAnd $ map (siphonConstraint pp b) $ transitions pp
sAnd $ map (siphonConstraint pp b) $ transitions pp
uTrapConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
uTrapConstraints pp x b =
bAnd $ map (trapConstraint pp b) $ elems x
sAnd $ map (trapConstraint pp b) $ elems x
uSiphonConstraints :: PopulationProtocol -> FlowVector -> SIMap State -> SBool
uSiphonConstraints pp x b =
bAnd $ map (siphonConstraint pp b) $ elems x
sAnd $ map (siphonConstraint pp b) $ elems x
statesMarkedByConfiguration :: PopulationProtocol -> Configuration -> SIMap State -> SBool
statesMarkedByConfiguration pp m b = sum (mval b $ elems m) .> 0
......@@ -187,9 +187,9 @@ statesPresetOfSequence pp x b = sum (mval b $ mpre pp $ elems x) .> 0
noOutputTransitionEnabled :: PopulationProtocol -> Configuration -> SIMap State -> SBool
noOutputTransitionEnabled pp m b =
bAnd $ map outputTransitionNotEnabled $ transitions pp
sAnd $ map outputTransitionNotEnabled $ transitions pp
where
outputTransitionNotEnabled t = outputTransitionOfB t ==> transitionNotEnabledInB t
outputTransitionNotEnabled t = outputTransitionOfB t .=> transitionNotEnabledInB t
outputTransitionOfB t = sum [val b q | (q, w) <- lpre pp t, val m q >= w] .> 0
transitionNotEnabledInB t = sum [val b q | (q, w) <- lpre pp t, val m q < w] .> 0
......@@ -197,10 +197,10 @@ nonemptySet :: (Ord a, Show a) => SIMap a -> SBool
nonemptySet b = sum (vals b) .> 0
checkBinary :: SIMap State -> SBool
checkBinary = bAnd . map (\x -> x .== 0 ||| x .== 1) . vals
checkBinary = sAnd . map (\x -> x .== 0 .|| x .== 1) . vals
checkSizeLimit :: SIMap State -> Maybe (Int, Integer) -> SBool
checkSizeLimit _ Nothing = true
checkSizeLimit _ Nothing = sTrue
checkSizeLimit b (Just (1, curSize)) = (.< literal curSize) $ sumVal b
checkSizeLimit b (Just (2, curSize)) = (.> literal curSize) $ sumVal b
checkSizeLimit _ (Just (_, _)) = error "minimization method not supported"
......@@ -212,12 +212,12 @@ minimizeMethod _ _ = error "minimization method not supported"
findTrapConstraints :: PopulationProtocol -> StrongConsensusCounterExample -> SIMap State -> Maybe (Int, Integer) -> SBool
findTrapConstraints pp (m0, m1, m2, x1, x2) b sizeLimit =
checkSizeLimit b sizeLimit &&&
checkBinary b &&&
trapConstraints pp b &&&
checkSizeLimit b sizeLimit .&&
checkBinary b .&&
trapConstraints pp b .&&
(
(statesPostsetOfSequence pp x1 b &&& statesUnmarkedByConfiguration pp m1 b) |||
(statesPostsetOfSequence pp x2 b &&& statesUnmarkedByConfiguration pp m2 b)
(statesPostsetOfSequence pp x1 b .&& statesUnmarkedByConfiguration pp m1 b) .||
(statesPostsetOfSequence pp x2 b .&& statesUnmarkedByConfiguration pp m2 b)
)