From a7e9c5819ff8100cc2a704fc134840c144088dc2 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sat, 14 Jan 2017 18:31:44 +0100
Subject: [PATCH] removed 'size-in-memory' output as it was outdated and
unreliable. added timing measurements for model construction and model
checking
---
.../jit/ExplicitJitJaniModelBuilder.cpp | 2 +-
src/storm/cli/cli.cpp | 43 +++++--
src/storm/cli/entrypoints.h | 116 +++++++++++-------
src/storm/logic/Formula.cpp | 5 +
src/storm/logic/Formula.h | 1 +
src/storm/logic/LabelSubstitutionVisitor.cpp | 25 +++-
src/storm/logic/LabelSubstitutionVisitor.h | 4 +-
.../modelchecker/results/CheckResult.cpp | 2 +-
src/storm/modelchecker/results/CheckResult.h | 2 +-
src/storm/models/ModelBase.h | 9 +-
src/storm/models/sparse/MarkovAutomaton.cpp | 5 -
src/storm/models/sparse/MarkovAutomaton.h | 4 +-
src/storm/models/sparse/Model.cpp | 13 --
src/storm/models/sparse/Model.h | 9 +-
.../models/sparse/StandardRewardModel.cpp | 16 ---
src/storm/models/sparse/StandardRewardModel.h | 7 --
src/storm/models/sparse/StateLabeling.cpp | 8 --
src/storm/models/sparse/StateLabeling.h | 9 +-
src/storm/models/symbolic/Model.cpp | 7 --
src/storm/models/symbolic/Model.h | 2 -
.../DeterministicSparseTransitionParser.cpp | 2 +-
src/storm/settings/modules/IOSettings.cpp | 1 -
.../solver/GmmxxLinearEquationSolver.cpp | 6 +-
src/storm/storage/SparseMatrix.cpp | 13 --
src/storm/storage/SparseMatrix.h | 7 --
.../storage/SymbolicModelDescription.cpp | 12 ++
src/storm/storage/SymbolicModelDescription.h | 1 +
src/storm/storage/jani/Property.cpp | 4 +
src/storm/storage/jani/Property.h | 6 +
src/storm/storage/prism/Program.cpp | 14 ++-
src/storm/storage/prism/Program.h | 7 ++
src/storm/storage/prism/ToJaniConverter.cpp | 19 ++-
src/storm/storage/prism/ToJaniConverter.h | 11 +-
src/storm/storm.cpp | 2 +-
src/storm/utility/Stopwatch.cpp | 51 ++++++++
src/storm/utility/Stopwatch.h | 86 ++++---------
src/storm/utility/storm.h | 18 ++-
37 files changed, 300 insertions(+), 249 deletions(-)
create mode 100644 src/storm/utility/Stopwatch.cpp
diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 0f37d1b45..2f3b639bd 100644
--- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -1546,7 +1546,7 @@ namespace storm {
STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::WrongFormatException, "Terminal label refers to non-boolean variable '" << variable.getName() << ".");
STORM_LOG_THROW(variable.isTransient(), storm::exceptions::WrongFormatException, "Terminal label refers to non-transient variable '" << variable.getName() << ".");
auto labelExpression = model.getLabelExpression(variable.asBooleanVariable(), parallelAutomata);
- if (terminalEntry.second) {
+ if (!terminalEntry.second) {
labelExpression = !labelExpression;
}
terminalExpressions.push_back(expressionTranslator.translate(shiftVariablesWrtLowerBound(labelExpression), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName)));
diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index e8f1e5f8b..7d0d514cb 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -227,16 +227,29 @@ namespace storm {
propertyFilter = storm::parsePropertyFilter(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getPropertyFilter());
}
+ auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+ auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
if (ioSettings.isPrismOrJaniInputSet()) {
storm::storage::SymbolicModelDescription model;
std::vector<storm::jani::Property> properties;
STORM_LOG_TRACE("Parsing symbolic input.");
+ boost::optional<std::map<std::string, std::string>> labelRenaming;
if (ioSettings.isPrismInputSet()) {
model = storm::parseProgram(ioSettings.getPrismInputFilename());
- if (ioSettings.isPrismToJaniSet()) {
- model = model.toJani(true);
+
+ bool transformToJani = ioSettings.isPrismToJaniSet();
+ bool transformToJaniForJit = coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse && ioSettings.isJitSet();
+ STORM_LOG_WARN_COND(transformToJani || !transformToJaniForJit, "The JIT-based model builder is only available for JANI models, automatically converting the PRISM input model.");
+ transformToJani |= transformToJaniForJit;
+
+ if (transformToJani) {
+ auto modelAndRenaming = model.toJaniWithLabelRenaming(true);
+ if (!modelAndRenaming.second.empty()) {
+ labelRenaming = modelAndRenaming.second;
+ }
+ model = modelAndRenaming.first;
}
} else if (ioSettings.isJaniInputSet()) {
auto input = storm::parseJaniModel(ioSettings.getJaniInputFilename());
@@ -256,11 +269,19 @@ namespace storm {
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
STORM_LOG_TRACE("Parsing properties.");
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
+ if (generalSettings.isPropertySet()) {
if (model.isJaniModel()) {
- properties = storm::parsePropertiesForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel(), propertyFilter);
+ properties = storm::parsePropertiesForJaniModel(generalSettings.getProperty(), model.asJaniModel(), propertyFilter);
+
+ if (labelRenaming) {
+ std::vector<storm::jani::Property> amendedProperties;
+ for (auto const& property : properties) {
+ amendedProperties.emplace_back(property.substituteLabels(labelRenaming.get()));
+ }
+ properties = std::move(amendedProperties);
+ }
} else {
- properties = storm::parsePropertiesForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram(), propertyFilter);
+ properties = storm::parsePropertiesForPrismProgram(generalSettings.getProperty(), model.asPrismProgram(), propertyFilter);
}
constantDefinitions = model.parseConstantDefinitions(constantDefinitionString);
@@ -279,13 +300,13 @@ namespace storm {
}
STORM_LOG_TRACE("Building and checking symbolic model.");
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
+ if (generalSettings.isParametricSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalFunction>(model, properties, true);
#else
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
#endif
- } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+ } else if (generalSettings.isExactSet()) {
#ifdef STORM_HAVE_CARL
buildAndCheckSymbolicModel<storm::RationalNumber>(model, properties, true);
#else
@@ -294,14 +315,14 @@ namespace storm {
} else {
buildAndCheckSymbolicModel<double>(model, properties, true);
}
- } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
- STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
+ } else if (ioSettings.isExplicitSet()) {
+ STORM_LOG_THROW(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
// If the model is given in an explicit format, we parse the properties without allowing expressions
// in formulas.
std::vector<storm::jani::Property> properties;
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
- properties = storm::parsePropertiesForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), propertyFilter);
+ if (generalSettings.isPropertySet()) {
+ properties = storm::parsePropertiesForExplicit(generalSettings.getProperty(), propertyFilter);
}
buildAndCheckExplicitModel<double>(properties, true);
diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h
index 9462f2643..4097d0bc3 100644
--- a/src/storm/cli/entrypoints.h
+++ b/src/storm/cli/entrypoints.h
@@ -7,6 +7,7 @@
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/utility/ExplicitExporter.h"
+#include "storm/utility/Stopwatch.h"
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/InvalidSettingsException.h"
@@ -18,23 +19,22 @@ namespace storm {
template<typename ValueType>
void applyFilterFunctionAndOutput(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) {
-
- if(result->isQuantitative()) {
- switch(ft) {
+ if (result->isQuantitative()) {
+ switch (ft) {
case storm::modelchecker::FilterType::VALUES:
- std::cout << *result << std::endl;
+ STORM_PRINT_AND_LOG(*result << std::endl);
return;
case storm::modelchecker::FilterType::SUM:
- std::cout << result->asQuantitativeCheckResult<ValueType>().sum();
+ STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().sum());
return;
case storm::modelchecker::FilterType::AVG:
- std::cout << result->asQuantitativeCheckResult<ValueType>().average();
+ STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().average());
return;
case storm::modelchecker::FilterType::MIN:
- std::cout << result->asQuantitativeCheckResult<ValueType>().getMin();
+ STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMin());
return;
case storm::modelchecker::FilterType::MAX:
- std::cout << result->asQuantitativeCheckResult<ValueType>().getMax();
+ STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMax());
return;
case storm::modelchecker::FilterType::ARGMIN:
case storm::modelchecker::FilterType::ARGMAX:
@@ -45,18 +45,18 @@ namespace storm {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for qualitative results");
}
} else {
- switch(ft) {
+ switch (ft) {
case storm::modelchecker::FilterType::VALUES:
- std::cout << *result << std::endl;
+ STORM_PRINT_AND_LOG(*result << std::endl);
return;
case storm::modelchecker::FilterType::EXISTS:
- std::cout << result->asQualitativeCheckResult().existsTrue();
+ STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue());
return;
case storm::modelchecker::FilterType::FORALL:
- std::cout << result->asQualitativeCheckResult().forallTrue();
+ STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue());
return;
case storm::modelchecker::FilterType::COUNT:
- std::cout << result->asQualitativeCheckResult().count();
+ STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count());
return;
case storm::modelchecker::FilterType::ARGMIN:
@@ -75,17 +75,19 @@ namespace storm {
template<typename ValueType>
void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
for (auto const& property : properties) {
- std::cout << std::endl << "Model checking property: " << property << " ...";
+ STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
+ storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+ modelCheckingWatch.stop();
if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
+ STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states): ");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
- std::cout << std::endl;
+ STORM_PRINT_AND_LOG(std::endl);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
}
}
}
@@ -96,17 +98,19 @@ namespace storm {
for (auto const& property : properties) {
STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs.");
- std::cout << std::endl << "Model checking property: " << property << " ...";
+ STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
+ storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+ modelCheckingWatch.stop();
if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
+ STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states): ");
result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates()));
applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType());
- std::cout << std::endl;
+ STORM_PRINT_AND_LOG(std::endl);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
}
if (storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultToFile()) {
@@ -120,15 +124,17 @@ namespace storm {
void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
typedef double ValueType;
for (auto const& property : properties) {
- std::cout << std::endl << "Model checking property: " << property << " ...";
+ STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
+ storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithAbstractionRefinementEngine<DdType, ValueType>(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+ modelCheckingWatch.stop();
if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
- std::cout << *result << std::endl;
+ STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states): ");
+ STORM_PRINT_AND_LOG(*result << std::endl);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
}
}
}
@@ -140,18 +146,22 @@ namespace storm {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
for (auto const& property : formulas) {
- std::cout << std::endl << "Model checking property: " << property << " ...";
+ STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
bool formulaSupported = false;
std::unique_ptr<storm::modelchecker::CheckResult> result;
+ storm::utility::Stopwatch modelCheckingWatch(false);
+
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(program);
storm::modelchecker::CheckTask<storm::logic::Formula> task(*property.getFilter().getFormula(), onlyInitialStatesRelevant);
formulaSupported = checker.canHandle(task);
if (formulaSupported) {
+ modelCheckingWatch.start();
result = checker.check(task);
+ modelCheckingWatch.stop();
}
} else if (program.getModelType() == storm::prism::Program::ModelType::MDP) {
storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<ValueType>> checker(program);
@@ -159,23 +169,25 @@ namespace storm {
formulaSupported = checker.canHandle(task);
if (formulaSupported) {
+ modelCheckingWatch.start();
result = checker.check(task);
+ modelCheckingWatch.stop();
}
} else {
// Should be catched before.
assert(false);
}
if (!formulaSupported) {
- std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the formula cannot be handled by the selected engine/method." << std::endl);
}
if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
+ STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states): ");
applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType());
- std::cout << std::endl;
+ STORM_PRINT_AND_LOG(std::endl);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
}
}
}
@@ -190,18 +202,21 @@ namespace storm {
template<storm::dd::DdType DdType>
void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& property : formulas) {
- std::cout << std::endl << "Model checking property: " << property << " ...";
+ STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
+
+ storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+ modelCheckingWatch.stop();
if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
+ STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states): ");
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
- std::cout << std::endl;
+ STORM_PRINT_AND_LOG(std::endl);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
}
}
}
@@ -209,17 +224,20 @@ namespace storm {
template<storm::dd::DdType DdType>
void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& property : formulas) {
- std::cout << std::endl << "Model checking property: " << property << " ...";
+ STORM_PRINT_AND_LOG(std::endl << "Model checking property: " << *property.getRawFormula() << " ..." << std::endl);
std::cout.flush();
+
+ storm::utility::Stopwatch modelCheckingWatch(true);
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant));
+ modelCheckingWatch.stop();
if (result) {
- std::cout << " done." << std::endl;
- std::cout << "Result (initial states): ";
+ STORM_PRINT_AND_LOG("Time for model checking: " << modelCheckingWatch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states): ");
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates()));
applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType());
- std::cout << std::endl;
+ STORM_PRINT_AND_LOG(std::endl);
} else {
- std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+ STORM_PRINT_AND_LOG(" skipped, because the modelling formalism is currently unsupported." << std::endl);
}
}
}
@@ -267,7 +285,10 @@ namespace storm {
template<storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
// Start by building the model.
+ storm::utility::Stopwatch modelBuildingWatch(true);
auto markovModel = buildSymbolicModel<double, LibraryType>(model, extractFormulasFromProperties(properties));
+ modelBuildingWatch.stop();
+ STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
// Print some information about the model.
markovModel->printModelInformationToStream(std::cout);
@@ -284,7 +305,10 @@ namespace storm {
void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) {
auto formulas = extractFormulasFromProperties(properties);
// Start by building the model.
+ storm::utility::Stopwatch modelBuildingWatch(true);
std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas);
+ modelBuildingWatch.stop();
+ STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl);
STORM_LOG_THROW(markovModel, storm::exceptions::UnexpectedException, "The model was not successfully built.");
@@ -359,7 +383,11 @@ namespace storm {
storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>();
STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
+
+ storm::utility::Stopwatch modelBuildingWatch(true);
std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none);
+ modelBuildingWatch.stop();
+ STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl);
// Preprocess the model if needed.
BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, extractFormulasFromProperties(properties));
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index d61129914..9038a2307 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -443,6 +443,11 @@ namespace storm {
return visitor.substitute(*this);
}
+ std::shared_ptr<Formula> Formula::substitute(std::map<std::string, std::string> const& labelSubstitution) const {
+ LabelSubstitutionVisitor visitor(labelSubstitution);
+ return visitor.substitute(*this);
+ }
+
storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) const {
ToExpressionVisitor visitor;
if (labelToExpressionMapping.empty()) {
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 80f31203f..2ad5e9477 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -197,6 +197,7 @@ namespace storm {
std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
std::shared_ptr<Formula> substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const;
+ std::shared_ptr<Formula> substitute(std::map<std::string, std::string> const& labelSubstitution) const;
/*!
* Takes the formula and converts it to an equivalent expression. The formula may contain atomic labels, but
diff --git a/src/storm/logic/LabelSubstitutionVisitor.cpp b/src/storm/logic/LabelSubstitutionVisitor.cpp
index 9794b2530..1e17649a3 100644
--- a/src/storm/logic/LabelSubstitutionVisitor.cpp
+++ b/src/storm/logic/LabelSubstitutionVisitor.cpp
@@ -5,22 +5,35 @@
namespace storm {
namespace logic {
- LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) : labelToExpressionMapping(labelToExpressionMapping) {
+ LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) : labelToExpressionMapping(&labelToExpressionMapping), labelToLabelMapping(nullptr) {
// Intentionally left empty.
}
+ LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, std::string> const& labelToLabelMapping) : labelToExpressionMapping(nullptr), labelToLabelMapping(&labelToLabelMapping) {
+ // Intentionally left empty.
+ }
+
std::shared_ptr<Formula> LabelSubstitutionVisitor::substitute(Formula const& f) const {
boost::any result = f.accept(*this, boost::any());
return boost::any_cast<std::shared_ptr<Formula>>(result);
}
boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
- auto it = labelToExpressionMapping.find(f.getLabel());
- if (it != labelToExpressionMapping.end()) {
- return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(it->second));
+ if (labelToExpressionMapping) {
+ auto it = labelToExpressionMapping->find(f.getLabel());
+ if (it != labelToExpressionMapping->end()) {
+ return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(it->second));
+ } else {
+ return f.asSharedPointer();
+ }
} else {
- return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f));
+ auto it = labelToLabelMapping->find(f.getLabel());
+ if (it != labelToLabelMapping->end()) {
+ return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(it->second));
+ } else {
+ return f.asSharedPointer();
+ }
}
- }
+ }
}
}
diff --git a/src/storm/logic/LabelSubstitutionVisitor.h b/src/storm/logic/LabelSubstitutionVisitor.h
index 928380be5..cac04fa72 100644
--- a/src/storm/logic/LabelSubstitutionVisitor.h
+++ b/src/storm/logic/LabelSubstitutionVisitor.h
@@ -13,13 +13,15 @@ namespace storm {
class LabelSubstitutionVisitor : public CloneVisitor {
public:
LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping);
+ LabelSubstitutionVisitor(std::map<std::string, std::string> const& labelToLabelMapping);
std::shared_ptr<Formula> substitute(Formula const& f) const;
virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
private:
- std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping;
+ std::map<std::string, storm::expressions::Expression> const* labelToExpressionMapping;
+ std::map<std::string, std::string> const* labelToLabelMapping;
};
}
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index 8410c8728..210ca3b59 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -39,7 +39,7 @@ namespace storm {
return false;
}
- std::ostream& operator<<(std::ostream& out, CheckResult& checkResult) {
+ std::ostream& operator<<(std::ostream& out, CheckResult const& checkResult) {
checkResult.writeToStream(out);
return out;
}
diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h
index 8c6b3a880..6cf39669d 100644
--- a/src/storm/modelchecker/results/CheckResult.h
+++ b/src/storm/modelchecker/results/CheckResult.h
@@ -106,7 +106,7 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const = 0;
};
- std::ostream& operator<<(std::ostream& out, CheckResult& checkResult);
+ std::ostream& operator<<(std::ostream& out, CheckResult const& checkResult);
}
}
diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h
index c1a696c03..cbef9a9dc 100644
--- a/src/storm/models/ModelBase.h
+++ b/src/storm/models/ModelBase.h
@@ -60,14 +60,7 @@ namespace storm {
* @return The number of (non-zero) transitions of the model.
*/
virtual uint_fast64_t getNumberOfTransitions() const = 0;
-
- /*!
- * Retrieves (an approximation of) the size of the model in bytes.
- *
- * @return The size of th model in bytes.
- */
- virtual std::size_t getSizeInBytes() const = 0;
-
+
/*!
* Prints information about the model to the specified stream.
*
diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp
index 40f9003c5..069ed1936 100644
--- a/src/storm/models/sparse/MarkovAutomaton.cpp
+++ b/src/storm/models/sparse/MarkovAutomaton.cpp
@@ -236,11 +236,6 @@ namespace storm {
}
}
- template <typename ValueType, typename RewardModelType>
- std::size_t MarkovAutomaton<ValueType, RewardModelType>::getSizeInBytes() const {
- return NondeterministicModel<ValueType, RewardModelType>::getSizeInBytes() + markovianStates.getSizeInBytes() + exitRates.size() * sizeof(ValueType);
- }
-
template <typename ValueType, typename RewardModelType>
void MarkovAutomaton<ValueType, RewardModelType>::turnRatesToProbabilities() {
this->exitRates.resize(this->getNumberOfStates());
diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h
index cd45b141b..477d0ee5f 100644
--- a/src/storm/models/sparse/MarkovAutomaton.h
+++ b/src/storm/models/sparse/MarkovAutomaton.h
@@ -194,9 +194,7 @@ namespace storm {
std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCTMC() const;
virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr, std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr, std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr, bool finalizeOutput = true) const override;
-
- std::size_t getSizeInBytes() const override;
-
+
virtual void printModelInformationToStream(std::ostream& out) const override;
private:
diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp
index 890cfdae7..3f7774759 100644
--- a/src/storm/models/sparse/Model.cpp
+++ b/src/storm/models/sparse/Model.cpp
@@ -188,18 +188,6 @@ namespace storm {
return static_cast<bool>(choiceLabeling);
}
- template<typename ValueType, typename RewardModelType>
- std::size_t Model<ValueType, RewardModelType>::getSizeInBytes() const {
- std::size_t result = transitionMatrix.getSizeInBytes() + stateLabeling.getSizeInBytes();
- for (auto const& rewardModel : this->rewardModels) {
- result += rewardModel.second.getSizeInBytes();
- }
- if (hasChoiceLabeling()) {
- result += getChoiceLabeling().size() * sizeof(LabelSet);
- }
- return result;
- }
-
template<typename ValueType, typename RewardModelType>
void Model<ValueType, RewardModelType>::printModelInformationToStream(std::ostream& out) const {
this->printModelInformationHeaderToStream(out);
@@ -219,7 +207,6 @@ namespace storm {
this->printRewardModelsInformationToStream(out);
this->getStateLabeling().printLabelingInformationToStream(out);
out << "choice labels: \t" << (this->hasChoiceLabeling() ? "yes" : "no") << std::noboolalpha << std::endl;
- out << "Size in memory: " << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
out << "-------------------------------------------------------------- " << std::endl;
}
diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h
index 70358191a..a545ae3ce 100644
--- a/src/storm/models/sparse/Model.h
+++ b/src/storm/models/sparse/Model.h
@@ -275,14 +275,7 @@ namespace storm {
* properties, but it preserves expected rewards.
*/
virtual void reduceToStateBasedRewards() = 0;
-
- /*!
- * Retrieves (an approximation of) the size of the model in bytes.
- *
- * @return The size of the internal representation of the model measured in bytes.
- */
- virtual std::size_t getSizeInBytes() const override;
-
+
/*!
* Prints information about the model to the specified stream.
*
diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp
index 59dfee941..fa2b63900 100644
--- a/src/storm/models/sparse/StandardRewardModel.cpp
+++ b/src/storm/models/sparse/StandardRewardModel.cpp
@@ -270,22 +270,6 @@ namespace storm {
return true;
}
-
- template<typename ValueType>
- std::size_t StandardRewardModel<ValueType>::getSizeInBytes() const {
- std::size_t result = 0;
- if (this->hasStateRewards()) {
- result += this->getStateRewardVector().size() * sizeof(ValueType);
- }
- if (this->hasStateActionRewards()) {
- result += this->getStateActionRewardVector().size() * sizeof(ValueType);
- }
- if (this->hasTransitionRewards()) {
- result += this->getTransitionRewardMatrix().getSizeInBytes();
- }
- return result;
- }
-
template <typename ValueType>
std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueType> const& rewardModel) {
out << std::boolalpha << "reward model [state reward: "
diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h
index 85d6b5382..dbf484c40 100644
--- a/src/storm/models/sparse/StandardRewardModel.h
+++ b/src/storm/models/sparse/StandardRewardModel.h
@@ -274,13 +274,6 @@ namespace storm {
* @param nrChoices The number of choices in the model
*/
bool isCompatible(uint_fast64_t nrStates, uint_fast64_t nrChoices) const;
-
- /*!
- * Retrieves (an approximation of) the size of the model in bytes.
- *
- * @return The size of the internal representation of the model measured in bytes.
- */
- std::size_t getSizeInBytes() const;
template <typename ValueTypePrime>
friend std::ostream& operator<<(std::ostream& out, StandardRewardModel<ValueTypePrime> const& rewardModel);
diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp
index b3037d173..55eaa76d5 100644
--- a/src/storm/models/sparse/StateLabeling.cpp
+++ b/src/storm/models/sparse/StateLabeling.cpp
@@ -109,14 +109,6 @@ namespace storm {
this->labelings[nameToLabelingIndexMap.at(label)] = labeling;
}
- std::size_t StateLabeling::getSizeInBytes() const {
- std::size_t result = sizeof(*this);
- if (!labelings.empty()) {
- result += labelings.size() * labelings.front().getSizeInBytes();
- }
- return result;
- }
-
void StateLabeling::printLabelingInformationToStream(std::ostream& out) const {
out << "Labels: \t" << this->getNumberOfLabels() << std::endl;
for (auto const& labelIndexPair : this->nameToLabelingIndexMap) {
diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h
index c3de34599..330a4d8fe 100644
--- a/src/storm/models/sparse/StateLabeling.h
+++ b/src/storm/models/sparse/StateLabeling.h
@@ -145,14 +145,7 @@ namespace storm {
* @param labeling A bit vector that represents the set of states that will get this label.
*/
void setStates(std::string const& label, storage::BitVector&& labeling);
-
- /*!
- * Returns (an approximation of) the size of the labeling measured in bytes.
- *
- * @return The size of the labeling measured in bytes.
- */
- std::size_t getSizeInBytes() const;
-
+
/*!
* Prints information about the labeling to the specified stream.
*
diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp
index 29f1d6ec7..1ebf69f48 100644
--- a/src/storm/models/symbolic/Model.cpp
+++ b/src/storm/models/symbolic/Model.cpp
@@ -114,12 +114,6 @@ namespace storm {
return this->getTransitionMatrix().notZero();
}
- template<storm::dd::DdType Type, typename ValueType>
- std::size_t Model<Type, ValueType>::getSizeInBytes() const {
- // FIXME: This assumes a fixed value of 16 bytes per node, which isn't necessarily true.
- return sizeof(*this) + 16 * (reachableStates.getNodeCount() + initialStates.getNodeCount() + transitionMatrix.getNodeCount());
- }
-
template<storm::dd::DdType Type, typename ValueType>
std::set<storm::expressions::Variable> const& Model<Type, ValueType>::getRowVariables() const {
return rowVariables;
@@ -222,7 +216,6 @@ namespace storm {
for (auto const& label : labelToExpressionMap) {
out << " * " << label.first << std::endl;
}
- out << "Size in memory: \t" << (this->getSizeInBytes())/1024 << " kbytes" << std::endl;
out << "-------------------------------------------------------------- " << std::endl;
}
diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h
index 629f39411..14c4edbc5 100644
--- a/src/storm/models/symbolic/Model.h
+++ b/src/storm/models/symbolic/Model.h
@@ -254,8 +254,6 @@ namespace storm {
*/
uint_fast64_t getNumberOfRewardModels() const;
- virtual std::size_t getSizeInBytes() const override;
-
virtual void printModelInformationToStream(std::ostream& out) const override;
virtual bool isSymbolicModel() const override;
diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp
index 984f3cbc2..7b53415cb 100644
--- a/src/storm/parser/DeterministicSparseTransitionParser.cpp
+++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp
@@ -54,7 +54,7 @@ namespace storm {
bool insertDiagonalEntriesIfMissing = !isRewardFile;
DeterministicSparseTransitionParser<ValueType>::FirstPassResult firstPass = DeterministicSparseTransitionParser<ValueType>::firstPass(file.getData(), insertDiagonalEntriesIfMissing);
- STORM_LOG_INFO("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " NonZeros.");
+ STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros.");
// If first pass returned zero, the file format was wrong.
if (firstPass.numberOfNonzeroEntries == 0) {
diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp
index c65b8797c..bf8055c31 100644
--- a/src/storm/settings/modules/IOSettings.cpp
+++ b/src/storm/settings/modules/IOSettings.cpp
@@ -195,7 +195,6 @@ namespace storm {
return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString());
}
-
bool IOSettings::isPrismCompatibilityEnabled() const {
return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet();
}
diff --git a/src/storm/solver/GmmxxLinearEquationSolver.cpp b/src/storm/solver/GmmxxLinearEquationSolver.cpp
index 5ecd10f4c..ecccd4682 100644
--- a/src/storm/solver/GmmxxLinearEquationSolver.cpp
+++ b/src/storm/solver/GmmxxLinearEquationSolver.cpp
@@ -138,7 +138,7 @@ namespace storm {
bool GmmxxLinearEquationSolver<ValueType>::solveEquations(std::vector<ValueType>& x, std::vector<ValueType> const& b) const {
auto method = this->getSettings().getSolutionMethod();
auto preconditioner = this->getSettings().getPreconditioner();
- STORM_LOG_INFO("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations).");
+ STORM_LOG_DEBUG("Using method '" << method << "' with preconditioner '" << preconditioner << "' (max. " << this->getSettings().getMaximalNumberOfIterations() << " iterations).");
if (method == GmmxxLinearEquationSolverSettings<ValueType>::SolutionMethod::Jacobi && preconditioner != GmmxxLinearEquationSolverSettings<ValueType>::Preconditioner::None) {
STORM_LOG_WARN("Jacobi method currently does not support preconditioners. The requested preconditioner will be ignored.");
}
@@ -193,7 +193,7 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (iter.converged()) {
- STORM_LOG_INFO("Iterative solver converged after " << iter.get_iteration() << " iterations.");
+ STORM_LOG_DEBUG("Iterative solver converged after " << iter.get_iteration() << " iterations.");
return true;
} else {
STORM_LOG_WARN("Iterative solver did not converge.");
@@ -204,7 +204,7 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
if (iterations < this->getSettings().getMaximalNumberOfIterations()) {
- STORM_LOG_INFO("Iterative solver converged after " << iterations << " iterations.");
+ STORM_LOG_DEBUG("Iterative solver converged after " << iterations << " iterations.");
return true;
} else {
STORM_LOG_WARN("Iterative solver did not converge.");
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index 8794ac759..3f70b8f2a 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -1295,19 +1295,6 @@ namespace storm {
}
}
- template<typename ValueType>
- std::size_t SparseMatrix<ValueType>::getSizeInBytes() const {
- uint_fast64_t size = sizeof(*this);
-
- // Add size of columns and values.
- size += sizeof(MatrixEntry<index_type, ValueType>) * columnsAndValues.capacity();
-
- // Add row_indications size.
- size += sizeof(uint_fast64_t) * rowIndications.capacity();
-
- return size;
- }
-
template<typename ValueType>
typename SparseMatrix<ValueType>::const_rows SparseMatrix<ValueType>::getRows(index_type startRow, index_type endRow) const {
return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]);
diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h
index a7cfc7b83..f897e1606 100644
--- a/src/storm/storage/SparseMatrix.h
+++ b/src/storm/storage/SparseMatrix.h
@@ -846,13 +846,6 @@ namespace storm {
* @out The stream to output to.
*/
void printAsMatlabMatrix(std::ostream& out) const;
-
- /*!
- * Returns the size of the matrix in memory measured in bytes.
- *
- * @return The size of the matrix in memory measured in bytes.
- */
- std::size_t getSizeInBytes() const;
/*!
* Calculates a hash value over all values contained in the matrix.
diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp
index da985d103..92b52c783 100644
--- a/src/storm/storage/SymbolicModelDescription.cpp
+++ b/src/storm/storage/SymbolicModelDescription.cpp
@@ -126,6 +126,18 @@ namespace storm {
}
}
+ std::pair<SymbolicModelDescription, std::map<std::string, std::string>> SymbolicModelDescription::toJaniWithLabelRenaming(bool makeVariablesGlobal) const {
+ if (this->isJaniModel()) {
+ return std::make_pair(*this, std::map<std::string, std::string>());
+ }
+ if (this->isPrismProgram()) {
+ auto modelAndRenaming = this->asPrismProgram().toJaniWithLabelRenaming(makeVariablesGlobal);
+ return std::make_pair(SymbolicModelDescription(modelAndRenaming.first), modelAndRenaming.second);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format.");
+ }
+ }
+
SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const {
std::map<storm::expressions::Variable, storm::expressions::Expression> substitution = parseConstantDefinitions(constantDefinitionString);
if (this->isJaniModel()) {
diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h
index 8ed9fa7e0..05daa5ec2 100644
--- a/src/storm/storage/SymbolicModelDescription.h
+++ b/src/storm/storage/SymbolicModelDescription.h
@@ -39,6 +39,7 @@ namespace storm {
std::vector<std::string> getParameterNames() const;
SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const;
+ std::pair<SymbolicModelDescription, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool makeVariablesGlobal = true) const;
SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
SymbolicModelDescription preprocess(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const;
diff --git a/src/storm/storage/jani/Property.cpp b/src/storm/storage/jani/Property.cpp
index 896810526..e46d2ee50 100644
--- a/src/storm/storage/jani/Property.cpp
+++ b/src/storm/storage/jani/Property.cpp
@@ -32,6 +32,10 @@ namespace storm {
return Property(name, filterExpression.substitute(substitution), comment);
}
+ Property Property::substituteLabels(std::map<std::string, std::string> const& substitution) const {
+ return Property(name, filterExpression.substituteLabels(substitution), comment);
+ }
+
FilterExpression const& Property::getFilter() const {
return this->filterExpression;
}
diff --git a/src/storm/storage/jani/Property.h b/src/storm/storage/jani/Property.h
index 9d28d715a..f97341c53 100644
--- a/src/storm/storage/jani/Property.h
+++ b/src/storm/storage/jani/Property.h
@@ -42,6 +42,11 @@ namespace storm {
FilterExpression substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
return FilterExpression(formula->substitute(substitution), ft);
}
+
+ FilterExpression substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const {
+ return FilterExpression(formula->substitute(labelSubstitution), ft);
+ }
+
private:
// For now, we assume that the states are always the initial states.
std::shared_ptr<storm::logic::Formula const> formula;
@@ -84,6 +89,7 @@ namespace storm {
std::string const& getComment() const;
Property substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+ Property substituteLabels(std::map<std::string, std::string> const& labelSubstitution) const;
FilterExpression const& getFilter() const;
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index c521d9c29..b96a1c7d2 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -5,6 +5,7 @@
#include <boost/algorithm/string/join.hpp>
#include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/Property.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/settings/SettingsManager.h"
@@ -1009,7 +1010,6 @@ namespace storm {
std::set<storm::expressions::Variable> variablesAndConstants;
std::set_union(variables.begin(), variables.end(), constants.begin(), constants.end(), std::inserter(variablesAndConstants, variablesAndConstants.begin()));
-
// Check the commands of the modules.
bool hasProbabilisticCommand = false;
bool hasMarkovianCommand = false;
@@ -1627,9 +1627,17 @@ namespace storm {
storm::jani::Model Program::toJani(bool allVariablesGlobal) const {
ToJaniConverter converter;
- return converter.convert(*this, allVariablesGlobal);
+ storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal);
+ STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
+ return resultingModel;
}
-
+
+ std::pair<storm::jani::Model, std::map<std::string, std::string>> Program::toJaniWithLabelRenaming(bool allVariablesGlobal) const {
+ ToJaniConverter converter;
+ storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal);
+ return std::make_pair(resultingModel, converter.getLabelRenaming());
+ }
+
storm::expressions::ExpressionManager& Program::getManager() const {
return *this->manager;
}
diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h
index a33484833..ccf56ead6 100644
--- a/src/storm/storage/prism/Program.h
+++ b/src/storm/storage/prism/Program.h
@@ -22,6 +22,7 @@
namespace storm {
namespace jani {
class Model;
+ class Property;
}
namespace prism {
@@ -587,6 +588,12 @@ namespace storm {
*/
storm::jani::Model toJani(bool allVariablesGlobal = false) const;
+ /*!
+ * Converts the PRISM model into an equivalent JANI model and retrieves possible label renamings that had
+ * to be performed in the process.
+ */
+ std::pair<storm::jani::Model, std::map<std::string, std::string>> toJaniWithLabelRenaming(bool allVariablesGlobal = false) const;
+
private:
/*!
* This function builds a command that corresponds to the synchronization of the given list of commands.
diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp
index 4e451d177..21a806374 100644
--- a/src/storm/storage/prism/ToJaniConverter.cpp
+++ b/src/storm/storage/prism/ToJaniConverter.cpp
@@ -12,7 +12,7 @@
namespace storm {
namespace prism {
- storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal) const {
+ storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal) {
std::shared_ptr<storm::expressions::ExpressionManager> manager = program.getManager().getSharedPointer();
// Start by creating an empty JANI model.
@@ -97,9 +97,14 @@ namespace storm {
// Go through the labels and construct assignments to transient variables that are added to the loctions.
std::vector<storm::jani::Assignment> transientLocationAssignments;
for (auto const& label : program.getLabels()) {
- auto newExpressionVariable = manager->declareBooleanVariable("label_" + label.getName());
+ bool renameLabel = manager->hasVariable(label.getName()) || program.hasRewardModel(label.getName());
+ std::string finalLabelName = renameLabel ? "label_" + label.getName() : label.getName();
+ if (renameLabel) {
+ STORM_LOG_WARN_COND(!renameLabel, "Label '" << label.getName() << "' was renamed to '" << finalLabelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists.");
+ labelRenaming[label.getName()] = finalLabelName;
+ }
+ auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName);
storm::jani::BooleanVariable const& newTransientVariable = janiModel.addVariable(storm::jani::BooleanVariable(newExpressionVariable.getName(), newExpressionVariable, manager->boolean(false), true));
-
transientLocationAssignments.emplace_back(newTransientVariable, label.getStatePredicateExpression());
}
@@ -284,5 +289,13 @@ namespace storm {
return janiModel;
}
+ bool ToJaniConverter::labelsWereRenamed() const {
+ return !labelRenaming.empty();
+ }
+
+ std::map<std::string, std::string> const& ToJaniConverter::getLabelRenaming() const {
+ return labelRenaming;
+ }
+
}
}
diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h
index bc32a3dd8..2ab5c0509 100644
--- a/src/storm/storage/prism/ToJaniConverter.h
+++ b/src/storm/storage/prism/ToJaniConverter.h
@@ -1,5 +1,8 @@
#pragma once
+#include <map>
+#include <string>
+
namespace storm {
namespace jani {
class Model;
@@ -11,7 +14,13 @@ namespace storm {
class ToJaniConverter {
public:
- storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false) const;
+ storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false);
+
+ bool labelsWereRenamed() const;
+ std::map<std::string, std::string> const& getLabelRenaming() const;
+
+ private:
+ std::map<std::string, std::string> labelRenaming;
};
}
diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp
index 7ce7611dc..20126f488 100644
--- a/src/storm/storm.cpp
+++ b/src/storm/storm.cpp
@@ -32,7 +32,7 @@ int main(const int argc, const char** argv) {
totalTimer.stop();
if (storm::settings::getModule<storm::settings::modules::ResourceSettings>().isPrintTimeAndMemorySet()) {
- storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeMilliseconds());
+ storm::cli::showTimeAndMemoryStatistics(totalTimer.getTimeInMilliseconds());
}
return 0;
} catch (storm::exceptions::BaseException const& exception) {
diff --git a/src/storm/utility/Stopwatch.cpp b/src/storm/utility/Stopwatch.cpp
new file mode 100644
index 000000000..fd77c0d59
--- /dev/null
+++ b/src/storm/utility/Stopwatch.cpp
@@ -0,0 +1,51 @@
+#include "storm/utility/Stopwatch.h"
+
+namespace storm {
+ namespace utility {
+
+ Stopwatch::Stopwatch(bool startNow) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
+ if (startNow) {
+ start();
+ }
+ }
+
+ Stopwatch::SecondType Stopwatch::getTimeInSeconds() const {
+ return std::chrono::duration_cast<std::chrono::seconds>(accumulatedTime).count();
+ }
+
+ Stopwatch::MilisecondType Stopwatch::getTimeInMilliseconds() const {
+ return std::chrono::duration_cast<std::chrono::milliseconds>(accumulatedTime).count();
+ }
+
+ Stopwatch::NanosecondType Stopwatch::getTimeInNanoseconds() const {
+ return accumulatedTime.count();
+ }
+
+ void Stopwatch::addToTime(std::chrono::nanoseconds timeNanoseconds) {
+ accumulatedTime += timeNanoseconds;
+ }
+
+ void Stopwatch::stop() {
+ STORM_LOG_WARN_COND(!stopped, "Stopwatch is already paused.");
+ stopped = true;
+ accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement;
+ }
+
+ void Stopwatch::start() {
+ STORM_LOG_WARN_COND(stopped, "Stopwatch is already running.");
+ stopped = false;
+ startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
+ }
+
+ void Stopwatch::reset() {
+ accumulatedTime = std::chrono::nanoseconds::zero();
+ stopped = true;
+ }
+
+ std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {
+ out << stopwatch.getTimeInSeconds() << "." << (stopwatch.getTimeInMilliseconds() % 1000) << "s";
+ return out;
+ }
+
+ }
+}
diff --git a/src/storm/utility/Stopwatch.h b/src/storm/utility/Stopwatch.h
index a30b40683..4f81ea8a8 100644
--- a/src/storm/utility/Stopwatch.h
+++ b/src/storm/utility/Stopwatch.h
@@ -13,106 +13,68 @@ namespace storm {
*/
class Stopwatch {
public:
-
+ typedef decltype(std::chrono::duration_cast<std::chrono::seconds>(std::chrono::seconds::zero()).count()) SecondType;
+ typedef decltype(std::chrono::duration_cast<std::chrono::milliseconds>(std::chrono::milliseconds::zero()).count()) MilisecondType;
+ typedef decltype(std::chrono::duration_cast<std::chrono::nanoseconds>(std::chrono::nanoseconds::zero()).count()) NanosecondType;
+
/*!
* Constructor.
*
* @param startNow If true, the stopwatch starts right away.
*/
- Stopwatch(bool startNow = false) : accumulatedTime(std::chrono::nanoseconds::zero()), stopped(true), startOfCurrentMeasurement(std::chrono::nanoseconds::zero()) {
- if (startNow) {
- start();
- }
- }
-
- /*!
- * Destructor.
- */
- ~Stopwatch() = default;
+ Stopwatch(bool startNow = false);
/*!
- * Get measured time in seconds.
- *
- * @return seconds as floating point number.
+ * Gets the measured time in seconds.
*/
- double getTimeSeconds() const {
- return std::chrono::duration<float>(accumulatedTime).count();
- }
+ SecondType getTimeInSeconds() const;
/*!
- * Get measured time in milliseconds.
- *
- * @return Milliseconds.
+ * Gets the measured time in milliseconds.
*/
- unsigned long long int getTimeMilliseconds() const {
- return std::chrono::duration_cast<std::chrono::milliseconds>(accumulatedTime).count();
- }
+ MilisecondType getTimeInMilliseconds() const;
/*!
- * Get measured time in nanoseconds.
- *
- * @return Nanoseconds.
+ * Gets the measured time in nanoseconds.
*/
- unsigned long long int getTimeNanoseconds() const {
- return accumulatedTime.count();
- }
+ NanosecondType getTimeInNanoseconds() const;
/*!
* Add given time to measured time.
*
* @param timeNanoseconds Additional time in nanoseconds.
*/
- void addToTime(std::chrono::nanoseconds timeNanoseconds) {
- accumulatedTime += timeNanoseconds;
- }
+ void addToTime(std::chrono::nanoseconds timeNanoseconds);
/*!
* Stop stopwatch and add measured time to total time.
*/
- void stop() {
- if (stopped) {
- // Assertions are only available in DEBUG build and therefore not used here.
- STORM_LOG_WARN("Stopwatch is already paused.");
- }
- stopped = true;
- accumulatedTime += std::chrono::high_resolution_clock::now() - startOfCurrentMeasurement;
- }
+ void stop();
/*!
* Start stopwatch (again) and start measuring time.
*/
- void start() {
- if (!stopped) {
- // Assertions are only available in DEBUG build and therefore not used here.
- STORM_LOG_WARN("Stopwatch is already running.");
- }
- stopped = false;
- startOfCurrentMeasurement = std::chrono::high_resolution_clock::now();
- }
+ void start();
/*!
- * Reset the stopwatch. Reset the measured time to zero and stop the stopwatch.
+ * Reset the stopwatch.
*/
- void reset() {
- accumulatedTime = std::chrono::nanoseconds::zero();
- stopped = true;
- }
+ void reset();
- friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch) {
- out << stopwatch.getTimeSeconds();
- return out;
- }
-
+ friend std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch);
private:
- // Total measured time
+ // The time accumulated so far.
std::chrono::nanoseconds accumulatedTime;
- // Flag indicating if the stopwatch is stopped right now.
+
+ // A flag indicating if the stopwatch is stopped right now.
bool stopped;
- // Timepoint when the stopwatch was started the last time.
- std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;
+ // The timepoint when the stopwatch was started the last time (if it's not stopped).
+ std::chrono::high_resolution_clock::time_point startOfCurrentMeasurement;
};
+
+ std::ostream& operator<<(std::ostream& out, Stopwatch const& stopwatch);
}
}
diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h
index 46fcfdb67..7e81f2a36 100644
--- a/src/storm/utility/storm.h
+++ b/src/storm/utility/storm.h
@@ -96,7 +96,7 @@
#include "storm/exceptions/NotImplementedException.h"
#include "storm/exceptions/NotSupportedException.h"
-#include "storm/storage/jani/JSONExporter.h"
+#include "storm/utility/Stopwatch.h"
namespace storm {
@@ -231,7 +231,11 @@ namespace storm {
template<typename ModelType>
std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ storm::utility::Stopwatch preprocessingWatch(true);
+
+ bool operationPerformed = false;
if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
+ operationPerformed = true;
std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
ma->close();
if (ma->hasOnlyTrivialNondeterminism()) {
@@ -241,6 +245,7 @@ namespace storm {
}
if (model->isSparseModel() && storm::settings::getModule<storm::settings::modules::GeneralSettings>().isBisimulationSet()) {
+ operationPerformed = true;
storm::storage::BisimulationType bisimType = storm::storage::BisimulationType::Strong;
if (storm::settings::getModule<storm::settings::modules::BisimulationSettings>().isWeakBisimulationSet()) {
bisimType = storm::storage::BisimulationType::Weak;
@@ -250,6 +255,11 @@ namespace storm {
return performBisimulationMinimization<ModelType>(model->template as<storm::models::sparse::Model<typename ModelType::ValueType>>(), formulas, bisimType);
}
+ preprocessingWatch.stop();
+ if (operationPerformed) {
+ STORM_PRINT_AND_LOG(std::endl << "Time for model preprocessing: " << preprocessingWatch << "." << std::endl << std::endl);
+ }
+
return model;
}
@@ -300,17 +310,17 @@ namespace storm {
switch(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine()) {
case storm::settings::modules::CoreSettings::Engine::Sparse: {
std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
- STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
+ STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model.");
return (sparseModel, formula, onlyInitialStatesRelevant);
}
case storm::settings::modules::CoreSettings::Engine::Hybrid: {
std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
- STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model");
+ STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a DD-based input model.");
return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant);
}
case storm::settings::modules::CoreSettings::Engine::Dd: {
std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
- STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
+ STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a DD-based input model.");
return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
}
default: {