From e4725aa4a18b26077e00a7abed822d5a73657e47 Mon Sep 17 00:00:00 2001 From: sjunges Date: Sat, 16 Jan 2016 14:16:03 +0100 Subject: [PATCH] Instead of returning the program, return the prepared formulas Former-commit-id: a06fbaad2b434f4772ba4aad5be690ced412a7ac --- src/cli/entrypoints.h | 39 ++++++++++----------------------- src/storage/ModelFormulasPair.h | 16 ++++++++++++++ src/storage/ModelProgramPair.h | 12 ---------- src/utility/storm.h | 27 ++++++++++++++++++----- 4 files changed, 50 insertions(+), 44 deletions(-) create mode 100644 src/storage/ModelFormulasPair.h delete mode 100644 src/storage/ModelProgramPair.h diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 93f9e1777..b93e4e9ae 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -108,47 +108,32 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - storm::storage::ModelProgramPair modelProgramPair = buildSymbolicModel(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(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 constantSubstitution; - for (auto const& constant : modelProgramPair.program.getConstants()) { - if (constant.isDefined()) { - constantSubstitution.emplace(constant.getExpressionVariable(), constant.getExpression()); - } - } - - std::vector> 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(program, modelProgramPair.model->as>(), formula); + for(auto const& formula : modelFormulasPair.formulas) { + generateCounterexample(program, modelFormulasPair.model->as>(), formula); } } else { - verifySparseModel(modelProgramPair.model->as>(), preparedFormulas); + verifySparseModel(modelFormulasPair.model->as>(), 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>(), preparedFormulas); + verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as>(), modelFormulasPair.formulas); } else { - verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); + verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as>(), modelFormulasPair.formulas); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); diff --git a/src/storage/ModelFormulasPair.h b/src/storage/ModelFormulasPair.h new file mode 100644 index 000000000..57181a566 --- /dev/null +++ b/src/storage/ModelFormulasPair.h @@ -0,0 +1,16 @@ +#pragma once +#include "../models/ModelBase.h" + + +namespace storm { + namespace logic { + class Formula; + } + + namespace storage { + struct ModelFormulasPair { + std::shared_ptr model; + std::vector> formulas; + }; + } +} \ No newline at end of file diff --git a/src/storage/ModelProgramPair.h b/src/storage/ModelProgramPair.h deleted file mode 100644 index c50b6d306..000000000 --- a/src/storage/ModelProgramPair.h +++ /dev/null @@ -1,12 +0,0 @@ -#include "../models/ModelBase.h" -#include "prism/Program.h" - - -namespace storm { - namespace storage { - struct ModelProgramPair { - std::shared_ptr model; - storm::prism::Program program; - }; - } -} \ No newline at end of file diff --git a/src/utility/storm.h b/src/utility/storm.h index af70bb89c..0739b2612 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -8,6 +8,7 @@ #include #include #include +#include #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> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); + + template - storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - storm::storage::ModelProgramPair result; + storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector> 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 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::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); @@ -113,9 +117,22 @@ namespace storm { storm::builder::DdPrismModelBuilder 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 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; }