diff --git a/examples/multiobjective/ma/polling/untitled.txt b/examples/multiobjective/ma/polling/untitled.txt deleted file mode 100644 index 2be3cb7df..000000000 --- a/examples/multiobjective/ma/polling/untitled.txt +++ /dev/null @@ -1,16 +0,0 @@ -mdp - -const int J = 0; - - -module test - - x : [0..1]; - j : [0..1] init 1; - z : [0..1]; - [] j=1 -> 1 : (x'=j); - [] j<1 -> 1 : (x'=0); - [] x=1 -> (z'=1); -endmodule - - diff --git a/src/logic/Bound.h b/src/logic/Bound.h index fbfc2fcf8..e56a2c04f 100644 --- a/src/logic/Bound.h +++ b/src/logic/Bound.h @@ -26,7 +26,7 @@ namespace storm { template std::ostream& operator<<(std::ostream& out, Bound const& bound) { - out << bound.comparisonType << storm::utility::convertNumber(bound.threshold); + out << bound.comparisonType << bound.threshold; return out; } } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index fd5495da6..633e0dda3 100644 --- a/src/logic/OperatorFormula.h +++ b/src/logic/OperatorFormula.h @@ -47,9 +47,6 @@ namespace storm { virtual bool isOperatorFormula() const override; OperatorInformation const& getOperatorInformation() const; - void setOperatorInformation(OperatorInformation newOperatorInformation) { - this->operatorInformation = newOperatorInformation; - } virtual bool hasQualitativeResult() const override; virtual bool hasQuantitativeResult() const override; diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp index fb63c037b..7f4442306 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp @@ -13,8 +13,6 @@ #include "src/exceptions/UnexpectedException.h" -#include "src/logic/CloneVisitor.h" - namespace storm { namespace modelchecker { namespace helper { @@ -25,8 +23,6 @@ namespace storm { ResultData resultData; resultData.overApproximation() = storm::storage::geometry::Polytope::createUniversalPolytope(); resultData.underApproximation() = storm::storage::geometry::Polytope::createEmptyPolytope(); - resultData.stopWatchWeightVectorChecker.pause(); - resultData.stopWatchWeightVectorChecker.reset(); // Set the maximum gap between lower and upper bound of the weightVectorChecker result. // This is the maximal edge length of the box we have to consider around each computed point @@ -151,7 +147,6 @@ namespace storm { if(optimizationRes.second) { resultData.setPrecisionOfResult(optimizationRes.first[optimizingObjIndex] - thresholds[optimizingObjIndex]); STORM_LOG_DEBUG("Solution can be improved by at most " << resultData.template getPrecisionOfResult()); - std::cout << "Current precision of the numerical result is " << resultData.template getPrecisionOfResult() << std::endl; } if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) { resultData.setOptimumIsAchievable(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)); @@ -170,58 +165,6 @@ namespace storm { WeightVector direction(preprocessorData.objectives.size(), storm::utility::zero()); direction[objIndex] = storm::utility::one(); performRefinementStep(std::move(direction), preprocessorData.produceSchedulers, weightVectorChecker, resultData); - - - - //TODO remove this code.. - std::cout << "multi(" << preprocessorData.originalFormula.getSubformula(0); - for(uint_fast64_t subFIndex = 1; subFIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subFIndex) { - std::cout << ", "; - RationalNumberType thresholdValue = - storm::utility::convertNumber(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationOffset); - - auto const& subF = preprocessorData.originalFormula.getSubformula(subFIndex); - if(subF.isOperatorFormula() && subF.asOperatorFormula().hasOptimalityType()) { - storm::logic::CloneVisitor cv; - auto copySubF = cv.clone(subF); - - if(subF.asOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize) { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::GreaterEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } else { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::LessEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } - std::cout << *copySubF; - } - } - std::cout << ")" << std::endl; - //TODO remove this code.. - std::cout << "multi("; - for(uint_fast64_t subFIndex = 0; subFIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subFIndex) { - if(subFIndex != 0) { - std::cout << ", "; - } - RationalNumberType thresholdValue = - storm::utility::convertNumber(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationOffset); - - auto const& subF = preprocessorData.originalFormula.getSubformula(subFIndex); - if(subF.isOperatorFormula() && subF.asOperatorFormula().hasOptimalityType()) { - storm::logic::CloneVisitor cv; - auto copySubF = cv.clone(subF); - - if(subF.asOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize) { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::GreaterEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } else { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::LessEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } - std::cout << *copySubF; - } - } - std::cout << ")" << std::endl; - } while(true) { @@ -240,65 +183,6 @@ namespace storm { } } resultData.setPrecisionOfResult(farestDistance); - std::cout << "Current precision of the approximation of the pareto curve is " << resultData.template getPrecisionOfResult() << std::endl; - - - - - //TODO remove this code.. - std::cout << "multi(" << preprocessorData.originalFormula.getSubformula(0); - for(uint_fast64_t subFIndex = 1; subFIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subFIndex) { - std::cout << ", "; - RationalNumberType thresholdValue = - storm::utility::convertNumber(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationOffset); - - auto const& subF = preprocessorData.originalFormula.getSubformula(subFIndex); - if(subF.isOperatorFormula() && subF.asOperatorFormula().hasOptimalityType()) { - storm::logic::CloneVisitor cv; - auto copySubF = cv.clone(subF); - - if(subF.asOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize) { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::GreaterEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } else { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::LessEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } - std::cout << *copySubF; - } - } - std::cout << ")" << std::endl; - //TODO remove this code.. - std::cout << "multi("; - for(uint_fast64_t subFIndex = 0; subFIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subFIndex) { - if(subFIndex != 0) { - std::cout << ", "; - } - RationalNumberType thresholdValue = - storm::utility::convertNumber(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber(preprocessorData.objectives[subFIndex].toOriginalValueTransformationOffset); - - auto const& subF = preprocessorData.originalFormula.getSubformula(subFIndex); - if(subF.isOperatorFormula() && subF.asOperatorFormula().hasOptimalityType()) { - storm::logic::CloneVisitor cv; - auto copySubF = cv.clone(subF); - - if(subF.asOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize) { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::GreaterEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } else { - storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound(storm::logic::ComparisonType::LessEqual, thresholdValue)); - copySubF->asOperatorFormula().setOperatorInformation(opInfo); - } - std::cout << *copySubF; - } - } - std::cout << ")" << std::endl; - - - - - - STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is " << resultData.template getPrecisionOfResult()); if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) { break; @@ -371,11 +255,7 @@ namespace storm { break; } } - - result.stopWatchWeightVectorChecker.unpause(); weightVectorChecker->check(storm::utility::vector::convertNumericVector(direction)); - result.stopWatchWeightVectorChecker.pause(); - if(oldMaximumLowerUpperBoundGap) { // Reset the precision back to the previous values weightVectorChecker->setMaximumLowerUpperBoundGap(*oldMaximumLowerUpperBoundGap); @@ -394,7 +274,6 @@ namespace storm { } updateOverApproximation(result.refinementSteps(), result.overApproximation()); updateUnderApproximation(result.refinementSteps(), result.underApproximation()); - std::cout << "number of performed refinement Steps is: " << result.refinementSteps().size() << std::endl; } template diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp index 1dd2c62c5..bda0873a4 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp @@ -41,8 +41,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type"); } - //STORM_LOG_INFO(getInfo(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch)); - std:: cout << getInfo(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch); + STORM_LOG_INFO(getInfo(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch)); exportPlot(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch); @@ -334,7 +333,7 @@ namespace storm { << preprocessorData.originalModel.getNumberOfTransitions() << ";" << preprocessorData.originalFormula << ";" << std::endl; - statistics << "result_Header;Iterations;Time Combined;Accuracy;Time Iterations;Time Computation Optimal Points" << std::endl; + statistics << "result_Header;Iterations;Time Combined;Accuracy;Time Iterations;" << std::endl; statistics << "result_data;" << resultData.refinementSteps().size() << ";" << combinedTime << ";"; @@ -348,7 +347,6 @@ namespace storm { } else { statistics << ";"; } - statistics << resultData.stopWatchWeightVectorChecker << ";"; statistics << std::endl; return statistics.str(); } diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h index 75f025fcd..5bb1f0f77 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h @@ -8,7 +8,6 @@ #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h" #include "src/storage/geometry/Polytope.h" #include "src/utility/macros.h" -#include "src/utility/Stopwatch.h" #include "src/exceptions/InvalidStateException.h" @@ -99,9 +98,6 @@ namespace storm { return maxStepsPerformed; } - //Keeps track of the time we spent with weight vector checking (i.e., computation of optimal points) - storm::utility::Stopwatch stopWatchWeightVectorChecker; - private: enum class Tribool { False, True, Indeterminate }; diff --git a/src/utility/vector.h b/src/utility/vector.h index f6680cf01..0ad7b70e2 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -99,13 +99,11 @@ namespace storm { iota_n(std::back_inserter(v), diff, min); return v; } - - /*! - * Retrieves a list of indices such that the first index points to the entry of the given vector - * with the highest value, the second index points to the entry with the second highest value, ... - * Example: v={3,8,4,5,1} yields res={1,3,2,0,4} + * Returns a list of indices such that the first index refers to the highest entry of the given vector, + * the second index refers to the entry with the second highest value, ... + * Example: v={3,8,4,5} yields res={1,3,2,0} */ template std::vector getSortedIndices(std::vector const& v){ @@ -114,9 +112,6 @@ namespace storm { return res; } - - - /*! * Selects the elements from a vector at the specified positions and writes them consecutively into another vector. * @param vector The vector into which the selected elements are to be written.