sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

cleaning up 

Former-commit-id: 1d33b0c600
main
TimQu 9 years ago
parent
80d9e6bb4e
commit
3d24f25fbc
7 changed files with 6 additions and 157 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 16
      examples/multiobjective/ma/polling/untitled.txt
  2. 2
      src/logic/Bound.h
  3. 3
      src/logic/OperatorFormula.h
  4. 121
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
  5. 6
      src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
  6. 4
      src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
  7. 11
      src/utility/vector.h

16
examples/multiobjective/ma/polling/untitled.txt
View File

@ -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

2
src/logic/Bound.h
View File

@ -26,7 +26,7 @@ namespace storm {
template<typename ValueType>
std::ostream& operator<<(std::ostream& out, Bound<ValueType> const& bound) {
out << bound.comparisonType << storm::utility::convertNumber<double>(bound.threshold);
out << bound.comparisonType << bound.threshold;
return out;
}
}

3
src/logic/OperatorFormula.h
View File

@ -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;

121
src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
View File

@ -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<RationalNumberType>::createUniversalPolytope();
resultData.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::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<double>());
std::cout << "Current precision of the numerical result is " << resultData.template getPrecisionOfResult<double>() << 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<RationalNumberType>());
direction[objIndex] = storm::utility::one<RationalNumberType>();
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<RationalNumberType>(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber<RationalNumberType>(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::RationalNumber>(storm::logic::ComparisonType::GreaterEqual, thresholdValue));
copySubF->asOperatorFormula().setOperatorInformation(opInfo);
} else {
storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound<storm::RationalNumber>(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<RationalNumberType>(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber<RationalNumberType>(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::RationalNumber>(storm::logic::ComparisonType::GreaterEqual, thresholdValue));
copySubF->asOperatorFormula().setOperatorInformation(opInfo);
} else {
storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound<storm::RationalNumber>(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<double>() << 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<RationalNumberType>(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber<RationalNumberType>(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::RationalNumber>(storm::logic::ComparisonType::GreaterEqual, thresholdValue));
copySubF->asOperatorFormula().setOperatorInformation(opInfo);
} else {
storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound<storm::RationalNumber>(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<RationalNumberType>(resultData.refinementSteps().back().getLowerBoundPoint()[subFIndex]) * storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[subFIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber<RationalNumberType>(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::RationalNumber>(storm::logic::ComparisonType::GreaterEqual, thresholdValue));
copySubF->asOperatorFormula().setOperatorInformation(opInfo);
} else {
storm::logic::OperatorInformation opInfo(boost::none, storm::logic::Bound<storm::RationalNumber>(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<double>());
if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) {
break;
@ -371,11 +255,7 @@ namespace storm {
break;
}
}
result.stopWatchWeightVectorChecker.unpause();
weightVectorChecker->check(storm::utility::vector::convertNumericVector<SparseModelValueType>(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 <class SparseModelType, typename RationalNumberType>

6
src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
View File

@ -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();
}

4
src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
View File

@ -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 };

11
src/utility/vector.h
View File

@ -100,12 +100,10 @@ namespace storm {
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<typename T>
std::vector<uint_fast64_t> getSortedIndices(std::vector<T> 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.

Write Preview
Loading…
Cancel
Save