From f327ff75e9e81c78404ae92cc0b83397cdd836ef Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 4 Sep 2017 09:28:15 +0200 Subject: [PATCH 1/2] showing progress for bisimulation --- .../storage/dd/BisimulationDecomposition.cpp | 24 +++++++++++++++++++ .../storage/dd/BisimulationDecomposition.h | 6 +++++ 2 files changed, 30 insertions(+) diff --git a/src/storm/storage/dd/BisimulationDecomposition.cpp b/src/storm/storage/dd/BisimulationDecomposition.cpp index 57190ff23..be19015ec 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.cpp +++ b/src/storm/storage/dd/BisimulationDecomposition.cpp @@ -9,6 +9,9 @@ #include "storm/models/symbolic/Mdp.h" #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/IOSettings.h" + #include "storm/utility/macros.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/NotSupportedException.h" @@ -29,16 +32,25 @@ namespace storm { template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { + auto const& ioSettings = storm::settings::getModule(); + showProgress = ioSettings.isExplorationShowProgressSet(); + showProgressDelay = ioSettings.getExplorationShowProgressDelay(); this->refineWrtRewardModels(); } template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, std::vector> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition::create(model, bisimulationType, preservationInformation))) { + auto const& ioSettings = storm::settings::getModule(); + showProgress = ioSettings.isExplorationShowProgressSet(); + showProgressDelay = ioSettings.getExplorationShowProgressDelay(); this->refineWrtRewardModels(); } template BisimulationDecomposition::BisimulationDecomposition(storm::models::symbolic::Model const& model, Partition const& initialPartition, bisimulation::PreservationInformation const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) { + auto const& ioSettings = storm::settings::getModule(); + showProgress = ioSettings.isExplorationShowProgressSet(); + showProgressDelay = ioSettings.getExplorationShowProgressDelay(); this->refineWrtRewardModels(); } @@ -55,12 +67,24 @@ namespace storm { #endif auto start = std::chrono::high_resolution_clock::now(); + auto timeOfLastMessage = start; uint64_t iterations = 0; bool refined = true; while (refined) { refined = refiner->refine(mode); + ++iterations; STORM_LOG_TRACE("After iteration " << iterations << " partition has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks."); + + if (showProgress) { + auto now = std::chrono::high_resolution_clock::now(); + auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); + if (static_cast(durationSinceLastMessage) >= showProgressDelay) { + auto durationSinceStart = std::chrono::duration_cast(now - start).count(); + std::cout << "State partition after " << iterations << " iterations (" << durationSinceStart << "ms) has " << refiner->getStatePartition().getNumberOfBlocks() << " blocks." << std::endl; + timeOfLastMessage = std::chrono::high_resolution_clock::now(); + } + } } auto end = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/storage/dd/BisimulationDecomposition.h b/src/storm/storage/dd/BisimulationDecomposition.h index 66e562bea..2a62c9fa4 100644 --- a/src/storm/storage/dd/BisimulationDecomposition.h +++ b/src/storm/storage/dd/BisimulationDecomposition.h @@ -60,6 +60,12 @@ namespace storm { // The refiner to use. std::unique_ptr> refiner; + + // A flag indicating whether progress is reported. + bool showProgress; + + // The delay between progress reports. + uint64_t showProgressDelay; }; } From b7e2aec82c5f6439bfbec013c0a9ed97ee119b35 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 6 Sep 2017 11:43:33 +0200 Subject: [PATCH 2/2] Fixed issue where variable names were reserved symbols of Exprtk --- CHANGELOG.md | 1 + .../storage/expressions/ExprtkExpressionEvaluator.cpp | 8 +++++--- src/storm/storage/expressions/ToExprtkStringVisitor.cpp | 2 +- 3 files changed, 7 insertions(+), 4 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 75d2a807c..8e2e6c883 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -13,6 +13,7 @@ Long run average computation via ValueIteration, LP based MDP model checking, pa - storm-cli-utilities now contains cli related stuff, instead of storm-lib - storm-pars: support for welldefinedness constraints in mdps. - symbolic (MT/BDD) bisimulation +- Fixed issue related to variable names that can not be used in Exprtk. ### Version 1.1.0 (2017/8) diff --git a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp index 42a405e49..70cd6e162 100755 --- a/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp +++ b/src/storm/storage/expressions/ExprtkExpressionEvaluator.cpp @@ -1,3 +1,5 @@ +#include + #include "storm/storage/expressions/ExprtkExpressionEvaluator.h" #include "storm/storage/expressions/ExpressionManager.h" @@ -13,11 +15,11 @@ namespace storm { for (auto const& variableTypePair : manager) { if (variableTypePair.second.isBooleanType()) { - symbolTable->add_variable(variableTypePair.first.getName(), this->booleanValues[variableTypePair.first.getOffset()]); + symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->booleanValues[variableTypePair.first.getOffset()]); } else if (variableTypePair.second.isIntegerType()) { - symbolTable->add_variable(variableTypePair.first.getName(), this->integerValues[variableTypePair.first.getOffset()]); + symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->integerValues[variableTypePair.first.getOffset()]); } else if (variableTypePair.second.isRationalType()) { - symbolTable->add_variable(variableTypePair.first.getName(), this->rationalValues[variableTypePair.first.getOffset()]); + symbolTable->add_variable("v" + std::to_string(variableTypePair.first.getIndex()), this->rationalValues[variableTypePair.first.getOffset()]); } } } diff --git a/src/storm/storage/expressions/ToExprtkStringVisitor.cpp b/src/storm/storage/expressions/ToExprtkStringVisitor.cpp index e0326dd09..d9098af2b 100644 --- a/src/storm/storage/expressions/ToExprtkStringVisitor.cpp +++ b/src/storm/storage/expressions/ToExprtkStringVisitor.cpp @@ -167,7 +167,7 @@ namespace storm { } boost::any ToExprtkStringVisitor::visit(VariableExpression const& expression, boost::any const&) { - stream << expression.getVariableName(); + stream << "v" + std::to_string(expression.getVariable().getIndex()); return boost::any(); }