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

Instead of returning the program, return the prepared formulas 

Former-commit-id: a06fbaad2b
tempestpy_adaptions
sjunges 9 years ago
parent
2d44d4f822
commit
e4725aa4a1
4 changed files with 50 additions and 44 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. 39
      src/cli/entrypoints.h
  2. 16
      src/storage/ModelFormulasPair.h
  3. 12
      src/storage/ModelProgramPair.h
  4. 27
      src/utility/storm.h

39
src/cli/entrypoints.h
View File

@ -108,47 +108,32 @@ 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) {
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.");
storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException, "Model could not be constructed for an unknown reason.");
// Preprocess the model if needed.
BRANCH_ON_MODELTYPE(modelProgramPair.model, modelProgramPair.model, ValueType, LibraryType, preprocessModel, formulas);
BRANCH_ON_MODELTYPE(modelFormulasPair.model, modelFormulasPair.model, ValueType, LibraryType, preprocessModel, formulas);
// Print some information about the model.
modelProgramPair.model->printModelInformationToStream(std::cout);
modelFormulasPair.model->printModelInformationToStream(std::cout);
// Verify the model, if a formula was given.
if (!formulas.empty()) {
// There may be constants of the model appearing in the formulas, so we replace all their occurrences
// by their definitions in the translated program.
// 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.program.getConstants()) {
if (constant.isDefined()) {
constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
}
}
std::vector<std::shared_ptr<storm::logic::Formula>> preparedFormulas;
for (auto const& formula : formulas) {
preparedFormulas.emplace_back(formula->substitute(constantSubstitution));
}
if (modelProgramPair.model->isSparseModel()) {
if (modelFormulasPair.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.model->as<storm::models::sparse::Model<ValueType>>(), formula);
for(auto const& formula : modelFormulasPair.formulas) {
generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
}
} else {
verifySparseModel<ValueType>(modelProgramPair.model->as<storm::models::sparse::Model<ValueType>>(), preparedFormulas);
verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas);
}
} else if (modelProgramPair.model->isSymbolicModel()) {
} else if (modelFormulasPair.model->isSymbolicModel()) {
if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
verifySymbolicModelWithHybridEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(), modelFormulasPair.formulas);
} else {
verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as<storm::models::symbolic::Model<LibraryType>>(), preparedFormulas);
verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(), modelFormulasPair.formulas);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");

16
src/storage/ModelFormulasPair.h
View File

@ -0,0 +1,16 @@
#pragma once
#include "../models/ModelBase.h"
namespace storm {
namespace logic {
class Formula;
}
namespace storage {
struct ModelFormulasPair {
std::shared_ptr<storm::models::ModelBase> model;
std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
};
}
}

12
src/storage/ModelProgramPair.h
View File

@ -1,12 +0,0 @@
#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;
};
}
}

27
src/utility/storm.h
View File

@ -8,6 +8,7 @@
#include <cstdio>
#include <sstream>
#include <memory>
#include <src/storage/ModelFormulasPair.h>
#include "initialize.h"
@ -46,7 +47,7 @@
// Headers for model processing.
#include "src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h"
#include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h"
#include "src/storage/ModelProgramPair.h"
#include "src/storage/ModelFormulasPair.h"
// Headers for model checking.
#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
@ -82,10 +83,13 @@ namespace storm {
storm::prism::Program parseProgram(std::string const& path);
std::vector<std::shared_ptr<storm::logic::Formula>> parseFormulasForExplicit(std::string const& inputString);
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>
storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelProgramPair result;
storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) {
storm::storage::ModelFormulasPair result;
storm::prism::Program translatedProgram;
storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings();
@ -105,7 +109,7 @@ namespace storm {
storm::builder::ExplicitPrismModelBuilder<ValueType> builder;
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
translatedProgram = 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);
@ -113,9 +117,22 @@ namespace storm {
storm::builder::DdPrismModelBuilder<LibraryType> builder;
result.model = builder.translateProgram(program, options);
result.program = builder.getTranslatedProgram();
translatedProgram = builder.getTranslatedProgram();
}
// There may be constants of the model appearing in the formulas, so we replace all their occurrences
// by their definitions in the translated program.
// 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 : translatedProgram.getConstants()) {
if (constant.isDefined()) {
constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression());
}
}
for (auto const& formula : formulas) {
result.formulas.emplace_back(formula->substitute(constantSubstitution));
}
return result;
}

Write Preview
Loading…
Cancel
Save