diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.h b/src/storm-dft/builder/ExplicitDFTModelBuilder.h index d61043368..2913a78fa 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.h @@ -7,6 +7,7 @@ #include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Model.h" #include "storm/storage/SparseMatrix.h" @@ -49,7 +50,7 @@ namespace storm { std::vector exitRates; // A vector that stores a labeling for each choice. - boost::optional>> choiceLabeling; + boost::optional choiceLabeling; }; const size_t INITIAL_BUCKETSIZE = 20000; diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h index 97439f47a..802aefe1b 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h +++ b/src/storm-dft/builder/ExplicitDFTModelBuilderApprox.h @@ -7,6 +7,7 @@ #include #include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/models/sparse/Model.h" #include "storm/storage/SparseMatrix.h" @@ -51,7 +52,7 @@ namespace storm { std::vector exitRates; // A vector that stores a labeling for each choice. - boost::optional>> choiceLabeling; + boost::optional choiceLabeling; // A flag indicating if the model is deterministic. bool deterministicModel; diff --git a/src/storm/builder/ExplicitModelBuilderResult.cpp b/src/storm/builder/ExplicitModelBuilderResult.cpp index b2d52522e..330be5aee 100644 --- a/src/storm/builder/ExplicitModelBuilderResult.cpp +++ b/src/storm/builder/ExplicitModelBuilderResult.cpp @@ -13,6 +13,11 @@ namespace storm { ExplicitModelBuilderResult::ExplicitModelBuilderResult(std::shared_ptr> model, std::shared_ptr stateValuations,std::shared_ptr choiceOrigins) : model(model), stateValuations(stateValuations), choiceOrigins(choiceOrigins) { // Intentionally left empty } + + template + bool ExplicitModelBuilderResult::hasModel() { + return static_cast(model); + } template std::shared_ptr>& ExplicitModelBuilderResult::getModel() { diff --git a/src/storm/builder/ExplicitModelBuilderResult.h b/src/storm/builder/ExplicitModelBuilderResult.h index 76a8e1161..ad1f4111b 100644 --- a/src/storm/builder/ExplicitModelBuilderResult.h +++ b/src/storm/builder/ExplicitModelBuilderResult.h @@ -11,8 +11,9 @@ namespace storm { template> class ExplicitModelBuilderResult { public: - ExplicitModelBuilderResult(std::shared_ptr> model, std::shared_ptr stateValuations,std::shared_ptr choiceOrigins); + ExplicitModelBuilderResult(std::shared_ptr> model, std::shared_ptr stateValuations = nullptr,std::shared_ptr choiceOrigins = nullptr); + bool hasModel(); std::shared_ptr>& getModel(); std::shared_ptr> const& getModel() const; diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 3135fe4a0..379f15412 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -15,7 +15,6 @@ #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" - #include "storm/builder/RewardModelInformation.h" #include "storm/models/sparse/Dtmc.h" @@ -458,7 +457,7 @@ namespace storm { } template - std::shared_ptr> ExplicitJitJaniModelBuilder::build() { + storm::builder::ExplicitModelBuilderResult ExplicitJitJaniModelBuilder::build() { // (0) Assemble information about the model. cpptempl::data_map modelData = generateModelData(); @@ -506,7 +505,7 @@ namespace storm { STORM_LOG_THROW(!error, storm::exceptions::WrongFormatException, "Model building failed. Reason: " << error.get()); // Return the constructed model. - return sparseModel; + return storm::builder::ExplicitModelBuilderResult(sparseModel); } template diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index 65321ad9f..6b291ffde 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -17,6 +17,8 @@ #include "storm/builder/BuilderOptions.h" #include "storm/builder/jit/JitModelBuilderInterface.h" #include "storm/builder/jit/ModelComponentsBuilder.h" +#include "storm/builder/ExplicitModelBuilderResult.h" + namespace storm { namespace models { @@ -57,7 +59,7 @@ namespace storm { /*! * Builds and returns the sparse model. */ - std::shared_ptr> build(); + storm::builder::ExplicitModelBuilderResult build(); /*! * Performs some checks that can help debug why the model builder does not work. Returns true if the diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index b43db8bd9..8f51a69a5 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -311,23 +311,27 @@ namespace storm { auto formulas = extractFormulasFromProperties(properties); // Start by building the model. storm::utility::Stopwatch modelBuildingWatch(true); - std::shared_ptr markovModel = buildSparseModel(model, formulas); + storm::builder::ExplicitModelBuilderResult builderResult = buildSparseModel(model, formulas); modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); - STORM_LOG_THROW(markovModel, storm::exceptions::UnexpectedException, "The model was not successfully built."); + // Extract the model from the result. + STORM_LOG_THROW(builderResult.hasModel(), storm::exceptions::UnexpectedException, "The model was not successfully built."); + std::shared_ptr markovModel = builderResult.getModel(); + builderResult.getModel().reset(); + STORM_LOG_WARN_COND(markovModel.unique(), "There are multiple references to the model. After preprocessing the model, the preprocessed as well as the original model might be stored in memory."); // Print some information about the model. markovModel->printModelInformationToStream(std::cout); // Preprocess the model. + STORM_LOG_WARN_COND(builderResult.hasStateValuations() || builderResult.hasChoiceOrigins(), "state valuations and choice origins might be invalidated if the model is preprocessed..."); // TODO: check this more carefully. BRANCH_ON_SPARSE_MODELTYPE(markovModel, markovModel, ValueType, preprocessModel, formulas); - std::shared_ptr> sparseModel = markovModel->template as>(); // Finally, treat the formulas. if (storm::settings::getModule().isCounterexampleSet()) { - generateCounterexamples(model, sparseModel, formulas); + generateCounterexamples(model, sparseModel, builderResult.getChoiceOrigins(), formulas); } else if (storm::settings::getModule().isParameterLiftingSet()) { STORM_LOG_THROW(storm::settings::getModule().isParametricSet(), storm::exceptions::InvalidSettingsException, "Invoked parameter lifting without enabling the parametric engine."); storm::performParameterLifting(sparseModel, formulas); diff --git a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h similarity index 82% rename from src/storm/counterexamples/MILPMinimalLabelSetGenerator.h rename to src/storm/counterexamples/MILPMinimalCommandSetGenerator.h index 537b844d6..adcf204b6 100644 --- a/src/storm/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h @@ -19,6 +19,8 @@ #include "storm/utility/solver.h" #include "storm/solver/LpSolver.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" + #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CounterexampleGeneratorSettings.h" @@ -28,10 +30,10 @@ namespace storm { /*! * This class provides functionality to generate a minimal counterexample to a probabilistic reachability - * property in terms of used labels. + * property in terms of used commands. */ template - class MILPMinimalLabelSetGenerator { + class MILPMinimalCommandSetGenerator { private: /*! * A helper class that provides the functionality to compute a hash value for pairs of state indices. @@ -55,21 +57,21 @@ namespace storm { }; /*! - * A helper struct capturing information about relevant and problematic choices of states and which labels + * A helper struct capturing information about relevant and problematic choices of states and which commands * are relevant. */ struct ChoiceInformation { std::unordered_map> relevantChoicesForRelevantStates; std::unordered_map> problematicChoicesForProblematicStates; - boost::container::flat_set allRelevantLabels; - boost::container::flat_set knownLabels; + boost::container::flat_set allRelevantCommands; + boost::container::flat_set knownCommands; }; /*! * A helper struct capturing information about the variables of the MILP formulation. */ struct VariableInformation { - std::unordered_map labelToVariableMap; + std::unordered_map commandToVariableMap; std::unordered_map> stateToChoiceVariablesMap; std::unordered_map initialStateToChoiceVariableMap; std::unordered_map stateToProbabilityVariableMap; @@ -87,16 +89,16 @@ namespace storm { * non-zero probability of satisfying phi until psi. Problematic states are relevant states that have at * least one scheduler such that the probability of satisfying phi until psi is zero. * - * @param labeledMdp The MDP whose states to search. + * @param mdp The MDP whose states to search. * @param phiStates A bit vector characterizing all states satisfying phi. * @param psiStates A bit vector characterizing all states satisfying psi. * @return A structure that stores the relevant and problematic states. */ - static struct StateInformation determineRelevantAndProblematicStates(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static struct StateInformation determineRelevantAndProblematicStates(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { StateInformation result; - result.relevantStates = storm::utility::graph::performProbGreater0E(labeledMdp.getBackwardTransitions(), phiStates, psiStates); + result.relevantStates = storm::utility::graph::performProbGreater0E(mdp.getBackwardTransitions(), phiStates, psiStates); result.relevantStates &= ~psiStates; - result.problematicStates = storm::utility::graph::performProb0E(labeledMdp.getTransitionMatrix(), labeledMdp.getNondeterministicChoiceIndices(), labeledMdp.getBackwardTransitions(), phiStates, psiStates); + result.problematicStates = storm::utility::graph::performProb0E(mdp.getTransitionMatrix(), mdp.getNondeterministicChoiceIndices(), mdp.getBackwardTransitions(), phiStates, psiStates); result.problematicStates &= result.relevantStates; STORM_LOG_DEBUG("Found " << phiStates.getNumberOfSetBits() << " filter states."); STORM_LOG_DEBUG("Found " << psiStates.getNumberOfSetBits() << " target states."); @@ -108,21 +110,20 @@ namespace storm { /*! * Determines the relevant and problematic choices of the given MDP with respect to the given parameters. * - * @param labeledMdp The MDP whose choices to search. + * @param mdp The MDP whose choices to search. * @param stateInformation The relevant and problematic states of the model. * @param psiStates A bit vector characterizing the psi states in the model. * @return A structure that stores the relevant and problematic choices in the model as well as the set - * of relevant labels. + * of relevant commands. */ - static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { + static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { // Create result and shortcuts to needed data for convenience. ChoiceInformation result; - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); // Now traverse all choices of all relevant states and check whether there is a relevant target state. - // If so, the associated labels become relevant. Also, if a choice of relevant state has at least one + // If so, the associated commands become relevant. Also, if a choice of relevant state has at least one // relevant successor, the choice is considered to be relevant. for (auto state : stateInformation.relevantStates) { result.relevantChoicesForRelevantStates.emplace(state, std::list()); @@ -133,10 +134,10 @@ namespace storm { bool currentChoiceRelevant = false; bool allSuccessorsProblematic = true; for (auto const& successorEntry : transitionMatrix.getRow(row)) { - // If there is a relevant successor, we need to add the labels of the current choice. + // If there is a relevant successor, we need to add the commands of the current choice. if (stateInformation.relevantStates.get(successorEntry.getColumn()) || psiStates.get(successorEntry.getColumn())) { - for (auto const& label : choiceLabeling[row]) { - result.allRelevantLabels.insert(label); + for (auto const& command : choiceOrigins.getCommandSet(row)) { + result.allRelevantCommands.insert(command); } if (!currentChoiceRelevant) { currentChoiceRelevant = true; @@ -156,30 +157,30 @@ namespace storm { } } - // Finally, determine the set of labels that are known to be taken. - result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, result.allRelevantLabels); - STORM_LOG_DEBUG("Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels."); + // Finally, determine the set of commands that are known to be taken. + result.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, choiceOrigins, psiStates, result.allRelevantCommands); + STORM_LOG_DEBUG("Found " << result.allRelevantCommands.size() << " relevant commands and " << result.knownCommands.size() << " known commands."); return result; } /*! - * Creates the variables for the labels of the model. + * Creates the variables for the commands of the model. * * @param solver The MILP solver. - * @param relevantLabels The set of relevant labels of the model. - * @return A mapping from labels to variable indices. + * @param relevantCommands The set of relevant commands of the model. + * @return A mapping from commands to variable indices. */ - static std::pair, uint_fast64_t> createLabelVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantLabels) { + static std::pair, uint_fast64_t> createCommandVariables(storm::solver::LpSolver& solver, boost::container::flat_set const& relevantCommands) { std::stringstream variableNameBuffer; std::unordered_map resultingMap; - for (auto const& label : relevantLabels) { + for (auto const& command : relevantCommands) { variableNameBuffer.str(""); variableNameBuffer.clear(); - variableNameBuffer << "label" << label; - resultingMap[label] = solver.addBinaryVariable(variableNameBuffer.str(), 1); + variableNameBuffer << "command" << command; + resultingMap[command] = solver.addBinaryVariable(variableNameBuffer.str(), 1); } - return std::make_pair(resultingMap, relevantLabels.size()); + return std::make_pair(resultingMap, relevantCommands.size()); } /*! @@ -214,16 +215,16 @@ namespace storm { * in the model. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states of the model. * @return A mapping from initial states to choice variable indices. */ - static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation) { + static std::pair, uint_fast64_t> createInitialChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; - for (auto initialState : labeledMdp.getStates("init")) { + for (auto initialState : mdp.getStates("init")) { // Only consider this initial state if it is relevant. if (stateInformation.relevantStates.get(initialState)) { variableNameBuffer.str(""); @@ -275,11 +276,11 @@ namespace storm { * Creates the variables for the problematic states in the model. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states in the model. * @return A mapping from problematic states to the index of the corresponding variables. */ - static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, uint_fast64_t> createProblematicStateVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map resultingMap; @@ -297,7 +298,7 @@ namespace storm { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(row)) { if (stateInformation.relevantStates.get(successorEntry.getColumn())) { if (resultingMap.find(successorEntry.getColumn()) == resultingMap.end()) { variableNameBuffer.str(""); @@ -317,12 +318,12 @@ namespace storm { * Creates the variables for the problematic choices in the model. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. * @return A mapping from problematic choices to the index of the corresponding variables. */ - static std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> createProblematicChoiceVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { std::stringstream variableNameBuffer; uint_fast64_t numberOfVariablesCreated = 0; std::unordered_map, storm::expressions::Variable, PairHash> resultingMap; @@ -330,7 +331,7 @@ namespace storm { for (auto state : stateInformation.problematicStates) { std::list const& relevantChoicesForState = choiceInformation.relevantChoicesForRelevantStates.at(state); for (uint_fast64_t row : relevantChoicesForState) { - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(row)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(row)) { if (stateInformation.relevantStates.get(successorEntry.getColumn())) { variableNameBuffer.str(""); variableNameBuffer.clear(); @@ -350,19 +351,19 @@ namespace storm { * passed to the solver. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. */ - static VariableInformation createVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { + static VariableInformation createVariables(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation) { // Create a struct that stores all information about variables. VariableInformation result; - // Create variables for involved labels. - std::pair, uint_fast64_t> labelVariableResult = createLabelVariables(solver, choiceInformation.allRelevantLabels); - result.labelToVariableMap = std::move(labelVariableResult.first); - result.numberOfVariables += labelVariableResult.second; - STORM_LOG_DEBUG("Created variables for labels."); + // Create variables for involved commands. + std::pair, uint_fast64_t> commandVariableResult = createCommandVariables(solver, choiceInformation.allRelevantCommands); + result.commandToVariableMap = std::move(commandVariableResult.first); + result.numberOfVariables += commandVariableResult.second; + STORM_LOG_DEBUG("Created variables for commands."); // Create scheduler variables for relevant states and their actions. std::pair>, uint_fast64_t> schedulerVariableResult = createSchedulerVariables(solver, stateInformation, choiceInformation); @@ -371,7 +372,7 @@ namespace storm { STORM_LOG_DEBUG("Created variables for nondeterministic choices."); // Create scheduler variables for nondeterministically choosing an initial state. - std::pair, uint_fast64_t> initialChoiceVariableResult = createInitialChoiceVariables(solver, labeledMdp, stateInformation); + std::pair, uint_fast64_t> initialChoiceVariableResult = createInitialChoiceVariables(solver, mdp, stateInformation); result.initialStateToChoiceVariableMap = std::move(initialChoiceVariableResult.first); result.numberOfVariables += initialChoiceVariableResult.second; STORM_LOG_DEBUG("Created variables for the nondeterministic choice of the initial state."); @@ -389,13 +390,13 @@ namespace storm { STORM_LOG_DEBUG("Created variables for the virtual initial state."); // Create variables for problematic states. - std::pair, uint_fast64_t> problematicStateVariableResult = createProblematicStateVariables(solver, labeledMdp, stateInformation, choiceInformation); + std::pair, uint_fast64_t> problematicStateVariableResult = createProblematicStateVariables(solver, mdp, stateInformation, choiceInformation); result.problematicStateToVariableMap = std::move(problematicStateVariableResult.first); result.numberOfVariables += problematicStateVariableResult.second; STORM_LOG_DEBUG("Created variables for the problematic states."); // Create variables for problematic choices. - std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> problematicTransitionVariableResult = createProblematicChoiceVariables(solver, labeledMdp, stateInformation, choiceInformation); + std::pair, storm::expressions::Variable, PairHash>, uint_fast64_t> problematicTransitionVariableResult = createProblematicChoiceVariables(solver, mdp, stateInformation, choiceInformation); result.problematicTransitionToVariableMap = problematicTransitionVariableResult.first; result.numberOfVariables += problematicTransitionVariableResult.second; STORM_LOG_DEBUG("Created variables for the problematic choices."); @@ -469,26 +470,25 @@ namespace storm { } /*! - * Asserts constraints that make sure the labels are included in the solution set if the policy selects a - * choice that is labeled with the label in question. + * Asserts constraints that make sure the commands are included in the solution set if the policy selects a + * choice that originates from the command in question. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertChoicesImplyLabels(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertChoicesImplyCommands(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); for (auto state : stateInformation.relevantStates) { std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { - for (auto label : choiceLabeling[choice]) { - storm::expressions::Expression constraint = variableInformation.labelToVariableMap.at(label) - *choiceVariableIterator >= solver.getConstant(0); - solver.addConstraint("ChoicesImplyLabels" + std::to_string(numberOfConstraintsCreated), constraint); + for (auto command : choiceOrigins.getCommandSet(choice)) { + storm::expressions::Expression constraint = variableInformation.commandToVariableMap.at(command) - *choiceVariableIterator >= solver.getConstant(0); + solver.addConstraint("ChoicesImplyCommands" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } ++choiceVariableIterator; @@ -524,14 +524,14 @@ namespace storm { * Asserts constraints that encode the correct reachability probabilities for all states. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param psiStates A bit vector characterizing the psi states in the model. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertReachabilityProbabilities(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); @@ -539,7 +539,7 @@ namespace storm { storm::expressions::Expression constraint = variableInformation.stateToProbabilityVariableMap.at(state); double rightHandSide = 1; - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(choice)) { if (stateInformation.relevantStates.get(successorEntry.getColumn())) { constraint = constraint - solver.getConstant(successorEntry.getValue()) * variableInformation.stateToProbabilityVariableMap.at(successorEntry.getColumn()); } else if (psiStates.get(successorEntry.getColumn())) { @@ -570,13 +570,13 @@ namespace storm { * Asserts constraints that make sure an unproblematic state is reachable from each problematic state. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertUnproblematicStateReachable(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; for (auto stateListPair : choiceInformation.problematicChoicesForProblematicStates) { @@ -590,7 +590,7 @@ namespace storm { } storm::expressions::Expression constraint = *choiceVariableIterator; - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(problematicChoice)) { constraint = constraint - variableInformation.problematicTransitionToVariableMap.at(std::make_pair(stateListPair.first, successorEntry.getColumn())); } constraint = constraint <= solver.getConstant(0); @@ -602,7 +602,7 @@ namespace storm { for (auto state : stateInformation.problematicStates) { for (auto problematicChoice : choiceInformation.problematicChoicesForProblematicStates.at(state)) { - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(problematicChoice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(problematicChoice)) { storm::expressions::Expression constraint = variableInformation.problematicStateToVariableMap.at(state); constraint = constraint - variableInformation.problematicStateToVariableMap.at(successorEntry.getColumn()); constraint = constraint + variableInformation.problematicTransitionToVariableMap.at(std::make_pair(state, successorEntry.getColumn())); @@ -617,19 +617,19 @@ namespace storm { } /* - * Asserts that labels that are on all paths from initial to target states are definitely taken. + * Asserts that commands that are on all paths from initial to target states are definitely taken. * * @param solver The MILP solver. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertKnownLabels(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static uint_fast64_t assertKnownCommands(storm::solver::LpSolver& solver, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { uint_fast64_t numberOfConstraintsCreated = 0; - for (auto label : choiceInformation.knownLabels) { - storm::expressions::Expression constraint = variableInformation.labelToVariableMap.at(label) == solver.getConstant(1); - solver.addConstraint("KnownLabels" + std::to_string(numberOfConstraintsCreated), constraint); + for (auto command : choiceInformation.knownCommands) { + storm::expressions::Expression constraint = variableInformation.commandToVariableMap.at(command) == solver.getConstant(1); + solver.addConstraint("KnownCommands" + std::to_string(numberOfConstraintsCreated), constraint); ++numberOfConstraintsCreated; } @@ -640,15 +640,15 @@ namespace storm { * Asserts constraints that rule out many suboptimal policies. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param psiStates A bit vector characterizing the psi states in the model. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. * @return The total number of constraints that were created. */ - static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + static uint_fast64_t assertSchedulerCuts(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { @@ -657,7 +657,7 @@ namespace storm { std::list::const_iterator choiceVariableIterator = variableInformation.stateToChoiceVariablesMap.at(state).begin(); for (auto choice : choiceInformation.relevantChoicesForRelevantStates.at(state)) { bool psiStateReachableInOneStep = false; - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(choice)) { if (psiStates.get(successorEntry.getColumn())) { psiStateReachableInOneStep = true; } @@ -665,7 +665,7 @@ namespace storm { if (!psiStateReachableInOneStep) { storm::expressions::Expression constraint = *choiceVariableIterator; - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(choice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(choice)) { if (state != successorEntry.getColumn() && stateInformation.relevantStates.get(successorEntry.getColumn())) { std::list const& successorChoiceVariableIndices = variableInformation.stateToChoiceVariablesMap.at(successorEntry.getColumn()); @@ -710,7 +710,7 @@ namespace storm { bool choiceTargetsCurrentState = false; // Check if the current choice targets the current state. - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(relevantChoice)) { if (state == successorEntry.getColumn()) { choiceTargetsCurrentState = true; break; @@ -727,7 +727,7 @@ namespace storm { // If the current state is an initial state and is selected as a successor state by the virtual // initial state, then this also justifies making a choice in the current state. - if (labeledMdp.getStates("init").get(state)) { + if (mdp.getStates("init").get(state)) { constraint = constraint - variableInformation.initialStateToChoiceVariableMap.at(state); } constraint = constraint <= solver.getConstant(0); @@ -738,7 +738,7 @@ namespace storm { // Assert that at least one initial state selects at least one action. storm::expressions::Expression constraint = solver.getConstant(0); - for (auto initialState : labeledMdp.getStates("init")) { + for (auto initialState : mdp.getStates("init")) { for (auto const& choiceVariable : variableInformation.stateToChoiceVariablesMap.at(initialState)) { constraint = constraint + choiceVariable; } @@ -770,7 +770,7 @@ namespace storm { bool choiceTargetsPsiState = false; // Check if the current choice targets the current state. - for (auto const& successorEntry : labeledMdp.getTransitionMatrix().getRow(relevantChoice)) { + for (auto const& successorEntry : mdp.getTransitionMatrix().getRow(relevantChoice)) { if (psiStates.get(successorEntry.getColumn())) { choiceTargetsPsiState = true; break; @@ -797,7 +797,7 @@ namespace storm { * the given threshold. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param psiStates A bit vector characterizing all psi states in the model. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. @@ -807,7 +807,7 @@ namespace storm { * @param includeSchedulerCuts If set to true, additional constraints are asserted that reduce the set of * possible choices. */ - static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { + static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, storm::storage::BitVector const& psiStates, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation, double probabilityThreshold, bool strictBound, bool includeSchedulerCuts = false) { // Assert that the reachability probability in the subsystem exceeds the given threshold. uint_fast64_t numberOfConstraints = assertProbabilityGreaterThanThreshold(solver, variableInformation, probabilityThreshold, strictBound); STORM_LOG_DEBUG("Asserted that reachability probability exceeds threshold."); @@ -816,9 +816,9 @@ namespace storm { numberOfConstraints += assertValidPolicy(solver, stateInformation, variableInformation); STORM_LOG_DEBUG("Asserted that policy is valid."); - // Add constraints that assert the labels that belong to some taken choices are taken as well. - numberOfConstraints += assertChoicesImplyLabels(solver, labeledMdp, stateInformation, choiceInformation, variableInformation); - STORM_LOG_DEBUG("Asserted that labels implied by choices are taken."); + // Add constraints that assert the commands that belong to some taken choices are taken as well. + numberOfConstraints += assertChoicesImplyCommands(solver, mdp, choiceOrigins, stateInformation, choiceInformation, variableInformation); + STORM_LOG_DEBUG("Asserted that commands implied by choices are taken."); // Add constraints that encode that the reachability probability from states which do not pick any action // is zero. @@ -826,20 +826,20 @@ namespace storm { STORM_LOG_DEBUG("Asserted that reachability probability is zero if no choice is taken."); // Add constraints that encode the reachability probabilities for states. - numberOfConstraints += assertReachabilityProbabilities(solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation); + numberOfConstraints += assertReachabilityProbabilities(solver, mdp, psiStates, stateInformation, choiceInformation, variableInformation); STORM_LOG_DEBUG("Asserted constraints for reachability probabilities."); // Add constraints that ensure the reachability of an unproblematic state from each problematic state. - numberOfConstraints += assertUnproblematicStateReachable(solver, labeledMdp, stateInformation, choiceInformation, variableInformation); + numberOfConstraints += assertUnproblematicStateReachable(solver, mdp, stateInformation, choiceInformation, variableInformation); STORM_LOG_DEBUG("Asserted that unproblematic state reachable from problematic states."); - // Add constraints that express that certain labels are already known to be taken. - numberOfConstraints += assertKnownLabels(solver, choiceInformation, variableInformation); - STORM_LOG_DEBUG("Asserted known labels are taken."); + // Add constraints that express that certain commands are already known to be taken. + numberOfConstraints += assertKnownCommands(solver, choiceInformation, variableInformation); + STORM_LOG_DEBUG("Asserted known commands are taken."); // If required, assert additional constraints that reduce the number of possible policies. if (includeSchedulerCuts) { - numberOfConstraints += assertSchedulerCuts(solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation); + numberOfConstraints += assertSchedulerCuts(solver, mdp, psiStates, stateInformation, choiceInformation, variableInformation); STORM_LOG_DEBUG("Asserted scheduler cuts."); } @@ -850,19 +850,19 @@ namespace storm { } /*! - * Computes the set of labels that was used in the given optimized model. + * Computes the set of commands that was used in the given optimized model. * * @param solver The MILP solver. * @param variableInformation A struct with information about the variables of the model. */ - static boost::container::flat_set getUsedLabelsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { + static boost::container::flat_set getUsedCommandsInSolution(storm::solver::LpSolver const& solver, VariableInformation const& variableInformation) { boost::container::flat_set result; - for (auto const& labelVariablePair : variableInformation.labelToVariableMap) { - bool labelTaken = solver.getBinaryValue(labelVariablePair.second); + for (auto const& commandVariablePair : variableInformation.commandToVariableMap) { + bool commandTaken = solver.getBinaryValue(commandVariablePair.second); - if (labelTaken) { - result.insert(labelVariablePair.first); + if (commandTaken) { + result.insert(commandVariablePair.first); } } return result; @@ -873,12 +873,12 @@ namespace storm { * it is selected by the subsystem computed by the solver. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param stateInformation The information about the states in the model. * @param choiceInformation The information about the choices in the model. * @param variableInformation A struct with information about the variables of the model. */ - static std::map getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& labeledMdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + static std::map getChoices(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { std::map result; for (auto state : stateInformation.relevantStates) { @@ -899,10 +899,10 @@ namespace storm { * Computes the reachability probability and the selected initial state in the given optimized MILP model. * * @param solver The MILP solver. - * @param labeledMdp The labeled MDP. + * @param mdp The MDP. * @param variableInformation A struct with information about the variables of the model. */ - static std::pair getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& labeledMdp, VariableInformation const& variableInformation) { + static std::pair getReachabilityProbability(storm::solver::LpSolver const& solver, storm::models::sparse::Mdp const& mdp, VariableInformation const& variableInformation) { uint_fast64_t selectedInitialState = 0; for (auto const& initialStateVariablePair : variableInformation.initialStateToChoiceVariableMap) { bool initialStateChosen = solver.getBinaryValue(initialStateVariablePair.second); @@ -917,18 +917,20 @@ namespace storm { } public: - static boost::container::flat_set getMinimalLabelSet(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { - // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabeling()) { - throw storm::exceptions::InvalidArgumentException() << "Minimal label set generation is impossible for unlabeled model."; - } + static boost::container::flat_set getMinimalCommandSet(storm::models::sparse::Mdp const& mdp, std::shared_ptr const& choiceOrigins, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeSchedulerCuts = false) { + // (0) Check whether there are choice origins available + STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origns."); + STORM_LOG_THROW(choiceOrigins->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + + storm::storage::sparse::PrismChoiceOrigins const& prismChoiceOrigins = choiceOrigins->asPrismChoiceOrigins(); + // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { storm::modelchecker::helper::SparseMdpPrctlHelper modelcheckerHelper; - std::vector result = std::move(modelcheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); - for (auto state : labeledMdp.getInitialStates()) { + std::vector result = std::move(modelcheckerHelper.computeUntilProbabilities(false, mdp.getTransitionMatrix(), mdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); + for (auto state : mdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); @@ -936,40 +938,41 @@ namespace storm { } // (2) Identify relevant and problematic states. - StateInformation stateInformation = determineRelevantAndProblematicStates(labeledMdp, phiStates, psiStates); + StateInformation stateInformation = determineRelevantAndProblematicStates(mdp, phiStates, psiStates); - // (3) Determine sets of relevant labels and problematic choices. - ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(labeledMdp, stateInformation, psiStates); + // (3) Determine sets of relevant commands and problematic choices. + ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, prismChoiceOrigins, stateInformation, psiStates); // (4) Encode resulting system as MILP problem. std::shared_ptr solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample"); // (4.1) Create variables. - VariableInformation variableInformation = createVariables(*solver, labeledMdp, stateInformation, choiceInformation); + VariableInformation variableInformation = createVariables(*solver, mdp, stateInformation, choiceInformation); // (4.2) Construct constraint system. - buildConstraintSystem(*solver, labeledMdp, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); + buildConstraintSystem(*solver, mdp, prismChoiceOrigins, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); // (4.3) Optimize the model. solver->optimize(); // (4.4) Read off result from variables. - boost::container::flat_set usedLabelSet = getUsedLabelsInSolution(*solver, variableInformation); - usedLabelSet.insert(choiceInformation.knownLabels.begin(), choiceInformation.knownLabels.end()); + boost::container::flat_set usedCommandSet = getUsedCommandsInSolution(*solver, variableInformation); + usedCommandSet.insert(choiceInformation.knownCommands.begin(), choiceInformation.knownCommands.end()); // (5) Return result. - return usedLabelSet; + return usedCommandSet; } /*! - * Computes a (minimally labeled) counterexample for the given model and (safety) formula. If the model satisfies the property, an exception is thrown. + * Computes a (minimal) counterexample with respect to the number of prism commands for the given model and (safety) formula. If the model satisfies the property, an exception is thrown. * - * @param labeledMdp A labeled MDP that is the model in which to generate the counterexample. + * @param mdp An MDP that is the model in which to generate the counterexample. + * @param choiceOrigins the choice origins generated for the mdp * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested * formula can be either an unbounded until formula or an eventually formula. */ - static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { - std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& choiceOrigins, std::shared_ptr const& formula) { + std::cout << std::endl << "Generating minimal command set counterexample for formula " << *formula << std::endl; STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); @@ -983,7 +986,7 @@ namespace storm { storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::SparsePropositionalModelChecker> modelchecker(labeledMdp); + storm::modelchecker::SparsePropositionalModelChecker> modelchecker(mdp); if (probabilityOperator.getSubformula().isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); @@ -1003,18 +1006,18 @@ namespace storm { storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); - phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); + phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true); psiStates = subQualitativeResult.getTruthValuesVector(); } // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedLabelSet = getMinimalLabelSet(labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); + boost::container::flat_set usedCommandSet = getMinimalCommandSet(mdp, choiceOrigins, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); - std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + std::cout << std::endl << "Computed minimal command set of size " << usedCommandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; std::cout << "Resulting program:" << std::endl; - storm::prism::Program restrictedProgram = program.restrictCommands(usedLabelSet); + storm::prism::Program restrictedProgram = program.restrictCommands(usedCommandSet); std::cout << restrictedProgram << std::endl; std::cout << std::endl << "-------------------------------------------" << std::endl; } diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h index 6359d04a6..3fde5bceb 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h @@ -8,6 +8,7 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" @@ -21,7 +22,7 @@ namespace storm { /*! * This class provides functionality to generate a minimal counterexample to a probabilistic reachability - * property in terms of used labels. + * property in terms of used commands. */ template class SMTMinimalCommandSetGenerator { @@ -31,11 +32,11 @@ namespace storm { // The set of relevant states in the model. storm::storage::BitVector relevantStates; - // The set of relevant labels. - boost::container::flat_set relevantLabels; + // The set of relevant commands. + boost::container::flat_set relevantCommands; - // A set of labels that is definitely known to be taken in the final solution. - boost::container::flat_set knownLabels; + // A set of commands that is definitely known to be taken in the final solution. + boost::container::flat_set knownCommands; // A list of relevant choices for each relevant state. std::map> relevantChoicesForRelevantStates; @@ -45,11 +46,11 @@ namespace storm { // The manager responsible for the constraints we are building. std::shared_ptr manager; - // The variables associated with the relevant labels. - std::vector labelVariables; + // The variables associated with the relevant commands. + std::vector commandVariables; - // A mapping from relevant labels to their indices in the variable vector. - std::map labelToIndexMap; + // A mapping from relevant commands to their indices in the variable vector. + std::map commandToIndexMap; // A set of original auxiliary variables needed for the Fu-Malik procedure. std::vector originalAuxiliaryVariables; @@ -80,21 +81,23 @@ namespace storm { }; /*! - * Computes the set of relevant labels in the model. Relevant labels are choice labels such that there exists + * Computes the set of relevant commands in the model. Relevant commands are choice origins such that there exists * a scheduler that satisfies phi until psi with a nonzero probability. * - * @param labeledMdp The MDP to search for relevant labels. + * @param mdp The MDP to search for relevant commands. + * @param choiceOrigins The choice origins of the mdp. * @param phiStates A bit vector representing all states that satisfy phi. * @param psiStates A bit vector representing all states that satisfy psi. - * @return A structure containing the relevant labels as well as states. + * @return A structure containing the relevant commands as well as states. */ - static RelevancyInformation determineRelevantStatesAndLabels(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + static RelevancyInformation determineRelevantStatesAndCommands(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { + // Create result. RelevancyInformation relevancyInformation; // Compute all relevant states, i.e. states for which there exists a scheduler that has a non-zero // probabilitiy of satisfying phi until psi. - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); relevancyInformation.relevantStates = storm::utility::graph::performProbGreater0E(backwardTransitions, phiStates, psiStates); relevancyInformation.relevantStates &= ~psiStates; @@ -102,12 +105,11 @@ namespace storm { STORM_LOG_DEBUG(relevancyInformation.relevantStates); // Retrieve some references for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); // Now traverse all choices of all relevant states and check whether there is a successor target state. - // If so, the associated labels become relevant. Also, if a choice of relevant state has at least one + // If so, the associated commands become relevant. Also, if a choice of relevant state has at least one // relevant successor, the choice becomes relevant. for (auto state : relevancyInformation.relevantStates) { relevancyInformation.relevantChoicesForRelevantStates.emplace(state, std::list()); @@ -116,10 +118,10 @@ namespace storm { bool currentChoiceRelevant = false; for (auto const& entry : transitionMatrix.getRow(row)) { - // If there is a relevant successor, we need to add the labels of the current choice. + // If there is a relevant successor, we need to add the commands of the current choice. if (relevancyInformation.relevantStates.get(entry.getColumn()) || psiStates.get(entry.getColumn())) { - for (auto const& label : choiceLabeling[row]) { - relevancyInformation.relevantLabels.insert(label); + for (auto const& command : choiceOrigins.getCommandSet(row)) { + relevancyInformation.relevantCommands.insert(command); } if (!currentChoiceRelevant) { currentChoiceRelevant = true; @@ -130,17 +132,17 @@ namespace storm { } } - // Compute the set of labels that are known to be taken in any case. - relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, relevancyInformation.relevantLabels); - if (!relevancyInformation.knownLabels.empty()) { - boost::container::flat_set remainingLabels; - std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); - relevancyInformation.relevantLabels = remainingLabels; + // Compute the set of commands that are known to be taken in any case. + relevancyInformation.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, choiceOrigins, psiStates, relevancyInformation.relevantCommands); + if (!relevancyInformation.knownCommands.empty()) { + boost::container::flat_set remainingCommands; + std::set_difference(relevancyInformation.relevantCommands.begin(), relevancyInformation.relevantCommands.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(remainingCommands, remainingCommands.end())); + relevancyInformation.relevantCommands = remainingCommands; } - std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels." << std::endl; + std::cout << "Found " << relevancyInformation.relevantCommands.size() << " relevant and " << relevancyInformation.knownCommands.size() << " known commands." << std::endl; - STORM_LOG_DEBUG("Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."); + STORM_LOG_DEBUG("Found " << relevancyInformation.relevantCommands.size() << " relevant and " << relevancyInformation.knownCommands.size() << " known commands."); return relevancyInformation; } @@ -148,31 +150,31 @@ namespace storm { * Creates all necessary variables. * * @param manager The manager in which to create the variables. - * @param relevantCommands A set of relevant labels for which to create the expressions. - * @return A mapping from relevant labels to their corresponding expressions. + * @param relevantCommands A set of relevant commands for which to create the expressions. + * @return A mapping from relevant commands to their corresponding expressions. */ - static VariableInformation createVariables(std::shared_ptr const& manager, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, RelevancyInformation const& relevancyInformation, bool createReachabilityVariables) { + static VariableInformation createVariables(std::shared_ptr const& manager, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, RelevancyInformation const& relevancyInformation, bool createReachabilityVariables) { VariableInformation variableInformation; variableInformation.manager = manager; // Create stringstream to build expression names. std::stringstream variableName; - // Create the variables for the relevant labels. - for (auto label : relevancyInformation.relevantLabels) { - variableInformation.labelToIndexMap[label] = variableInformation.labelVariables.size(); + // Create the variables for the relevant commands. + for (auto command : relevancyInformation.relevantCommands) { + variableInformation.commandToIndexMap[command] = variableInformation.commandVariables.size(); // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); - variableName << "c" << label; + variableName << "c" << command; - variableInformation.labelVariables.push_back(manager->declareBooleanVariable(variableName.str())); + variableInformation.commandVariables.push_back(manager->declareBooleanVariable(variableName.str())); // Clear contents of the stream to construct new expression name. variableName.clear(); variableName.str(""); - variableName << "h" << label; + variableName << "h" << command; variableInformation.originalAuxiliaryVariables.push_back(manager->declareBooleanVariable(variableName.str())); } @@ -188,7 +190,7 @@ namespace storm { if (createReachabilityVariables) { variableInformation.hasReachabilityVariables = true; - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); for (auto state : relevancyInformation.relevantStates) { variableInformation.relevantStatesToOrderVariableIndexMap[state] = variableInformation.stateOrderVariables.size(); @@ -245,16 +247,16 @@ namespace storm { * Asserts the constraints that are initially needed for the Fu-Malik procedure. * * @param program The program for which to build the constraints. - * @param labeledMdp The MDP that results from the given program. + * @param mdp The MDP that results from the given program. * @param context The Z3 context in which to build the expressions. * @param solver The solver in which to assert the constraints. - * @param variableInformation A structure with information about the variables for the labels. + * @param variableInformation A structure with information about the variables for the commands. */ - static void assertFuMalikInitialConstraints(storm::prism::Program const& program, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, z3::context& context, z3::solver& solver, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { - // Assert that at least one of the labels must be taken. - z3::expr formula = variableInformation.labelVariables.at(0); - for (uint_fast64_t index = 1; index < variableInformation.labelVariables.size(); ++index) { - formula = formula || variableInformation.labelVariables.at(index); + static void assertFuMalikInitialConstraints(storm::prism::Program const& program, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, z3::context& context, z3::solver& solver, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation) { + // Assert that at least one of the commands must be taken. + z3::expr formula = variableInformation.commandVariables.at(0); + for (uint_fast64_t index = 1; index < variableInformation.commandVariables.size(); ++index) { + formula = formula || variableInformation.commandVariables.at(index); } solver.add(formula); } @@ -263,68 +265,68 @@ namespace storm { * Asserts cuts that are derived from the explicit representation of the model and rule out a lot of * suboptimal solutions. * - * @param labeledMdp The labeled MDP for which to compute the cuts. + * @param mdp The MDP for which to compute the cuts. * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertExplicitCuts(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertExplicitCuts(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { // Walk through the MDP and - // * identify labels enabled in initial states - // * identify labels that can directly precede a given action - // * identify labels that directly reach a target state - // * identify labels that can directly follow a given action + // * identify commands enabled in initial states + // * identify commands that can directly precede a given action + // * identify commands that directly reach a target state + // * identify commands that can directly follow a given action - boost::container::flat_set initialLabels; + boost::container::flat_set initialCommands; std::set> initialCombinations; - std::map> precedingLabels; - boost::container::flat_set targetLabels; + std::map> precedingCommands; + boost::container::flat_set targetCommands; boost::container::flat_set> targetCombinations; - std::map, std::set>> followingLabels; - std::map>> synchronizingLabels; + std::map, std::set>> followingCommands; + std::map>> synchronizingCommands; // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - storm::storage::BitVector const& initialStates = labeledMdp.getInitialStates(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + storm::storage::BitVector const& initialStates = mdp.getInitialStates(); + storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { + boost::container::flat_set const& commandsOfCurrentChoice = choiceOrigins.getCommandSet(currentChoice); // If the choice is a synchronization choice, we need to record it. - if (choiceLabeling[currentChoice].size() > 1) { - for (auto label : choiceLabeling[currentChoice]) { - synchronizingLabels[label].emplace(choiceLabeling[currentChoice]); + if (commandsOfCurrentChoice.size() > 1) { + for (auto command : commandsOfCurrentChoice) { + synchronizingCommands[command].emplace(commandsOfCurrentChoice); } } - // If the state is initial, we need to add all the choice labels to the initial label set. + // If the state is initial, we need to add all the choice commands to the initial command set. if (initialStates.get(currentState)) { - initialLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); - initialCombinations.insert(choiceLabeling[currentChoice]); + initialCommands.insert(commandsOfCurrentChoice.begin(), commandsOfCurrentChoice.end()); + initialCombinations.insert(commandsOfCurrentChoice); } - // Iterate over successors and add relevant choices of relevant successors to the following label set. + // Iterate over successors and add relevant choices of relevant successors to the following command set. bool canReachTargetState = false; for (auto const& entry : transitionMatrix.getRow(currentChoice)) { if (relevancyInformation.relevantStates.get(entry.getColumn())) { for (auto relevantChoice : relevancyInformation.relevantChoicesForRelevantStates.at(entry.getColumn())) { - followingLabels[choiceLabeling[currentChoice]].insert(choiceLabeling[relevantChoice]); + followingCommands[commandsOfCurrentChoice].insert(choiceOrigins.getCommandSet(relevantChoice)); } } else if (psiStates.get(entry.getColumn())) { canReachTargetState = true; } } - // If the choice can reach a target state directly, we add all the labels to the target label set. + // If the choice can reach a target state directly, we add all the commands to the target command set. if (canReachTargetState) { - targetLabels.insert(choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end()); - targetCombinations.insert(choiceLabeling[currentChoice]); + targetCommands.insert(commandsOfCurrentChoice.begin(), commandsOfCurrentChoice.end()); + targetCombinations.insert(commandsOfCurrentChoice); } } // Iterate over predecessors and add all choices that target the current state to the preceding - // label set of all labels of all relevant choices of the current state. + // command set of all commands of all relevant choices of the current state. for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) { @@ -337,9 +339,9 @@ namespace storm { if (choiceTargetsCurrentState) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { - for (auto labelToAdd : choiceLabeling[predecessorChoice]) { - for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) { - precedingLabels[labelForWhichToAdd].insert(labelToAdd); + for (auto commandToAdd : choiceOrigins.getCommandSet(predecessorChoice)) { + for (auto commandForWhichToAdd : choiceOrigins.getCommandSet(currentChoice)) { + precedingCommands[commandForWhichToAdd].insert(commandToAdd); } } } @@ -355,19 +357,19 @@ namespace storm { { std::vector formulae; - // Start by asserting that we take at least one initial label. We may do so only if there is no initial + // Start by asserting that we take at least one initial command. We may do so only if there is no initial // combination that is already known. Otherwise this condition would be too strong. bool initialCombinationKnown = false; for (auto const& combination : initialCombinations) { boost::container::flat_set tmpSet; - std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); if (tmpSet.size() == 0) { initialCombinationKnown = true; break; } else { storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto label : tmpSet) { - conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : tmpSet) { + conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } formulae.push_back(conj); } @@ -385,14 +387,14 @@ namespace storm { bool targetCombinationKnown = false; for (auto const& combination : targetCombinations) { boost::container::flat_set tmpSet; - std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(combination.begin(), combination.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); if (tmpSet.size() == 0) { targetCombinationKnown = true; break; } else { storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto label : tmpSet) { - conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : tmpSet) { + conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } formulae.push_back(conj); } @@ -402,94 +404,94 @@ namespace storm { } } - // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor. + // Compute the sets of commands such that the transitions originating from this set possess at least one known successor. boost::container::flat_set> hasKnownSuccessor; - for (auto const& labelSetFollowingSetsPair : followingLabels) { - for (auto const& set : labelSetFollowingSetsPair.second) { - if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { + for (auto const& commandSetFollowingSetsPair : followingCommands) { + for (auto const& set : commandSetFollowingSetsPair.second) { + if (std::includes(relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), set.begin(), set.end())) { hasKnownSuccessor.insert(set); break; } } } - STORM_LOG_DEBUG("Asserting taken labels are followed by another label if they are not a target label."); - // Now assert that for each non-target label, we take a following label. - for (auto const& labelSetFollowingSetsPair : followingLabels) { + STORM_LOG_DEBUG("Asserting taken commands are followed by another command if they are not a target command."); + // Now assert that for each non-target command, we take a following command. + for (auto const& commandSetFollowingSetsPair : followingCommands) { std::vector formulae; // Only build a constraint if the combination does not lead to a target state and // no successor set is already known. - if (targetCombinations.find(labelSetFollowingSetsPair.first) == targetCombinations.end() && hasKnownSuccessor.find(labelSetFollowingSetsPair.first) == hasKnownSuccessor.end()) { + if (targetCombinations.find(commandSetFollowingSetsPair.first) == targetCombinations.end() && hasKnownSuccessor.find(commandSetFollowingSetsPair.first) == hasKnownSuccessor.end()) { - // Compute the set of unknown labels on the left-hand side of the implication. - boost::container::flat_set unknownLhsLabels; - std::set_difference(labelSetFollowingSetsPair.first.begin(), labelSetFollowingSetsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); - for (auto label : unknownLhsLabels) { - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + // Compute the set of unknown commands on the left-hand side of the implication. + boost::container::flat_set unknownLhsCommands; + std::set_difference(commandSetFollowingSetsPair.first.begin(), commandSetFollowingSetsPair.first.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownLhsCommands, unknownLhsCommands.end())); + for (auto command : unknownLhsCommands) { + formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); } - for (auto const& followingSet : labelSetFollowingSetsPair.second) { + for (auto const& followingSet : commandSetFollowingSetsPair.second) { boost::container::flat_set tmpSet; - // Check which labels of the current following set are not known. This set must be non-empty, because + // Check which commands of the current following set are not known. This set must be non-empty, because // otherwise a successor combination would already be known and control cannot reach this point. - std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); - // Construct an expression that enables all unknown labels of the current following set. + // Construct an expression that enables all unknown commands of the current following set. storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto label : tmpSet) { - conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : tmpSet) { + conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } formulae.push_back(conj); } - if (labelSetFollowingSetsPair.first.size() > 1) { - // Taking all commands of a combination does not necessarily mean that a following label set needs to be taken. + if (commandSetFollowingSetsPair.first.size() > 1) { + // Taking all commands of a combination does not necessarily mean that a following command set needs to be taken. // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need // to add an additional clause that says that the right-hand side of the implication is also true if all commands // of the current choice have enabled synchronization options. storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false); - for (auto label : labelSetFollowingSetsPair.first) { - storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); - std::set> const& synchsForCommand = synchronizingLabels.at(label); + for (auto command : commandSetFollowingSetsPair.first) { + storm::expressions::Expression alternativeExpressionForCommand = variableInformation.manager->boolean(false); + std::set> const& synchsForCommand = synchronizingCommands.at(command); for (auto const& synchSet : synchsForCommand) { storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true); // If the current synchSet is the same as left-hand side of the implication, we need to skip it. - if (synchSet == labelSetFollowingSetsPair.first) continue; + if (synchSet == commandSetFollowingSetsPair.first) continue; - // Now that we have the labels that are unknown and "missing", we still need to check whether this other + // Now that we have the commands that are unknown and "missing", we still need to check whether this other // synchronizing set already has a known successor or leads directly to a target state. if (hasKnownSuccessor.find(synchSet) == hasKnownSuccessor.end() && targetCombinations.find(synchSet) == targetCombinations.end()) { // If not, we can assert that we take one of its possible successors. boost::container::flat_set unknownSynchs; - std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end())); - unknownSynchs.erase(label); + std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownSynchs, unknownSynchs.end())); + unknownSynchs.erase(command); - for (auto label : unknownSynchs) { - alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : unknownSynchs) { + alternativeExpression = alternativeExpression && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } storm::expressions::Expression disjunctionOverSuccessors = variableInformation.manager->boolean(false); - for (auto successorSet : followingLabels.at(synchSet)) { - storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true); - for (auto label : successorSet) { - if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { - conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto successorSet : followingCommands.at(synchSet)) { + storm::expressions::Expression conjunctionOverCommands = variableInformation.manager->boolean(true); + for (auto command : successorSet) { + if (relevancyInformation.knownCommands.find(command) == relevancyInformation.knownCommands.end()) { + conjunctionOverCommands = conjunctionOverCommands && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } } - disjunctionOverSuccessors = disjunctionOverSuccessors || conjunctionOverLabels; + disjunctionOverSuccessors = disjunctionOverSuccessors || conjunctionOverCommands; } alternativeExpression = alternativeExpression && disjunctionOverSuccessors; } - alternativeExpressionForLabel = alternativeExpressionForLabel || alternativeExpression; + alternativeExpressionForCommand = alternativeExpressionForCommand || alternativeExpression; } - finalDisjunct = finalDisjunct && alternativeExpressionForLabel; + finalDisjunct = finalDisjunct && alternativeExpressionForCommand; } formulae.push_back(finalDisjunct); @@ -502,24 +504,24 @@ namespace storm { } STORM_LOG_DEBUG("Asserting synchronization cuts."); - // Finally, assert that if we take one of the synchronizing labels, we also take one of the combinations - // the label appears in. - for (auto const& labelSynchronizingSetsPair : synchronizingLabels) { + // Finally, assert that if we take one of the synchronizing commands, we also take one of the combinations + // the command appears in. + for (auto const& commandSynchronizingSetsPair : synchronizingCommands) { std::vector formulae; - if (relevancyInformation.knownLabels.find(labelSynchronizingSetsPair.first) == relevancyInformation.knownLabels.end()) { - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelSynchronizingSetsPair.first))); + if (relevancyInformation.knownCommands.find(commandSynchronizingSetsPair.first) == relevancyInformation.knownCommands.end()) { + formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(commandSynchronizingSetsPair.first))); } - // We need to be careful, because there may be one synchronisation set out of which all labels are + // We need to be careful, because there may be one synchronisation set out of which all commands are // known, which means we must not assert anything. bool allImplicantsKnownForOneSet = false; - for (auto const& synchronizingSet : labelSynchronizingSetsPair.second) { + for (auto const& synchronizingSet : commandSynchronizingSetsPair.second) { storm::expressions::Expression currentCombination = variableInformation.manager->boolean(true); bool allImplicantsKnownForCurrentSet = true; - for (auto label : synchronizingSet) { - if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end() && label != labelSynchronizingSetsPair.first) { - currentCombination = currentCombination && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : synchronizingSet) { + if (relevancyInformation.knownCommands.find(command) == relevancyInformation.knownCommands.end() && command != commandSynchronizingSetsPair.first) { + currentCombination = currentCombination && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } } formulae.push_back(currentCombination); @@ -544,31 +546,31 @@ namespace storm { * @param program The symbolic representation of the model in terms of a program. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Mdp const& labeledMdp, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { - // A container storing the label sets that may precede a given label set. - std::map, std::set>> precedingLabelSets; + static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + // A container storing the command sets that may precede a given command set. + std::map, std::set>> precedingCommandSets; - // A container that maps labels to their reachable synchronization sets. - std::map>> synchronizingLabels; + // A container that maps commands to their reachable synchronization sets. + std::map>> synchronizingCommands; // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); - // Compute the set of labels that may precede a given action. + // Compute the set of commands that may precede a given action. for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { + boost::container::flat_set const& commandsOfCurrentChoice = choiceOrigins.getCommandSet(currentChoice); // If the choice is a synchronization choice, we need to record it. - if (choiceLabeling[currentChoice].size() > 1) { - for (auto label : choiceLabeling[currentChoice]) { - synchronizingLabels[label].emplace(choiceLabeling[currentChoice]); + if (commandsOfCurrentChoice.size() > 1) { + for (auto command : commandsOfCurrentChoice) { + synchronizingCommands[command].emplace(commandsOfCurrentChoice); } } // Iterate over predecessors and add all choices that target the current state to the preceding - // label set of all labels of all relevant choices of the current state. + // command set of all commands of all relevant choices of the current state. for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { if (relevancyInformation.relevantStates.get(predecessorEntry.getColumn())) { for (auto predecessorChoice : relevancyInformation.relevantChoicesForRelevantStates.at(predecessorEntry.getColumn())) { @@ -580,7 +582,7 @@ namespace storm { } if (choiceTargetsCurrentState) { - precedingLabelSets[choiceLabeling.at(currentChoice)].insert(choiceLabeling.at(predecessorChoice)); + precedingCommandSets[commandsOfCurrentChoice].insert(choiceOrigins.getCommandSet(predecessorChoice)); } } } @@ -630,13 +632,13 @@ namespace storm { // Construct an expression that exactly characterizes the initial state. storm::expressions::Expression initialStateExpression = program.getInitialStatesExpression(); - // Store the found implications in a container similar to the preceding label sets. + // Store the found implications in a container similar to the preceding command sets. std::map, std::set>> backwardImplications; // Now check for possible backward cuts. - for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) { + for (auto const& commandSetAndPrecedingCommandSetsPair : precedingCommandSets) { - // Find out the commands for the currently considered label set. + // Find out the commands for the currently considered command set. std::vector> currentCommandVector; for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { storm::prism::Module const& module = program.getModule(moduleIndex); @@ -645,7 +647,7 @@ namespace storm { storm::prism::Command const& command = module.getCommand(commandIndex); // If the current command is one of the commands we need to consider, store a reference to it in the container. - if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) { + if (commandSetAndPrecedingCommandSetsPair.first.find(command.getGlobalIndex()) != commandSetAndPrecedingCommandSetsPair.first.end()) { currentCommandVector.push_back(command); } } @@ -683,8 +685,8 @@ namespace storm { ++setIterator; } } else { - throw storm::exceptions::InvalidStateException() << "Choice label set is empty."; - STORM_LOG_DEBUG("Choice label set is empty."); + throw storm::exceptions::InvalidStateException() << "Choice command set is empty."; + STORM_LOG_DEBUG("Choice command set is empty."); } STORM_LOG_DEBUG("About to assert disjunction of negated guards."); @@ -700,12 +702,12 @@ namespace storm { localSolver->add(guardExpression); STORM_LOG_DEBUG("Asserted disjunction of negated guards."); - // Now check the possible preceding label sets for the essential ones. - for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) { + // Now check the possible preceding command sets for the essential ones. + for (auto const& precedingCommandSet : commandSetAndPrecedingCommandSetsPair.second) { // Create a restore point so we can easily pop-off all weakest precondition expressions. localSolver->push(); - // Find out the commands for the currently considered preceding label set. + // Find out the commands for the currently considered preceding command set. std::vector> currentPrecedingCommandVector; for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { storm::prism::Module const& module = program.getModule(moduleIndex); @@ -714,7 +716,7 @@ namespace storm { storm::prism::Command const& command = module.getCommand(commandIndex); // If the current command is one of the commands we need to consider, store a reference to it in the container. - if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) { + if (precedingCommandSet.find(command.getGlobalIndex()) != precedingCommandSet.end()) { currentPrecedingCommandVector.push_back(command); } } @@ -770,7 +772,7 @@ namespace storm { STORM_LOG_DEBUG("Asserted disjunction of all weakest preconditions."); if (localSolver->check() == storm::solver::SmtSolver::CheckResult::Sat) { - backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet); + backwardImplications[commandSetAndPrecedingCommandSetsPair.first].insert(precedingCommandSet); } localSolver->pop(); @@ -781,96 +783,96 @@ namespace storm { } } - // Compute the sets of labels such that the transitions labeled with this set possess at least one known successor. + // Compute the sets of commands such that the transitions originating from this set possess at least one known successor. boost::container::flat_set> hasKnownPredecessor; - for (auto const& labelSetImplicationsPair : backwardImplications) { - for (auto const& set : labelSetImplicationsPair.second) { - if (std::includes(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), set.begin(), set.end())) { + for (auto const& commandSetImplicationsPair : backwardImplications) { + for (auto const& set : commandSetImplicationsPair.second) { + if (std::includes(relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), set.begin(), set.end())) { hasKnownPredecessor.insert(set); break; } } } - STORM_LOG_DEBUG("Asserting taken labels are preceded by another label if they are not an initial label."); - // Now assert that for each non-target label, we take a following label. - for (auto const& labelSetImplicationsPair : backwardImplications) { + STORM_LOG_DEBUG("Asserting taken commands are preceded by another command if they are not an initial command."); + // Now assert that for each non-target command, we take a following command. + for (auto const& commandSetImplicationsPair : backwardImplications) { std::vector formulae; // Only build a constraint if the combination no predecessor set is already known. - if (hasKnownPredecessor.find(labelSetImplicationsPair.first) == hasKnownPredecessor.end()) { + if (hasKnownPredecessor.find(commandSetImplicationsPair.first) == hasKnownPredecessor.end()) { - // Compute the set of unknown labels on the left-hand side of the implication. - boost::container::flat_set unknownLhsLabels; - std::set_difference(labelSetImplicationsPair.first.begin(), labelSetImplicationsPair.first.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); - for (auto label : unknownLhsLabels) { - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + // Compute the set of unknown commands on the left-hand side of the implication. + boost::container::flat_set unknownLhsCommands; + std::set_difference(commandSetImplicationsPair.first.begin(), commandSetImplicationsPair.first.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownLhsCommands, unknownLhsCommands.end())); + for (auto command : unknownLhsCommands) { + formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); } - for (auto const& precedingSet : labelSetImplicationsPair.second) { + for (auto const& precedingSet : commandSetImplicationsPair.second) { boost::container::flat_set tmpSet; - // Check which labels of the current following set are not known. This set must be non-empty, because + // Check which commands of the current following set are not known. This set must be non-empty, because // otherwise a predecessor combination would already be known and control cannot reach this point. - std::set_difference(precedingSet.begin(), precedingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + std::set_difference(precedingSet.begin(), precedingSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(tmpSet, tmpSet.end())); - // Construct an expression that enables all unknown labels of the current following set. + // Construct an expression that enables all unknown commands of the current following set. storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto label : tmpSet) { - conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : tmpSet) { + conj = conj && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } formulae.push_back(conj); } - if (labelSetImplicationsPair.first.size() > 1) { - // Taking all commands of a combination does not necessarily mean that a predecessor label set needs to be taken. + if (commandSetImplicationsPair.first.size() > 1) { + // Taking all commands of a combination does not necessarily mean that a predecessor command set needs to be taken. // This is because it could be that the commands are taken to enable other synchronizations. Therefore, we need // to add an additional clause that says that the right-hand side of the implication is also true if all commands // of the current choice have enabled synchronization options. storm::expressions::Expression finalDisjunct = variableInformation.manager->boolean(false); - for (auto label : labelSetImplicationsPair.first) { - storm::expressions::Expression alternativeExpressionForLabel = variableInformation.manager->boolean(false); - std::set> const& synchsForCommand = synchronizingLabels.at(label); + for (auto command : commandSetImplicationsPair.first) { + storm::expressions::Expression alternativeExpressionForCommand = variableInformation.manager->boolean(false); + std::set> const& synchsForCommand = synchronizingCommands.at(command); for (auto const& synchSet : synchsForCommand) { storm::expressions::Expression alternativeExpression = variableInformation.manager->boolean(true); // If the current synchSet is the same as left-hand side of the implication, we need to skip it. - if (synchSet == labelSetImplicationsPair.first) continue; + if (synchSet == commandSetImplicationsPair.first) continue; - // Now that we have the labels that are unknown and "missing", we still need to check whether this other + // Now that we have the commands that are unknown and "missing", we still need to check whether this other // synchronizing set already has a known predecessor. if (hasKnownPredecessor.find(synchSet) == hasKnownPredecessor.end()) { // If not, we can assert that we take one of its possible predecessors. boost::container::flat_set unknownSynchs; - std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownSynchs, unknownSynchs.end())); - unknownSynchs.erase(label); + std::set_difference(synchSet.begin(), synchSet.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownSynchs, unknownSynchs.end())); + unknownSynchs.erase(command); - for (auto label : unknownSynchs) { - alternativeExpression = alternativeExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto command : unknownSynchs) { + alternativeExpression = alternativeExpression && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } storm::expressions::Expression disjunctionOverPredecessors = variableInformation.manager->boolean(false); - auto precedingLabelSetsIterator = precedingLabelSets.find(synchSet); - if (precedingLabelSetsIterator != precedingLabelSets.end()) { - for (auto precedingSet : precedingLabelSetsIterator->second) { - storm::expressions::Expression conjunctionOverLabels = variableInformation.manager->boolean(true); - for (auto label : precedingSet) { - if (relevancyInformation.knownLabels.find(label) == relevancyInformation.knownLabels.end()) { - conjunctionOverLabels = conjunctionOverLabels && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + auto precedingCommandSetsIterator = precedingCommandSets.find(synchSet); + if (precedingCommandSetsIterator != precedingCommandSets.end()) { + for (auto precedingSet : precedingCommandSetsIterator->second) { + storm::expressions::Expression conjunctionOverCommands = variableInformation.manager->boolean(true); + for (auto command : precedingSet) { + if (relevancyInformation.knownCommands.find(command) == relevancyInformation.knownCommands.end()) { + conjunctionOverCommands = conjunctionOverCommands && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command)); } } - disjunctionOverPredecessors = disjunctionOverPredecessors || conjunctionOverLabels; + disjunctionOverPredecessors = disjunctionOverPredecessors || conjunctionOverCommands; } } alternativeExpression = alternativeExpression && disjunctionOverPredecessors; } - alternativeExpressionForLabel = alternativeExpressionForLabel || alternativeExpression; + alternativeExpressionForCommand = alternativeExpressionForCommand || alternativeExpression; } - finalDisjunct = finalDisjunct && alternativeExpressionForLabel; + finalDisjunct = finalDisjunct && alternativeExpressionForCommand; } formulae.push_back(finalDisjunct); @@ -886,23 +888,22 @@ namespace storm { /*! * Asserts constraints necessary to encode the reachability of at least one target state from the initial states. */ - static void assertReachabilityCuts(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertReachabilityCuts(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { if (!variableInformation.hasReachabilityVariables) { throw storm::exceptions::InvalidStateException() << "Impossible to assert reachability cuts without the necessary variables."; } // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); // First, we add the formulas that encode // (1) if an incoming transition is chosen, an outgoing one is chosen as well (for non-initial states) // (2) an outgoing transition out of the initial states is taken. storm::expressions::Expression initialStateExpression = variableInformation.manager->boolean(false); for (auto relevantState : relevancyInformation.relevantStates) { - if (!labeledMdp.getInitialStates().get(relevantState)) { + if (!mdp.getInitialStates().get(relevantState)) { // Assert the constraints (1). boost::container::flat_set relevantPredecessors; for (auto const& predecessorEntry : backwardTransitions.getRow(relevantState)) { @@ -963,17 +964,17 @@ namespace storm { } } } - storm::expressions::Expression labelExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second); + storm::expressions::Expression commandExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second); for (auto choice : choicesForStatePair) { storm::expressions::Expression choiceExpression = variableInformation.manager->boolean(true); - for (auto element : choiceLabeling.at(choice)) { - if (relevancyInformation.knownLabels.find(element) == relevancyInformation.knownLabels.end()) { - choiceExpression = choiceExpression && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(element)); + for (auto element : choiceOrigins.getCommandSet(choice)) { + if (relevancyInformation.knownCommands.find(element) == relevancyInformation.knownCommands.end()) { + choiceExpression = choiceExpression && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(element)); } } - labelExpression = labelExpression || choiceExpression; + commandExpression = commandExpression || choiceExpression; } - solver.add(labelExpression); + solver.add(commandExpression); // Assert constraint for (2). storm::expressions::Expression orderExpression = !variableInformation.statePairVariables.at(statePairIndexPair.second) || variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(sourceState)).getExpression() < variableInformation.stateOrderVariables.at(variableInformation.relevantStatesToOrderVariableIndexMap.at(targetState)).getExpression(); @@ -1198,7 +1199,7 @@ namespace storm { * * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. - * @param variableInformation A structure with information about the variables for the labels. + * @param variableInformation A structure with information about the variables for the commands. * @return True iff the constraint system was satisfiable. */ static bool fuMalikMaxsatStep(z3::context& context, z3::solver& solver, std::vector& auxiliaryVariables, std::vector& softConstraints, uint_fast64_t& nextFreeVariableIndex) { @@ -1263,13 +1264,13 @@ namespace storm { * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. * @param commandSet The command set to rule out as a solution. - * @param variableInformation A structure with information about the variables for the labels. + * @param variableInformation A structure with information about the variables for the commands. */ static void ruleOutSolution(z3::context& context, z3::solver& solver, boost::container::flat_set const& commandSet, VariableInformation const& variableInformation) { z3::expr blockSolutionExpression = context.bool_val(false); - for (auto labelIndexPair : variableInformation.labelToIndexMap) { - if (commandSet.find(labelIndexPair.first) != commandSet.end()) { - blockSolutionExpression = blockSolutionExpression || variableInformation.labelVariables[labelIndexPair.second]; + for (auto commandIndexPair : variableInformation.commandToIndexMap) { + if (commandSet.find(commandIndexPair.first) != commandSet.end()) { + blockSolutionExpression = blockSolutionExpression || variableInformation.commandVariables[commandIndexPair.second]; } } @@ -1277,18 +1278,18 @@ namespace storm { } /*! - * Determines the set of labels that was chosen by the given model. + * Determines the set of commands that was chosen by the given model. * * @param model The model from which to extract the information. * @param variableInformation A structure with information about the variables of the solver. */ - static boost::container::flat_set getUsedLabelSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { + static boost::container::flat_set getUsedCommandSet(storm::solver::SmtSolver::ModelReference const& model, VariableInformation const& variableInformation) { boost::container::flat_set result; - for (auto const& labelIndexPair : variableInformation.labelToIndexMap) { - bool commandIncluded = model.getBooleanValue(variableInformation.labelVariables.at(labelIndexPair.second)); + for (auto const& commandIndexPair : variableInformation.commandToIndexMap) { + bool commandIncluded = model.getBooleanValue(variableInformation.commandVariables.at(commandIndexPair.second)); if (commandIncluded) { - result.insert(labelIndexPair.first); + result.insert(commandIndexPair.first); } } return result; @@ -1305,7 +1306,7 @@ namespace storm { std::stringstream variableName; std::vector result; - std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.labelVariables); + std::vector adderVariables = createCounterCircuit(variableInformation, variableInformation.commandVariables); for (uint_fast64_t i = 0; i < adderVariables.size(); ++i) { variableName.str(""); variableName.clear(); @@ -1318,13 +1319,13 @@ namespace storm { } /*! - * Finds the smallest set of labels such that the constraint system of the solver is still satisfiable. + * Finds the smallest set of commands such that the constraint system of the solver is still satisfiable. * * @param solver The solver to use for the satisfiability evaluation. * @param variableInformation A structure with information about the variables of the solver. - * @param currentBound The currently known lower bound for the number of labels that need to be enabled + * @param currentBound The currently known lower bound for the number of commands that need to be enabled * in order to satisfy the constraint system. - * @return The smallest set of labels such that the constraint system of the solver is satisfiable. + * @return The smallest set of commands such that the constraint system of the solver is satisfiable. */ static boost::container::flat_set findSmallestCommandSet(storm::solver::SmtSolver& solver, VariableInformation& variableInformation, uint_fast64_t& currentBound) { // Check if we can find a solution with the current bound. @@ -1339,9 +1340,9 @@ namespace storm { assumption = !variableInformation.auxiliaryVariables.back(); } - // At this point we know that the constraint system was satisfiable, so compute the induced label + // At this point we know that the constraint system was satisfiable, so compute the induced command // set and return it. - return getUsedLabelSet(*solver.getModel(), variableInformation); + return getUsedCommandSet(*solver.getModel(), variableInformation); } /*! @@ -1355,7 +1356,7 @@ namespace storm { * @param commandSet The currently chosen set of commands. * @param variableInformation A structure with information about the variables of the solver. */ - static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, storm::models::sparse::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeZeroProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, storm::storage::sparse::PrismChoiceOrigins const& subChoiceOrigins, storm::models::sparse::Mdp const& originalMdp, storm::storage::sparse::PrismChoiceOrigins const& originalChoiceOrigins, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); STORM_LOG_DEBUG("Analyzing solution with zero probability."); @@ -1371,10 +1372,9 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); - std::vector> const& subChoiceLabeling = subMdp.getChoiceLabeling(); - // Now determine which states and labels are actually reachable. - boost::container::flat_set reachableLabels; + // Now determine which states and commands are actually reachable. + boost::container::flat_set reachableCommands; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1395,8 +1395,8 @@ namespace storm { } if (choiceTargetsRelevantState) { - for (auto label : subChoiceLabeling[currentChoice]) { - reachableLabels.insert(label); + for (auto command : subChoiceOrigins.getCommandSet(currentChoice)) { + reachableCommands.insert(command); } } } @@ -1412,19 +1412,18 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); - boost::container::flat_set locallyRelevantLabels; - std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); + boost::container::flat_set locallyRelevantCommands; + std::set_difference(relevancyInformation.relevantCommands.begin(), relevancyInformation.relevantCommands.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantCommands, locallyRelevantCommands.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantLabels); - STORM_LOG_DEBUG("Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states."); + std::vector> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, originalChoiceOrigins, statesThatCanReachTargetStates, locallyRelevantCommands); + STORM_LOG_DEBUG("Found " << reachableCommands.size() << " reachable commands and " << reachableStates.getNumberOfSetBits() << " reachable states."); // Search for states on the border of the reachable state space, i.e. states that are still reachable // and possess a (disabled) option to leave the reachable part of the state space. - std::vector> const& choiceLabeling = originalMdp.getChoiceLabeling(); - std::set> cutLabels; + std::set> cutCommands; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - if (!std::includes(commandSet.begin(), commandSet.end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end())) { + if (!std::includes(commandSet.begin(), commandSet.end(), originalChoiceOrigins.getCommandSet(currentChoice).begin(), originalChoiceOrigins.getCommandSet(currentChoice).end())) { bool isBorderChoice = false; // Determine whether the state has the option to leave the reachable state space and go to the unreachable relevant states. @@ -1435,15 +1434,15 @@ namespace storm { } if (isBorderChoice) { - boost::container::flat_set currentLabelSet; - for (auto label : choiceLabeling.at(currentChoice)) { - if (commandSet.find(label) == commandSet.end()) { - currentLabelSet.insert(label); + boost::container::flat_set currentCommandSet; + for (auto command : originalChoiceOrigins.getCommandSet(currentChoice)) { + if (commandSet.find(command) == commandSet.end()) { + currentCommandSet.insert(command); } } - std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); + std::set_difference(guaranteedCommandSets[state].begin(), guaranteedCommandSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentCommandSet, currentCommandSet.end())); - cutLabels.insert(currentLabelSet); + cutCommands.insert(currentCommandSet); } } } @@ -1451,15 +1450,15 @@ namespace storm { // Given the results of the previous analysis, we construct the implications. std::vector formulae; - boost::container::flat_set unknownReachableLabels; - std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); - for (auto label : unknownReachableLabels) { - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + boost::container::flat_set unknownReachableCommands; + std::set_difference(reachableCommands.begin(), reachableCommands.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownReachableCommands, unknownReachableCommands.end())); + for (auto command : unknownReachableCommands) { + formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); } - for (auto const& cutLabelSet : cutLabels) { + for (auto const& cutCommandSet : cutCommands) { storm::expressions::Expression cube = variableInformation.manager->boolean(true); - for (auto cutLabel : cutLabelSet) { - cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel)); + for (auto cutCommand : cutCommandSet) { + cube = cube && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(cutCommand)); } formulae.push_back(cube); @@ -1481,7 +1480,7 @@ namespace storm { * @param commandSet The currently chosen set of commands. * @param variableInformation A structure with information about the variables of the solver. */ - static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, storm::models::sparse::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeInsufficientProbabilitySolution(storm::solver::SmtSolver& solver, storm::models::sparse::Mdp const& subMdp, storm::storage::sparse::PrismChoiceOrigins const& subChoiceOrigins, storm::models::sparse::Mdp const& originalMdp, storm::storage::sparse::PrismChoiceOrigins const& originalChoiceOrigins, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::container::flat_set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { STORM_LOG_DEBUG("Analyzing solution with insufficient probability."); @@ -1497,10 +1496,9 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); - std::vector> const& subChoiceLabeling = subMdp.getChoiceLabeling(); - // Now determine which states and labels are actually reachable. - boost::container::flat_set reachableLabels; + // Now determine which states and commands are actually reachable. + boost::container::flat_set reachableCommands; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); stack.pop_back(); @@ -1521,8 +1519,8 @@ namespace storm { } if (choiceTargetsRelevantState) { - for (auto label : subChoiceLabeling[currentChoice]) { - reachableLabels.insert(label); + for (auto command : subChoiceOrigins.getCommandSet(currentChoice)) { + reachableCommands.insert(command); } } } @@ -1532,41 +1530,40 @@ namespace storm { storm::storage::BitVector unreachableRelevantStates = ~reachableStates & relevancyInformation.relevantStates; storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp.getBackwardTransitions(), phiStates, psiStates); - boost::container::flat_set locallyRelevantLabels; - std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); + boost::container::flat_set locallyRelevantCommands; + std::set_difference(relevancyInformation.relevantCommands.begin(), relevancyInformation.relevantCommands.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantCommands, locallyRelevantCommands.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, originalChoiceOrigins, statesThatCanReachTargetStates, locallyRelevantCommands); // Search for states for which we could enable another option and possibly improve the reachability probability. - std::vector> const& choiceLabeling = originalMdp.getChoiceLabeling(); - std::set> cutLabels; + std::set> cutCommands; for (auto state : reachableStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { - if (!std::includes(commandSet.begin(), commandSet.end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end())) { - boost::container::flat_set currentLabelSet; - for (auto label : choiceLabeling[currentChoice]) { - if (commandSet.find(label) == commandSet.end()) { - currentLabelSet.insert(label); + if (!std::includes(commandSet.begin(), commandSet.end(), originalChoiceOrigins.getCommandSet(currentChoice).begin(), originalChoiceOrigins.getCommandSet(currentChoice).end())) { + boost::container::flat_set currentCommandSet; + for (auto command : originalChoiceOrigins.getCommandSet(currentChoice)) { + if (commandSet.find(command) == commandSet.end()) { + currentCommandSet.insert(command); } } - std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentLabelSet, currentLabelSet.end())); + std::set_difference(guaranteedCommandSets[state].begin(), guaranteedCommandSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(currentCommandSet, currentCommandSet.end())); - cutLabels.insert(currentLabelSet); + cutCommands.insert(currentCommandSet); } } } // Given the results of the previous analysis, we construct the implications std::vector formulae; - boost::container::flat_set unknownReachableLabels; - std::set_difference(reachableLabels.begin(), reachableLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownReachableLabels, unknownReachableLabels.end())); - for (auto label : unknownReachableLabels) { - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + boost::container::flat_set unknownReachableCommands; + std::set_difference(reachableCommands.begin(), reachableCommands.end(), relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end(), std::inserter(unknownReachableCommands, unknownReachableCommands.end())); + for (auto command : unknownReachableCommands) { + formulae.push_back(!variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(command))); } - for (auto const& cutLabelSet : cutLabels) { + for (auto const& cutCommandSet : cutCommands) { storm::expressions::Expression cube = variableInformation.manager->boolean(true); - for (auto cutLabel : cutLabelSet) { - cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel)); + for (auto cutCommand : cutCommandSet) { + cube = cube && variableInformation.commandVariables.at(variableInformation.commandToIndexMap.at(cutCommand)); } formulae.push_back(cube); @@ -1579,12 +1576,62 @@ namespace storm { public: + /*! + * Returns the submdp obtained from removing all choices that do not originate from the specified commandset. + * Also returns the choiceorigins of the submdp + */ + static std::pair, std::shared_ptr> restrictMdpToCommandSet(storm::models::sparse::Mdp const& mdp, std::shared_ptr const& choiceOrigins, boost::container::flat_set const& enabledCommands) { + STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origins."); + STORM_LOG_THROW(choiceOrigins->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + + storm::storage::sparse::PrismChoiceOrigins const& prismChoiceOrigins = choiceOrigins->asPrismChoiceOrigins(); + + storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, mdp.getTransitionMatrix().getColumnCount(), 0, true, true, mdp.getTransitionMatrix().getRowGroupCount()); + std::vector subMdpChoiceIndexMapping; + + // Check for each choice of each state, whether the choice commands are fully contained in the given command set. + uint_fast64_t currentRow = 0; + for(uint_fast64_t state = 0; state < mdp.getNumberOfStates(); ++state) { + bool stateHasValidChoice = false; + for (uint_fast64_t choice = mdp.getTransitionMatrix().getRowGroupIndices()[state]; choice < mdp.getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { + bool choiceValid = std::includes(enabledCommands.begin(), enabledCommands.end(), prismChoiceOrigins.getCommandSet(choice).begin(), prismChoiceOrigins.getCommandSet(choice).end()); + + // If the choice is valid, copy over all its elements. + if (choiceValid) { + if (!stateHasValidChoice) { + transitionMatrixBuilder.newRowGroup(currentRow); + } + stateHasValidChoice = true; + for (auto const& entry : mdp.getTransitionMatrix().getRow(choice)) { + transitionMatrixBuilder.addNextValue(currentRow, entry.getColumn(), entry.getValue()); + } + subMdpChoiceIndexMapping.push_back(choice); + ++currentRow; + } + } + + // If no choice of the current state may be taken, we insert a self-loop to the state instead. + if (!stateHasValidChoice) { + transitionMatrixBuilder.newRowGroup(currentRow); + transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one()); + subMdpChoiceIndexMapping.push_back(std::numeric_limits::max()); + ++currentRow; + } + } + + storm::models::sparse::Mdp resultMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(mdp.getStateLabeling())); + std::shared_ptr resultOrigins = prismChoiceOrigins.selectChoices(subMdpChoiceIndexMapping); + + return std::make_pair(std::move(resultMdp), std::move(resultOrigins)); + } + /*! * Computes the minimal command set that is needed in the given MDP to exceed the given probability threshold for satisfying phi until psi. * * @param program The program that was used to build the MDP. * @param constantDefinitionString A string defining the undefined constants in the given program. - * @param labeledMdp The MDP in which to find the minimal command set. + * @param mdp The MDP in which to find the minimal command set. + * @param choiceOrigins The choice origins of the mdp * @param phiStates A bit vector characterizing all phi states in the model. * @param psiStates A bit vector characterizing all psi states in the model. * @param probabilityThreshold The probability value that must be achieved or exceeded. @@ -1593,8 +1640,10 @@ namespace storm { * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check * is made and fails, an exception is thrown. */ - static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { -#ifdef STORM_HAVE_Z3 + static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& choiceOrigins, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { +#ifdef STORM_HAVE_Z3 + + // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); auto localClock = std::chrono::high_resolution_clock::now(); @@ -1612,22 +1661,21 @@ namespace storm { auto analysisClock = std::chrono::high_resolution_clock::now(); decltype(std::chrono::high_resolution_clock::now() - analysisClock) totalAnalysisTime(0); + STORM_LOG_THROW(choiceOrigins && choiceOrigins->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to Prism command set is impossible for model without Prism choice origins."); + + storm::storage::sparse::PrismChoiceOrigins const& prismChoiceOrigins = choiceOrigins->asPrismChoiceOrigins(); + std::map constantDefinitions = storm::utility::cli::parseConstantDefinitionString(program.getManager(), constantDefinitionString); storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions); preparedProgram = preparedProgram.substituteConstants(); - // (0) Check whether the MDP is indeed labeled. - if (!labeledMdp.hasChoiceLabeling()) { - throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model."; - } - // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; if (checkThresholdFeasible) { storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; STORM_LOG_DEBUG("Invoking model checker."); - std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, labeledMdp.getTransitionMatrix(), labeledMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); - for (auto state : labeledMdp.getInitialStates()) { + std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, mdp.getTransitionMatrix(), mdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); + for (auto state : mdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); @@ -1635,30 +1683,30 @@ namespace storm { } // (2) Identify all states and commands that are relevant, because only these need to be considered later. - RelevancyInformation relevancyInformation = determineRelevantStatesAndLabels(labeledMdp, phiStates, psiStates); + RelevancyInformation relevancyInformation = determineRelevantStatesAndCommands(mdp, prismChoiceOrigins, phiStates, psiStates); // (3) Create a solver. std::shared_ptr manager(new storm::expressions::ExpressionManager()); std::unique_ptr solver(new storm::solver::Z3SmtSolver(*manager)); // (4) Create the variables for the relevant commands. - VariableInformation variableInformation = createVariables(manager, labeledMdp, psiStates, relevancyInformation, includeReachabilityEncoding); + VariableInformation variableInformation = createVariables(manager, mdp, psiStates, relevancyInformation, includeReachabilityEncoding); STORM_LOG_DEBUG("Created variables."); - // (5) Now assert an adder whose result variables can later be used to constrain the nummber of label - // variables that were set to true. Initially, we are looking for a solution that has no label enabled + // (5) Now assert an adder whose result variables can later be used to constrain the nummber of command + // variables that were set to true. Initially, we are looking for a solution that has no command enabled // and subsequently relax that. variableInformation.adderVariables = assertAdder(*solver, variableInformation); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(*solver, variableInformation, 0)); // (6) Add constraints that cut off a lot of suboptimal solutions. STORM_LOG_DEBUG("Asserting cuts."); - assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, *solver); + assertExplicitCuts(mdp, prismChoiceOrigins, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted explicit cuts."); - assertSymbolicCuts(preparedProgram, labeledMdp, variableInformation, relevancyInformation, *solver); + assertSymbolicCuts(preparedProgram, mdp, prismChoiceOrigins, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted symbolic cuts."); if (includeReachabilityEncoding) { - assertReachabilityCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, *solver); + assertReachabilityCuts(mdp, prismChoiceOrigins, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } @@ -1666,12 +1714,12 @@ namespace storm { totalSetupTime = std::chrono::high_resolution_clock::now() - setupTimeClock; // (7) Find the smallest set of commands that satisfies all constraints. If the probability of - // satisfying phi until psi exceeds the given threshold, the set of labels is minimal and can be returned. + // satisfying phi until psi exceeds the given threshold, the set of commands is minimal and can be returned. // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from // the solver. // Set up some variables for the iterations. - boost::container::flat_set commandSet(relevancyInformation.relevantLabels); + boost::container::flat_set commandSet(relevancyInformation.relevantCommands); bool done = false; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; @@ -1682,12 +1730,16 @@ namespace storm { solverClock = std::chrono::high_resolution_clock::now(); commandSet = findSmallestCommandSet(*solver, variableInformation, currentBound); totalSolverTime += std::chrono::high_resolution_clock::now() - solverClock; - STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownLabels.size()) << "."); + STORM_LOG_DEBUG("Computed minimal command set of size " << (commandSet.size() + relevancyInformation.knownCommands.size()) << "."); - // Restrict the given MDP to the current set of labels and compute the reachability probability. + // Restrict the given MDP to the current set of commands and compute the reachability probability. modelCheckingClock = std::chrono::high_resolution_clock::now(); - commandSet.insert(relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end()); - storm::models::sparse::Mdp subMdp = labeledMdp.restrictChoiceLabels(commandSet); + commandSet.insert(relevancyInformation.knownCommands.begin(), relevancyInformation.knownCommands.end()); + auto subMdpChoiceOrigins = restrictMdpToCommandSet(mdp, choiceOrigins, commandSet); + storm::models::sparse::Mdp const& subMdp = subMdpChoiceOrigins.first; + STORM_LOG_THROW(subMdpChoiceOrigins.second && subMdpChoiceOrigins.second->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Expected prism choice origins for submodel."); + storm::storage::sparse::PrismChoiceOrigins const& subPrismChoiceOrigins = subMdpChoiceOrigins.second->asPrismChoiceOrigins(); + storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; STORM_LOG_DEBUG("Invoking model checker."); std::vector result = std::move(modelCheckerHelper.computeUntilProbabilities(false, subMdp.getTransitionMatrix(), subMdp.getBackwardTransitions(), phiStates, psiStates, false, false, storm::solver::GeneralMinMaxLinearEquationSolverFactory()).values); @@ -1696,7 +1748,7 @@ namespace storm { // Now determine the maximal reachability probability by checking all initial states. maximalReachabilityProbability = 0; - for (auto state : labeledMdp.getInitialStates()) { + for (auto state : mdp.getInitialStates()) { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } @@ -1707,11 +1759,11 @@ namespace storm { ++zeroProbabilityCount; // If there was no target state reachable, analyze the solution and guide the solver into the right direction. - analyzeZeroProbabilitySolution(*solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeZeroProbabilitySolution(*solver, subMdp, subPrismChoiceOrigins, mdp, prismChoiceOrigins, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } else { // If the reachability probability was greater than zero (i.e. there is a reachable target state), but the probability was insufficient to exceed // the given threshold, we analyze the solution and try to guide the solver into the right direction. - analyzeInsufficientProbabilitySolution(*solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeInsufficientProbabilitySolution(*solver, subMdp, subPrismChoiceOrigins, mdp, prismChoiceOrigins, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } } else { done = true; @@ -1749,9 +1801,9 @@ namespace storm { #endif } - static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& labeledMdp, std::shared_ptr const& formula) { + static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& choiceOrigins, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 - std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; + std::cout << std::endl << "Generating minimal command set counterexample for formula " << *formula << std::endl; STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element."); storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula(); @@ -1765,7 +1817,7 @@ namespace storm { storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; - storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(labeledMdp); + storm::modelchecker::SparseMdpPrctlModelChecker> modelchecker(mdp); if (probabilityOperator.getSubformula().isUntilFormula()) { storm::logic::UntilFormula const& untilFormula = probabilityOperator.getSubformula().asUntilFormula(); @@ -1785,18 +1837,18 @@ namespace storm { storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); - phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); + phiStates = storm::storage::BitVector(mdp.getNumberOfStates(), true); psiStates = subQualitativeResult.getTruthValuesVector(); } // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalCommandSet(program, constantDefinitionString, labeledMdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); + auto commandSet = getMinimalCommandSet(program, constantDefinitionString, mdp, choiceOrigins, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); - std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; + std::cout << std::endl << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; std::cout << "Resulting program:" << std::endl << std::endl; - storm::prism::Program restrictedProgram = program.restrictCommands(labelSet); + storm::prism::Program restrictedProgram = program.restrictCommands(commandSet); std::cout << restrictedProgram << std::endl; std::cout << std::endl << "-------------------------------------------" << std::endl; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 015d64509..0332421b9 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -617,7 +617,10 @@ namespace storm { identifiers.reserve(dataForChoiceOrigins.size()); std::map commandSetToIdentifierMap; - uint_fast64_t currentIdentifier = 0; + // The empty commandset (i.e., the choices without origin) always has to get identifier getIdentifierForChoicesWithNoOrigin() -- which is assumed to be 0 + STORM_LOG_ASSERT(storm::storage::sparse::ChoiceOrigins::getIdentifierForChoicesWithNoOrigin() == 0, "The no origin identifier is assumed to be zero"); + commandSetToIdentifierMap.insert(std::make_pair(CommandSet(), 0)); + uint_fast64_t currentIdentifier = 1; for (boost::any& originData : dataForChoiceOrigins) { STORM_LOG_ASSERT(originData.empty() || boost::any_cast(&originData) != nullptr, "Origin data has unexpected type: " << originData.type().name() << "."); diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index a43aded44..b22eb2baa 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -10,7 +10,7 @@ namespace storm { template Ctmc::Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { exitRates = createExitRateVector(this->getTransitionMatrix()); } @@ -18,7 +18,7 @@ namespace storm { template Ctmc::Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere. exitRates = createExitRateVector(this->getTransitionMatrix()); @@ -27,7 +27,7 @@ namespace storm { template Ctmc::Ctmc(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), exitRates(exitRates) { } diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index 3bf6dc78c..09da1d420 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -24,7 +24,7 @@ namespace storm { */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -36,7 +36,7 @@ namespace storm { */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); /*! * Constructs a model from the given data. @@ -49,7 +49,7 @@ namespace storm { */ Ctmc(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); Ctmc(Ctmc const& ctmc) = default; diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index de37f1fa3..430c31c6f 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -11,7 +11,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { // Intentionally left empty. } @@ -21,7 +21,7 @@ namespace storm { storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // Intentionally left empty. } diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index c823b91cf..bba22eb09 100644 --- a/src/storm/models/sparse/DeterministicModel.h +++ b/src/storm/models/sparse/DeterministicModel.h @@ -27,7 +27,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -42,7 +42,7 @@ namespace storm { storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); DeterministicModel(DeterministicModel const& other) = default; DeterministicModel& operator=(DeterministicModel const& other) = default; diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index 319a06ee9..c0ec2b933 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -13,14 +13,14 @@ namespace storm { Dtmc::Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } template Dtmc::Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, boost::optional>&& optionalChoiceLabeling) + std::unordered_map&& rewardModels, boost::optional&& optionalChoiceLabeling) : DeterministicModel(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } diff --git a/src/storm/models/sparse/Dtmc.h b/src/storm/models/sparse/Dtmc.h index 4f2d0dfb1..291cfdf25 100644 --- a/src/storm/models/sparse/Dtmc.h +++ b/src/storm/models/sparse/Dtmc.h @@ -24,7 +24,7 @@ namespace storm { Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -36,7 +36,7 @@ namespace storm { */ Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); Dtmc(Dtmc const& dtmc) = default; Dtmc& operator=(Dtmc const& dtmc) = default; diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 88a77b43d..9849d4f4a 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -20,7 +20,7 @@ namespace storm { storm::storage::BitVector const& markovianStates, std::vector const& exitRates, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(this->checkIsClosed()) { this->turnRatesToProbabilities(); } @@ -31,7 +31,7 @@ namespace storm { storm::storage::BitVector const& markovianStates, std::vector const& exitRates, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(this->checkIsClosed()) { this->turnRatesToProbabilities(); } @@ -42,7 +42,7 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, storm::storage::BitVector const& markovianStates, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates) { turnRatesToProbabilities(); this->closed = checkIsClosed(); @@ -53,7 +53,7 @@ namespace storm { storm::models::sparse::StateLabeling&& stateLabeling, storm::storage::BitVector&& markovianStates, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates) { turnRatesToProbabilities(); this->closed = checkIsClosed(); @@ -67,7 +67,7 @@ namespace storm { std::vector const& exitRates, bool probabilities, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(this->checkIsClosed()) { STORM_LOG_ASSERT(probabilities, "Matrix must be probabilistic."); STORM_LOG_ASSERT(this->getTransitionMatrix().isProbabilistic(), "Matrix must be probabilistic."); @@ -147,7 +147,7 @@ namespace storm { } } if(this->hasChoiceLabeling()) { - storm::utility::vector::filterVectorInPlace(this->getOptionalChoiceLabeling().get(), keptChoices); + this->getChoiceLabeling().getSubLabeling(keptChoices); } // Mark the automaton as closed. @@ -327,15 +327,13 @@ namespace storm { STORM_LOG_TRACE("New CTMC matrix:" << std::endl << rateMatrix); // Construct CTMC storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates); - boost::optional> optionalChoiceLabeling = this->getOptionalChoiceLabeling(); - if (optionalChoiceLabeling) { - storm::utility::vector::filterVectorInPlace(optionalChoiceLabeling.get(), keepStates); - } - //TODO update reward models according to kept states + + //TODO update reward models and choice labels according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); std::unordered_map rewardModels = this->getRewardModels(); + STORM_LOG_WARN_COND(!this->hasChoiceLabeling(), "Conversion of MA to CTMC does not preserve choice labels."); - return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)); + return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels)); } diff --git a/src/storm/models/sparse/MarkovAutomaton.h b/src/storm/models/sparse/MarkovAutomaton.h index 5e1cb7862..88c03a863 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -30,7 +30,7 @@ namespace storm { storm::storage::BitVector const& markovianStates, std::vector const& exitRates, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model from the given data. @@ -48,7 +48,7 @@ namespace storm { storm::models::sparse::StateLabeling const& stateLabeling, storm::storage::BitVector const& markovianStates, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model from the given data. @@ -66,7 +66,7 @@ namespace storm { storm::models::sparse::StateLabeling&& stateLabeling, storm::storage::BitVector&& markovianStates, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -83,7 +83,7 @@ namespace storm { storm::storage::BitVector const& markovianStates, std::vector const& exitRates, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -102,7 +102,7 @@ namespace storm { std::vector const& exitRates, bool probabilities, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); MarkovAutomaton(MarkovAutomaton const& other) = default; MarkovAutomaton& operator=(MarkovAutomaton const& other) = default; diff --git a/src/storm/models/sparse/Mdp.cpp b/src/storm/models/sparse/Mdp.cpp index 394ed75d4..e9fdba8f3 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -15,7 +15,7 @@ namespace storm { Mdp::Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } @@ -25,56 +25,11 @@ namespace storm { Mdp::Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : NondeterministicModel(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { STORM_LOG_THROW(transitionMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } - template - Mdp Mdp::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const { - STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for unlabeled model."); - - std::vector const& choiceLabeling = this->getChoiceLabeling(); - - storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true); - std::vector newChoiceLabeling; - - // Check for each choice of each state, whether the choice labels are fully contained in the given label set. - uint_fast64_t currentRow = 0; - for(uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { - bool stateHasValidChoice = false; - for (uint_fast64_t choice = this->getTransitionMatrix().getRowGroupIndices()[state]; choice < this->getTransitionMatrix().getRowGroupIndices()[state + 1]; ++choice) { - bool choiceValid = std::includes(enabledChoiceLabels.begin(), enabledChoiceLabels.end(), choiceLabeling[choice].begin(), choiceLabeling[choice].end()); - - // If the choice is valid, copy over all its elements. - if (choiceValid) { - if (!stateHasValidChoice) { - transitionMatrixBuilder.newRowGroup(currentRow); - } - stateHasValidChoice = true; - for (auto const& entry : this->getTransitionMatrix().getRow(choice)) { - transitionMatrixBuilder.addNextValue(currentRow, entry.getColumn(), entry.getValue()); - } - newChoiceLabeling.emplace_back(choiceLabeling[choice]); - ++currentRow; - } - } - - // If no choice of the current state may be taken, we insert a self-loop to the state instead. - if (!stateHasValidChoice) { - transitionMatrixBuilder.newRowGroup(currentRow); - transitionMatrixBuilder.addNextValue(currentRow, state, storm::utility::one()); - newChoiceLabeling.emplace_back(); - ++currentRow; - } - } - - Mdp restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()), - std::unordered_map(this->getRewardModels()), boost::optional>(newChoiceLabeling)); - - return restrictedMdp; - } - template Mdp Mdp::restrictChoices(storm::storage::BitVector const& enabledChoices) const { storm::storage::SparseMatrix restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledChoices); @@ -83,12 +38,10 @@ namespace storm { newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); } if(this->hasChoiceLabeling()) { - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional>(storm::utility::vector::filterVector(this->getChoiceLabeling(), enabledChoices))); + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getChoiceLabeling().getSubLabeling(enabledChoices)); } else { - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, boost::optional>()); + return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels); } - - } template diff --git a/src/storm/models/sparse/Mdp.h b/src/storm/models/sparse/Mdp.h index ba231cd72..542b184af 100644 --- a/src/storm/models/sparse/Mdp.h +++ b/src/storm/models/sparse/Mdp.h @@ -26,7 +26,7 @@ namespace storm { Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -39,7 +39,7 @@ namespace storm { Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); Mdp(Mdp const& other) = default; Mdp& operator=(Mdp const& other) = default; @@ -47,17 +47,6 @@ namespace storm { Mdp(Mdp&& other) = default; Mdp& operator=(Mdp&& other) = default; - /*! - * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones - * whose label set is contained in the given label set. Note that is is only valid to call this method - * if the MDP has choice labels. - * - * @param enabledChoiceLabels A set of labels that determines which choices of the original model can be taken - * and which ones need to be ignored. - * @return A restricted version of the current MDP that only uses choice labels from the given set. - */ - Mdp restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const; - /*! * Constructs an MDP by copying the current MDP and restricting the choices of each state to the ones given by the bitvector. * diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index d75065299..90bafbd51 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -19,7 +19,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : ModelBase(modelType), transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), choiceLabeling(optionalChoiceLabeling) { for (auto const& rewardModel : this->getRewardModels()) { @@ -32,7 +32,7 @@ namespace storm { storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : ModelBase(modelType), transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), choiceLabeling(std::move(optionalChoiceLabeling)) { for (auto const& rewardModel : this->getRewardModels()) { @@ -160,17 +160,17 @@ namespace storm { } template - std::vector const& Model::getChoiceLabeling() const { + storm::models::sparse::ChoiceLabeling const& Model::getChoiceLabeling() const { return choiceLabeling.get(); } template - boost::optional> const& Model::getOptionalChoiceLabeling() const { + boost::optional const& Model::getOptionalChoiceLabeling() const { return choiceLabeling; } template - boost::optional>& Model::getOptionalChoiceLabeling() { + boost::optional& Model::getOptionalChoiceLabeling() { return choiceLabeling; } diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 206b364b7..4b8959972 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -3,11 +3,11 @@ #include #include -#include #include #include "storm/models/ModelBase.h" #include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/SparseMatrix.h" #include "storm/utility/OsDetection.h" @@ -25,9 +25,6 @@ namespace storm { namespace models { namespace sparse { - // The type used for storing a set of labels. - typedef boost::container::flat_set LabelSet; - template class StandardRewardModel; @@ -60,7 +57,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -75,7 +72,7 @@ namespace storm { storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); /*! * Retrieves the backward transition relation of the model, i.e. a set of transitions between states @@ -227,21 +224,21 @@ namespace storm { * * @return The labels for the choices of the model. */ - std::vector const& getChoiceLabeling() const; + storm::models::sparse::ChoiceLabeling const& getChoiceLabeling() const; /*! * Retrieves an optional value that contains the choice labeling if there is one. * * @return The labels for the choices, if they're saved. */ - boost::optional> const& getOptionalChoiceLabeling() const; + boost::optional const& getOptionalChoiceLabeling() const; /*! * Retrieves an optional value that contains the choice labeling if there is one. * * @return The labels for the choices, if they're saved. */ - boost::optional>& getOptionalChoiceLabeling(); + boost::optional& getOptionalChoiceLabeling(); /*! * Returns the state labeling associated with this model. @@ -365,7 +362,7 @@ namespace storm { std::unordered_map rewardModels; // If set, a vector representing the labels of choices. - boost::optional> choiceLabeling; + boost::optional choiceLabeling; }; #ifdef STORM_HAVE_CARL diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 7f221cabe..1a49c8da0 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -15,7 +15,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalChoiceLabeling) + boost::optional const& optionalChoiceLabeling) : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { // Intentionally left empty. } @@ -25,7 +25,7 @@ namespace storm { storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, - boost::optional>&& optionalChoiceLabeling) + boost::optional&& optionalChoiceLabeling) : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { // Intentionally left empty. @@ -46,43 +46,7 @@ namespace storm { auto indices = this->getNondeterministicChoiceIndices(); return indices[state+1] - indices[state]; } - - template - void NondeterministicModel::modifyStateActionRewards(RewardModelType& rewardModel, std::map, typename RewardModelType::ValueType> const& modifications) const { - STORM_LOG_THROW(rewardModel.hasStateActionRewards(), storm::exceptions::InvalidOperationException, "Cannot modify state-action rewards, because the reward model does not have state-action rewards."); - STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidOperationException, "Cannot modify state-action rewards, because the model does not have an action labeling."); - std::vector const& choiceLabels = this->getChoiceLabeling(); - for (auto const& modification : modifications) { - uint_fast64_t stateIndex = modification.first.first; - for (uint_fast64_t row = this->getNondeterministicChoiceIndices()[stateIndex]; row < this->getNondeterministicChoiceIndices()[stateIndex + 1]; ++row) { - // If the action label of the row matches the requested one, we set the reward value accordingly. - if (choiceLabels[row] == modification.first.second) { - rewardModel.setStateActionRewardValue(row, modification.second); - } - } - } - } - - template - template - void NondeterministicModel::modifyStateActionRewards(std::string const& modelName, std::map const& modifications) { - RewardModelType& rewardModel = this->rewardModel(modelName); - size_t i = 0; - for(auto const& mod : modifications) { - std::cout << i++ << "/" << modifications.size() << std::endl; - rewardModel.setStateActionReward(mod.first, mod.second); - } - } - template - template - void NondeterministicModel::modifyStateRewards(std::string const& modelName, std::map const& modifications) { - RewardModelType& rewardModel = this->rewardModel(modelName); - for(auto const& mod : modifications) { - rewardModel.setStateReward(mod.first, mod.second); - } - } - template void NondeterministicModel::reduceToStateBasedRewards() { for (auto& rewardModel : this->getRewardModels()) { @@ -173,11 +137,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class NondeterministicModel; - template class NondeterministicModel>; - template void NondeterministicModel>::modifyStateActionRewards(std::string const& modelName, std::map const& modifications); - template void NondeterministicModel>::modifyStateRewards(std::string const& modelName, std::map const& modifications); - template class NondeterministicModel; #endif } diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index b0f32e688..bb2443b05 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -27,7 +27,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalChoiceLabeling = boost::optional>()); + boost::optional const& optionalChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -42,7 +42,7 @@ namespace storm { storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalChoiceLabeling = boost::optional>()); + boost::optional&& optionalChoiceLabeling = boost::none); NondeterministicModel(NondeterministicModel const& other) = default; NondeterministicModel& operator=(NondeterministicModel const& other) = default; @@ -71,21 +71,6 @@ namespace storm { */ uint_fast64_t getNumberOfChoices(uint_fast64_t state) const; - /*! - * Modifies the state-action reward vector of the given reward model by setting the value specified in - * the map for the corresponding state-action pairs. - * - * @param rewardModel The reward model whose state-action rewards to modify. - * @param modifications A mapping from state-action pairs to the their new reward values. - */ - void modifyStateActionRewards(RewardModelType& rewardModel, std::map, typename RewardModelType::ValueType> const& modifications) const; - - template - void modifyStateActionRewards(std::string const& modelName, std::map const& modifications); - template - void modifyStateRewards(std::string const& modelName, std::map const& modifications); - - virtual void reduceToStateBasedRewards() override; virtual void printModelInformationToStream(std::ostream& out) const override; diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp index 6ac6f93e4..e0b4576f1 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp @@ -13,8 +13,8 @@ namespace storm { storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels, - boost::optional> const& optionalPlayer1ChoiceLabeling, - boost::optional> const& optionalPlayer2ChoiceLabeling) + boost::optional const& optionalPlayer1ChoiceLabeling, + boost::optional const& optionalPlayer2ChoiceLabeling) : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1ChoiceLabeling(optionalPlayer1ChoiceLabeling) { // Intentionally left empty. } @@ -25,8 +25,8 @@ namespace storm { storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels, - boost::optional>&& optionalPlayer1ChoiceLabeling, - boost::optional>&& optionalPlayer2ChoiceLabeling) + boost::optional&& optionalPlayer1ChoiceLabeling, + boost::optional&& optionalPlayer2ChoiceLabeling) : NondeterministicModel(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1ChoiceLabeling(std::move(optionalPlayer1ChoiceLabeling)) { // Intentionally left empty. } @@ -47,7 +47,7 @@ namespace storm { } template - std::vector const& StochasticTwoPlayerGame::getPlayer1ChoiceLabeling() const { + storm::models::sparse::ChoiceLabeling const& StochasticTwoPlayerGame::getPlayer1ChoiceLabeling() const { return player1ChoiceLabeling.get(); } @@ -57,7 +57,7 @@ namespace storm { } template - std::vector const& StochasticTwoPlayerGame::getPlayer2ChoiceLabeling() const { + storm::models::sparse::ChoiceLabeling const& StochasticTwoPlayerGame::getPlayer2ChoiceLabeling() const { return this->getChoiceLabeling(); } diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.h b/src/storm/models/sparse/StochasticTwoPlayerGame.h index a589decc1..9c850e83d 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.h +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.h @@ -29,8 +29,8 @@ namespace storm { storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional> const& optionalPlayer1ChoiceLabeling = boost::optional>(), - boost::optional> const& optionalPlayer2ChoiceLabeling = boost::optional>()); + boost::optional const& optionalPlayer1ChoiceLabeling = boost::none, + boost::optional const& optionalPlayer2ChoiceLabeling = boost::none); /*! * Constructs a model by moving the given data. @@ -46,8 +46,8 @@ namespace storm { storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional>&& optionalPlayer1ChoiceLabeling = boost::optional>(), - boost::optional>&& optionalPlayer2ChoiceLabeling = boost::optional>()); + boost::optional&& optionalPlayer1ChoiceLabeling = boost::none, + boost::optional&& optionalPlayer2ChoiceLabeling = boost::none); StochasticTwoPlayerGame(StochasticTwoPlayerGame const& other) = default; StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame const& other) = default; @@ -82,7 +82,7 @@ namespace storm { * * @return A vector containing the labels of each player 1 choice. */ - std::vector const& getPlayer1ChoiceLabeling() const; + storm::models::sparse::ChoiceLabeling const& getPlayer1ChoiceLabeling() const; /*! * Retrieves whether the game has labels attached to player 2 states. @@ -96,7 +96,7 @@ namespace storm { * * @return A vector containing the labels of each player 2 choice. */ - std::vector const& getPlayer2ChoiceLabeling() const; + storm::models::sparse::ChoiceLabeling const& getPlayer2ChoiceLabeling() const; private: // A matrix that stores the player 1 choices. This matrix contains a row group for each player 1 node. Every @@ -107,7 +107,7 @@ namespace storm { // An (optional) vector of labels attached to the choices of player 1. Each row of the matrix can be equipped // with a set of labels to tag certain choices. - boost::optional> player1ChoiceLabeling; + boost::optional player1ChoiceLabeling; // The matrix and labels for player 2 are stored in the superclass. }; diff --git a/src/storm/parser/DeterministicModelParser.cpp b/src/storm/parser/DeterministicModelParser.cpp index e962193c2..9976e67dc 100644 --- a/src/storm/parser/DeterministicModelParser.cpp +++ b/src/storm/parser/DeterministicModelParser.cpp @@ -60,7 +60,7 @@ namespace storm { if (!stateRewardFilename.empty() || !transitionRewardFilename.empty()) { rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); } - return storm::models::sparse::Ctmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::optional>>()); + return storm::models::sparse::Ctmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), boost::none); } template class DeterministicModelParser; diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h index ba1056401..1c7a6c3f0 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm/parser/DirectEncodingParser.h @@ -79,7 +79,7 @@ namespace storm { std::unordered_map rewardModels; // A vector that stores a labeling for each choice. - boost::optional> choiceLabeling; + boost::optional choiceLabeling; // The exit rates for MAs. std::vector exitRates; diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm/parser/NondeterministicModelParser.cpp index 5ea7952ba..e93ca6a23 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm/parser/NondeterministicModelParser.cpp @@ -40,9 +40,10 @@ namespace storm { } // Only parse choice labeling if a file is given. - boost::optional> choiceLabeling; + boost::optional choiceLabeling; if (!choiceLabelingFilename.empty()) { - choiceLabeling = std::move(storm::parser::SparseChoiceLabelingParser::parseChoiceLabeling(transitions.getRowGroupIndices(), choiceLabelingFilename)); + STORM_LOG_ERROR("Parsing choice labels is currently not implemented"); // TODO + //choiceLabeling = std::move(storm::parser::SparseChoiceLabelingParser::parseChoiceLabeling(transitions.getRowGroupIndices(), choiceLabelingFilename)); } // Construct the result. diff --git a/src/storm/parser/NondeterministicModelParser.h b/src/storm/parser/NondeterministicModelParser.h index c095fabd1..8ce22e13e 100644 --- a/src/storm/parser/NondeterministicModelParser.h +++ b/src/storm/parser/NondeterministicModelParser.h @@ -64,7 +64,7 @@ namespace storm { /*! * Optional choice labeling. */ - boost::optional> choiceLabeling; + boost::optional choiceLabeling; }; /*! diff --git a/src/storm/parser/SparseChoiceLabelingParser.cpp b/src/storm/parser/SparseChoiceLabelingParser.cpp index 26395d057..b51e8b97c 100644 --- a/src/storm/parser/SparseChoiceLabelingParser.cpp +++ b/src/storm/parser/SparseChoiceLabelingParser.cpp @@ -1,5 +1,6 @@ #include "storm/parser/SparseChoiceLabelingParser.h" +#include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/OutOfRangeException.h" #include "storm/exceptions/FileIoException.h" @@ -11,7 +12,7 @@ namespace storm { using namespace storm::utility::cstring; - std::vector SparseChoiceLabelingParser::parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename) { + std::vector> SparseChoiceLabelingParser::parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename) { // Open file. MappedFile file(filename.c_str()); char const* buf = file.getData(); @@ -19,7 +20,7 @@ namespace storm { uint_fast64_t totalNumberOfChoices = nondeterministicChoiceIndices.back(); // Create choice labeling vector with given choice count. - std::vector result(totalNumberOfChoices); + std::vector> result(totalNumberOfChoices); // Now parse state reward assignments. uint_fast64_t state = 0; diff --git a/src/storm/parser/SparseChoiceLabelingParser.h b/src/storm/parser/SparseChoiceLabelingParser.h index 20091306a..a0b509b69 100644 --- a/src/storm/parser/SparseChoiceLabelingParser.h +++ b/src/storm/parser/SparseChoiceLabelingParser.h @@ -1,7 +1,9 @@ #ifndef STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ #define STORM_PARSER_SPARSECHOICELABELINGPARSER_H_ -#include "storm/models/sparse/Model.h" +#include +#include +#include namespace storm { namespace parser { @@ -18,7 +20,7 @@ namespace storm { * @param filename The name of the file to parse. * @return The resulting choice labeling. */ - static std::vector parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename); + static std::vector> parseChoiceLabeling(std::vector const& nondeterministicChoiceIndices, std::string const& filename); }; } } diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index d9a045482..465500ea4 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/src/storm/storage/sparse/ChoiceOrigins.cpp @@ -45,6 +45,10 @@ namespace storm { return indexToIdentifier[choiceIndex]; } + uint_fast64_t ChoiceOrigins::getIdentifierForChoicesWithNoOrigin() { + return 0; + } + std::string const& ChoiceOrigins::getIdentifierInfo(uint_fast64_t identifier) const { return identifierToInfo[identifier]; } @@ -60,8 +64,15 @@ namespace storm { } std::shared_ptr ChoiceOrigins::selectChoices(std::vector const& selectedChoices) const { - std::vector indexToIdentifierMapping(selectedChoices.size()); - storm::utility::vector::selectVectorValues(indexToIdentifierMapping, selectedChoices, indexToIdentifier); + std::vector indexToIdentifierMapping; + indexToIdentifierMapping.reserve(selectedChoices.size()); + for (auto const& selectedChoice : selectedChoices){ + if (selectedChoice < this->indexToIdentifier.size()) { + indexToIdentifierMapping.push_back(indexToIdentifier[selectedChoice]); + } else { + indexToIdentifierMapping.push_back(getIdentifierForChoicesWithNoOrigin()); + } + } return cloneWithNewIndexToIdentifierMapping(std::move(indexToIdentifierMapping)); } } diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index e869658ea..3b1a1faad 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -34,6 +34,12 @@ namespace storm { */ uint_fast64_t getIdentifier(uint_fast64_t choiceIndex) const; + /* + * Returns the identifier that is used for choices without an origin in the input specification + * E.g., Selfloops introduced on deadlock states + */ + static uint_fast64_t getIdentifierForChoicesWithNoOrigin(); + /* * Returns the information for the given choice origin identifier as a (human readable) string */ diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index ec417bdff..d087b5a54 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/src/storm/storage/sparse/PrismChoiceOrigins.cpp @@ -1,16 +1,18 @@ #include "storm/storage/sparse/PrismChoiceOrigins.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace storage { namespace sparse { PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector const& indexToIdentifierMapping, std::vector const& identifierToInfoMapping, std::vector const& identifierToCommandSetMapping) : ChoiceOrigins(indexToIdentifierMapping, identifierToInfoMapping), program(prismProgram), identifierToCommandSet(identifierToCommandSetMapping) { - // Intentionally left empty + STORM_LOG_THROW(identifierToCommandSet[this->getIdentifierForChoicesWithNoOrigin()].empty(), storm::exceptions::InvalidArgumentException, "The given command set for the choices without origin is non-empty"); } PrismChoiceOrigins::PrismChoiceOrigins(std::shared_ptr const& prismProgram, std::vector&& indexToIdentifierMapping, std::vector&& identifierToInfoMapping, std::vector&& identifierToCommandSetMapping) : ChoiceOrigins(std::move(indexToIdentifierMapping), std::move(identifierToInfoMapping)), program(prismProgram), identifierToCommandSet(std::move(identifierToCommandSetMapping)) { - // Intentionally left empty + STORM_LOG_THROW(identifierToCommandSet[this->getIdentifierForChoicesWithNoOrigin()].empty(), storm::exceptions::InvalidArgumentException, "The given command set for the choices without origin is non-empty"); } bool PrismChoiceOrigins::isPrismChoiceOrigins() const { diff --git a/src/storm/transformer/StateDuplicator.h b/src/storm/transformer/StateDuplicator.h index 72328013c..b9c697b81 100644 --- a/src/storm/transformer/StateDuplicator.h +++ b/src/storm/transformer/StateDuplicator.h @@ -59,24 +59,29 @@ namespace storm { // Transform the ingedients of the model storm::storage::SparseMatrix matrix = transformMatrix(originalModel.getTransitionMatrix(), result, gateStates); - storm::models::sparse::StateLabeling labeling(matrix.getRowGroupCount()); - for(auto const& label : originalModel.getStateLabeling().getLabels()){ + storm::models::sparse::StateLabeling stateLabeling(matrix.getRowGroupCount()); + for (auto const& label : originalModel.getStateLabeling().getLabels()) { storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), result); - if(label=="init"){ + if (label=="init") { newBitVectorForLabel &= (result.firstCopy | result.gateStates); } - labeling.addLabel(label, std::move(newBitVectorForLabel)); + stateLabeling.addLabel(label, std::move(newBitVectorForLabel)); } + std::unordered_map rewardModels; - for(auto const& rewardModel : originalModel.getRewardModels()){ + for (auto const& rewardModel : originalModel.getRewardModels()) { rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, originalModel.getTransitionMatrix().getRowGroupIndices(), result, gateStates))); } - boost::optional> choiceLabeling; - if(originalModel.hasChoiceLabeling()){ - choiceLabeling = transformActionValueVector(originalModel.getChoiceLabeling(), originalModel.getTransitionMatrix().getRowGroupIndices(), result); + + boost::optional choiceLabeling; + if (originalModel.hasChoiceLabeling()) { + for (auto const& label : originalModel.getChoiceLabeling().getLabels()) { + storm::storage::BitVector newBitVectorForLabel = transformActionBitVector(originalModel.getChoiceLabeling().getChoices(label), originalModel.getTransitionMatrix().getRowGroupIndices(), result); + choiceLabeling->addLabel(label, std::move(newBitVectorForLabel)); + } } - result.model = std::make_shared(createTransformedModel(originalModel, result, matrix, labeling, rewardModels, choiceLabeling)); + result.model = std::make_shared(createTransformedModel(originalModel, result, matrix, stateLabeling, rewardModels, choiceLabeling)); STORM_LOG_DEBUG("State duplicator is done. Resulting model has " << result.model->getNumberOfStates() << " states, where " << result.firstCopy.getNumberOfSetBits() << " are in the first copy."); return result; } @@ -109,9 +114,9 @@ namespace storm { result.firstCopyOldToNewStateIndexMapping = std::vector(originalModel.getNumberOfStates(), std::numeric_limits::max()); result.secondCopyOldToNewStateIndexMapping = std::vector(originalModel.getNumberOfStates(), std::numeric_limits::max()); uint_fast64_t newState = 0; - for(auto const& oldState : result.reachableStates){ + for (auto const& oldState : result.reachableStates) { result.newToOldStateIndexMapping[newState] = oldState; - if(statesForFirstCopy.get(oldState)){ + if (statesForFirstCopy.get(oldState)) { result.firstCopyOldToNewStateIndexMapping[oldState] = newState; } else { result.secondCopyOldToNewStateIndexMapping[oldState] = newState; @@ -120,7 +125,7 @@ namespace storm { } // The remaining states are duplicates. All these states belong to the second copy. - for(auto const& oldState : result.duplicatedStates) { + for (auto const& oldState : result.duplicatedStates) { result.newToOldStateIndexMapping[newState] = oldState; result.secondCopyOldToNewStateIndexMapping[oldState] = newState; ++newState; @@ -136,13 +141,13 @@ namespace storm { boost::optional> stateRewardVector; boost::optional> stateActionRewardVector; boost::optional> transitionRewardMatrix; - if(originalRewardModel.hasStateRewards()){ + if (originalRewardModel.hasStateRewards()) { stateRewardVector = transformStateValueVector(originalRewardModel.getStateRewardVector(), result); } - if(originalRewardModel.hasStateActionRewards()){ + if (originalRewardModel.hasStateActionRewards()) { stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), originalRowGroupIndices, result); } - if(originalRewardModel.hasTransitionRewards()){ + if (originalRewardModel.hasTransitionRewards()) { transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result, gateStates); } return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix)); @@ -154,7 +159,7 @@ namespace storm { uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); uint_fast64_t numRows = 0; uint_fast64_t numEntries = 0; - for(auto const& oldState : result.newToOldStateIndexMapping){ + for (auto const& oldState : result.newToOldStateIndexMapping) { numRows += originalMatrix.getRowGroupSize(oldState); numEntries += originalMatrix.getRowGroupEntryCount(oldState); } @@ -162,22 +167,22 @@ namespace storm { // Fill in the data uint_fast64_t newRow = 0; - for(uint_fast64_t newState = 0; newState < numStates; ++newState){ - if(!originalMatrix.hasTrivialRowGrouping()){ + for (uint_fast64_t newState = 0; newState < numStates; ++newState) { + if (!originalMatrix.hasTrivialRowGrouping()) { builder.newRowGroup(newRow); } uint_fast64_t oldState = result.newToOldStateIndexMapping[newState]; - for (uint_fast64_t oldRow = originalMatrix.getRowGroupIndices()[oldState]; oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; ++oldRow){ - for(auto const& entry : originalMatrix.getRow(oldRow)){ - if(result.firstCopy.get(newState) && !gateStates.get(entry.getColumn())){ + for (uint_fast64_t oldRow = originalMatrix.getRowGroupIndices()[oldState]; oldRow < originalMatrix.getRowGroupIndices()[oldState+1]; ++oldRow) { + for (auto const& entry : originalMatrix.getRow(oldRow)) { + if (result.firstCopy.get(newState) && !gateStates.get(entry.getColumn())) { builder.addNextValue(newRow, result.firstCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); - } else if (!result.duplicatedStates.get(entry.getColumn())){ + } else if (!result.duplicatedStates.get(entry.getColumn())) { builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); } } //To add values in the right order, transitions to duplicated states have to be added in a second run. - for(auto const& entry : originalMatrix.getRow(oldRow)){ - if (result.secondCopy.get(newState) && result.duplicatedStates.get(entry.getColumn())){ + for (auto const& entry : originalMatrix.getRow(oldRow)) { + if (result.secondCopy.get(newState) && result.duplicatedStates.get(entry.getColumn())) { builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); } } @@ -192,13 +197,13 @@ namespace storm { template static std::vector transformActionValueVector(std::vectorconst& originalVector, std::vector const& originalRowGroupIndices, StateDuplicatorReturnType const& result) { uint_fast64_t numActions = 0; - for(auto const& oldState : result.newToOldStateIndexMapping){ + for (auto const& oldState : result.newToOldStateIndexMapping) { numActions += originalRowGroupIndices[oldState+1] - originalRowGroupIndices[oldState]; } std::vector v; v.reserve(numActions); - for(auto const& oldState : result.newToOldStateIndexMapping){ - for (uint_fast64_t oldAction = originalRowGroupIndices[oldState]; oldAction < originalRowGroupIndices[oldState+1]; ++oldAction){ + for (auto const& oldState : result.newToOldStateIndexMapping) { + for (uint_fast64_t oldAction = originalRowGroupIndices[oldState]; oldAction < originalRowGroupIndices[oldState+1]; ++oldAction) { v.push_back(originalVector[oldAction]); } } @@ -211,17 +216,36 @@ namespace storm { uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); std::vector v; v.reserve(numStates); - for(auto const& oldState : result.newToOldStateIndexMapping){ + for (auto const& oldState : result.newToOldStateIndexMapping) { v.push_back(originalVector[oldState]); } STORM_LOG_ASSERT(v.size() == numStates, "Unexpected vector size."); return v; } - static storm::storage::BitVector transformStateBitVector(storm::storage::BitVector const& originalBitVector, StateDuplicatorReturnType const& result) { + static storm::storage::BitVector transformActionBitVector(storm::storage::BitVector const& originalBitVector, std::vector const& originalRowGroupIndices, StateDuplicatorReturnType const& result) { + uint_fast64_t numActions = 0; + for (auto const& oldState : result.newToOldStateIndexMapping) { + numActions += originalRowGroupIndices[oldState+1] - originalRowGroupIndices[oldState]; + } + storm::storage::BitVector bv(numActions, false); + uint_fast64_t newAction = 0; + for (auto const& oldState : result.newToOldStateIndexMapping) { + for (uint_fast64_t oldAction = originalRowGroupIndices[oldState]; oldAction < originalRowGroupIndices[oldState+1]; ++oldAction) { + if (originalBitVector.get(oldAction)) { + bv.set(newAction, true); + } + ++newAction; + } + } + STORM_LOG_ASSERT(newAction == numActions, "Unexpected vector size."); + return bv; + } + + static storm::storage::BitVector transformStateBitVector(storm::storage::BitVector const& originalBitVector, StateDuplicatorReturnType const& result) { uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); storm::storage::BitVector bv(numStates); - for(uint_fast64_t newState = 0; newState < numStates; ++newState){ + for (uint_fast64_t newState = 0; newState < numStates; ++newState) { uint_fast64_t oldState = result.newToOldStateIndexMapping[newState]; bv.set(newState, originalBitVector.get(oldState)); } @@ -241,7 +265,7 @@ namespace storm { storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map& rewardModels, - boost::optional>& choiceLabeling ) { + boost::optional& choiceLabeling ) { return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); } @@ -255,7 +279,7 @@ namespace storm { storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map& rewardModels, - boost::optional>& choiceLabeling ) { + boost::optional& choiceLabeling ) { storm::storage::BitVector markovianStates = transformStateBitVector(originalModel.getMarkovianStates(), result); std::vector exitRates = transformStateValueVector(originalModel.getExitRates(), result); return MT(std::move(matrix), std::move(stateLabeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels), std::move(choiceLabeling)); diff --git a/src/storm/transformer/SubsystemBuilder.h b/src/storm/transformer/SubsystemBuilder.h index 78474d800..55dbb80fe 100644 --- a/src/storm/transformer/SubsystemBuilder.h +++ b/src/storm/transformer/SubsystemBuilder.h @@ -58,7 +58,7 @@ namespace storm { uint_fast64_t subsystemStateCount = subsystemStates.getNumberOfSetBits(); STORM_LOG_THROW(subsystemStateCount != 0, storm::exceptions::InvalidArgumentException, "Invoked SubsystemBuilder for an empty subsystem."); - if(subsystemStateCount == subsystemStates.size() && subsystemActions.full()) { + if (subsystemStateCount == subsystemStates.size() && subsystemActions.full()) { result.model = std::make_shared(originalModel); result.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, result.model->getNumberOfStates()); result.keptActions = storm::storage::BitVector(result.model->getTransitionMatrix().getRowCount(), true); @@ -67,13 +67,13 @@ namespace storm { result.newToOldStateIndexMapping.reserve(subsystemStateCount); result.keptActions = storm::storage::BitVector(originalModel.getTransitionMatrix().getRowCount(), false); - for(auto subsysState : subsystemStates) { + for (auto subsysState : subsystemStates) { result.newToOldStateIndexMapping.push_back(subsysState); bool stateHasOneChoiceLeft = false; - for(uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) { + for (uint_fast64_t row = subsystemActions.getNextSetIndex(originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState]); row < originalModel.getTransitionMatrix().getRowGroupIndices()[subsysState+1]; row = subsystemActions.getNextSetIndex(row+1)) { bool allRowEntriesStayInSubsys = true; - for(auto const& entry : originalModel.getTransitionMatrix().getRow(row)) { - if(!subsystemStates.get(entry.getColumn())) { + for (auto const& entry : originalModel.getTransitionMatrix().getRow(row)) { + if (!subsystemStates.get(entry.getColumn())) { allRowEntriesStayInSubsys = false; break; } @@ -85,19 +85,15 @@ namespace storm { } // Transform the ingedients of the model - storm::storage::SparseMatrix matrix = transformMatrix(originalModel.getTransitionMatrix(), subsystemStates, result.keptActions); - storm::models::sparse::StateLabeling labeling(matrix.getRowGroupCount()); - for(auto const& label : originalModel.getStateLabeling().getLabels()){ - storm::storage::BitVector newBitVectorForLabel = transformStateBitVector(originalModel.getStateLabeling().getStates(label), subsystemStates); - labeling.addLabel(label, std::move(newBitVectorForLabel)); - } + storm::storage::SparseMatrix matrix = originalModel.getTransitionMatrix().getSubmatrix(false, result.keptActions, subsystemStates); + storm::models::sparse::StateLabeling labeling = originalModel.getStateLabeling().getSubLabeling(subsystemStates); std::unordered_map rewardModels; - for(auto const& rewardModel : originalModel.getRewardModels()){ + for (auto const& rewardModel : originalModel.getRewardModels()){ rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, result.keptActions))); } - boost::optional> choiceLabeling; - if(originalModel.hasChoiceLabeling()){ - choiceLabeling = transformActionValueVector(originalModel.getChoiceLabeling(), result.keptActions); + boost::optional choiceLabeling; + if (originalModel.hasChoiceLabeling()) { + choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(result.keptActions); } result.model = std::make_shared(createTransformedModel(originalModel, subsystemStates, matrix, labeling, rewardModels, choiceLabeling)); STORM_LOG_DEBUG("Subsystem Builder is done. Resulting model has " << result.model->getNumberOfStates() << " states."); @@ -111,49 +107,18 @@ namespace storm { boost::optional> stateRewardVector; boost::optional> stateActionRewardVector; boost::optional> transitionRewardMatrix; - if(originalRewardModel.hasStateRewards()){ - stateRewardVector = transformStateValueVector(originalRewardModel.getStateRewardVector(), subsystem); + if (originalRewardModel.hasStateRewards()){ + stateRewardVector = storm::utility::vector::filterVector(originalRewardModel.getStateRewardVector(), subsystem); } - if(originalRewardModel.hasStateActionRewards()){ - stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), subsystemActions); + if (originalRewardModel.hasStateActionRewards()){ + stateActionRewardVector = storm::utility::vector::filterVector(originalRewardModel.getStateActionRewardVector(), subsystemActions); } - if(originalRewardModel.hasTransitionRewards()){ - transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), subsystem, subsystemActions); + if (originalRewardModel.hasTransitionRewards()){ + transitionRewardMatrix = originalRewardModel.getTransitionRewardMatrix().getSubmatrix(false, subsystemActions, subsystem); } return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix)); } - template - static storm::storage::SparseMatrix transformMatrix(storm::storage::SparseMatrix const& originalMatrix, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& subsystemActions) { - return originalMatrix.getSubmatrix(false, subsystemActions, subsystem); - } - - - template - static std::vector transformActionValueVector(std::vector const& originalVector, storm::storage::BitVector const& subsystemActions) { - std::vector v; - v.reserve(subsystemActions.getNumberOfSetBits()); - for(auto action : subsystemActions){ - v.push_back(originalVector[action]); - } - return v; - } - - template - static std::vector transformStateValueVector(std::vector const& originalVector, storm::storage::BitVector const& subsystem) { - std::vector v; - v.reserve(subsystem.getNumberOfSetBits()); - for(auto state : subsystem){ - v.push_back(originalVector[state]); - } - return v; - } - - static storm::storage::BitVector transformStateBitVector(storm::storage::BitVector const& originalBitVector, storm::storage::BitVector const& subsystem) { - return originalBitVector % subsystem; - } - - template static typename std::enable_if< std::is_same>::value || @@ -165,7 +130,7 @@ namespace storm { storm::storage::SparseMatrix& matrix, storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map& rewardModels, - boost::optional>& choiceLabeling ) { + boost::optional& choiceLabeling ) { return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); } @@ -179,13 +144,12 @@ namespace storm { storm::models::sparse::StateLabeling& stateLabeling, std::unordered_map& rewardModels, - boost::optional>& choiceLabeling ) { - storm::storage::BitVector markovianStates = transformStateBitVector(originalModel.getMarkovianStates(), subsystem); - std::vector exitRates = transformStateValueVector(originalModel.getExitRates(), subsystem); + boost::optional& choiceLabeling ) { + storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % subsystem; + std::vector exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), subsystem); return MT(std::move(matrix), std::move(stateLabeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels), std::move(choiceLabeling)); } - }; } } diff --git a/src/storm/utility/ModelInstantiator.h b/src/storm/utility/ModelInstantiator.h index 4af867c35..d784c49ea 100644 --- a/src/storm/utility/ModelInstantiator.h +++ b/src/storm/utility/ModelInstantiator.h @@ -103,7 +103,7 @@ namespace storm { initializeModelSpecificData(PMT const& parametricModel) { auto player1MatrixCopy = parametricModel.getPlayer1Matrix(); auto stateLabelingCopy = parametricModel.getStateLabeling(); - boost::optional> player1ChoiceLabeling, player2ChoiceLabeling; + boost::optional player1ChoiceLabeling, player2ChoiceLabeling; if(parametricModel.hasPlayer1ChoiceLabeling()) player1ChoiceLabeling = parametricModel.getPlayer1ChoiceLabeling(); if(parametricModel.hasPlayer2ChoiceLabeling()) player2ChoiceLabeling = parametricModel.getPlayer2ChoiceLabeling(); this->instantiatedModel = std::make_shared(std::move(player1MatrixCopy), buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(player1ChoiceLabeling), std::move(player2ChoiceLabeling)); diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h index 12cb9bb03..19848b6b0 100644 --- a/src/storm/utility/counterexamples.h +++ b/src/storm/utility/counterexamples.h @@ -4,29 +4,30 @@ #include #include +#include "storm/storage/sparse/PrismChoiceOrigins.h" + namespace storm { namespace utility { namespace counterexamples { /*! - * Computes a set of action labels that is visited along all paths from any state to a target state. + * Computes a set of Prism commands that is executed along all paths from any state to a target state. * - * @return The set of action labels that is visited on all paths from any state to a target state. + * @return The set of Prism commands that is visited on all paths from any state to a target state. */ template - std::vector> getGuaranteedLabelSets(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + std::vector> getGuaranteedCommandSets(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantCommands) { // Get some data from the MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = labeledMdp.getNondeterministicChoiceIndices(); - std::vector> const& choiceLabeling = labeledMdp.getChoiceLabeling(); - storm::storage::SparseMatrix backwardTransitions = labeledMdp.getBackwardTransitions(); + storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); + storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); - // Now we compute the set of labels that is present on all paths from the initial to the target states. - std::vector> analysisInformation(labeledMdp.getNumberOfStates(), relevantLabels); + // Now we compute the set of commands that is present on all paths from the initial to the target states. + std::vector> analysisInformation(mdp.getNumberOfStates(), relevantCommands); std::queue worklist; - storm::storage::BitVector statesInWorkList(labeledMdp.getNumberOfStates()); - storm::storage::BitVector markedStates(labeledMdp.getNumberOfStates()); + storm::storage::BitVector statesInWorkList(mdp.getNumberOfStates()); + storm::storage::BitVector markedStates(mdp.getNumberOfStates()); // Initially, put all predecessors of target states in the worklist and empty the analysis information them. for (auto state : psiStates) { @@ -60,13 +61,13 @@ namespace storm { // If we can reach the target state with this choice, we need to intersect the current // analysis information with the union of the new analysis information of the target state - // and the choice labels. + // and the choice commands. if (modifiedChoice) { for (auto const& entry : transitionMatrix.getRow(currentChoice)) { if (markedStates.get(entry.getColumn())) { boost::container::flat_set tmpIntersection; std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceLabeling[currentChoice].begin(), choiceLabeling[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), choiceOrigins.getCommandSet(currentChoice).begin(), choiceOrigins.getCommandSet(currentChoice).end(), std::inserter(tmpIntersection, tmpIntersection.begin())); analysisInformation[currentState] = std::move(tmpIntersection); } } @@ -96,22 +97,22 @@ namespace storm { } /*! - * Computes a set of action labels that is visited along all paths from an initial state to a target state. + * Computes a set of prism commands that is executed along all paths from an initial state to a target state. * - * @return The set of action labels that is visited on all paths from an initial state to a target state. + * @return The set of prism commands that is executed on all paths from an initial state to a target state. */ template - boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(labeledMdp, psiStates, relevantLabels); + boost::container::flat_set getGuaranteedCommandSet(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantCommands) { + std::vector> guaranteedCommands = getGuaranteedCommandSets(mdp, choiceOrigins, psiStates, relevantCommands); - boost::container::flat_set knownLabels(relevantLabels); + boost::container::flat_set knownCommands(relevantCommands); boost::container::flat_set tempIntersection; - for (auto initialState : labeledMdp.getInitialStates()) { - std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); - std::swap(knownLabels, tempIntersection); + for (auto initialState : mdp.getInitialStates()) { + std::set_intersection(knownCommands.begin(), knownCommands.end(), guaranteedCommands[initialState].begin(), guaranteedCommands[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); + std::swap(knownCommands, tempIntersection); } - return knownLabels; + return knownCommands; } } // namespace counterexample diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 7d296d04d..b07c1f439 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -86,7 +86,7 @@ #include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h" // Headers for counterexample generation. -#include "storm/counterexamples/MILPMinimalLabelSetGenerator.h" +#include "storm/counterexamples/MILPMinimalCommandSetGenerator.h" #include "storm/counterexamples/SMTMinimalCommandSetGenerator.h" // Headers related to model building. @@ -135,18 +135,19 @@ namespace storm { std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); template - std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + storm::builder::ExplicitModelBuilderResult buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { storm::builder::BuilderOptions options(formulas); if (storm::settings::getModule().isBuildFullModelSet()) { options.setBuildAllLabels(); options.setBuildAllRewardModels(); + options.setBuildChoiceLabels(true); options.clearTerminalStates(); } // Generate command labels if we are going to build a counterexample later. if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { - options.setBuildChoiceLabels(true); + options.setBuildChoiceOrigins(true); } if (storm::settings::getModule().isJitSet()) { @@ -171,7 +172,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Cannot build sparse model from this symbolic model description."); } storm::builder::ExplicitModelBuilder builder(generator); - return builder.build().getModel(); + return builder.build(); } } @@ -259,6 +260,7 @@ namespace storm { ma->close(); if (ma->hasOnlyTrivialNondeterminism()) { // Markov automaton can be converted into CTMC. + STORM_PRINT_AND_LOG(std::endl << "Converting deterministic MA to a CTMC..." << std::endl); model = ma->convertToCTMC(); } } @@ -285,7 +287,7 @@ namespace storm { } template - void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr const& formula) { + void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr choiceOrigins, std::shared_ptr const& formula) { if (storm::settings::getModule().isMinimalCommandSetGenerationSet()) { STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for PRISM models."); STORM_LOG_THROW(markovModel->getType() == storm::models::ModelType::Mdp, storm::exceptions::InvalidTypeException, "Minimal command set generation is only available for MDPs."); @@ -297,9 +299,9 @@ namespace storm { bool useMILP = storm::settings::getModule().isUseMilpBasedMinimalCommandSetGenerationSet(); if (useMILP) { - storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formula); + storm::counterexamples::MILPMinimalCommandSetGenerator::computeCounterexample(program, *mdp, choiceOrigins, formula); } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, formula); + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, choiceOrigins, formula); } } else { @@ -309,20 +311,20 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { + inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr, std::shared_ptr const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for exact arithmetic model."); } template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr const& ) { + inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr, std::shared_ptr const& ) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model."); } #endif template - void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::vector> const& formulas) { + void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr choiceOrigins, std::vector> const& formulas) { for (auto const& formula : formulas) { - generateCounterexample(model, markovModel, formula); + generateCounterexample(model, markovModel, choiceOrigins, formula); } } diff --git a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp b/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp index 99211ecc7..b4b87e958 100644 --- a/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp +++ b/src/test/builder/ExplicitJitJaniModelBuilderTest.cpp @@ -14,31 +14,31 @@ TEST(ExplicitJitJaniModelBuilderTest, Dtmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(13ul, model->getNumberOfStates()); EXPECT_EQ(20ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/brp-16-2.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(677ul, model->getNumberOfStates()); EXPECT_EQ(867ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-5-5.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(273ul, model->getNumberOfStates()); EXPECT_EQ(397ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/nand-5-2.pm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(1728ul, model->getNumberOfStates()); EXPECT_EQ(2505ul, model->getNumberOfTransitions()); } @@ -50,31 +50,31 @@ TEST(ExplicitJitJaniModelBuilderTest, Ctmc) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/cluster2.sm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(276ul, model->getNumberOfStates()); EXPECT_EQ(1120ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/embedded2.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(3478ul, model->getNumberOfStates()); EXPECT_EQ(14639ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/polling2.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(22ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/fms2.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(810ul, model->getNumberOfStates()); EXPECT_EQ(3699ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ctmc/tandem5.sm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(66ul, model->getNumberOfStates()); EXPECT_EQ(189ul, model->getNumberOfTransitions()); } @@ -83,37 +83,37 @@ TEST(ExplicitJitJaniModelBuilderTest, Mdp) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(169ul, model->getNumberOfStates()); EXPECT_EQ(436ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(364ul, model->getNumberOfStates()); EXPECT_EQ(654ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(272ul, model->getNumberOfStates()); EXPECT_EQ(492ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(1038ul, model->getNumberOfStates()); EXPECT_EQ(1282ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/firewire3-0.5.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(4093ul, model->getNumberOfStates()); EXPECT_EQ(5585ul, model->getNumberOfTransitions()); program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0-2-2.nm"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(37ul, model->getNumberOfStates()); EXPECT_EQ(59ul, model->getNumberOfTransitions()); } @@ -122,7 +122,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/simple.ma"); storm::jani::Model janiModel = program.toJani(); - std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + std::shared_ptr> model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(8ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -130,7 +130,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/hybrid_states.ma"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(5ul, model->getNumberOfStates()); EXPECT_EQ(13ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -138,7 +138,7 @@ TEST(ExplicitJitJaniModelBuilderTest, Ma) { program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); janiModel = program.toJani(); - model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(); + model = storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();; EXPECT_EQ(12ul, model->getNumberOfStates()); EXPECT_EQ(14ul, model->getNumberOfTransitions()); ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); @@ -149,7 +149,7 @@ TEST(ExplicitJitJaniModelBuilderTest, FailComposition) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/system_composition.nm"); storm::jani::Model janiModel = program.toJani(); - ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build(), storm::exceptions::WrongFormatException); + ASSERT_THROW(storm::builder::jit::ExplicitJitJaniModelBuilder(janiModel).build().getModel();, storm::exceptions::WrongFormatException); } TEST(ExplicitJitJaniModelBuilderTest, IllegalSynchronizingWrites) { diff --git a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp index 0314c3e56..c6a13347c 100644 --- a/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseDtmcParameterLiftingTest.cpp @@ -17,7 +17,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -47,7 +47,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -77,7 +77,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -108,7 +108,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Prob_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -141,7 +141,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -174,7 +174,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Bounded_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -207,7 +207,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_Infty) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -233,7 +233,7 @@ TEST(SparseDtmcParameterLiftingTest, Brp_Rew_4Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -264,7 +264,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -297,7 +297,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_stepBounded) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -331,7 +331,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_1Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -362,7 +362,7 @@ TEST(SparseDtmcParameterLiftingTest, Crowds_Prob_Const) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); diff --git a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp index 8ba599bde..e1390e171 100644 --- a/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMaPcaaModelCheckerTest.cpp @@ -56,7 +56,7 @@ TEST(SparseMaPcaaModelCheckerTest, server) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); @@ -85,7 +85,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_3Obj) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); @@ -116,7 +116,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_achievability_3Obj) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); @@ -137,7 +137,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_quantitative_3Obj) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *ma->getInitialStates().begin(); @@ -158,7 +158,7 @@ TEST(SparseMaPcaaModelCheckerTest, jobscheduler_pareto_2Obj) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> ma = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> ma = storm::buildSparseModel(program, formulas).getModel()->as>(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*ma, formulas[0]->asMultiObjectiveFormula()); ASSERT_TRUE(result->isExplicitParetoCurveCheckResult()); diff --git a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp index 81832d240..59f1eb9f4 100644 --- a/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp +++ b/src/test/modelchecker/SparseMdpParameterLiftingTest.cpp @@ -16,7 +16,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -46,7 +46,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -76,7 +76,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -106,7 +106,7 @@ TEST(SparseMdpParameterLiftingTest, two_dice_Prob_bounded_exactValidation) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaFile, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -134,7 +134,7 @@ TEST(SparseMdpParameterLiftingTest, coin_Prob) { storm::prism::Program program = storm::parseProgram(programFile); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -164,7 +164,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Prop) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -195,7 +195,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -225,7 +225,7 @@ TEST(SparseMdpParameterLiftingTest, brp_Rew_bounded) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -256,7 +256,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_Infty) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); @@ -282,7 +282,7 @@ TEST(SparseMdpParameterLiftingTest, Brp_Rew_4Par) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, constantsAsString); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulaAsString, program)); - std::shared_ptr> model = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> model = storm::buildSparseModel(program, formulas).getModel()->as>(); auto modelParameters = storm::models::sparse::getProbabilityParameters(*model); auto rewParameters = storm::models::sparse::getRewardParameters(*model); diff --git a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp index 369a768ac..8fc87d315 100644 --- a/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp +++ b/src/test/modelchecker/SparseMdpPcaaModelCheckerTest.cpp @@ -23,7 +23,7 @@ TEST(SparseMdpPcaaModelCheckerTest, consensus) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin();; std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); @@ -49,7 +49,7 @@ TEST(SparseMdpPcaaModelCheckerTest, zeroconf) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); @@ -66,7 +66,7 @@ TEST(SparseMdpPcaaModelCheckerTest, team3with3objectives) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); @@ -83,7 +83,7 @@ TEST(SparseMdpPcaaModelCheckerTest, scheduler) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula()); @@ -99,7 +99,7 @@ TEST(SparseMdpPcaaModelCheckerTest, dpm) { storm::prism::Program program = storm::parseProgram(programFile); program = storm::utility::prism::preprocess(program, ""); std::vector> formulas = storm::extractFormulasFromProperties(storm::parsePropertiesForPrismProgram(formulasAsString, program)); - std::shared_ptr> mdp = storm::buildSparseModel(program, formulas)->as>(); + std::shared_ptr> mdp = storm::buildSparseModel(program, formulas).getModel()->as>(); uint_fast64_t const initState = *mdp->getInitialStates().begin(); std::unique_ptr result = storm::modelchecker::multiobjective::performPcaa(*mdp, formulas[0]->asMultiObjectiveFormula());