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

replaced stdpair by struct for model,program pairs 

Former-commit-id: 11177caa6f
tempestpy_adaptions
sjunges 9 years ago
parent
194db381b4
commit
e45ce6f293
3 changed files with 30 additions and 17 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. 22
      src/cli/entrypoints.h
  2. 12
      src/storage/ModelProgramPair.h
  3. 13
      src/utility/storm.h

22
src/cli/entrypoints.h
View File

@ -108,14 +108,14 @@ namespace storm {
template<typename ValueType, storm::dd::DdType LibraryType>
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelProgramPair.first != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelProgramPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed.
BRANCH_ON_MODELTYPE(modelProgramPair.first, modelProgramPair.first, ValueType, LibraryType, preprocessModel, formulas);
BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
// Print some information about the model.
modelProgramPair.first->printModelInformationToStream(std::cout);
modelProgramPair.model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (!formulas.empty()) {
@ -124,7 +124,7 @@ namespace storm {
// Start by building a mapping from constants of the (translated) model to their defining expressions.
std::map<storm::expressions::Variable, storm::expressions::Expression> constantSubstitution;
for (auto const& constant : modelProgramPair.second.getConstants()) {
for (auto const& constant : modelProgramPair.program.getConstants()) {
if (constant.isDefined()) {
constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
}
@ -135,20 +135,20 @@ namespace storm {
preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
}
if (modelProgramPair.first->isSparseModel()) {
if (modelProgramPair.model->isSparseModel()) {
if(storm::settings::generalSettings().isCounterexampleSet()) {
// If we were requested to generate a counterexample, we now do so for each formula.
for(auto const& formula : preparedFormulas) {
generateCounterexample<ValueType>(program, modelProgramPair.first->as<storm::models::sparse::Model<ValueType>>(), formula);
generateCounterexample<ValueType>(program, modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(modelProgramPair.first->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
}
} else if (modelProgramPair.first->isSymbolicModel()) {
} else if (modelProgramPair.model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(modelProgramPair.first->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
} else {
verifySymbolicModelWithSymbolicEngine(modelProgramPair.first->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");

12
src/storage/ModelProgramPair.h
View File

@ -0,0 +1,12 @@
#include "../models/ModelBase.h"
#include "prism/Program.h"
namespace storm {
namespace storage {
struct ModelProgramPair {
std::shared_ptr<storm::models::ModelBase> model;
storm::prism::Program program;
};
}
}

13
src/utility/storm.h
View File

@ -46,6 +46,7 @@
// Headers for model processing.
#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
#include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
#include "src/storage/ModelProgramPair.h"
// Headers for model checking.
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@ -83,8 +84,8 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
std::pair<std::shared_ptr<storm::models::ModelBase>, storm::prism::Program> result;
storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelProgramPair result;
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
@ -103,16 +104,16 @@ namespace storm {
}
storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
result.first = builder.translateProgram(program, options);
result.second = builder.getTranslatedProgram();
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
} else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Dd || settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
options.addConstantDefinitionsFromString(program, constants);
storm::builder::DdPrismModelBuilder<LibraryType> builder;
result.first = builder.translateProgram(program, options);
result.second = builder.getTranslatedProgram();
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
}
return result;

Write Preview
Loading…
Cancel
Save