diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 45dcc5e36..c1dcf8c09 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -32,7 +32,7 @@ namespace storm { PcaaObjective& currentObjective = result.objectives.back(); currentObjective.originalFormula = subFormula; if(currentObjective.originalFormula->isOperatorFormula()) { - preprocessFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); + preprocessOperatorFormula(currentObjective.originalFormula->asOperatorFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the subformula " << *subFormula << " of " << originalFormula << " because it is not supported"); } @@ -93,7 +93,7 @@ namespace storm { } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { // Get a unique name for the new reward model. currentObjective.rewardModelName = "objective" + std::to_string(result.objectives.size()); @@ -124,11 +124,11 @@ namespace storm { } if(formula.isProbabilityOperatorFormula()){ - preprocessFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); + preprocessProbabilityOperatorFormula(formula.asProbabilityOperatorFormula(), result, currentObjective); } else if(formula.isRewardOperatorFormula()){ - preprocessFormula(formula.asRewardOperatorFormula(), result, currentObjective); + preprocessRewardOperatorFormula(formula.asRewardOperatorFormula(), result, currentObjective); } else if(formula.isTimeOperatorFormula()){ - preprocessFormula(formula.asTimeOperatorFormula(), result, currentObjective); + preprocessTimeOperatorFormula(formula.asTimeOperatorFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Could not preprocess the objective " << formula << " because it is not supported"); } @@ -140,52 +140,52 @@ namespace storm { } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { if(formula.getSubformula().isUntilFormula()){ - preprocessFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); + preprocessUntilFormula(formula.getSubformula().asUntilFormula(), result, currentObjective); } else if(formula.getSubformula().isBoundedUntilFormula()){ - preprocessFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); + preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), result, currentObjective); } else if(formula.getSubformula().isGloballyFormula()){ - preprocessFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); + preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), result, currentObjective); } else if(formula.getSubformula().isEventuallyFormula()){ - preprocessFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { // Check if the reward model is uniquely specified STORM_LOG_THROW((formula.hasRewardModelName() && result.preprocessedModel.hasRewardModel(formula.getRewardModelName())) || result.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model."); if(formula.getSubformula().isEventuallyFormula()){ - preprocessFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective, formula.getOptionalRewardModelName()); } else if(formula.getSubformula().isCumulativeRewardFormula()) { - preprocessFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); + preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); } else if(formula.getSubformula().isTotalRewardFormula()) { - preprocessFormula(formula.getSubformula().asTotalRewardFormula(), result, currentObjective, formula.getOptionalRewardModelName()); + preprocessTotalRewardFormula(result, currentObjective, formula.getOptionalRewardModelName()); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { // Time formulas are only supported for Markov automata STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); if(formula.getSubformula().isEventuallyFormula()){ - preprocessFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); + preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), result, currentObjective); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { CheckTask phiTask(formula.getLeftSubformula()); CheckTask psiTask(formula.getRightSubformula()); storm::modelchecker::SparsePropositionalModelChecker mc(result.preprocessedModel); @@ -223,7 +223,7 @@ namespace storm { } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { if(formula.hasDiscreteTimeBound()) { currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getDiscreteTimeBound()); @@ -240,11 +240,11 @@ namespace storm { } currentObjective.upperTimeBound = storm::utility::convertNumber(formula.getIntervalBounds().second); } - preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); + preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), result, currentObjective); } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { + void SparsePcaaPreprocessor::preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective) { // The formula will be transformed to an until formula for the complementary event. // If the original formula minimizes, the complementary one will maximize and vice versa. // Hence, the decision whether to consider positive or negative rewards flips. @@ -255,13 +255,13 @@ namespace storm { auto negatedSubformula = std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, formula.getSubformula().asSharedPointer()); - preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), result, currentObjective); + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), negatedSubformula), result, currentObjective); } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { + void SparsePcaaPreprocessor::preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { if(formula.isReachabilityProbabilityFormula()){ - preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); + preprocessUntilFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), result, currentObjective); return; } @@ -304,7 +304,7 @@ namespace storm { } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { + void SparsePcaaPreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(result.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << "."); STORM_LOG_THROW(formula.getDiscreteTimeBound()>0, storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a positive discrete time bound but got " << formula << "."); @@ -324,7 +324,7 @@ namespace storm { } template - void SparsePcaaPreprocessor::preprocessFormula(storm::logic::TotalRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { + void SparsePcaaPreprocessor::preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName) { RewardModelType objectiveRewards = result.preprocessedModel.getRewardModel(optionalRewardModelName ? optionalRewardModelName.get() : ""); objectiveRewards.reduceToStateBasedRewards(result.preprocessedModel.getTransitionMatrix(), false); if(!currentObjective.rewardsArePositive){ @@ -341,7 +341,7 @@ namespace storm { template void SparsePcaaPreprocessor::analyzeEndComponents(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { - + result.ecActions = storm::storage::BitVector(result.preprocessedModel.getNumberOfChoices(), false); std::vector ecs; auto mecDecomposition = storm::storage::MaximalEndComponentDecomposition(result.preprocessedModel.getTransitionMatrix(), backwardTransitions); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h index b5209d4ff..fb35fa9d1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.h @@ -50,16 +50,16 @@ namespace storm { * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective * @param optionalRewardModelName the reward model name that is considered for the formula (if available) */ - static void preprocessFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); - static void preprocessFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); - static void preprocessFormula(storm::logic::TotalRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessOperatorFormula(storm::logic::OperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessRewardOperatorFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective); + static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessTotalRewardFormula(ReturnType& result, PcaaObjective& currentObjective, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. /*! * Analyzes the end components of the preprocessed model. That is: diff --git a/src/storm/modelchecker/region/ApproximationModel.cpp b/src/storm/modelchecker/region/ApproximationModel.cpp index 8b82b5002..9646193f6 100644 --- a/src/storm/modelchecker/region/ApproximationModel.cpp +++ b/src/storm/modelchecker/region/ApproximationModel.cpp @@ -57,7 +57,7 @@ namespace storm { //Now pre-compute the information for the equation system. initializeProbabilities(parametricModel, newIndices); if(this->computeRewards){ - initializeRewards(parametricModel, newIndices); + initializeRewards(parametricModel); } this->matrixData.assignment.shrink_to_fit(); this->vectorData.assignment.shrink_to_fit(); @@ -198,7 +198,7 @@ namespace storm { } template - void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices){ + void ApproximationModel::initializeRewards(ParametricSparseModelType const& parametricModel){ STORM_LOG_DEBUG("Approximation model initialization for Rewards"); //Note: Since the original model is assumed to be a DTMC, there is no outgoing transition of a maybeState that leads to an infinity state. //Hence, we do not have to set entries of the eqSys vector to infinity (as it would be required for mdp model checking...) diff --git a/src/storm/modelchecker/region/ApproximationModel.h b/src/storm/modelchecker/region/ApproximationModel.h index 5d707580e..986c555bd 100644 --- a/src/storm/modelchecker/region/ApproximationModel.h +++ b/src/storm/modelchecker/region/ApproximationModel.h @@ -81,7 +81,7 @@ namespace storm { typedef typename std::unordered_map::value_type FunctionEntry; void initializeProbabilities(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); - void initializeRewards(ParametricSparseModelType const& parametricModel, std::vector const& newIndices); + void initializeRewards(ParametricSparseModelType const& parametricModel); void initializePlayer1Matrix(ParametricSparseModelType const& parametricModel); void instantiate(ParameterRegion const& region, bool computeLowerBounds); void invokeSolver(bool computeLowerBounds, storm::storage::TotalScheduler& scheduler, bool allowEarlyTermination); diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp index 5ef4cd589..31d4d5f79 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.cpp @@ -253,19 +253,19 @@ namespace storm { } template - bool SparseMdpRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction) { - if(this->checkFormulaOnSamplingPoint(point)){ - if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){ - region.setSatPoint(point); - if(region.getCheckResult()==RegionCheckResult::EXISTSVIOLATED){ - region.setCheckResult(RegionCheckResult::EXISTSBOTH); - return true; - } - region.setCheckResult(RegionCheckResult::EXISTSSAT); - } - } - else{ - if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){ + bool SparseMdpRegionModelChecker::checkPoint(ParameterRegion& region, std::mapconst& point, bool /*favorViaFunction*/) { + if(this->checkFormulaOnSamplingPoint(point)){ + if (region.getCheckResult()!=RegionCheckResult::EXISTSSAT){ + region.setSatPoint(point); + if(region.getCheckResult()==RegionCheckResult::EXISTSVIOLATED){ + region.setCheckResult(RegionCheckResult::EXISTSBOTH); + return true; + } + region.setCheckResult(RegionCheckResult::EXISTSSAT); + } + } + else{ + if (region.getCheckResult()!=RegionCheckResult::EXISTSVIOLATED){ region.setViolatedPoint(point); if(region.getCheckResult()==RegionCheckResult::EXISTSSAT){ region.setCheckResult(RegionCheckResult::EXISTSBOTH); @@ -278,7 +278,7 @@ namespace storm { } template - bool SparseMdpRegionModelChecker::checkSmt(ParameterRegion& region) { + bool SparseMdpRegionModelChecker::checkSmt(ParameterRegion& /*region*/) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "checkSmt invoked but smt solving has not been implemented for MDPs."); } diff --git a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h index e772bad95..54f63a598 100644 --- a/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h +++ b/src/storm/modelchecker/region/SparseMdpRegionModelChecker.h @@ -67,7 +67,7 @@ namespace storm { * * @return true if an violated point as well as a sat point has been found, i.e., the check result is changed to EXISTSOTH */ - virtual bool checkPoint(ParameterRegion& region, std::mapconst& point, bool favorViaFunction=false); + virtual bool checkPoint(ParameterRegion& region, std::mapconst& point, bool /*favorViaFunction*/); /*! * Starts the SMTSolver to get the result. @@ -77,7 +77,7 @@ namespace storm { * A Sat- or Violated point is set, if the solver has found one (not yet implemented!). * The region checkResult of the given region is changed accordingly. */ - virtual bool checkSmt(ParameterRegion& region); + virtual bool checkSmt(ParameterRegion& /*region*/); }; } //namespace region diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp index 790f9395c..e98ba6485 100644 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp @@ -115,7 +115,7 @@ namespace storm { template SparseRegionModelCheckerSettings const& SparseRegionModelChecker::getSettings() const { return this->settings; - }; + } diff --git a/src/storm/solver/SmtlibSmtSolver.cpp b/src/storm/solver/SmtlibSmtSolver.cpp index e6295993e..de33d4f0b 100644 --- a/src/storm/solver/SmtlibSmtSolver.cpp +++ b/src/storm/solver/SmtlibSmtSolver.cpp @@ -23,7 +23,7 @@ namespace storm { namespace solver { - SmtlibSmtSolver::SmtlibModelReference::SmtlibModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager) { + SmtlibSmtSolver::SmtlibModelReference::SmtlibModelReference(storm::expressions::ExpressionManager const& manager) : ModelReference(manager) { // Intentionally left empty. } diff --git a/src/storm/solver/SmtlibSmtSolver.h b/src/storm/solver/SmtlibSmtSolver.h index 8fdad3686..5c4d86158 100644 --- a/src/storm/solver/SmtlibSmtSolver.h +++ b/src/storm/solver/SmtlibSmtSolver.h @@ -22,15 +22,11 @@ namespace storm { class SmtlibModelReference : public SmtSolver::ModelReference { public: - SmtlibModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter); + SmtlibModelReference(storm::expressions::ExpressionManager const& manager); virtual bool getBooleanValue(storm::expressions::Variable const& variable) const override; virtual int_fast64_t getIntegerValue(storm::expressions::Variable const& variable) const override; virtual double getRationalValue(storm::expressions::Variable const& variable) const override; - private: - - // The expression adapter that is used to translate the variable names. - //storm::adapters::Smt2ExpressionAdapter& expressionAdapter; }; public: diff --git a/src/storm/storage/geometry/Polytope.cpp b/src/storm/storage/geometry/Polytope.cpp index c969e73c5..a0dbd7185 100644 --- a/src/storm/storage/geometry/Polytope.cpp +++ b/src/storm/storage/geometry/Polytope.cpp @@ -91,12 +91,6 @@ namespace storm { // Intentionally left empty } - template - std::vector::Point> Polytope::getVertices() const{ - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return std::vector(); - } - #ifdef STORM_HAVE_CARL template <> std::vector::Point> Polytope::getVerticesInClockwiseOrder() const{ @@ -151,7 +145,6 @@ namespace storm { return result; } #endif - template std::vector::Point> Polytope::getVerticesInClockwiseOrder() const{ @@ -160,78 +153,12 @@ namespace storm { // checking whether the distance between halfspace and point is zero is problematic otherwise. return std::vector(); } - - template - std::vector> Polytope::getHalfspaces() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return std::vector>(); - } - - template - bool Polytope::isEmpty() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return false; - } - - template - bool Polytope::isUniversal() const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return false; - } - - template - bool Polytope::contains(Point const& point) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return false; - } - - template - bool Polytope::contains(std::shared_ptr> const& other) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return false; - } - - template - std::shared_ptr> Polytope::intersection(std::shared_ptr> const& rhs) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return nullptr; - } - - template - std::shared_ptr> Polytope::intersection(Halfspace const& halfspace) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return nullptr; - } - - template - std::shared_ptr> Polytope::convexUnion(std::shared_ptr> const& rhs) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return nullptr; - } - - template - std::shared_ptr> Polytope::minkowskiSum(std::shared_ptr> const& rhs) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return nullptr; - } - - template - std::shared_ptr> Polytope::affineTransformation(std::vector const& matrix, Point const& vector) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return nullptr; - } - + template std::shared_ptr> Polytope::downwardClosure() const { return createDownwardClosure(this->getVertices()); } - template - std::pair::Point, bool> Polytope::optimize(Point const& direction) const { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented."); - return std::make_pair(Point(), false); - } - template template std::shared_ptr> Polytope::convertNumberRepresentation() const { diff --git a/src/storm/storage/geometry/Polytope.h b/src/storm/storage/geometry/Polytope.h index d9230b38e..fc24c4d9a 100644 --- a/src/storm/storage/geometry/Polytope.h +++ b/src/storm/storage/geometry/Polytope.h @@ -50,7 +50,7 @@ namespace storm { /*! * Returns the vertices of this polytope. */ - virtual std::vector getVertices() const; + virtual std::vector getVertices() const = 0; /*! * Returns the vertices of this 2D-polytope in clockwise order. @@ -61,43 +61,43 @@ namespace storm { /*! * Returns the halfspaces of this polytope. */ - virtual std::vector> getHalfspaces() const; + virtual std::vector> getHalfspaces() const = 0; /*! * Returns whether this polytope is the empty set. */ - virtual bool isEmpty() const; + virtual bool isEmpty() const = 0; /*! * Returns whether this polytope is universal (i.e., equals R^n). */ - virtual bool isUniversal() const; + virtual bool isUniversal() const = 0; /*! * Returns true iff the given point is inside of the polytope. */ - virtual bool contains(Point const& point) const; + virtual bool contains(Point const& point) const = 0; /*! * Returns true iff the given polytope is a subset of this polytope. */ - virtual bool contains(std::shared_ptr> const& other) const; + virtual bool contains(std::shared_ptr> const& other) const = 0; /*! * Intersects this polytope with rhs and returns the result. */ - virtual std::shared_ptr> intersection(std::shared_ptr> const& rhs) const; - virtual std::shared_ptr> intersection(Halfspace const& halfspace) const; + virtual std::shared_ptr> intersection(std::shared_ptr> const& rhs) const = 0; + virtual std::shared_ptr> intersection(Halfspace const& halfspace) const = 0; /*! * Returns the convex union of this polytope and rhs. */ - virtual std::shared_ptr> convexUnion(std::shared_ptr> const& rhs) const; + virtual std::shared_ptr> convexUnion(std::shared_ptr> const& rhs) const = 0; /*! * Returns the minkowskiSum of this polytope and rhs. */ - virtual std::shared_ptr> minkowskiSum(std::shared_ptr> const& rhs) const; + virtual std::shared_ptr> minkowskiSum(std::shared_ptr> const& rhs) const = 0; /*! * Returns the affine transformation of this polytope P w.r.t. the given matrix A and vector b. @@ -106,7 +106,7 @@ namespace storm { * @param matrix the transformation matrix, given as vector of rows * @param vector the transformation offset */ - virtual std::shared_ptr> affineTransformation(std::vector const& matrix, Point const& vector) const; + virtual std::shared_ptr> affineTransformation(std::vector const& matrix, Point const& vector) const = 0; /*! * Returns the downward closure of this, i.e., the set { x | ex. y \in P : x<=y} where P is this Polytope. @@ -120,7 +120,7 @@ namespace storm { * - The polytope is empty * - The polytope is not bounded in the given direction */ - virtual std::pair optimize(Point const& direction) const; + virtual std::pair optimize(Point const& direction) const = 0; /*! * converts the intern number representation of the polytope to the given target type diff --git a/src/storm/transformer/StateDuplicator.h b/src/storm/transformer/StateDuplicator.h index 8d0f6aa80..72328013c 100644 --- a/src/storm/transformer/StateDuplicator.h +++ b/src/storm/transformer/StateDuplicator.h @@ -235,8 +235,8 @@ namespace storm { std::is_same>::value || std::is_same>::value, MT>::type - createTransformedModel(MT const& originalModel, - StateDuplicatorReturnType const& result, + createTransformedModel(MT const& /*originalModel*/, + StateDuplicatorReturnType const& /*result*/, storm::storage::SparseMatrix& matrix, storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map>::value || std::is_same>::value, MT>::type - createTransformedModel(MT const& originalModel, - storm::storage::BitVector const& subsystem, + createTransformedModel(MT const& /*originalModel*/, + storm::storage::BitVector const& /*subsystem*/, storm::storage::SparseMatrix& matrix, storm::models::sparse::StateLabeling& stateLabeling, - std::unordered_map& rewardModels, + std::unordered_map& rewardModels, boost::optional>& choiceLabeling ) { return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); } diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index b91b1f7b3..589a531a4 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -464,7 +464,7 @@ namespace storm { regionModelChecker.reset(); // Program and formula storm::prism::Program program = parseProgram(programFilePath); - program.checkValidity(); + program = storm::utility::prism::preprocess(program, constantsString); std::vector> formulas = parseFormulasForPrismProgram(formulaString, program); if(formulas.size()!=1) { STORM_LOG_ERROR("The given formulaString does not specify exactly one formula");