Browse Source

modified the entry point code to deal with the new generator-builder-structure

Former-commit-id: f01a19e346
tempestpy_adaptions
dehnert 9 years ago
parent
commit
9f6bd1805f
  1. 2
      src/builder/ExplicitModelBuilder.cpp
  2. 13
      src/generator/PrismNextStateGenerator.cpp
  3. 18
      src/utility/storm.h

2
src/builder/ExplicitModelBuilder.cpp

@ -32,7 +32,7 @@ namespace storm {
template <typename ValueType> template <typename ValueType>
class RewardModelBuilder { class RewardModelBuilder {
public: public:
RewardModelBuilder(storm::generator::RewardModelInformation const& rewardModelInformation) : rewardModelName(rewardModelInformation.getName()), stateRewards(rewardModelInformation.hasStateRewards()), stateRewardVector(), stateActionRewards(rewardModelInformation.hasStateActionRewards()), stateActionRewardVector() {
RewardModelBuilder(storm::generator::RewardModelInformation const& rewardModelInformation) : rewardModelName(rewardModelInformation.getName()), stateRewards(rewardModelInformation.hasStateRewards()), stateActionRewards(rewardModelInformation.hasStateActionRewards()), stateRewardVector(), stateActionRewardVector() {
STORM_LOG_THROW(!rewardModelInformation.hasTransitionRewards(), storm::exceptions::InvalidArgumentException, "Unable to treat transition rewards."); STORM_LOG_THROW(!rewardModelInformation.hasTransitionRewards(), storm::exceptions::InvalidArgumentException, "Unable to treat transition rewards.");
} }

13
src/generator/PrismNextStateGenerator.cpp

@ -8,6 +8,7 @@
#include "src/utility/constants.h" #include "src/utility/constants.h"
#include "src/utility/macros.h" #include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
namespace storm { namespace storm {
@ -19,7 +20,19 @@ namespace storm {
// Extract the reward models from the program based on the names we were given. // Extract the reward models from the program based on the names we were given.
for (auto const& rewardModelName : this->options.getRewardModelNames()) { for (auto const& rewardModelName : this->options.getRewardModelNames()) {
if (program.hasRewardModel(rewardModelName)) {
rewardModels.push_back(program.getRewardModel(rewardModelName)); rewardModels.push_back(program.getRewardModel(rewardModelName));
} else {
STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
STORM_LOG_THROW(program.getNumberOfRewardModels() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
STORM_LOG_THROW(program.getNumberOfRewardModels() > 0, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is invalid, because there is no reward model.");
}
}
// If no reward model was yet added, but there was one that was given in the options, we try to build
// standard reward model.
if (rewardModels.empty() && !this->options.getRewardModelNames().empty()) {
rewardModels.push_back(program.getRewardModel(0));
} }
// If there are terminal states we need to handle, we now need to translate all labels to expressions. // If there are terminal states we need to handle, we now need to translate all labels to expressions.

18
src/utility/storm.h

@ -72,7 +72,8 @@
#include "src/counterexamples/MILPMinimalLabelSetGenerator.h" #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
#include "src/counterexamples/SMTMinimalCommandSetGenerator.h" #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
// Headers related to program preprocessing.
// Headers related to PRISM model building.
#include "src/generator/PrismNextStateGenerator.h"
#include "src/utility/prism.h" #include "src/utility/prism.h"
// Headers related to exception handling. // Headers related to exception handling.
@ -99,25 +100,23 @@ namespace storm {
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD> template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
storm::storage::ModelFormulasPair result; storm::storage::ModelFormulasPair result;
storm::prism::Program translatedProgram;
// Get the string that assigns values to the unknown currently undefined constants in the model. // Get the string that assigns values to the unknown currently undefined constants in the model.
std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString(); std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
translatedProgram = storm::utility::prism::preprocess<ValueType>(program, constantDefinitionString);
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = translatedProgram.getConstantsSubstitution();
storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess<ValueType>(program, constantDefinitionString);
std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preprocessedProgram.getConstantsSubstitution();
// Customize and perform model-building. // Customize and perform model-building.
if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) { if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) {
typename storm::builder::ExplicitModelBuilder<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>::Options options;
options = typename storm::builder::ExplicitModelBuilder<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>::Options(formulas);
options.addConstantDefinitionsFromString(program, constants);
storm::generator::NextStateGeneratorOptions options(formulas);
// Generate command labels if we are going to build a counterexample later. // Generate command labels if we are going to build a counterexample later.
if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) { if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
options.buildCommandLabels = true;
options.setBuildChoiceLabels(true);
} }
storm::builder::ExplicitModelBuilder<ValueType> builder(program, options);
std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(preprocessedProgram, options);
storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
result.model = builder.translate(); result.model = builder.translate();
} else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { } else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options; typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
@ -126,7 +125,6 @@ namespace storm {
storm::builder::DdPrismModelBuilder<LibraryType> builder; storm::builder::DdPrismModelBuilder<LibraryType> builder;
result.model = builder.translateProgram(program, options); result.model = builder.translateProgram(program, options);
translatedProgram = builder.getTranslatedProgram();
} }
// There may be constants of the model appearing in the formulas, so we replace all their occurrences // There may be constants of the model appearing in the formulas, so we replace all their occurrences

Loading…
Cancel
Save