sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

making game solver respect equation solver format

main
dehnert 7 years ago
parent
10da10a7d1
commit
a08cb4ac18
10 changed files with 245 additions and 96 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 252
      src/storm-pars-cli/storm-pars.cpp
  2. 27
      src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp
  3. 28
      src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h
  4. 6
      src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
  5. 6
      src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp
  6. 2
      src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
  7. 6
      src/storm-pars/settings/modules/ParametricSettings.cpp
  8. 6
      src/storm-pars/settings/modules/ParametricSettings.h
  9. 4
      src/storm/solver/StandardGameSolver.cpp
  10. 4
      src/storm/solver/TopologicalLinearEquationSolver.cpp

252
src/storm-pars-cli/storm-pars.cpp
View File

@ -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);

27
src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.cpp
View File

@ -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>;
}
}

28
src/storm-pars/modelchecker/instantiation/SparseCtmcInstantiationModelChecker.h
View File

@ -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;
};
}
}

6
src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
View File

@ -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>;
}
}
}

6
src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.cpp
View File

@ -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>;
}

2
src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
View File

@ -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

6
src/storm-pars/settings/modules/ParametricSettings.cpp
View File

@ -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

6
src/storm-pars/settings/modules/ParametricSettings.h
View File

@ -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

4
src/storm/solver/StandardGameSolver.cpp
View File

@ -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));
}

4
src/storm/solver/TopologicalLinearEquationSolver.cpp
View File

@ -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

Write Preview
Loading…
Cancel
Save