diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index 1c24bc091..93f9e1777 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -108,14 +108,14 @@ namespace storm { template void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::pair, storm::prism::Program> modelProgramPair = buildSymbolicModel(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(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 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(program, modelProgramPair.first->as>(), formula); + generateCounterexample(program, modelProgramPair.model->as>(), formula); } } else { - verifySparseModel(modelProgramPair.first->as>(), preparedFormulas); + verifySparseModel(modelProgramPair.model->as>(), 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>(), preparedFormulas); + verifySymbolicModelWithHybridEngine(modelProgramPair.model->as>(), preparedFormulas); } else { - verifySymbolicModelWithSymbolicEngine(modelProgramPair.first->as>(), preparedFormulas); + verifySymbolicModelWithSymbolicEngine(modelProgramPair.model->as>(), preparedFormulas); } } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type."); diff --git a/src/storage/ModelProgramPair.h b/src/storage/ModelProgramPair.h new file mode 100644 index 000000000..c50b6d306 --- /dev/null +++ b/src/storage/ModelProgramPair.h @@ -0,0 +1,12 @@ +#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 d607f01ad..af70bb89c 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -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> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); template - std::pair, storm::prism::Program> buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { - std::pair, storm::prism::Program> result; + storm::storage::ModelProgramPair buildSymbolicModel(storm::prism::Program const& program, std::vector> const& formulas) { + storm::storage::ModelProgramPair result; storm::settings::modules::GeneralSettings settings = storm::settings::generalSettings(); @@ -103,16 +104,16 @@ namespace storm { } storm::builder::ExplicitPrismModelBuilder 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::Options options; options = typename storm::builder::DdPrismModelBuilder::Options(formulas); options.addConstantDefinitionsFromString(program, constants); storm::builder::DdPrismModelBuilder builder; - result.first = builder.translateProgram(program, options); - result.second = builder.getTranslatedProgram(); + result.model = builder.translateProgram(program, options); + result.program = builder.getTranslatedProgram(); } return result;