From 6655ee41d81e0a5d1c674e548011e17cb9e4fcc2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 8 Jun 2016 16:57:26 +0200 Subject: [PATCH] started to restructure explicit model builder to make it fit for JANI models Former-commit-id: 69603dd97b070f4f21bb68a20d3969a005db93a6 --- ...elBuilder.cpp => ExplicitModelBuilder.cpp} | 165 +++-------- src/builder/ExplicitModelBuilder.h | 178 ++++++++++++ src/builder/ExplicitPrismModelBuilder.h | 268 ------------------ src/generator/NextStateGenerator.cpp | 174 ++++++++++++ src/generator/NextStateGenerator.h | 111 ++++++++ src/generator/PrismNextStateGenerator.cpp | 74 +++-- src/generator/PrismNextStateGenerator.h | 21 +- src/generator/PrismStateLabelingGenerator.cpp | 50 ---- src/generator/PrismStateLabelingGenerator.h | 31 -- src/generator/StateLabelingGenerator.h | 20 -- src/storage/prism/Program.cpp | 4 +- src/utility/storm.h | 8 +- .../builder/ExplicitPrismModelBuilderTest.cpp | 44 +-- .../GmmxxCtmcCslModelCheckerTest.cpp | 22 +- .../GmmxxDtmcPrctlModelCheckerTest.cpp | 4 +- .../GmmxxMdpPrctlModelCheckerTest.cpp | 6 +- .../NativeCtmcCslModelCheckerTest.cpp | 22 +- .../MilpPermissiveSchedulerTest.cpp | 8 +- .../SmtPermissiveSchedulerTest.cpp | 8 +- ...sticModelBisimulationDecompositionTest.cpp | 4 +- test/functional/utility/GraphTest.cpp | 10 +- .../utility/ModelInstantiatorTest.cpp | 12 +- 22 files changed, 628 insertions(+), 616 deletions(-) rename src/builder/{ExplicitPrismModelBuilder.cpp => ExplicitModelBuilder.cpp} (64%) create mode 100644 src/builder/ExplicitModelBuilder.h delete mode 100644 src/builder/ExplicitPrismModelBuilder.h create mode 100644 src/generator/NextStateGenerator.cpp delete mode 100644 src/generator/PrismStateLabelingGenerator.cpp delete mode 100644 src/generator/PrismStateLabelingGenerator.h delete mode 100644 src/generator/StateLabelingGenerator.h diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp similarity index 64% rename from src/builder/ExplicitPrismModelBuilder.cpp rename to src/builder/ExplicitModelBuilder.cpp index b94cb9f47..c6917ff54 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitModelBuilder.cpp @@ -1,4 +1,4 @@ -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include @@ -13,7 +13,6 @@ #include "src/settings/modules/IOSettings.h" #include "src/generator/PrismNextStateGenerator.h" -#include "src/generator/PrismStateLabelingGenerator.h" #include "src/utility/prism.h" #include "src/utility/constants.h" @@ -33,19 +32,19 @@ namespace storm { template struct RewardModelBuilder { public: - RewardModelBuilder(bool deterministicModel, bool hasStateRewards, bool hasStateActionRewards, bool hasTransitionRewards) : hasStateRewards(hasStateRewards), hasStateActionRewards(hasStateActionRewards), hasTransitionRewards(hasTransitionRewards), stateRewardVector(), stateActionRewardVector() { + RewardModelBuilder(std::string const& rewardModelName) : rewardModelName(rewardModelName), stateRewardVector(), stateActionRewardVector() { // Intentionally left empty. } storm::models::sparse::StandardRewardModel build(uint_fast64_t rowCount, uint_fast64_t columnCount, uint_fast64_t rowGroupCount) { boost::optional> optionalStateRewardVector; - if (hasStateRewards) { + if (!stateRewardVector.empty()) { stateRewardVector.resize(rowGroupCount); optionalStateRewardVector = std::move(stateRewardVector); } boost::optional> optionalStateActionRewardVector; - if (hasStateActionRewards) { + if (!stateActionRewardVector.empty()) { stateActionRewardVector.resize(rowCount); optionalStateActionRewardVector = std::move(stateActionRewardVector); } @@ -53,9 +52,7 @@ namespace storm { return storm::models::sparse::StandardRewardModel(std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector)); } - bool hasStateRewards; - bool hasStateActionRewards; - bool hasTransitionRewards; + std::string rewardModelName; // The state reward vector. std::vector stateRewardVector; @@ -65,147 +62,49 @@ namespace storm { }; template - ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { + ExplicitModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildStateValuations(false) { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { - this->preserveFormula(formula); - } - - template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { - if (formulas.empty()) { - this->buildAllRewardModels = true; - this->buildAllLabels = true; - } else { - for (auto const& formula : formulas) { - this->preserveFormula(*formula); - } - if (formulas.size() == 1) { - this->setTerminalStatesFromFormula(*formulas.front()); - } - } - } - - template - void ExplicitPrismModelBuilder::Options::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { - if (formula.isAtomicExpressionFormula()) { - terminalStates = formula.asAtomicExpressionFormula().getExpression(); - } else if (formula.isAtomicLabelFormula()) { - terminalStates = formula.asAtomicLabelFormula().getLabel(); - } else if (formula.isEventuallyFormula()) { - storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); - if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } else if (formula.isUntilFormula()) { - storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); - if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { - this->setTerminalStatesFromFormula(right); - } - storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); - if (left.isAtomicExpressionFormula()) { - negatedTerminalStates = left.asAtomicExpressionFormula().getExpression(); - } else if (left.isAtomicLabelFormula()) { - negatedTerminalStates = left.asAtomicLabelFormula().getLabel(); - } - } else if (formula.isProbabilityOperatorFormula()) { - storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); - if (sub.isEventuallyFormula() || sub.isUntilFormula()) { - this->setTerminalStatesFromFormula(sub); - } - } - } - - template - void ExplicitPrismModelBuilder::Options::preserveFormula(storm::logic::Formula const& formula) { - // If we already had terminal states, we need to erase them. - if (terminalStates) { - terminalStates.reset(); - } - if (negatedTerminalStates) { - negatedTerminalStates.reset(); - } - - // If we are not required to build all reward models, we determine the reward models we need to build. - if (!buildAllRewardModels) { - std::set referencedRewardModels = formula.getReferencedRewardModels(); - rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end()); - } - - // Extract all the labels used in the formula. - if (!buildAllLabels) { - if (!labelsToBuild) { - labelsToBuild = std::set(); - } - - std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); - for (auto const& formula : atomicLabelFormulas) { - labelsToBuild.get().insert(formula.get()->getLabel()); - } - } - - // Extract all the expressions used in the formula. - std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); - for (auto const& formula : atomicExpressionFormulas) { - if (!expressionLabels) { - expressionLabels = std::vector(); - } - expressionLabels.get().push_back(formula.get()->getExpression()); - } - } - - template - void ExplicitPrismModelBuilder::Options::addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString) { - constantDefinitions = storm::utility::prism::parseConstantDefinitionString(program, constantDefinitionString); - } - - template - ExplicitPrismModelBuilder::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options), variableInformation(this->program), stateStorage(variableInformation.getTotalBitOffset(true)) { + ExplicitModelBuilder::ExplicitModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options), variableInformation(this->program), stateStorage(variableInformation.getTotalBitOffset(true)) { // Intentionally left empty. } template - storm::storage::sparse::StateValuations const& ExplicitPrismModelBuilder::getStateValuations() const { + storm::storage::sparse::StateValuations const& ExplicitModelBuilder::getStateValuations() const { STORM_LOG_THROW(static_cast(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build."); return stateValuations.get(); } template - storm::prism::Program const& ExplicitPrismModelBuilder::getTranslatedProgram() const { - return program; - } - - template - std::shared_ptr> ExplicitPrismModelBuilder::translate() { + std::shared_ptr> ExplicitModelBuilder::translate() { STORM_LOG_DEBUG("Building representation of program:" << std::endl << program << std::endl); STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder); - // Select the appropriate reward models (after the constants have been substituted). - std::vector> selectedRewardModels; - // First, we make sure that all selected reward models actually exist. for (auto const& rewardModelName : options.rewardModelsToBuild) { STORM_LOG_THROW(rewardModelName.empty() || program.hasRewardModel(rewardModelName), storm::exceptions::InvalidArgumentException, "Model does not possess a reward model with the name '" << rewardModelName << "'."); } - for (auto const& rewardModel : program.getRewardModels()) { - if (options.buildAllRewardModels || options.rewardModelsToBuild.find(rewardModel.getName()) != options.rewardModelsToBuild.end()) { - selectedRewardModels.push_back(rewardModel); - } - } - // If no reward model was selected until now and a referenced reward model appears to be unique, we build - // the only existing reward model (given that no explicit name was given for the referenced reward model). - if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { - selectedRewardModels.push_back(program.getRewardModel(0)); + std::vector selectedRewardModels; + if (options.buildAllRewardModels) { +// for (auto const& rewardModel : program.getRewardModels()) { +// selectedRewardModels.push_back(rewardModel); +// } + } else { + selectedRewardModels = std::vector(options.rewardModelsToBuild.begin(), options.rewardModelsToBuild.end()); } +// // If no reward model was selected until now and a referenced reward model appears to be unique, we build +// // the only existing reward model (given that no explicit name was given for the referenced reward model). +// if (selectedRewardModels.empty() && program.getNumberOfRewardModels() == 1 && options.rewardModelsToBuild.size() == 1 && *options.rewardModelsToBuild.begin() == "") { +// selectedRewardModels.push_back(program.getRewardModel(0)); +// } ModelComponents modelComponents = buildModelComponents(selectedRewardModels); @@ -229,7 +128,7 @@ namespace storm { } template - StateType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state) { + StateType ExplicitModelBuilder::getOrAddStateIndex(CompressedState const& state) { StateType newIndex = static_cast(stateStorage.getNumberOfStates()); // Check, if the state was already registered. @@ -252,7 +151,7 @@ namespace storm { } template - boost::optional>> ExplicitPrismModelBuilder::buildMatrices(std::vector> const& selectedRewardModels, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { + boost::optional>> ExplicitModelBuilder::buildMatrices(std::vector> const& selectedRewardModels, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression) { // Create choice labels, if requested, boost::optional>> choiceLabels; if (options.buildCommandLabels) { @@ -269,7 +168,7 @@ namespace storm { } // Create a callback for the next-state generator to enable it to request the index of states. - std::function stateToIdCallback = std::bind(&ExplicitPrismModelBuilder::getOrAddStateIndex, this, std::placeholders::_1); + std::function stateToIdCallback = std::bind(&ExplicitModelBuilder::getOrAddStateIndex, this, std::placeholders::_1); // If the exploration order is something different from breadth-first, we need to keep track of the remapping // from state ids to row groups. For this, we actually store the reversed mapping of row groups to state-ids @@ -408,7 +307,7 @@ namespace storm { } template - typename ExplicitPrismModelBuilder::ModelComponents ExplicitPrismModelBuilder::buildModelComponents(std::vector> const& selectedRewardModels) { + typename ExplicitModelBuilder::ModelComponents ExplicitModelBuilder::buildModelComponents(std::vector const& selectedRewardModels) { ModelComponents modelComponents; // Determine whether we have to combine different choices to one or whether this model can have more than @@ -418,8 +317,8 @@ namespace storm { // Prepare the transition matrix builder and the reward model builders. storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); std::vector> rewardModelBuilders; - for (auto const& rewardModel : selectedRewardModels) { - rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards()); + for (auto const& rewardModelName : selectedRewardModels) { + rewardModelBuilders.emplace_back(rewardModelName); } // If we were asked to treat some states as terminal states, we determine an expression characterizing the @@ -477,17 +376,17 @@ namespace storm { } template - storm::models::sparse::StateLabeling ExplicitPrismModelBuilder::buildStateLabeling() { + storm::models::sparse::StateLabeling ExplicitModelBuilder::buildStateLabeling() { storm::generator::PrismStateLabelingGenerator generator(program, variableInformation); return generator.generate(stateStorage.stateToId, stateStorage.initialStateIndices); } // Explicitly instantiate the class. - template class ExplicitPrismModelBuilder, uint32_t>; + template class ExplicitModelBuilder, uint32_t>; #ifdef STORM_HAVE_CARL - template class ExplicitPrismModelBuilder, uint32_t>; - template class ExplicitPrismModelBuilder, uint32_t>; + template class ExplicitModelBuilder, uint32_t>; + template class ExplicitModelBuilder, uint32_t>; #endif } } diff --git a/src/builder/ExplicitModelBuilder.h b/src/builder/ExplicitModelBuilder.h new file mode 100644 index 000000000..3d21299da --- /dev/null +++ b/src/builder/ExplicitModelBuilder.h @@ -0,0 +1,178 @@ +#ifndef STORM_BUILDER_ExplicitModelBuilder_H +#define STORM_BUILDER_ExplicitModelBuilder_H + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "src/storage/prism/Program.h" +#include "src/storage/expressions/SimpleValuation.h" +#include "src/storage/expressions/ExpressionEvaluator.h" +#include "src/storage/BitVectorHashMap.h" +#include "src/logic/Formulas.h" +#include "src/models/sparse/StateAnnotation.h" +#include "src/models/sparse/Model.h" +#include "src/models/sparse/StateLabeling.h" +#include "src/storage/SparseMatrix.h" +#include "src/storage/sparse/StateValuations.h" +#include "src/storage/sparse/StateStorage.h" +#include "src/settings/SettingsManager.h" + +#include "src/utility/prism.h" + +#include "src/builder/ExplorationOrder.h" + +#include "src/generator/CompressedState.h" +#include "src/generator/VariableInformation.h" + +namespace storm { + namespace utility { + template class ConstantsComparator; + } + + namespace generator { + template + class NextStateGenerator; + } + + namespace builder { + + using namespace storm::utility::prism; + using namespace storm::generator; + + // Forward-declare classes. + template struct RewardModelBuilder; + + template, typename StateType = uint32_t> + class ExplicitModelBuilder { + public: + // A structure holding the individual components of a model. + struct ModelComponents { + ModelComponents(); + + // The transition matrix. + storm::storage::SparseMatrix transitionMatrix; + + // The state labeling. + storm::models::sparse::StateLabeling stateLabeling; + + // The reward models associated with the model. + std::unordered_map> rewardModels; + + // A vector that stores a labeling for each choice. + boost::optional>> choiceLabeling; + }; + + struct Options { + /*! + * Creates an object representing the default building options. + */ + Options(); + + // The order in which to explore the model. + ExplorationOrder explorationOrder; + + // A flag that indicates whether or not to store the state information after successfully building the + // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful + // call to translateProgram. + bool buildStateValuations; + }; + + /*! + * Creates an explicit model builder that uses the provided generator.. + * + * @param generator The generator to build. + */ + ExplicitModelBuilder(std::shared_ptr> const& generator, Options const& options = Options()); + + /*! + * Convert the program given at construction time to an abstract model. The type of the model is the one + * specified in the program. The given reward model name selects the rewards that the model will contain. + * + * @param program The program to translate. + * @param constantDefinitionString A string that contains a comma-separated definition of all undefined + * constants in the model. + * @param rewardModel The reward model that is to be built. + * @return The explicit model that was given by the probabilistic program. + */ + std::shared_ptr> translate(); + + /*! + * If requested in the options, information about the variable valuations in the reachable states can be + * retrieved via this function. + * + * @return A structure that stores information about all reachable states. + */ + storm::storage::sparse::StateValuations const& getStateValuations() const; + + private: + /*! + * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to + * the lists of all states with a new id. If the state was already known, the object that is pointed to by + * the given state pointer is deleted and the old state id is returned. Note that the pointer should not be + * used after invoking this method. + * + * @param state A pointer to a state for which to retrieve the index. This must not be used after the call. + * @return A pair indicating whether the state was already discovered before and the state id of the state. + */ + StateType getOrAddStateIndex(CompressedState const& state); + + /*! + * Builds the transition matrix and the transition reward matrix based for the given program. + * + * @param transitionMatrixBuilder The builder of the transition matrix. + * @param rewardModelBuilders The builders for the selected reward models. + * @param terminalExpression If given, states satisfying this expression are not explored further. + * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin + * and a vector containing the labels associated with each choice. + */ + boost::optional>> buildMatrices(storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); + + /*! + * Explores the state space of the given program and returns the components of the model as a result. + * + * @param selectedRewardModels The reward models that are to be considered. + * @return A structure containing the components of the resulting model. + */ + ModelComponents buildModelComponents(std::vector const& selectedRewardModels); + + /*! + * Builds the state labeling for the given program. + * + * @return The state labeling of the given program. + */ + storm::models::sparse::StateLabeling buildStateLabeling(); + + /// The generator to use for the building process. + std::shared_ptr> generator; + + /// The options to be used for the building process. + Options options; + + /// Internal information about the states that were explored. + storm::storage::sparse::StateStorage stateStorage; + + /// This member holds information about reachable states that can be retrieved from the outside after a + /// successful build. + boost::optional stateValuations; + + /// A set of states that still need to be explored. + std::deque statesToExplore; + + /// An optional mapping from state indices to the row groups in which they actually reside. This needs to be + /// built in case the exploration order is not BFS. + boost::optional> stateRemapping; + + }; + + } // namespace adapters +} // namespace storm + +#endif /* STORM_BUILDER_ExplicitModelBuilder_H */ diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h deleted file mode 100644 index 92de20f2f..000000000 --- a/src/builder/ExplicitPrismModelBuilder.h +++ /dev/null @@ -1,268 +0,0 @@ -#ifndef STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H -#define STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H - -#include -#include -#include -#include -#include -#include -#include -#include -#include -#include - -#include "src/storage/prism/Program.h" -#include "src/storage/expressions/SimpleValuation.h" -#include "src/storage/expressions/ExpressionEvaluator.h" -#include "src/storage/BitVectorHashMap.h" -#include "src/logic/Formulas.h" -#include "src/models/sparse/StateAnnotation.h" -#include "src/models/sparse/Model.h" -#include "src/models/sparse/StateLabeling.h" -#include "src/storage/SparseMatrix.h" -#include "src/storage/sparse/StateValuations.h" -#include "src/storage/sparse/StateStorage.h" -#include "src/settings/SettingsManager.h" - -#include "src/utility/prism.h" - -#include "src/builder/ExplorationOrder.h" - -#include "src/generator/CompressedState.h" -#include "src/generator/VariableInformation.h" - -namespace storm { - namespace utility { - template class ConstantsComparator; - } - - namespace builder { - - using namespace storm::utility::prism; - using namespace storm::generator; - - // Forward-declare classes. - template struct RewardModelBuilder; - - template, typename StateType = uint32_t> - class ExplicitPrismModelBuilder { - public: - // A structure holding the individual components of a model. - struct ModelComponents { - ModelComponents(); - - // The transition matrix. - storm::storage::SparseMatrix transitionMatrix; - - // The state labeling. - storm::models::sparse::StateLabeling stateLabeling; - - // The reward models associated with the model. - std::unordered_map> rewardModels; - - // A vector that stores a labeling for each choice. - boost::optional>> choiceLabeling; - }; - - struct Options { - /*! - * Creates an object representing the default building options. - */ - Options(); - - /*! - * Copies the given set of options. - */ - Options(Options const& other) = default; - - /*! Creates an object representing the suggested building options assuming that the given formula is the - * only one to check. Additional formulas may be preserved by calling preserveFormula. - * - * @param formula The formula based on which to choose the building options. - */ - Options(storm::logic::Formula const& formula); - - /*! Creates an object representing the suggested building options assuming that the given formulas are - * the only ones to check. Additional formulas may be preserved by calling preserveFormula. - * - * @param formula Thes formula based on which to choose the building options. - */ - Options(std::vector> const& formulas); - - /*! - * Sets the constants definitions from the given string. The string must be of the form 'X=a,Y=b,Z=c', - * etc. where X,Y,Z are the variable names and a,b,c are the values of the constants. - * - * @param program The program managing the constants that shall be defined. Note that the program itself - * is not modified whatsoever. - * @param constantDefinitionString The string from which to parse the constants' values. - */ - void addConstantDefinitionsFromString(storm::prism::Program const& program, std::string const& constantDefinitionString); - - /*! - * Changes the options in a way that ensures that the given formula can be checked on the model once it - * has been built. - * - * @param formula The formula that is to be ''preserved''. - */ - void preserveFormula(storm::logic::Formula const& formula); - - /*! - * Analyzes the given formula and sets an expression for the states states of the model that can be - * treated as terminal states. Note that this may interfere with checking properties different than the - * one provided. - * - * @param formula The formula used to (possibly) derive an expression for the terminal states of the - * model. - */ - void setTerminalStatesFromFormula(storm::logic::Formula const& formula); - - // The order in which to explore the model. - ExplorationOrder explorationOrder; - - // A flag that indicates whether or not command labels are to be built. - bool buildCommandLabels; - - // A flag that indicates whether or not all reward models are to be build. - bool buildAllRewardModels; - - // A flag that indicates whether or not to store the state information after successfully building the - // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful - // call to translateProgram. - bool buildStateValuations; - - // A list of reward models to be build in case not all reward models are to be build. - std::set rewardModelsToBuild; - - // An optional mapping that, if given, contains defining expressions for undefined constants. - boost::optional> constantDefinitions; - - // A flag that indicates whether all labels are to be build. - bool buildAllLabels; - - // An optional set of labels that, if given, restricts the labels that are built. - boost::optional> labelsToBuild; - - // An optional set of expressions for which labels need to be built. - boost::optional> expressionLabels; - - // An optional expression or label that characterizes (a subset of) the terminal states of the model. If - // this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional> terminalStates; - - // An optional expression or label whose negation characterizes (a subset of) the terminal states of the - // model. If this is set, the outgoing transitions of these states are replaced with a self-loop. - boost::optional> negatedTerminalStates; - }; - - /*! - * Creates a builder for the given program. - * - * @param program The program to build. - */ - ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options = Options()); - - /*! - * Convert the program given at construction time to an abstract model. The type of the model is the one - * specified in the program. The given reward model name selects the rewards that the model will contain. - * - * @param program The program to translate. - * @param constantDefinitionString A string that contains a comma-separated definition of all undefined - * constants in the model. - * @param rewardModel The reward model that is to be built. - * @return The explicit model that was given by the probabilistic program. - */ - std::shared_ptr> translate(); - - /*! - * If requested in the options, information about the variable valuations in the reachable states can be - * retrieved via this function. - * - * @return A structure that stores information about all reachable states. - */ - storm::storage::sparse::StateValuations const& getStateValuations() const; - - /*! - * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). - * - * @return The translated program. - */ - storm::prism::Program const& getTranslatedProgram() const; - - private: - /*! - * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to - * the lists of all states with a new id. If the state was already known, the object that is pointed to by - * the given state pointer is deleted and the old state id is returned. Note that the pointer should not be - * used after invoking this method. - * - * @param state A pointer to a state for which to retrieve the index. This must not be used after the call. - * @return A pair indicating whether the state was already discovered before and the state id of the state. - */ - StateType getOrAddStateIndex(CompressedState const& state); - - /*! - * Builds the transition matrix and the transition reward matrix based for the given program. - * - * @param program The program for which to build the matrices. - * @param variableInformation A structure containing information about the variables in the program. - * @param transitionRewards A list of transition rewards that are to be considered in the transition reward - * matrix. - * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not. - * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this - * function. - * @param rewardModelBuilders A vector of reward model builders that is used to build the vector of selected - * reward models. - * @param terminalExpression If given, terminal states are not explored further. - * @return A tuple containing a vector with all rows at which the nondeterministic choices of each state begin - * and a vector containing the labels associated with each choice. - */ - boost::optional>> buildMatrices(std::vector> const& selectedRewardModels, storm::storage::SparseMatrixBuilder& transitionMatrixBuilder, std::vector>& rewardModelBuilders, boost::optional const& terminalExpression); - - /*! - * Explores the state space of the given program and returns the components of the model as a result. - * - * @param program The program whose state space to explore. - * @param selectedRewardModels The reward models that are to be considered. - * @param options A set of options used to customize the building process. - * @return A structure containing the components of the resulting model. - */ - ModelComponents buildModelComponents(std::vector> const& selectedRewardModels); - - /*! - * Builds the state labeling for the given program. - * - * @return The state labeling of the given program. - */ - storm::models::sparse::StateLabeling buildStateLabeling(); - - // The program to translate. The necessary transformations are performed upon construction of the builder. - storm::prism::Program program; - - // The options to be used for translating the program. - Options options; - - // The variable information. - VariableInformation variableInformation; - - // Internal information about the states that were explored. - storm::storage::sparse::StateStorage stateStorage; - - // This member holds information about reachable states that can be retrieved from the outside after a - // successful build. - boost::optional stateValuations; - - // A set of states that still need to be explored. - std::deque statesToExplore; - - // An optional mapping from state indices to the row groups in which they actually reside. This needs to be - // built in case the exploration order is not BFS. - boost::optional> stateRemapping; - - }; - - } // namespace adapters -} // namespace storm - -#endif /* STORM_BUILDER_EXPLICITPRISMMODELBUILDER_H */ diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp new file mode 100644 index 000000000..fae2fcc43 --- /dev/null +++ b/src/generator/NextStateGenerator.cpp @@ -0,0 +1,174 @@ +#include "src/generator/NextStateGenerator.h" + +#include "src/adapters/CarlAdapter.h" + +#include "src/logic/Formulas.h" + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace generator { + + LabelOrExpression::LabelOrExpression(storm::expressions::Expression const& expression) : labelOrExpression(expression) { + // Intentionally left empty. + } + + LabelOrExpression::LabelOrExpression(std::string const& label) : labelOrExpression(label) { + // Intentionally left empty. + } + + bool LabelOrExpression::isLabel() const { + return labelOrExpression.which() == 0; + } + + std::string const& LabelOrExpression::getLabel() const { + return boost::get(labelOrExpression); + } + + bool LabelOrExpression::isExpression() const { + return labelOrExpression.which() == 1; + } + + storm::expressions::Expression const& LabelOrExpression::getExpression() const { + return boost::get(labelOrExpression); + } + + NextStateGeneratorOptions::NextStateGeneratorOptions(storm::logic::Formula const& formula) { + this->preserveFormula(formula); + this->setTerminalStatesFromFormula(formula); + } + + NextStateGeneratorOptions::NextStateGeneratorOptions(std::vector> const& formulas) { + if (!formulas.empty()) { + for (auto const& formula : formulas) { + this->preserveFormula(*formula); + } + if (formulas.size() == 1) { + this->setTerminalStatesFromFormula(*formulas.front()); + } + } + } + + void NextStateGeneratorOptions::preserveFormula(storm::logic::Formula const& formula) { + // If we already had terminal states, we need to erase them. + if (hasTerminalStates()) { + clearTerminalStates(); + } + + // Determine the reward models we need to build. + std::set referencedRewardModels = formula.getReferencedRewardModels(); + for (auto const& rewardModelName : referencedRewardModels) { + rewardModelNames.push_back(rewardModelName); + } + + // Extract all the labels used in the formula. + std::vector> atomicLabelFormulas = formula.getAtomicLabelFormulas(); + for (auto const& formula : atomicLabelFormulas) { + addLabel(formula->getLabel()); + } + + // Extract all the expressions used in the formula. + std::vector> atomicExpressionFormulas = formula.getAtomicExpressionFormulas(); + for (auto const& formula : atomicExpressionFormulas) { + addLabel(formula->getExpression()); + } + } + + void NextStateGeneratorOptions::setTerminalStatesFromFormula(storm::logic::Formula const& formula) { + if (formula.isAtomicExpressionFormula()) { + addTerminalExpression(formula.asAtomicExpressionFormula().getExpression(), true); + } else if (formula.isAtomicLabelFormula()) { + addTerminalLabel(formula.asAtomicLabelFormula().getLabel(), true); + } else if (formula.isEventuallyFormula()) { + storm::logic::Formula const& sub = formula.asEventuallyFormula().getSubformula(); + if (sub.isAtomicExpressionFormula() || sub.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } else if (formula.isUntilFormula()) { + storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula(); + if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) { + this->setTerminalStatesFromFormula(right); + } + storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula(); + if (left.isAtomicExpressionFormula()) { + addTerminalExpression(left.asAtomicExpressionFormula().getExpression(), false); + } else if (left.isAtomicLabelFormula()) { + addTerminalLabel(left.asAtomicLabelFormula().getLabel(), false); + } + } else if (formula.isProbabilityOperatorFormula()) { + storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula(); + if (sub.isEventuallyFormula() || sub.isUntilFormula()) { + this->setTerminalStatesFromFormula(sub); + } + } + } + + std::vector const& NextStateGeneratorOptions::getRewardModelNames() const { + return rewardModelNames; + } + + std::set const& NextStateGeneratorOptions::getLabels() const { + return labels; + } + + std::vector const& NextStateGeneratorOptions::getLabelExpressions() const { + return labelExpressions; + } + + std::vector> const& NextStateGeneratorOptions::getTerminalStates() const { + return terminalStates; + } + + bool NextStateGeneratorOptions::hasTerminalStates() const { + return !terminalStates.empty(); + } + + void NextStateGeneratorOptions::clearTerminalStates() { + terminalStates.clear(); + } + + bool NextStateGeneratorOptions::isBuildChoiceLabelsSet() const { + return buildChoiceLabels; + } + + NextStateGeneratorOptions& NextStateGeneratorOptions::addRewardModel(std::string const& rewardModelName) { + rewardModelNames.emplace_back(rewardModelName); + return *this; + } + + NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(storm::expressions::Expression const& expression) { + labelExpressions.emplace_back(expression); + return *this; + } + + NextStateGeneratorOptions& NextStateGeneratorOptions::addLabel(std::string const& label) { + labels.insert(label); + return *this; + } + + NextStateGeneratorOptions& NextStateGeneratorOptions::addTerminalExpression(storm::expressions::Expression const& expression, bool value) { + terminalStates.push_back(std::make_pair(LabelOrExpression(expression), value)); + return *this; + } + + NextStateGeneratorOptions& NextStateGeneratorOptions::addTerminalLabel(std::string const& label, bool value) { + terminalStates.push_back(std::make_pair(LabelOrExpression(label), value)); + return *this; + } + + NextStateGeneratorOptions& NextStateGeneratorOptions::setBuildChoiceLabels(bool newValue) { + buildChoiceLabels = newValue; + return *this; + } + + template + NextStateGenerator::NextStateGenerator(NextStateGeneratorOptions const& options) : options(options) { + // Intentionally left empty. + } + + template class NextStateGenerator; + template class NextStateGenerator; + + } +} \ No newline at end of file diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h index 7dab9f470..a4063d2aa 100644 --- a/src/generator/NextStateGenerator.h +++ b/src/generator/NextStateGenerator.h @@ -4,24 +4,135 @@ #include #include +#include + #include "src/storage/expressions/Expression.h" #include "src/generator/CompressedState.h" #include "src/generator/StateBehavior.h" namespace storm { + namespace expressions { + class Expression; + } + + namespace storage { + template + class BitVectorHashMap; + } + + namespace models { + namespace sparse { + class StateLabeling; + } + } + + namespace logic { + class Formula; + } + namespace generator { + class LabelOrExpression { + public: + LabelOrExpression(storm::expressions::Expression const& expression); + LabelOrExpression(std::string const& label); + + bool isLabel() const; + std::string const& getLabel() const; + bool isExpression() const; + storm::expressions::Expression const& getExpression() const; + + private: + /// An optional label for the expression. + boost::variant labelOrExpression; + }; + + class NextStateGeneratorOptions { + public: + /*! + * Creates an object representing the suggested building options assuming that the given formula is the + * only one to check. Additional formulas may be preserved by calling preserveFormula. + * + * @param formula The formula based on which to choose the building options. + */ + NextStateGeneratorOptions(storm::logic::Formula const& formula); + + /*! + * Creates an object representing the suggested building options assuming that the given formulas are + * the only ones to check. Additional formulas may be preserved by calling preserveFormula. + * + * @param formula Thes formula based on which to choose the building options. + */ + NextStateGeneratorOptions(std::vector> const& formulas); + + /*! + * Changes the options in a way that ensures that the given formula can be checked on the model once it + * has been built. + * + * @param formula The formula that is to be ''preserved''. + */ + void preserveFormula(storm::logic::Formula const& formula); + + /*! + * Analyzes the given formula and sets an expression for the states states of the model that can be + * treated as terminal states. Note that this may interfere with checking properties different than the + * one provided. + * + * @param formula The formula used to (possibly) derive an expression for the terminal states of the + * model. + */ + void setTerminalStatesFromFormula(storm::logic::Formula const& formula); + + std::vector const& getRewardModelNames() const; + std::set const& getLabels() const; + std::vector const& getLabelExpressions() const; + std::vector> const& getTerminalStates() const; + bool hasTerminalStates() const; + void clearTerminalStates(); + bool isBuildChoiceLabelsSet() const; + + NextStateGeneratorOptions& addRewardModel(std::string const& rewardModelName); + NextStateGeneratorOptions& addLabel(storm::expressions::Expression const& expression); + NextStateGeneratorOptions& addLabel(std::string const& label); + NextStateGeneratorOptions& addTerminalExpression(storm::expressions::Expression const& expression, bool value); + NextStateGeneratorOptions& addTerminalLabel(std::string const& label, bool value); + NextStateGeneratorOptions& setBuildChoiceLabels(bool newValue); + + private: + /// The names of the reward models to generate. + std::vector rewardModelNames; + + /// A set of labels to build. + std::set labels; + + /// The expression that are to be used for creating the state labeling. + std::vector labelExpressions; + + /// If one of these labels/expressions evaluates to the given bool, the state generator can abort the exploration. + std::vector> terminalStates; + + /// A flag indicating whether or not to build choice labels. + bool buildChoiceLabels; + }; + template class NextStateGenerator { public: typedef std::function StateToIdCallback; + NextStateGenerator(NextStateGeneratorOptions const& options); + virtual bool isDeterministicModel() const = 0; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) = 0; virtual void load(CompressedState const& state) = 0; virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) = 0; virtual bool satisfies(storm::expressions::Expression const& expression) const = 0; + + virtual storm::models::sparse::StateLabeling generateLabeling(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) = 0; + + protected: + NextStateGeneratorOptions options; }; } } diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp index d82db2e6b..8286a6418 100644 --- a/src/generator/PrismNextStateGenerator.cpp +++ b/src/generator/PrismNextStateGenerator.cpp @@ -2,6 +2,10 @@ #include +#include "src/models/sparse/StateLabeling.h" + +#include "src/storage/BitVectorHashMap.h" + #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" @@ -10,21 +14,15 @@ namespace storm { namespace generator { template - PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), state(nullptr), comparator() { + PrismNextStateGenerator::PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options) : NextStateGenerator(options), program(program), rewardModels(), variableInformation(VariableInformation(program)), evaluator(program.getManager()), state(nullptr), comparator() { STORM_LOG_THROW(!program.specifiesSystemComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); + + // Extract the reward models from the program based on the names we were given. + for (auto const& rewardModelName : this->options.getRewardModelNames()) { + rewardModels.push_back(program.getRewardModel(rewardModelName)); + } } - template - void PrismNextStateGenerator::addRewardModel(storm::prism::RewardModel const& rewardModel) { - selectedRewardModels.push_back(rewardModel); - hasStateActionRewards |= rewardModel.hasStateActionRewards(); - } - - template - void PrismNextStateGenerator::setTerminalExpression(storm::expressions::Expression const& terminalExpression) { - this->terminalExpression = terminalExpression; - } - template bool PrismNextStateGenerator::isDeterministicModel() const { return program.isDeterministicModel(); @@ -72,7 +70,7 @@ namespace storm { // First, construct the state rewards, as we may return early if there are no choices later and we already // need the state rewards then. - for (auto const& rewardModel : selectedRewardModels) { + for (auto const& rewardModel : rewardModels) { ValueType stateRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateRewards()) { for (auto const& stateReward : rewardModel.get().getStateRewards()) { @@ -85,8 +83,12 @@ namespace storm { } // If a terminal expression was set and we must not expand this state, return now. - if (terminalExpression && evaluator.asBool(terminalExpression.get())) { - return result; + if (this->options.hasTerminalExpression()) { + for (auto const& expression : this->options.getTerminalExpressions()) { + if (evaluator.asBool(expression) { + return result; + } + } } // Get all choices for the state. @@ -126,13 +128,13 @@ namespace storm { totalExitRate += choice.getTotalMass(); } - if (buildChoiceLabeling) { + if (this->options.isBuildChoiceLabelsSet()) { globalChoice.addChoiceLabels(choice.getChoiceLabels()); } } // Now construct the state-action reward for all selected reward models. - for (auto const& rewardModel : selectedRewardModels) { + for (auto const& rewardModel : rewardModels) { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { @@ -262,7 +264,7 @@ namespace storm { Choice& choice = result.back(); // Remember the command labels only if we were asked to. - if (buildChoiceLabeling) { + if (this->options.isBuildChoiceLabelsSet()) { choice.addChoiceLabel(command.getGlobalIndex()); } @@ -282,7 +284,7 @@ namespace storm { } // Create the state-action reward for the newly created choice. - for (auto const& rewardModel : selectedRewardModels) { + for (auto const& rewardModel : rewardModels) { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { @@ -365,7 +367,7 @@ namespace storm { Choice& choice = result.back(); // Remember the command labels only if we were asked to. - if (buildChoiceLabeling) { + if (this->options.isBuildChoiceLabelsSet()) { // Add the labels of all commands to this choice. for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { choice.addChoiceLabel(iteratorList[i]->get().getGlobalIndex()); @@ -384,7 +386,7 @@ namespace storm { STORM_LOG_THROW(!program.isDiscreteTimeModel() || !comparator.isConstant(probabilitySum) || comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ")."); // Create the state-action reward for the newly created choice. - for (auto const& rewardModel : selectedRewardModels) { + for (auto const& rewardModel : rewardModels) { ValueType stateActionRewardValue = storm::utility::zero(); if (rewardModel.get().hasStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { @@ -420,6 +422,36 @@ namespace storm { return result; } + template + storm::models::sparse::StateLabeling PrismNextStateGenerator::generateLabeling(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { + std::vector const& labels = program.getLabels(); + + storm::models::sparse::StateLabeling result(states.size()); + + // Initialize labeling. + for (auto const& label : labels) { + result.addLabel(label.getName()); + } + for (auto const& stateIndexPair : states) { + unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator); + + for (auto const& label : labels) { + // Add label to state, if the corresponding expression is true. + if (evaluator.asBool(label.getStatePredicateExpression())) { + result.addLabelToState(label.getName(), stateIndexPair.second); + } + } + } + + // Also label the initial state with the special label "init". + result.addLabel("init"); + for (auto index : initialStateIndices) { + result.addLabelToState("init", index); + } + + return result; + } + template class PrismNextStateGenerator; template class PrismNextStateGenerator; } diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h index fe997d73a..27d43864a 100644 --- a/src/generator/PrismNextStateGenerator.h +++ b/src/generator/PrismNextStateGenerator.h @@ -17,17 +17,7 @@ namespace storm { public: typedef typename NextStateGenerator::StateToIdCallback StateToIdCallback; - PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling); - - /*! - * Adds a reward model to the list of selected reward models () - */ - void addRewardModel(storm::prism::RewardModel const& rewardModel); - - /*! - * Sets an expression such that if it evaluates to true in a state, prevents the exploration. - */ - void setTerminalExpression(storm::expressions::Expression const& terminalExpression); + PrismNextStateGenerator(storm::prism::Program const& program, NextStateGeneratorOptions const& options = NextStateGeneratorOptions()); virtual bool isDeterministicModel() const override; virtual std::vector getInitialStates(StateToIdCallback const& stateToIdCallback) override; @@ -36,6 +26,8 @@ namespace storm { virtual StateBehavior expand(StateToIdCallback const& stateToIdCallback) override; virtual bool satisfies(storm::expressions::Expression const& expression) const override; + virtual storm::models::sparse::StateLabeling generateLabeling(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; + private: /*! * Applies an update to the state currently loaded into the evaluator and applies the resulting values to @@ -89,18 +81,13 @@ namespace storm { // A flag that stores whether at least one of the selected reward models has state-action rewards. bool hasStateActionRewards; - // A flag that stores whether or not to build the choice labeling. - bool buildChoiceLabeling; - - // An optional expression that governs which states must not be explored. - boost::optional terminalExpression; - // Information about how the variables are packed. VariableInformation const& variableInformation; // An evaluator used to evaluate expressions. storm::expressions::ExpressionEvaluator evaluator; + // The currently loaded state. CompressedState const* state; // A comparator used to compare constants. diff --git a/src/generator/PrismStateLabelingGenerator.cpp b/src/generator/PrismStateLabelingGenerator.cpp deleted file mode 100644 index 6022ce063..000000000 --- a/src/generator/PrismStateLabelingGenerator.cpp +++ /dev/null @@ -1,50 +0,0 @@ -#include "src/generator/PrismStateLabelingGenerator.h" - -#include "src/generator/CompressedState.h" - -#include "src/storage/expressions/ExpressionEvaluator.h" - -namespace storm { - namespace generator { - - template - PrismStateLabelingGenerator::PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation) : program(program), variableInformation(variableInformation) { - // Intentionally left empty. - } - - template - storm::models::sparse::StateLabeling PrismStateLabelingGenerator::generate(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices) { - std::vector const& labels = program.getLabels(); - - storm::expressions::ExpressionEvaluator evaluator(program.getManager()); - storm::models::sparse::StateLabeling result(states.size()); - - // Initialize labeling. - for (auto const& label : labels) { - result.addLabel(label.getName()); - } - for (auto const& stateIndexPair : states) { - unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, evaluator); - - for (auto const& label : labels) { - // Add label to state, if the corresponding expression is true. - if (evaluator.asBool(label.getStatePredicateExpression())) { - result.addLabelToState(label.getName(), stateIndexPair.second); - } - } - } - - // Also label the initial state with the special label "init". - result.addLabel("init"); - for (auto index : initialStateIndices) { - result.addLabelToState("init", index); - } - - return result; - } - - template class PrismStateLabelingGenerator; - template class PrismStateLabelingGenerator; - - } -} \ No newline at end of file diff --git a/src/generator/PrismStateLabelingGenerator.h b/src/generator/PrismStateLabelingGenerator.h deleted file mode 100644 index 9859453ba..000000000 --- a/src/generator/PrismStateLabelingGenerator.h +++ /dev/null @@ -1,31 +0,0 @@ -#ifndef STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ -#define STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ - -#include "src/generator/StateLabelingGenerator.h" - -#include "src/generator/VariableInformation.h" - -#include "src/storage/prism/Program.h" - -namespace storm { - namespace generator { - - template - class PrismStateLabelingGenerator : public StateLabelingGenerator { - public: - PrismStateLabelingGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation); - - virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) override; - - private: - // The program for which to generate the labels. - storm::prism::Program const& program; - - // Information about how the variables are packed. - VariableInformation const& variableInformation; - }; - - } -} - -#endif /* STORM_GENERATOR_PRISMSTATELABELINGGENERATOR_H_ */ \ No newline at end of file diff --git a/src/generator/StateLabelingGenerator.h b/src/generator/StateLabelingGenerator.h deleted file mode 100644 index 17401c703..000000000 --- a/src/generator/StateLabelingGenerator.h +++ /dev/null @@ -1,20 +0,0 @@ -#ifndef STORM_GENERATOR_STATELABELINGGENERATOR_H_ -#define STORM_GENERATOR_STATELABELINGGENERATOR_H_ - -#include "src/models/sparse/StateLabeling.h" - -#include "src/storage/BitVectorHashMap.h" - -namespace storm { - namespace generator { - - template - class StateLabelingGenerator { - public: - virtual storm::models::sparse::StateLabeling generate(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices = {}) = 0; - }; - - } -} - -#endif /* STORM_GENERATOR_STATELABELINGGENERATOR_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index b7b080a48..66758a72e 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -1560,7 +1560,7 @@ namespace storm { automaton.addBoundedIntegerVariable(newIntegerVariable); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; - } else { //if (!accessingModuleIndices.empty()) { + } else if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. janiModel.addBoundedIntegerVariable(newIntegerVariable); storm::expressions::Expression variableInitialExpression = variable.getExpressionVariable() == variable.getInitialValueExpression(); @@ -1575,7 +1575,7 @@ namespace storm { automaton.addBooleanVariable(newBooleanVariable); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); initialStatesExpression = initialStatesExpression.isInitialized() ? initialStatesExpression && variableInitialExpression : variableInitialExpression; - } else { //if (!accessingModuleIndices.empty()) { + } else if (!accessingModuleIndices.empty()) { // Otherwise, we need to make it global. janiModel.addBooleanVariable(newBooleanVariable); storm::expressions::Expression variableInitialExpression = storm::expressions::iff(variable.getExpressionVariable(), variable.getInitialValueExpression()); diff --git a/src/utility/storm.h b/src/utility/storm.h index 9f909c815..964ef4f56 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -46,7 +46,7 @@ #include "src/storage/jani/Model.h" // Headers of builders. -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/builder/DdPrismModelBuilder.h" // Headers for model processing. @@ -109,8 +109,8 @@ namespace storm { // Customize and perform model-building. if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) { - typename storm::builder::ExplicitPrismModelBuilder>::Options options; - options = typename storm::builder::ExplicitPrismModelBuilder>::Options(formulas); + typename storm::builder::ExplicitModelBuilder>::Options options; + options = typename storm::builder::ExplicitModelBuilder>::Options(formulas); options.addConstantDefinitionsFromString(program, constants); // Generate command labels if we are going to build a counterexample later. @@ -118,7 +118,7 @@ namespace storm { options.buildCommandLabels = true; } - storm::builder::ExplicitPrismModelBuilder builder(program, options); + storm::builder::ExplicitModelBuilder builder(program, options); result.model = builder.translate(); translatedProgram = builder.getTranslatedProgram(); } else if (storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) { diff --git a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp index 38b0771d3..159966d76 100644 --- a/test/functional/builder/ExplicitPrismModelBuilderTest.cpp +++ b/test/functional/builder/ExplicitPrismModelBuilderTest.cpp @@ -3,104 +3,104 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/settings/SettingMemento.h" #include "src/parser/PrismParser.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/settings/modules/IOSettings.h" -TEST(ExplicitPrismModelBuilderTest, Dtmc) { +TEST(ExplicitModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } -TEST(ExplicitPrismModelBuilderTest, Ctmc) { +TEST(ExplicitModelBuilderTest, Ctmc) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } -TEST(ExplicitPrismModelBuilderTest, Mdp) { +TEST(ExplicitModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); } -TEST(ExplicitPrismModelBuilderTest, Fail) { +TEST(ExplicitModelBuilderTest, Fail) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm"); - ASSERT_THROW(storm::builder::ExplicitPrismModelBuilder(program).translate(), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::builder::ExplicitModelBuilder(program).translate(), storm::exceptions::WrongFormatException); } diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 6b6fb9d3f..b3afe2657 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -4,7 +4,7 @@ #include "src/parser/PrismParser.h" #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/solver/GmmxxLinearEquationSolver.h" #include "src/models/sparse/StandardRewardModel.h" @@ -29,13 +29,13 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { // Build the model. #ifdef WINDOWS - storm::builder::ExplicitPrismModelBuilder::Options options; + storm::builder::ExplicitModelBuilder::Options options; #else - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -112,13 +112,13 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) { // Build the model. #ifdef WINDOWS - storm::builder::ExplicitPrismModelBuilder::Options options; + storm::builder::ExplicitModelBuilder::Options options; #else - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -180,7 +180,7 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -222,12 +222,12 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) { // Build the model. #ifdef WINDOWS - storm::builder::ExplicitPrismModelBuilder::Options options; + storm::builder::ExplicitModelBuilder::Options options; #else - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; #endif options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index 1c3b8a83b..55a015eeb 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -14,7 +14,7 @@ #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); @@ -284,7 +284,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { TEST(GmmxxDtmcPrctlModelCheckerTest, Conditional) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_EQ(4ul, model->getNumberOfStates()); ASSERT_EQ(5ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 74535e8da..917dbfe6a 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -15,7 +15,7 @@ #include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" #include "src/parser/PrismParser.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { std::shared_ptr> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew"); @@ -197,7 +197,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(4ul, model->getNumberOfStates()); EXPECT_EQ(11ul, model->getNumberOfTransitions()); @@ -247,7 +247,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, tiny_rewards) { // A parser that we use for conveniently constructing the formulas. storm::parser::FormulaParser formulaParser; - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); EXPECT_EQ(3ul, model->getNumberOfStates()); EXPECT_EQ(4ul, model->getNumberOfTransitions()); diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index da8f47228..ecee3f5a4 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -4,7 +4,7 @@ #include "src/parser/PrismParser.h" #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/utility/solver.h" #include "src/models/sparse/StandardRewardModel.h" @@ -27,13 +27,13 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) { // Build the model. #ifdef WINDOWS - storm::builder::ExplicitPrismModelBuilder::Options options; + storm::builder::ExplicitModelBuilder::Options options; #else - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("num_repairs"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -103,13 +103,13 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) { // Build the model. #ifdef WINDOWS - storm::builder::ExplicitPrismModelBuilder::Options options; + storm::builder::ExplicitModelBuilder::Options options; #else - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("up"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -164,7 +164,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) { std::shared_ptr formula(nullptr); // Build the model. - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); @@ -199,13 +199,13 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) { // Build the model with the customers reward structure. #ifdef WINDOWS - storm::builder::ExplicitPrismModelBuilder::Options options; + storm::builder::ExplicitModelBuilder::Options options; #else - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; #endif options.buildAllRewardModels = false; options.rewardModelsToBuild.insert("customers"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program, options).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).translate(); ASSERT_EQ(storm::models::ModelType::Ctmc, model->getType()); std::shared_ptr> ctmc = model->as>(); uint_fast64_t initialState = *ctmc->getInitialStates().begin(); diff --git a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp index 657d36575..a7b025009 100644 --- a/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/MilpPermissiveSchedulerTest.cpp @@ -5,7 +5,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/permissivesched/PermissiveSchedulers.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -22,13 +22,13 @@ TEST(MilpPermissiveSchedulerTest, DieSelection) { auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.17 [ F \"one\"]")->asProbabilityOperatorFormula(); // Customize and perform model-building. - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; - options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula02); + options = typename storm::builder::ExplicitModelBuilder::Options(formula02); options.addConstantDefinitionsFromString(program, ""); options.buildCommandLabels = true; - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); boost::optional> perms = storm::ps::computePermissiveSchedulerViaMILP<>(*mdp, formula02); EXPECT_NE(perms, boost::none); diff --git a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp index 2790cd86a..f61c18c41 100644 --- a/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp +++ b/test/functional/permissiveschedulers/SmtPermissiveSchedulerTest.cpp @@ -5,7 +5,7 @@ #include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/permissivesched/PermissiveSchedulers.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" @@ -25,13 +25,13 @@ TEST(SmtPermissiveSchedulerTest, DieSelection) { auto formula001b = formulaParser.parseSingleFormulaFromString("P<=0.05 [ F \"one\"]")->asProbabilityOperatorFormula(); // Customize and perform model-building. - typename storm::builder::ExplicitPrismModelBuilder::Options options; + typename storm::builder::ExplicitModelBuilder::Options options; - options = typename storm::builder::ExplicitPrismModelBuilder::Options(formula02b); + options = typename storm::builder::ExplicitModelBuilder::Options(formula02b); options.addConstantDefinitionsFromString(program, ""); options.buildCommandLabels = true; - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); // boost::optional> perms = storm::ps::computePermissiveSchedulerViaSMT<>(*mdp, formula02); // EXPECT_NE(perms, boost::none); diff --git a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp index 65c5ef132..19ea6f8a6 100644 --- a/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp +++ b/test/functional/storage/NondeterministicModelBisimulationDecompositionTest.cpp @@ -4,7 +4,7 @@ #include "src/parser/PrismParser.h" #include "src/parser/FormulaParser.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h" #include "src/models/sparse/Mdp.h" @@ -14,7 +14,7 @@ TEST(NondeterministicModelBisimulationDecomposition, TwoDice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); // Build the die model without its reward model. - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); diff --git a/test/functional/utility/GraphTest.cpp b/test/functional/utility/GraphTest.cpp index 4c6bf0d50..cf1517013 100644 --- a/test/functional/utility/GraphTest.cpp +++ b/test/functional/utility/GraphTest.cpp @@ -9,7 +9,7 @@ #include "src/models/sparse/Mdp.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/builder/DdPrismModelBuilder.h" -#include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/ExplicitModelBuilder.h" #include "src/utility/graph.h" #include "src/storage/dd/Add.h" #include "src/storage/dd/Bdd.h" @@ -181,7 +181,7 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { TEST(GraphTest, ExplicitProb01) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); @@ -202,7 +202,7 @@ TEST(GraphTest, ExplicitProb01) { TEST(GraphTest, ExplicitProb01MinMax) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm"); - std::shared_ptr> model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -217,7 +217,7 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); @@ -238,7 +238,7 @@ TEST(GraphTest, ExplicitProb01MinMax) { EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm"); - model = storm::builder::ExplicitPrismModelBuilder(program).translate(); + model = storm::builder::ExplicitModelBuilder(program).translate(); ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp index dea5da735..9caf16632 100644 --- a/test/functional/utility/ModelInstantiatorTest.cpp +++ b/test/functional/utility/ModelInstantiatorTest.cpp @@ -30,10 +30,10 @@ TEST(ModelInstantiatorTest, BrpProb) { std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + typename storm::builder::ExplicitModelBuilder::Options options = storm::builder::ExplicitModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); EXPECT_FALSE(dtmc->hasRewardModel()); @@ -151,10 +151,10 @@ TEST(ModelInstantiatorTest, Brp_Rew) { std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + typename storm::builder::ExplicitModelBuilder::Options options = storm::builder::ExplicitModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> dtmc = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + std::shared_ptr> dtmc = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Dtmc> modelInstantiator(*dtmc); @@ -224,10 +224,10 @@ TEST(ModelInstantiatorTest, Consensus) { std::vector> formulas = storm::parseFormulasForProgram(formulaAsString, program); ASSERT_TRUE(formulas.size()==1); // Parametric model - typename storm::builder::ExplicitPrismModelBuilder::Options options = storm::builder::ExplicitPrismModelBuilder::Options(*formulas[0]); + typename storm::builder::ExplicitModelBuilder::Options options = storm::builder::ExplicitModelBuilder::Options(*formulas[0]); options.addConstantDefinitionsFromString(program, constantsAsString); options.preserveFormula(*formulas[0]); - std::shared_ptr> mdp = storm::builder::ExplicitPrismModelBuilder(program, options).translate()->as>(); + std::shared_ptr> mdp = storm::builder::ExplicitModelBuilder(program, options).translate()->as>(); storm::utility::ModelInstantiator, storm::models::sparse::Mdp> modelInstantiator(*mdp);