From 744126a380c6b04c142ac89b35ac2ca664716d38 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 15 Mar 2017 18:49:35 +0100 Subject: [PATCH] visualization of result :) --- .../parametric/ParameterLifting.cpp | 58 ++++++++++++++++++- .../parametric/ParameterLifting.h | 2 + src/storm/utility/storm.h | 12 +++- 3 files changed, 69 insertions(+), 3 deletions(-) diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp index 61523ef72..a0ab01eeb 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.cpp +++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp @@ -1,3 +1,5 @@ +#include + #include "storm/modelchecker/parametric/ParameterLifting.h" #include "storm/adapters/CarlAdapter.h" @@ -200,7 +202,7 @@ namespace storm { currentFormula = checkTask.getFormula().asSharedPointer(); } } - + template <> void ParameterLifting, double>::simplifyParametricModel(CheckTask const& checkTask) { storm::transformer::SparseParametricMdpSimplifier> simplifier(parametricModel); @@ -213,6 +215,60 @@ namespace storm { } } + template + std::string ParameterLifting::visualizeResult(std::vector, RegionCheckResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y) { + + typedef typename storm::storage::ParameterRegion::CoefficientType ValueType; + + std::stringstream stream; + + uint_fast64_t const size = 64; + + stream << "Parameter lifting result (visualization):" << std::endl; + stream << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl; + for (uint_fast64_t i = 0; i < 2*size+2; ++i) stream << "#"; stream << std::endl; + + ValueType deltaX = (parameterSpace.getUpperBoundary(x) - parameterSpace.getLowerBoundary(x)) / storm::utility::convertNumber(size); + ValueType deltaY = (parameterSpace.getUpperBoundary(y) - parameterSpace.getLowerBoundary(y)) / storm::utility::convertNumber(size); + ValueType printedRegionArea = deltaX * deltaY; + for (ValueType yUpper = parameterSpace.getUpperBoundary(y); yUpper != parameterSpace.getLowerBoundary(y); yUpper -= deltaY) { + ValueType yLower = yUpper - deltaY; + stream << "#"; + for (ValueType xLower = parameterSpace.getLowerBoundary(x); xLower != parameterSpace.getUpperBoundary(x); xLower += deltaX) { + ValueType xUpper = xLower + deltaX; + bool currRegionSafe = false; + bool currRegionUnSafe = false; + bool currRegionComplete = false; + ValueType coveredArea = storm::utility::zero(); + for (auto const& r : result) { + ValueType instersectionArea = std::max(storm::utility::zero(), std::min(yUpper, r.first.getUpperBoundary(y)) - std::max(yLower, r.first.getLowerBoundary(y))); + instersectionArea *= std::max(storm::utility::zero(), std::min(xUpper, r.first.getUpperBoundary(x)) - std::max(xLower, r.first.getLowerBoundary(x))); + if(!storm::utility::isZero(instersectionArea)) { + currRegionSafe = currRegionSafe || r.second == RegionCheckResult::AllSat; + currRegionUnSafe = currRegionUnSafe || r.second == RegionCheckResult::AllViolated; + coveredArea += instersectionArea; + if(currRegionSafe && currRegionUnSafe) { + break; + } + if(coveredArea == printedRegionArea) { + currRegionComplete = true; + break; + } + } + } + if (currRegionComplete && currRegionSafe && !currRegionUnSafe) { + stream << "SS"; + } else if (currRegionComplete && currRegionUnSafe && !currRegionSafe) { + stream << " "; + } else { + stream << "--"; + } + } + stream << "#" << std::endl; + } + for (uint_fast64_t i = 0; i < 2*size+2; ++i) stream << "#"; stream << std::endl; + return stream.str(); + } #ifdef STORM_HAVE_CARL template class ParameterLifting, double>; diff --git a/src/storm/modelchecker/parametric/ParameterLifting.h b/src/storm/modelchecker/parametric/ParameterLifting.h index 1557a00d0..b0ea7ef65 100644 --- a/src/storm/modelchecker/parametric/ParameterLifting.h +++ b/src/storm/modelchecker/parametric/ParameterLifting.h @@ -43,6 +43,8 @@ namespace storm { SparseParameterLiftingModelChecker const& getParameterLiftingChecker() const; SparseInstantiationModelChecker const& getInstantiationChecker() const; + static std::string visualizeResult(std::vector, RegionCheckResult>> const& result, storm::storage::ParameterRegion const& parameterSpace, typename storm::storage::ParameterRegion::VariableType const& x, typename storm::storage::ParameterRegion::VariableType const& y); + private: SparseModelType const& getConsideredParametricModel() const; diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 241f7d378..e0d1deff9 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -330,15 +330,24 @@ namespace storm { STORM_PRINT_AND_LOG("Performing parameter lifting for property " << *formula << " with parameter space " << parameterSpace.toString(true) << " and refinement threshold " << storm::utility::convertNumber(refinementThreshold) << " ..." << std::endl); storm::modelchecker::CheckTask task(*formula, true); + std::string resultVisualization; if (markovModel->isOfType(storm::models::ModelType::Dtmc)) { storm::modelchecker::parametric::ParameterLifting , double> parameterLiftingContext(*markovModel->template as>()); parameterLiftingContext.specifyFormula(task); result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold); + parameterLiftingStopWatch.stop(); + if (modelParameters.size() == 2) { + resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); + } } else if (markovModel->isOfType(storm::models::ModelType::Mdp)) { storm::modelchecker::parametric::ParameterLifting, double> parameterLiftingContext(*markovModel->template as>()); parameterLiftingContext.specifyFormula(task); result = parameterLiftingContext.performRegionRefinement(parameterSpace, refinementThreshold); + parameterLiftingStopWatch.stop(); + if (modelParameters.size() == 2) { + resultVisualization = parameterLiftingContext.visualizeResult(result, parameterSpace, *modelParameters.begin(), *(modelParameters.rbegin())); + } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to perform parameterLifting on the provided model type."); } @@ -363,13 +372,12 @@ namespace storm { break; } } - STORM_PRINT_AND_LOG("Done! Found " << numOfSatRegions << " safe regions and " << numOfUnsatRegions << " unsafe regions." << std::endl); STORM_PRINT_AND_LOG(storm::utility::convertNumber(satArea / parameterSpace.area()) * 100 << "% of the parameter space is safe, and " << storm::utility::convertNumber(unsatArea / parameterSpace.area()) * 100 << "% of the parameter space is unsafe." << std::endl); - parameterLiftingStopWatch.stop(); STORM_PRINT_AND_LOG("Model checking with parameter lifting took " << parameterLiftingStopWatch << " seconds." << std::endl); + STORM_PRINT_AND_LOG(resultVisualization); if (storm::settings::getModule().exportResultToFile()) { std::string path = storm::settings::getModule().exportResultPath();