From a08cb4ac1854491a5852977a8bc8c08457734f3c Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 12 Jul 2018 11:51:11 +0200
Subject: [PATCH] making game solver respect equation solver format
---
src/storm-pars-cli/storm-pars.cpp | 252 ++++++++++++------
.../SparseCtmcInstantiationModelChecker.cpp | 27 ++
.../SparseCtmcInstantiationModelChecker.h | 28 ++
.../SparseDtmcInstantiationModelChecker.cpp | 6 +-
.../SparseInstantiationModelChecker.cpp | 6 +-
.../SparseMdpInstantiationModelChecker.cpp | 2 +-
.../settings/modules/ParametricSettings.cpp | 6 +
.../settings/modules/ParametricSettings.h | 6 +
src/storm/solver/StandardGameSolver.cpp | 4 +-
.../TopologicalLinearEquationSolver.cpp | 4 +-
10 files changed, 245 insertions(+), 96 deletions(-)
create mode 100644 src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp
create mode 100644 src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index ff7c075f8..32d63ae52 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -15,6 +15,8 @@
#include "storm/utility/Stopwatch.h"
#include "storm/utility/macros.h"
+#include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h"
+
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/IOSettings.h"
@@ -29,7 +31,19 @@ namespace storm {
typedef typename storm::cli::SymbolicInput SymbolicInput;
-
+ template <typename ValueType>
+ struct SampleInformation {
+ SampleInformation(bool graphPreserving = false) : graphPreserving(graphPreserving) {
+ // Intentionally left empty.
+ }
+
+ bool empty() const {
+ return cartesianProducts.empty();
+ }
+
+ std::vector<std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>>> cartesianProducts;
+ bool graphPreserving;
+ };
template <typename ValueType>
std::vector<storm::storage::ParameterRegion<ValueType>> parseRegions(std::shared_ptr<storm::models::ModelBase> const& model) {
@@ -42,12 +56,12 @@ namespace storm {
}
template <typename ValueType>
- std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> parseSamples(std::shared_ptr<storm::models::ModelBase> const& model, std::string const& sampleString) {
+ SampleInformation<ValueType> parseSamples(std::shared_ptr<storm::models::ModelBase> const& model, std::string const& sampleString, bool graphPreserving) {
STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Sampling is only supported for sparse models.");
- std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> samplesForVariables;
+ SampleInformation<ValueType> sampleInfo(graphPreserving);
if (sampleString.empty()) {
- return samplesForVariables;
+ return sampleInfo;
}
// Get all parameters from the model.
@@ -56,52 +70,59 @@ namespace storm {
modelParameters = storm::models::sparse::getProbabilityParameters(sparseModel);
auto rewParameters = storm::models::sparse::getRewardParameters(sparseModel);
modelParameters.insert(rewParameters.begin(), rewParameters.end());
-
- // Get the values string for each variable.
- std::vector<std::string> valuesForVariables;
- boost::split(valuesForVariables, sampleString, boost::is_any_of(","));
- for (auto& values : valuesForVariables) {
- boost::trim(values);
- }
-
- std::set<typename utility::parametric::VariableType<ValueType>::type> encounteredParameters;
- for (auto const& varValues : valuesForVariables) {
- auto equalsPosition = varValues.find("=");
- STORM_LOG_THROW(equalsPosition != varValues.npos, storm::exceptions::WrongFormatException, "Incorrect format of samples.");
- std::string variableName = varValues.substr(0, equalsPosition);
- boost::trim(variableName);
- std::string values = varValues.substr(equalsPosition + 1);
- boost::trim(values);
+
+ std::vector<std::string> cartesianProducts;
+ boost::split(cartesianProducts, sampleString, boost::is_any_of(";"));
+ for (auto& product : cartesianProducts) {
+ boost::trim(product);
- bool foundParameter = false;
- typename utility::parametric::VariableType<ValueType>::type theParameter;
- for (auto const& parameter : modelParameters) {
- std::stringstream parameterStream;
- parameterStream << parameter;
- std::cout << parameterStream.str() << " vs " << variableName << std::endl;
- if (parameterStream.str() == variableName) {
- foundParameter = true;
- theParameter = parameter;
- encounteredParameters.insert(parameter);
- }
+ // Get the values string for each variable.
+ std::vector<std::string> valuesForVariables;
+ boost::split(valuesForVariables, product, boost::is_any_of(","));
+ for (auto& values : valuesForVariables) {
+ boost::trim(values);
}
- STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'.");
-
- std::vector<std::string> splitValues;
- boost::split(splitValues, values, boost::is_any_of(":"));
- STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter.");
- auto& list = samplesForVariables[theParameter];
- for (auto& value : splitValues) {
- boost::trim(value);
+ std::set<typename utility::parametric::VariableType<ValueType>::type> encounteredParameters;
+ sampleInfo.cartesianProducts.emplace_back();
+ auto& newCartesianProduct = sampleInfo.cartesianProducts.back();
+ for (auto const& varValues : valuesForVariables) {
+ auto equalsPosition = varValues.find("=");
+ STORM_LOG_THROW(equalsPosition != varValues.npos, storm::exceptions::WrongFormatException, "Incorrect format of samples.");
+ std::string variableName = varValues.substr(0, equalsPosition);
+ boost::trim(variableName);
+ std::string values = varValues.substr(equalsPosition + 1);
+ boost::trim(values);
+
+ bool foundParameter = false;
+ typename utility::parametric::VariableType<ValueType>::type theParameter;
+ for (auto const& parameter : modelParameters) {
+ std::stringstream parameterStream;
+ parameterStream << parameter;
+ if (parameterStream.str() == variableName) {
+ foundParameter = true;
+ theParameter = parameter;
+ encounteredParameters.insert(parameter);
+ }
+ }
+ STORM_LOG_THROW(foundParameter, storm::exceptions::WrongFormatException, "Unknown parameter '" << variableName << "'.");
+
+ std::vector<std::string> splitValues;
+ boost::split(splitValues, values, boost::is_any_of(":"));
+ STORM_LOG_THROW(!splitValues.empty(), storm::exceptions::WrongFormatException, "Expecting at least one value per parameter.");
- list.push_back(storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(value));
+ auto& list = newCartesianProduct[theParameter];
+
+ for (auto& value : splitValues) {
+ boost::trim(value);
+ list.push_back(storm::utility::convertNumber<typename utility::parametric::CoefficientType<ValueType>::type>(value));
+ }
}
+
+ STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples.");
}
- STORM_LOG_THROW(encounteredParameters == modelParameters, storm::exceptions::WrongFormatException, "Variables for all parameters are required when providing samples.")
-
- return samplesForVariables;
+ return sampleInfo;
}
template <typename ValueType>
@@ -169,9 +190,24 @@ namespace storm {
}
template<typename ValueType>
- void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr) {
+ void printInitialStatesResult(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::jani::Property const& property, storm::utility::Stopwatch* watch = nullptr, storm::utility::parametric::Valuation<ValueType> const* valuation = nullptr) {
if (result) {
- STORM_PRINT_AND_LOG("Result (initial states): " << std::endl);
+ STORM_PRINT_AND_LOG("Result (initial states)");
+ if (valuation) {
+ bool first = true;
+ std::stringstream ss;
+ for (auto const& entry : *valuation) {
+ if (!first) {
+ ss << ", ";
+ } else {
+ first = false;
+ }
+ ss << entry.first << "=" << entry.second;
+ }
+
+ STORM_PRINT_AND_LOG(" for instance [" << ss.str() << "]");
+ }
+ STORM_PRINT_AND_LOG(": ")
auto const* regionCheckResult = dynamic_cast<storm::modelchecker::RegionCheckResult<ValueType> const*>(result.get());
if (regionCheckResult != nullptr) {
@@ -195,7 +231,7 @@ namespace storm {
STORM_PRINT_AND_LOG(*result << std::endl);
}
if (watch) {
- STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl);
+ STORM_PRINT_AND_LOG("Time for model checking: " << *watch << "." << std::endl << std::endl);
}
} else {
STORM_PRINT_AND_LOG(" failed, property is unsupported by selected engine/settings." << std::endl);
@@ -214,8 +250,78 @@ namespace storm {
}
}
+ template<template<typename, typename> class ModelCheckerType, typename ModelType, typename ValueType, typename SolveValueType = double>
+ void verifyPropertiesAtSamplePoints(ModelType const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
+
+ // When samples are provided, we create an instantiation model checker.
+ ModelCheckerType<ModelType, SolveValueType> modelchecker(model);
+
+ for (auto const& property : input.properties) {
+ storm::cli::printModelCheckingProperty(property);
+
+ modelchecker.specifyFormula(storm::api::createTask<ValueType>(property.getRawFormula(), true));
+ modelchecker.setInstantiationsAreGraphPreserving(samples.graphPreserving);
+
+ storm::utility::parametric::Valuation<ValueType> valuation;
+
+ std::vector<typename utility::parametric::VariableType<ValueType>::type> parameters;
+ std::vector<typename std::vector<typename utility::parametric::CoefficientType<ValueType>::type>::const_iterator> iterators;
+ std::vector<typename std::vector<typename utility::parametric::CoefficientType<ValueType>::type>::const_iterator> iteratorEnds;
+
+ storm::utility::Stopwatch watch(true);
+ for (auto const& product : samples.cartesianProducts) {
+ parameters.clear();
+ iterators.clear();
+ iteratorEnds.clear();
+
+ for (auto const& entry : product) {
+ parameters.push_back(entry.first);
+ iterators.push_back(entry.second.cbegin());
+ iteratorEnds.push_back(entry.second.cend());
+ }
+
+ bool done = false;
+ while (!done) {
+ // Read off valuation.
+ for (uint64_t i = 0; i < parameters.size(); ++i) {
+ valuation[parameters[i]] = *iterators[i];
+ }
+
+ storm::utility::Stopwatch valuationWatch(true);
+ std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker.check(Environment(), valuation);
+ valuationWatch.stop();
+
+ if (result) {
+ result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model.getInitialStates()));
+ }
+ printInitialStatesResult<ValueType>(result, property, &valuationWatch, &valuation);
+
+ for (uint64_t i = 0; i < parameters.size(); ++i) {
+ ++iterators[i];
+ if (iterators[i] == iteratorEnds[i]) {
+ // Reset iterator and proceed to move next iterator.
+ iterators[i] = product.at(parameters[i]).cbegin();
+
+ // If the last iterator was removed, we are done.
+ if (i == parameters.size() - 1) {
+ done = true;
+ }
+ } else {
+ // If an iterator was moved but not reset, we have another valuation to check.
+ break;
+ }
+ }
+
+ }
+ }
+
+ watch.stop();
+ STORM_PRINT_AND_LOG("Overall time for sampling all instances: " << watch << std::endl << std::endl);
+ }
+ }
+
template <typename ValueType>
- void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> const& samples) {
+ void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, SampleInformation<ValueType> const& samples) {
if (samples.empty()) {
verifyProperties<ValueType>(input.properties,
@@ -235,43 +341,15 @@ namespace storm {
}
});
} else {
- STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs.");
-
- // When samples are provided, we create an instantiation model checker.
- std::unique_ptr<storm::modelchecker::SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<ValueType>, double>> modelchecker(*model->template as<storm::models::sparse::Dtmc<ValueType>>());
-
- for (auto const& property : input.properties) {
- storm::cli::printModelCheckingProperty(property);
-
- modelchecker->specifyFormula(property.getRawFormula(storm::api::createTask<ValueType>(property.getRawFormula(), true)));
-
- // TODO: check.
- modelchecker->setInstantiationsAreGraphPreserving(true);
-
- storm::utility::parametric::Valuation<ValueType> valuation;
-
- // Enumerate all sample points.
- for () {
- bool first = true;
- std::stringstream ss;
- ss << "Treating instance [";
- for (auto const& entry : valuation) {
- if (!first) {
- ss << ", ";
- } else {
- first = false;
- }
- ss << entry.first << ": " << entry.second;
- }
- ss << "]...";
- STORM_PRINT_AND_LOG(ss.str());
-
- storm::utility::Stopwatch watch(true);
- std::unique_ptr<storm::modelchecker::CheckResult> result = modelchecker->check(Environment(), valuation);
- watch.stop();
-
- printInitialStatesResult<ValueType>(result, property, &watch);
- }
+ STORM_LOG_TRACE("Sampling the model at given points.");
+ if (model->isOfType(storm::models::ModelType::Dtmc)) {
+ verifyPropertiesAtSamplePoints<storm::modelchecker::SparseDtmcInstantiationModelChecker, storm::models::sparse::Dtmc<ValueType>, ValueType, double>(*model->template as<storm::models::sparse::Dtmc<ValueType>>(), input, samples);
+ } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
+ verifyPropertiesAtSamplePoints<storm::modelchecker::SparseCtmcInstantiationModelChecker, storm::models::sparse::Ctmc<ValueType>, ValueType, double>(*model->template as<storm::models::sparse::Ctmc<ValueType>>(), input, samples);
+ } else if (model->isOfType(storm::models::ModelType::Ctmc)) {
+ verifyPropertiesAtSamplePoints<storm::modelchecker::SparseMdpInstantiationModelChecker, storm::models::sparse::Mdp<ValueType>, ValueType, double>(*model->template as<storm::models::sparse::Mdp<ValueType>>(), input, samples);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Sampling is currently only supported for DTMCs, CTMCs and MDPs.");
}
}
}
@@ -331,7 +409,7 @@ namespace storm {
}
template <typename ValueType>
- void verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> const& samples) {
+ void verifyWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
if (regions.empty()) {
storm::pars::verifyPropertiesWithSparseEngine(model, input, samples);
} else {
@@ -340,7 +418,7 @@ namespace storm {
}
template <storm::dd::DdType DdType, typename ValueType>
- void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> const& samples) {
+ void verifyParametricModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, SampleInformation<ValueType> const& samples) {
STORM_LOG_ASSERT(model->isSparseModel(), "Unexpected model type.");
storm::pars::verifyWithSparseEngine<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), input, regions, samples);
}
@@ -376,7 +454,7 @@ namespace storm {
}
std::vector<storm::storage::ParameterRegion<ValueType>> regions = parseRegions<ValueType>(model);
- std::map<typename utility::parametric::VariableType<ValueType>::type, std::vector<typename utility::parametric::CoefficientType<ValueType>::type>> samples = parseSamples<ValueType>(model, parSettings.getSamples());
+ SampleInformation<ValueType> samples = parseSamples<ValueType>(model, parSettings.getSamples(), parSettings.isSamplesAreGraphPreservingSet());
if (model) {
storm::cli::exportModel<DdType, ValueType>(model, input);
diff --git a/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp
new file mode 100644
index 000000000..4af65eb19
--- /dev/null
+++ b/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp
@@ -0,0 +1,27 @@
+#include "storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h"
+
+#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
+
+#include "storm/exceptions/InvalidStateException.h"
+
+namespace storm {
+ namespace modelchecker {
+
+ template <typename SparseModelType, typename ConstantType>
+ SparseCtmcInstantiationModelChecker<SparseModelType, ConstantType>::SparseCtmcInstantiationModelChecker(SparseModelType const& parametricModel) : SparseInstantiationModelChecker<SparseModelType, ConstantType>(parametricModel), modelInstantiator(parametricModel) {
+ //Intentionally left empty
+ }
+
+ template <typename SparseModelType, typename ConstantType>
+ std::unique_ptr<CheckResult> SparseCtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+ STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
+ auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+ storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ConstantType>> modelChecker(instantiatedModel);
+
+ return modelChecker.check(env, *this->currentCheckTask);
+ }
+
+ template class SparseCtmcInstantiationModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>, double>;
+ template class SparseCtmcInstantiationModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::RationalNumber>;
+ }
+}
diff --git a/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h
new file mode 100644
index 000000000..4e4b7643f
--- /dev/null
+++ b/src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h
@@ -0,0 +1,28 @@
+#pragma once
+
+#include <memory>
+#include <boost/optional.hpp>
+
+#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"
+#include "storm-pars/utility/ModelInstantiator.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+
+namespace storm {
+ namespace modelchecker {
+
+ /*!
+ * Class to efficiently check a formula on a parametric model with different parameter instantiations.
+ */
+ template <typename SparseModelType, typename ConstantType>
+ class SparseCtmcInstantiationModelChecker : public SparseInstantiationModelChecker<SparseModelType, ConstantType> {
+ public:
+ SparseCtmcInstantiationModelChecker(SparseModelType const& parametricModel);
+
+ virtual std::unique_ptr<CheckResult> check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+
+ storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Ctmc<ConstantType>> modelInstantiator;
+ };
+ }
+}
diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
index d13f3bf44..5de3d8fd3 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
@@ -20,11 +20,11 @@ namespace storm {
std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
- STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
+ STORM_LOG_THROW(instantiatedModel.getTransitionMatrix().isProbabilistic(), storm::exceptions::InvalidArgumentException, "Instantiation point is invalid as the transition matrix becomes non-stochastic.");
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(instantiatedModel);
// Check if there are some optimizations implemented for the specified property
- if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
+ if (this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
return checkReachabilityProbabilityFormula(env, modelChecker);
} else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
return checkReachabilityRewardFormula(env, modelChecker);
@@ -144,4 +144,4 @@ namespace storm {
template class SparseDtmcInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
}
-}
\ No newline at end of file
+}
diff --git a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp
index d81d5b9a6..7d5143a50 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp
@@ -2,6 +2,7 @@
#include "storm/adapters/RationalFunctionAdapter.h"
#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
@@ -12,10 +13,9 @@ namespace storm {
template <typename SparseModelType, typename ConstantType>
SparseInstantiationModelChecker<SparseModelType, ConstantType>::SparseInstantiationModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel), instantiationsAreGraphPreserving(false) {
- //Intentionally left empty
+ // Intentionally left empty
}
-
template <typename SparseModelType, typename ConstantType>
void SparseInstantiationModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
currentFormula = checkTask.getFormula().asSharedPointer();
@@ -33,9 +33,11 @@ namespace storm {
}
template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
+ template class SparseInstantiationModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>, double>;
template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, double>;
template class SparseInstantiationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
+ template class SparseInstantiationModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>, storm::RationalNumber>;
template class SparseInstantiationModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>, storm::RationalNumber>;
}
diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
index a2a6c0094..3dc4866d3 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
@@ -23,7 +23,7 @@ namespace storm {
std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
- STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
+ STORM_LOG_THROW(instantiatedModel.getTransitionMatrix().isProbabilistic(), storm::exceptions::InvalidArgumentException, "Instantiation point is invalid as the transition matrix becomes non-stochastic.");
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(instantiatedModel);
// Check if there are some optimizations implemented for the specified property
diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp
index a02851dac..54b959e05 100644
--- a/src/storm-pars/settings/modules/ParametricSettings.cpp
+++ b/src/storm-pars/settings/modules/ParametricSettings.cpp
@@ -19,6 +19,7 @@ namespace storm {
const std::string ParametricSettings::transformContinuousShortOptionName = "tc";
const std::string ParametricSettings::onlyWellformednessConstraintsOptionName = "onlyconstraints";
const std::string ParametricSettings::samplesOptionName = "samples";
+ const std::string ParametricSettings::samplesGraphPreservingOptionName = "samples-graph-preserving";
ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
@@ -28,6 +29,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, onlyWellformednessConstraintsOptionName, false, "Sets whether you only want to obtain the wellformedness constraints").build());
this->addOption(storm::settings::OptionBuilder(moduleName, samplesOptionName, false, "The points at which to sample the model.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("samples", "The samples given in the form 'Var1=Val1:Val2:...:Valk,Var2=...").setDefaultValueString("").build()).build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, samplesGraphPreservingOptionName, false, "Sets whether it can be assumed that the samples are graph-preserving.").build());
}
bool ParametricSettings::exportResultToFile() const {
@@ -54,6 +56,10 @@ namespace storm {
return this->getOption(samplesOptionName).getArgumentByName("samples").getValueAsString();
}
+ bool ParametricSettings::isSamplesAreGraphPreservingSet() const {
+ return this->getOption(samplesGraphPreservingOptionName).getHasOptionBeenSet();
+ }
+
} // namespace modules
} // namespace settings
} // namespace storm
diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h
index 195b0936c..374c8e839 100644
--- a/src/storm-pars/settings/modules/ParametricSettings.h
+++ b/src/storm-pars/settings/modules/ParametricSettings.h
@@ -54,6 +54,11 @@ namespace storm {
*/
std::string getSamples() const;
+ /*!
+ * Retrieves whether the samples are graph preserving.
+ */
+ bool isSamplesAreGraphPreservingSet() const;
+
const static std::string moduleName;
private:
@@ -63,6 +68,7 @@ namespace storm {
const static std::string transformContinuousShortOptionName;
const static std::string onlyWellformednessConstraintsOptionName;
const static std::string samplesOptionName;
+ const static std::string samplesGraphPreservingOptionName;
};
} // namespace modules
diff --git a/src/storm/solver/StandardGameSolver.cpp b/src/storm/solver/StandardGameSolver.cpp
index 6140a5c15..9656af643 100644
--- a/src/storm/solver/StandardGameSolver.cpp
+++ b/src/storm/solver/StandardGameSolver.cpp
@@ -123,7 +123,9 @@ namespace storm {
} else {
// Update the solver.
getInducedMatrixVector(x, b, player1Choices, player2Choices, submatrix, subB);
- submatrix.convertToEquationSystem();
+ if (this->linearEquationSolverFactory->getEquationProblemFormat(environmentOfSolver) == LinearEquationSolverProblemFormat::EquationSystem) {
+ submatrix.convertToEquationSystem();
+ }
submatrixSolver->setMatrix(std::move(submatrix));
}
diff --git a/src/storm/solver/TopologicalLinearEquationSolver.cpp b/src/storm/solver/TopologicalLinearEquationSolver.cpp
index 0e6896370..877ba76dd 100644
--- a/src/storm/solver/TopologicalLinearEquationSolver.cpp
+++ b/src/storm/solver/TopologicalLinearEquationSolver.cpp
@@ -169,8 +169,8 @@ namespace storm {
if (asEquationSystem) {
sccA.convertToEquationSystem();
}
- //std::cout << "Solving SCC " << scc << std::endl;
- //std::cout << "Matrix is " << sccA << std::endl;
+// std::cout << "Solving SCC " << scc << std::endl;
+// std::cout << "Matrix is " << sccA << std::endl;
this->sccSolver->setMatrix(std::move(sccA));
// x Vector