From a728c013229f4dfda9b2d7ed2b8c0d4aee08f055 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Wed, 22 Apr 2020 13:52:58 +0200 Subject: [PATCH 01/10] BitVector: Fixed an issue with the move assignment operator. The 'other' BitVector was left in an invalid state. --- src/storm/storage/BitVector.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index a4ad5fca9..8df237df3 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -156,6 +156,7 @@ namespace storm { // Only perform the assignment if the source and target are not identical. if (this != &other) { bitCount = other.bitCount; + other.bitCount = 0; if (this->buckets) { delete[] this->buckets; } From 4eed592811ae61e2ed6eb69acc3bef5a3c071000 Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Mon, 27 Apr 2020 11:39:07 +0200 Subject: [PATCH 02/10] --timeout now just sends a SIGALRM signal (which can be catched by the signal handler). --- src/storm-cli-utilities/cli.cpp | 2 +- src/storm/utility/resources.h | 21 --------------------- 2 files changed, 1 insertion(+), 22 deletions(-) diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp index 12d5771bd..9105bc9a2 100644 --- a/src/storm-cli-utilities/cli.cpp +++ b/src/storm-cli-utilities/cli.cpp @@ -202,7 +202,7 @@ namespace storm { // If we were given a time limit, we put it in place now. if (resources.isTimeoutSet()) { - storm::utility::resources::setCPULimit(resources.getTimeoutInSeconds()); + storm::utility::resources::setTimeoutAlarm(resources.getTimeoutInSeconds()); } // register signal handler to handle aborts diff --git a/src/storm/utility/resources.h b/src/storm/utility/resources.h index eb84d73c0..349796acd 100644 --- a/src/storm/utility/resources.h +++ b/src/storm/utility/resources.h @@ -13,27 +13,6 @@ namespace storm { namespace utility { namespace resources { - /*! - * Get CPU limit. - * @return CPU limit in seconds. - */ - inline std::size_t getCPULimit() { - rlimit rl; - getrlimit(RLIMIT_CPU, &rl); - return rl.rlim_cur; - } - - /*! - * Set CPU limit. - * @param seconds CPU limit in seconds. - */ - inline void setCPULimit(std::size_t seconds) { - rlimit rl; - getrlimit(RLIMIT_CPU, &rl); - rl.rlim_cur = seconds; - setrlimit(RLIMIT_CPU, &rl); - } - /*! * Get used CPU time. * @return CPU time in seconds. From 5a221acbd0eb5702972a178aeea58ffafbce13be Mon Sep 17 00:00:00 2001 From: Tim Quatmann Date: Thu, 30 Apr 2020 15:38:08 +0200 Subject: [PATCH 03/10] Multi-objective model checking: Fixed incorrect computations for some models with end components. (Github Issue #75) --- .../multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp index 307d91c3f..db0fa99f1 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp @@ -563,6 +563,7 @@ namespace storm { if (rowLeadsToDefinedScheduler && (rowStaysInEC || !statesThatShouldStayInTheirEC.get(state))) { originalOptimalChoices[state] = row - transitionMatrix.getRowGroupIndices()[state]; statesWithUndefSched.set(state, false); + break; } } } From f45db73afead4c75612d11e56d07de432fab2fe0 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Apr 2020 16:38:45 +0200 Subject: [PATCH 04/10] Support coloured output for GCC --- CMakeLists.txt | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index d1b58879e..134b6577a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -263,6 +263,9 @@ if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG) set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-export_dynamic") endif() elseif (STORM_COMPILER_GCC) + if(FORCE_COLOR) + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fdiagnostics-color=always") + endif() set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14") set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fprefetch-loop-arrays") set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic") From d3c8093e0f5f841ea3bf0f51a7c1769f04820407 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Apr 2020 16:41:06 +0200 Subject: [PATCH 05/10] Removed unnecessary semicolons --- src/storm-gspn/storage/gspn/GSPN.cpp | 4 ++-- .../region/ValidatingSparseParameterLiftingModelChecker.cpp | 2 +- src/storm-pomdp/transformer/MakePOMDPCanonic.cpp | 2 +- src/storm/generator/JaniNextStateGenerator.cpp | 4 ++-- src/storm/generator/PrismNextStateGenerator.cpp | 2 +- src/storm/models/sparse/Pomdp.cpp | 2 +- 6 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index bac028c27..c9d1ff7cd 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -94,7 +94,7 @@ namespace storm { } } return nullptr; - }; + } storm::gspn::Place* GSPN::getPlace(std::string const& name) { for (auto& place : places) { @@ -103,7 +103,7 @@ namespace storm { } } return nullptr; - }; + } storm::gspn::TimedTransition const* GSPN::getTimedTransition(std::string const& name) const { for (auto& trans : timedTransitions) { diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp index 002a43692..4065f236b 100644 --- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp @@ -25,7 +25,7 @@ namespace storm { template bool ValidatingSparseParameterLiftingModelChecker::canHandle(std::shared_ptr parametricModel, CheckTask const& checkTask) const { return getImpreciseChecker().canHandle(parametricModel, checkTask) && getPreciseChecker().canHandle(parametricModel, checkTask); - }; + } template RegionResult ValidatingSparseParameterLiftingModelChecker::analyzeRegion(Environment const& env, storm::storage::ParameterRegion const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) { diff --git a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp index da03d47ca..d4791ec45 100644 --- a/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp +++ b/src/storm-pomdp/transformer/MakePOMDPCanonic.cpp @@ -47,7 +47,7 @@ namespace storm { ++it2; } return it1 == end1 && it2 == end2; - }; + } bool operator<(ActionIdentifier const& lhs, ActionIdentifier const& rhs) { diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 6c260746b..87baa0b98 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -169,7 +169,7 @@ namespace storm { template bool JaniNextStateGenerator::isPartiallyObservable() const { return false; - }; + } template uint64_t JaniNextStateGenerator::getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const { @@ -1201,7 +1201,7 @@ namespace storm { storm::storage::BitVector JaniNextStateGenerator::evaluateObservationLabels(CompressedState const& state) const { STORM_LOG_WARN("There are no observation labels in JANI currenty"); return storm::storage::BitVector(0); - }; + } template diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index a0fb216e5..6bec68bed 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -734,7 +734,7 @@ namespace storm { result.setFromInt(64*i,64,this->evaluator->asInt(program.getObservationLabels()[i].getStatePredicateExpression())); } return result; - }; + } template diff --git a/src/storm/models/sparse/Pomdp.cpp b/src/storm/models/sparse/Pomdp.cpp index 02293dba8..2ba70383b 100644 --- a/src/storm/models/sparse/Pomdp.cpp +++ b/src/storm/models/sparse/Pomdp.cpp @@ -62,7 +62,7 @@ namespace storm { template bool Pomdp::isCanonic() const { return canonicFlag; - }; + } From a61ea32aea292c06b75c930f323346537976c630 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Apr 2020 16:41:39 +0200 Subject: [PATCH 06/10] Fixed some GCC warnings --- .../results/RegionRefinementCheckResult.cpp | 10 ++++++++-- src/storm-parsers/parser/DirectEncodingParser.cpp | 2 -- src/storm/logic/CumulativeRewardFormula.cpp | 3 --- src/storm/logic/InstantaneousRewardFormula.cpp | 2 +- 4 files changed, 9 insertions(+), 8 deletions(-) diff --git a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp index 320dda2e8..7c2a5e18c 100644 --- a/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp +++ b/src/storm-pars/modelchecker/results/RegionRefinementCheckResult.cpp @@ -48,7 +48,10 @@ namespace storm { out << "Region refinement Check result (visualization):" << std::endl; out << " \t x-axis: " << x << " \t y-axis: " << y << " \t S=safe, [ ]=unsafe, -=ambiguous " << std::endl; - for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) { + out << "#"; + } + out << std::endl; CoefficientType deltaX = (getParameterSpace().getUpperBoundary(x) - getParameterSpace().getLowerBoundary(x)) / storm::utility::convertNumber(sizeX); CoefficientType deltaY = (getParameterSpace().getUpperBoundary(y) - getParameterSpace().getLowerBoundary(y)) / storm::utility::convertNumber(sizeY); @@ -94,7 +97,10 @@ namespace storm { } out << "#" << std::endl; } - for (uint_fast64_t i = 0; i < sizeX+2; ++i) out << "#"; out << std::endl; + for (uint_fast64_t i = 0; i < sizeX+2; ++i) { + out << "#"; + } + out << std::endl; } else { STORM_LOG_WARN("Writing illustration of region check result to a stream is only implemented for two parameters."); } diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index 683a87d77..1dd6322d9 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -164,7 +164,6 @@ namespace storm { // Iterate over all lines std::string line; size_t row = 0; - size_t firstRowOfState = 0; size_t state = 0; bool firstState = true; bool firstActionForState = true; @@ -197,7 +196,6 @@ namespace storm { STORM_LOG_TRACE("new Row Group starts at " << row << "."); builder.newRowGroup(row); } - firstRowOfState = row; if (continuousTime) { // Parse exit rate for CTMC or MA diff --git a/src/storm/logic/CumulativeRewardFormula.cpp b/src/storm/logic/CumulativeRewardFormula.cpp index 7abcdc7e4..33633b319 100644 --- a/src/storm/logic/CumulativeRewardFormula.cpp +++ b/src/storm/logic/CumulativeRewardFormula.cpp @@ -99,7 +99,6 @@ namespace storm { double CumulativeRewardFormula::getBound(unsigned i) const { checkNoVariablesInBound(bounds.at(i).getBound()); double value = bounds.at(i).getBound().evaluateAsDouble(); - STORM_LOG_THROW(value >= 0.0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } @@ -107,7 +106,6 @@ namespace storm { storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const { checkNoVariablesInBound(bounds.at(i).getBound()); storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational(); - STORM_LOG_THROW(value >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } @@ -115,7 +113,6 @@ namespace storm { uint64_t CumulativeRewardFormula::getBound(unsigned i) const { checkNoVariablesInBound(bounds.at(i).getBound()); uint64_t value = bounds.at(i).getBound().evaluateAsInt(); - STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } diff --git a/src/storm/logic/InstantaneousRewardFormula.cpp b/src/storm/logic/InstantaneousRewardFormula.cpp index 37bdee1c9..1ed2c1f66 100644 --- a/src/storm/logic/InstantaneousRewardFormula.cpp +++ b/src/storm/logic/InstantaneousRewardFormula.cpp @@ -55,7 +55,7 @@ namespace storm { template <> uint64_t InstantaneousRewardFormula::getBound() const { checkNoVariablesInBound(bound); - uint64_t value = bound.evaluateAsInt(); + int64_t value = bound.evaluateAsInt(); STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); return value; } From 1a1664e35011da3d8e8406653cc5c10f0626eff7 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Apr 2020 16:46:07 +0200 Subject: [PATCH 07/10] Updated .gitignore --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 71a15cc93..48ebde709 100644 --- a/.gitignore +++ b/.gitignore @@ -50,6 +50,7 @@ src/storm/utility/storm-version.cpp nbproject/ .DS_Store .idea +.vscode *.out resources/3rdparty/cudd-3.0.0/Makefile.in resources/3rdparty/cudd-3.0.0/aclocal.m4 From 06941e7c48745f9393b9ca9a41ec345f8e28a416 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 30 Apr 2020 17:38:23 +0200 Subject: [PATCH 08/10] Setting 'dft-statistics' prints information about intermediate approximation results --- CHANGELOG.md | 1 + src/storm-dft-cli/storm-dft.cpp | 5 +++-- .../modelchecker/dft/DFTModelChecker.cpp | 22 ++++++++++++++----- .../settings/modules/DftIOSettings.cpp | 9 ++++---- .../settings/modules/DftIOSettings.h | 7 +++--- 5 files changed, 30 insertions(+), 14 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 2c11fea31..51a33bc11 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,7 @@ Version 1.5.x - Scheduler export: Properly handle models with end components. Added export in .json format. - CMake: Search for Gurobi prefers new versions - Tests: Enabled tests for permissive schedulers +- `storm-dft`: Renamed setting `--show-dft-stats` to `dft-statistics` and added approximation information to statistics. ## Version 1.5.1 (2020/03) - Jani models are now parsed using exact arithmetic. diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 87338ff30..f7a5093a7 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -40,9 +40,10 @@ void processOptions() { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model given."); } - // DFT statistics - if (dftIOSettings.isDisplayStatsSet()) { + // Show statistics about DFT (number of gates, etc.) + if (dftIOSettings.isShowDftStatisticsSet()) { dft->writeStatsToStream(std::cout); + std::cout << std::endl; } // Export to json diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp index 00fe1d0d9..241027e8f 100644 --- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp @@ -13,6 +13,7 @@ #include "storm-dft/api/storm-dft.h" #include "storm-dft/builder/ExplicitDFTModelBuilder.h" #include "storm-dft/storage/dft/DFTIsomorphism.h" +#include "storm-dft/settings/modules/DftIOSettings.h" #include "storm-dft/settings/modules/FaultTreeSettings.h" @@ -305,6 +306,8 @@ namespace storm { storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains, storm::transformer::EliminationLabelBehavior labelBehavior) { explorationTimer.start(); + auto ioSettings = storm::settings::getModule(); + auto dftIOSettings = storm::settings::getModule(); // Find symmetries std::map>> emptySymmetry; @@ -355,12 +358,12 @@ namespace storm { STORM_LOG_DEBUG("Getting model for lower bound..."); model = builder.getModelApproximation(true, !probabilityFormula); // We only output the info from the lower bound as the info for the upper bound is the same - if (printInfo) { + if (printInfo && dftIOSettings.isShowDftStatisticsSet()) { + std::cout << "Model in iteration " << (iteration + 1) << ":" << std::endl; model->printModelInformationToStream(std::cout); } buildingTimer.stop(); - auto ioSettings = storm::settings::getModule(); if (ioSettings.isExportExplicitSet()) { std::vector parameterNames; // TODO fill parameter names @@ -388,24 +391,33 @@ namespace storm { << approxResult.second); approxResult.second = newResult[0]; - ++iteration; STORM_LOG_ASSERT(comparator.isLess(approxResult.first, approxResult.second) || comparator.isEqual(approxResult.first, approxResult.second), "Under-approximation " << approxResult.first << " is greater than over-approximation " << approxResult.second); - STORM_LOG_DEBUG("Result after iteration " << iteration << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); totalTimer.stop(); - printTimings(); + if (printInfo && dftIOSettings.isShowDftStatisticsSet()) { + std::cout << "Result after iteration " << (iteration + 1) << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")" << std::endl; + printTimings(); + std::cout << std::endl; + } else { + STORM_LOG_DEBUG("Result after iteration " << (iteration + 1) << ": (" << std::setprecision(10) << approxResult.first << ", " << approxResult.second << ")"); + } + totalTimer.start(); STORM_LOG_THROW(!storm::utility::isInfinity(approxResult.first) && !storm::utility::isInfinity(approxResult.second), storm::exceptions::NotSupportedException, "Approximation does not work if result might be infinity."); + ++iteration; } while (!isApproximationSufficient(approxResult.first, approxResult.second, approximationError, probabilityFormula)); //STORM_LOG_INFO("Finished approximation after " << iteration << " iteration" << (iteration > 1 ? "s." : ".")); + if (printInfo) { + model->printModelInformationToStream(std::cout); + } dft_results results; results.push_back(approxResult); return results; diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp index 662fd0f34..fca700e5a 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.cpp +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -26,7 +26,8 @@ namespace storm { const std::string DftIOSettings::maxValueOptionName = "max"; const std::string DftIOSettings::exportToJsonOptionName = "export-json"; const std::string DftIOSettings::exportToSmtOptionName = "export-smt"; - const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats"; + const std::string DftIOSettings::dftStatisticsOptionName = "dft-statistics"; + const std::string DftIOSettings::dftStatisticsOptionShortName = "dftstats"; DftIOSettings::DftIOSettings() : ModuleSettings(moduleName) { @@ -62,7 +63,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the smtlib2 file to export to.").build()) .build()); - this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, dftStatisticsOptionName, false, "Sets whether to display DFT statistics if available.").setShortName(dftStatisticsOptionShortName).build()); } bool DftIOSettings::isDftFileSet() const { @@ -136,8 +137,8 @@ namespace storm { return this->getOption(exportToSmtOptionName).getArgumentByName("filename").getValueAsString(); } - bool DftIOSettings::isDisplayStatsSet() const { - return this->getOption(displayStatsOptionName).getHasOptionBeenSet(); + bool DftIOSettings::isShowDftStatisticsSet() const { + return this->getOption(dftStatisticsOptionName).getHasOptionBeenSet(); } void DftIOSettings::finalize() { diff --git a/src/storm-dft/settings/modules/DftIOSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h index 60369b36e..37a5fb464 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -130,11 +130,11 @@ namespace storm { std::string getExportSmtFilename() const; /*! - * Retrieves whether statistics for the DFT should be displayed. + * Retrieves whether statistics about the DFT analysis should be displayed. * * @return True if the statistics option was set. */ - bool isDisplayStatsSet() const; + bool isShowDftStatisticsSet() const; bool check() const override; void finalize() override; @@ -157,7 +157,8 @@ namespace storm { static const std::string maxValueOptionName; static const std::string exportToJsonOptionName; static const std::string exportToSmtOptionName; - static const std::string displayStatsOptionName; + static const std::string dftStatisticsOptionName; + static const std::string dftStatisticsOptionShortName; }; From 356eb0b3b1451efd565c2fcd6c75984651779914 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 2 May 2020 18:55:38 -0700 Subject: [PATCH 09/10] fix debugging assistance code that is no longer valid when you compute multiple counterexamples --- .../counterexamples/SMTMinimalLabelSetGenerator.h | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 58f13ae10..4d4dd9629 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1220,10 +1220,6 @@ namespace storm { // try with an increased bound. while (solver.checkWithAssumptions({assumption}) == storm::solver::SmtSolver::CheckResult::Unsat) { STORM_LOG_DEBUG("Constraint system is unsatisfiable with at most " << currentBound << " taken commands; increasing bound."); -#ifndef NDEBUG - STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable."); - STORM_LOG_ASSERT(solver.check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore."); -#endif solver.add(variableInformation.auxiliaryVariables.back()); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(solver, variableInformation, ++currentBound)); assumption = !variableInformation.auxiliaryVariables.back(); @@ -1755,6 +1751,10 @@ namespace storm { if (result.size() > 0 && iterations > firstCounterexampleFound + options.maximumExtraIterations) { break; } + if (result.size() == 0) { + STORM_LOG_DEBUG("Sanity check to see whether constraint system is still satisfiable."); + STORM_LOG_ASSERT(solver->check() == storm::solver::SmtSolver::CheckResult::Sat, "Constraint system is not satisfiable anymore."); + } STORM_LOG_DEBUG("Computing minimal command set."); solverClock = std::chrono::high_resolution_clock::now(); boost::optional> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound); From 0a5717aee704f6529daadcd0566d67f64fefcd20 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 2 May 2020 18:56:33 -0700 Subject: [PATCH 10/10] lowlevel storing/loading bitvectors from a string (without any error handling, that is). Helpful to store bitvecots in python --- src/storm/storage/BitVector.cpp | 30 ++++++++++++++++++++++++++++++ src/storm/storage/BitVector.h | 3 +++ 2 files changed, 33 insertions(+) diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 8df237df3..6edf61f1b 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1240,6 +1240,36 @@ namespace storm { return h1 ^ h2; } + + void BitVector::store(std::ostream& os) const { + os << bitCount; + for (uint64_t i = 0; i < bucketCount(); ++i) { + os << " " << buckets[i]; + } + } + + BitVector BitVector::load(std::string const& description) { + std::vector splitted; + std::stringstream ss(description); + ss >> std::noskipws; + std::string field; + char ws_delim; + while(true) { + if( ss >> field ) + splitted.push_back(field); + else if (ss.eof()) + break; + else + splitted.push_back(std::string()); + ss.clear(); + ss >> ws_delim; + } + BitVector bv(std::stoul(splitted[0])); + for(uint64_t i = 0; i < splitted.size()-1; ++i) { + bv.buckets[i] = std::stoul(splitted[i+1]); + } + return bv; + } // All necessary explicit template instantiations. template BitVector::BitVector(uint_fast64_t length, std::vector::iterator begin, std::vector::iterator end); diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 64b823652..323020b48 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -538,6 +538,9 @@ namespace storm { friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); + void store(std::ostream&) const; + static BitVector load(std::string const& description); + friend struct std::hash; friend struct FNV1aBitVectorHash;