diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp index 1a3feb96b..5add225ce 100644 --- a/src/storm/builder/ExplicitModelBuilder.cpp +++ b/src/storm/builder/ExplicitModelBuilder.cpp @@ -33,8 +33,9 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/ConstantsComparator.h" -#include "storm/exceptions/WrongFormatException.h" +#include "storm/utility/builder.h" +#include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidOperationException.h" @@ -42,12 +43,7 @@ namespace storm { namespace builder { template - ExplicitModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { - // Intentionally left empty. - } - - template - ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()), buildStateValuations(false) { + ExplicitModelBuilder::Options::Options() : explorationOrder(storm::settings::getModule().getExplorationOrder()) { // Intentionally left empty. } @@ -67,30 +63,23 @@ namespace storm { } template - ExplicitModelBuilderResult ExplicitModelBuilder::build() { + std::shared_ptr> ExplicitModelBuilder::build() { STORM_LOG_DEBUG("Exploration order is: " << options.explorationOrder); - ModelComponents modelComponents = buildModelComponents(); - std::shared_ptr> resultModel; switch (generator->getModelType()) { case storm::generator::ModelType::DTMC: - resultModel = std::shared_ptr>(new storm::models::sparse::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); - break; + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Dtmc, buildModelComponents()); case storm::generator::ModelType::CTMC: - resultModel = std::shared_ptr>(new storm::models::sparse::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); - break; + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Ctmc, buildModelComponents()); case storm::generator::ModelType::MDP: - resultModel = std::shared_ptr>(new storm::models::sparse::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); - break; + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::Mdp, buildModelComponents()); case storm::generator::ModelType::MA: - resultModel = std::shared_ptr>(new storm::models::sparse::MarkovAutomaton(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), *std::move(modelComponents.markovianStates), std::move(modelComponents.rewardModels), std::move(modelComponents.choiceLabeling))); - break; + return storm::utility::builder::buildModelFromComponents(storm::models::ModelType::MarkovAutomaton, buildModelComponents()); default: STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Error while creating model: cannot handle this model type."); - break; } - return ExplicitModelBuilderResult(resultModel, modelComponents.stateValuations, modelComponents.choiceOrigins); + return nullptr; } template @@ -278,32 +267,30 @@ namespace storm { } template - typename ExplicitModelBuilder::ModelComponents ExplicitModelBuilder::buildModelComponents() { - ModelComponents modelComponents; - + storm::storage::sparse::ModelComponents ExplicitModelBuilder::buildModelComponents() { + // Determine whether we have to combine different choices to one or whether this model can have more than // one choice per state. bool deterministicModel = generator->isDeterministicModel(); - // Prepare the transition matrix builder and the reward model builders. + // Prepare the component builders storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, 0, 0, false, !deterministicModel, 0); std::vector> rewardModelBuilders; for (uint64_t i = 0; i < generator->getNumberOfRewardModels(); ++i) { rewardModelBuilders.emplace_back(generator->getRewardModelInformation(i)); } - ChoiceInformationBuilder choiceInformationBuilder; - buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, modelComponents.markovianStates); - modelComponents.transitionMatrix = transitionMatrixBuilder.build(); + boost::optional markovianStates; + + buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates); + + // initialize the model components with the obtained information. + storm::storage::sparse::ModelComponents modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map(), !generator->isDiscreteTimeModel(), std::move(markovianStates)); // Now finalize all reward models. for (auto& rewardModelBuilder : rewardModelBuilders) { modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount())); } - - // Build the state labeling. - modelComponents.stateLabeling = buildStateLabeling(); - // Build the choice labeling modelComponents.choiceLabeling = choiceInformationBuilder.buildChoiceLabeling(modelComponents.transitionMatrix.getRowCount()); @@ -315,8 +302,10 @@ namespace storm { } modelComponents.stateValuations = storm::storage::sparse::StateValuations(std::move(valuations)); } - auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount()); - modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData); + if (generator->getOptions().isBuildChoiceOriginsSet()) { + auto originData = choiceInformationBuilder.buildDataOfChoiceOrigins(modelComponents.transitionMatrix.getRowCount()); + modelComponents.choiceOrigins = generator->generateChoiceOrigins(originData); + } return modelComponents; } diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index aa64be986..501111673 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -20,14 +20,13 @@ #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/ChoiceLabeling.h" #include "storm/storage/SparseMatrix.h" -#include "storm/storage/sparse/ChoiceOrigins.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/storage/sparse/StateStorage.h" #include "storm/settings/SettingsManager.h" #include "storm/utility/prism.h" #include "storm/builder/ExplorationOrder.h" -#include "storm/builder/ExplicitModelBuilderResult.h" #include "storm/generator/NextStateGenerator.h" #include "storm/generator/CompressedState.h" @@ -50,32 +49,6 @@ namespace storm { template, typename StateType = uint32_t> class ExplicitModelBuilder { public: - // A structure holding the individual components of a model. - struct ModelComponents { - ModelComponents(); - - // The transition matrix. - storm::storage::SparseMatrix transitionMatrix; - - // The state labeling. - storm::models::sparse::StateLabeling stateLabeling; - - // The reward models associated with the model. - std::unordered_map> rewardModels; - - // A vector that stores a labeling for each choice. - boost::optional choiceLabeling; - - // A vector that stores which states are markovian. - boost::optional markovianStates; - - // If generated, stores for each state to which variable valuation it belongs - boost::optional stateValuations; - - // If generated, stores for each choice from which parts of the input model description it originates - boost::optional> choiceOrigins; - - }; struct Options { /*! @@ -115,7 +88,7 @@ namespace storm { * @return The explicit model that was given by the probabilistic program as well as additional * information (if requested). */ - ExplicitModelBuilderResult build(); + std::shared_ptr> build(); private: /*! @@ -144,7 +117,7 @@ namespace storm { * * @return A structure containing the components of the resulting model. */ - ModelComponents buildModelComponents(); + storm::storage::sparse::ModelComponents buildModelComponents(); /*! * Builds the state labeling for the given program. diff --git a/src/storm/builder/ExplicitModelBuilderResult.cpp b/src/storm/builder/ExplicitModelBuilderResult.cpp deleted file mode 100644 index 330be5aee..000000000 --- a/src/storm/builder/ExplicitModelBuilderResult.cpp +++ /dev/null @@ -1,78 +0,0 @@ -#include "storm/builder/ExplicitModelBuilderResult.h" - -#include "storm/utility/macros.h" -#include "storm/exceptions/InvalidOperationException.h" - -#include "storm/adapters/CarlAdapter.h" -#include "storm/models/sparse/StandardRewardModel.h" - -namespace storm { - namespace builder { - - template - 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() { - STORM_LOG_THROW(model, storm::exceptions::InvalidOperationException, "Retrieving the model failed since it is not set."); - return model; - } - - template - std::shared_ptr> const& ExplicitModelBuilderResult::getModel() const { - STORM_LOG_THROW(model, storm::exceptions::InvalidOperationException, "Retrieving the model failed since it is not set."); - return model; - } - - template - bool ExplicitModelBuilderResult::hasStateValuations() { - return static_cast(stateValuations); - } - - template - std::shared_ptr& ExplicitModelBuilderResult::getStateValuations() { - STORM_LOG_THROW(stateValuations, storm::exceptions::InvalidOperationException, "Retrieving the state valuations failed since they are not set."); - return stateValuations; - } - - template - std::shared_ptr const& ExplicitModelBuilderResult::getStateValuations() const { - STORM_LOG_THROW(stateValuations, storm::exceptions::InvalidOperationException, "Retrieving the state valuations failed since they are not set."); - return stateValuations; - } - - template - bool ExplicitModelBuilderResult::hasChoiceOrigins() { - return static_cast(choiceOrigins); - } - - template - std::shared_ptr& ExplicitModelBuilderResult::getChoiceOrigins() { - STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidOperationException, "Retrieving the choice origins failed since they are not set."); - return choiceOrigins; - } - - template - std::shared_ptr const& ExplicitModelBuilderResult::getChoiceOrigins() const { - STORM_LOG_THROW(choiceOrigins, storm::exceptions::InvalidOperationException, "Retrieving the choice origins failed since they are not set."); - return choiceOrigins; - } - - // Explicitly instantiate the class. - template class ExplicitModelBuilderResult>; - -#ifdef STORM_HAVE_CARL - template class ExplicitModelBuilderResult>; - template class ExplicitModelBuilderResult>; - template class ExplicitModelBuilderResult>; -#endif - - } -} \ No newline at end of file diff --git a/src/storm/builder/ExplicitModelBuilderResult.h b/src/storm/builder/ExplicitModelBuilderResult.h deleted file mode 100644 index ad1f4111b..000000000 --- a/src/storm/builder/ExplicitModelBuilderResult.h +++ /dev/null @@ -1,34 +0,0 @@ -#pragma once - -#include -#include "storm/models/sparse/Model.h" -#include "storm/storage/sparse/StateValuations.h" -#include "storm/storage/sparse/ChoiceOrigins.h" - -namespace storm { - namespace builder { - - template> - class ExplicitModelBuilderResult { - public: - 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; - - bool hasStateValuations(); - std::shared_ptr& getStateValuations(); - std::shared_ptr const& getStateValuations() const; - - bool hasChoiceOrigins(); - std::shared_ptr& getChoiceOrigins(); - std::shared_ptr const& getChoiceOrigins() const; - - private: - std::shared_ptr> model; - std::shared_ptr stateValuations; - std::shared_ptr choiceOrigins; - }; - } -} \ No newline at end of file diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index 379f15412..b053e201c 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -15,6 +15,7 @@ #include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/jani/CompositionInformationVisitor.h" + #include "storm/builder/RewardModelInformation.h" #include "storm/models/sparse/Dtmc.h" @@ -134,7 +135,7 @@ namespace storm { stream << "."; STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " + stream.str()); } - + #ifdef STORM_HAVE_CARL else if (std::is_same::value && !this->model.undefinedConstantsAreGraphPreserving()) { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); @@ -142,7 +143,7 @@ namespace storm { #endif //STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition"); - // Comment this in to print the JANI model for debugging purposes. + // Comment this in to print the JANI model for debugging purposes. // this->model.makeStandardJaniCompliant(); // storm::jani::JsonExporter::toStream(this->model, std::vector>(), std::cout, false); } @@ -230,7 +231,7 @@ namespace storm { return result; } - + template bool ExplicitJitJaniModelBuilder::checkCompilerFlagsWork() const { bool result = true; @@ -238,7 +239,7 @@ namespace storm { try { std::string emptyProgram = R"( #include - + int main() { return 0; } @@ -249,7 +250,7 @@ namespace storm { outputFile += ".out"; std::string outputFilename = boost::filesystem::absolute(outputFile).string(); boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -o " + outputFilename); - + if (error) { result = false; STORM_LOG_ERROR(problem); @@ -261,7 +262,7 @@ namespace storm { result = false; STORM_LOG_ERROR(problem); } - + return result; } @@ -272,7 +273,7 @@ namespace storm { try { std::string program = R"( #include - + int main() { return 0; } @@ -283,7 +284,7 @@ namespace storm { outputFile += ".out"; std::string outputFilename = boost::filesystem::absolute(outputFile).string(); boost::optional error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + boostIncludeDirectory + " -o " + outputFilename); - + if (error) { result = false; STORM_LOG_ERROR(problem); @@ -297,7 +298,7 @@ namespace storm { } return result; } - + template bool ExplicitJitJaniModelBuilder::checkBoostDllAvailable() const { bool result = true; @@ -330,7 +331,7 @@ namespace storm { } return result; } - + template bool ExplicitJitJaniModelBuilder::checkStormHeadersAvailable() const { bool result = true; @@ -364,7 +365,7 @@ namespace storm { } return result; } - + template bool ExplicitJitJaniModelBuilder::checkCarlAvailable() const { bool result = true; @@ -457,7 +458,7 @@ namespace storm { } template - storm::builder::ExplicitModelBuilderResult ExplicitJitJaniModelBuilder::build() { + std::shared_ptr> ExplicitJitJaniModelBuilder::build() { // (0) Assemble information about the model. cpptempl::data_map modelData = generateModelData(); @@ -505,7 +506,7 @@ namespace storm { STORM_LOG_THROW(!error, storm::exceptions::WrongFormatException, "Model building failed. Reason: " << error.get()); // Return the constructed model. - return storm::builder::ExplicitModelBuilderResult(sparseModel); + return sparseModel; } template diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h index 6b291ffde..65321ad9f 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.h @@ -17,8 +17,6 @@ #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 { @@ -59,7 +57,7 @@ namespace storm { /*! * Builds and returns the sparse model. */ - storm::builder::ExplicitModelBuilderResult build(); + std::shared_ptr> build(); /*! * Performs some checks that can help debug why the model builder does not work. Returns true if the diff --git a/src/storm/builder/jit/ModelComponentsBuilder.cpp b/src/storm/builder/jit/ModelComponentsBuilder.cpp index 752ab9b31..ec07e80f7 100644 --- a/src/storm/builder/jit/ModelComponentsBuilder.cpp +++ b/src/storm/builder/jit/ModelComponentsBuilder.cpp @@ -133,17 +133,7 @@ namespace storm { } else if (modelType == storm::jani::ModelType::MDP || modelType == storm::jani::ModelType::LTS) { return new storm::models::sparse::Mdp>(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels)); } else if (modelType == storm::jani::ModelType::MA) { - std::vector exitRates(transitionMatrix.getRowGroupCount(), storm::utility::zero()); - for (auto state : *markovianStates) { - for (auto const& element : transitionMatrix.getRow(transitionMatrix.getRowGroupIndices()[state])) { - exitRates[state] += element.getValue(); - } - for (auto& element : transitionMatrix.getRow(transitionMatrix.getRowGroupIndices()[state])) { - element.setValue(element.getValue() / exitRates[state]); - } - } - - return new storm::models::sparse::MarkovAutomaton>(std::move(transitionMatrix), std::move(stateLabeling), std::move(*markovianStates), std::move(exitRates), std::move(rewardModels)); + return new storm::models::sparse::MarkovAutomaton>(std::move(transitionMatrix), std::move(stateLabeling), std::move(*markovianStates), std::move(rewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Model type unsupported by JIT builder."); } diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index 25be46969..7f385cd57 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -311,27 +311,21 @@ namespace storm { auto formulas = extractFormulasFromProperties(properties); // Start by building the model. storm::utility::Stopwatch modelBuildingWatch(true); - storm::builder::ExplicitModelBuilderResult builderResult = buildSparseModel(model, formulas); + std::shared_ptr markovModel = buildSparseModel(model, formulas); + STORM_LOG_THROW(markovModel, storm::exceptions::UnexpectedException, "The model was not successfully built."); modelBuildingWatch.stop(); STORM_PRINT_AND_LOG("Time for model construction: " << modelBuildingWatch << "." << std::endl << std::endl); - // 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, builderResult.getChoiceOrigins(), formulas); + generateCounterexamples(model, sparseModel, 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/MILPMinimalCommandSetGenerator.h b/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h index adcf204b6..43648af82 100644 --- a/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/MILPMinimalCommandSetGenerator.h @@ -116,11 +116,12 @@ namespace storm { * @return A structure that stores the relevant and problematic choices in the model as well as the set * of relevant commands. */ - static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { + static struct ChoiceInformation determineRelevantAndProblematicChoices(storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, storm::storage::BitVector const& psiStates) { // Create result and shortcuts to needed data for convenience. ChoiceInformation result; storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Now traverse all choices of all relevant states and check whether there is a relevant target state. // If so, the associated commands become relevant. Also, if a choice of relevant state has at least one @@ -158,7 +159,7 @@ namespace storm { } // Finally, determine the set of commands that are known to be taken. - result.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, choiceOrigins, psiStates, result.allRelevantCommands); + result.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, psiStates, result.allRelevantCommands); STORM_LOG_DEBUG("Found " << result.allRelevantCommands.size() << " relevant commands and " << result.knownCommands.size() << " known commands."); return result; @@ -480,7 +481,9 @@ namespace storm { * @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 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) { + static uint_fast64_t assertChoicesImplyCommands(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, StateInformation const& stateInformation, ChoiceInformation const& choiceInformation, VariableInformation const& variableInformation) { + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); + uint_fast64_t numberOfConstraintsCreated = 0; for (auto state : stateInformation.relevantStates) { @@ -807,7 +810,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& 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) { + static void buildConstraintSystem(storm::solver::LpSolver& solver, storm::models::sparse::Mdp const& mdp, 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."); @@ -817,7 +820,7 @@ namespace storm { STORM_LOG_DEBUG("Asserted that policy is valid."); // Add constraints that assert the commands that belong to some taken choices are taken as well. - numberOfConstraints += assertChoicesImplyCommands(solver, mdp, choiceOrigins, stateInformation, choiceInformation, variableInformation); + numberOfConstraints += assertChoicesImplyCommands(solver, mdp, 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 @@ -917,13 +920,10 @@ namespace storm { } public: - 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) { + static boost::container::flat_set getMinimalCommandSet(storm::models::sparse::Mdp const& mdp, 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(); - + STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origns."); + STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; @@ -941,7 +941,7 @@ namespace storm { StateInformation stateInformation = determineRelevantAndProblematicStates(mdp, phiStates, psiStates); // (3) Determine sets of relevant commands and problematic choices. - ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, prismChoiceOrigins, stateInformation, psiStates); + ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(mdp, stateInformation, psiStates); // (4) Encode resulting system as MILP problem. std::shared_ptr solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample"); @@ -950,7 +950,7 @@ namespace storm { VariableInformation variableInformation = createVariables(*solver, mdp, stateInformation, choiceInformation); // (4.2) Construct constraint system. - buildConstraintSystem(*solver, mdp, prismChoiceOrigins, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); + buildConstraintSystem(*solver, mdp, psiStates, stateInformation, choiceInformation, variableInformation, probabilityThreshold, strictBound, includeSchedulerCuts); // (4.3) Optimize the model. solver->optimize(); @@ -967,11 +967,10 @@ namespace storm { * 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 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& mdp, std::shared_ptr const& choiceOrigins, std::shared_ptr const& formula) { + static void computeCounterexample(storm::prism::Program const& program, storm::models::sparse::Mdp const& mdp, 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."); @@ -1012,7 +1011,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - boost::container::flat_set usedCommandSet = getMinimalCommandSet(mdp, choiceOrigins, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); + boost::container::flat_set usedCommandSet = getMinimalCommandSet(mdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isUseSchedulerCutsSet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << usedCommandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h index 3fde5bceb..dd8602baa 100644 --- a/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalCommandSetGenerator.h @@ -85,12 +85,11 @@ namespace storm { * a scheduler that satisfies phi until psi with a nonzero probability. * * @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 commands as well as states. */ - 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) { + static RelevancyInformation determineRelevantStatesAndCommands(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) { // Create result. RelevancyInformation relevancyInformation; @@ -107,6 +106,7 @@ namespace storm { // Retrieve some references for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Now traverse all choices of all relevant states and check whether there is a successor target state. // If so, the associated commands become relevant. Also, if a choice of relevant state has at least one @@ -133,7 +133,7 @@ namespace storm { } // 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); + relevancyInformation.knownCommands = storm::utility::counterexamples::getGuaranteedCommandSet(mdp, 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())); @@ -269,7 +269,7 @@ namespace storm { * @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& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, 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::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { // Walk through the MDP and // * identify commands enabled in initial states // * identify commands that can directly precede a given action @@ -288,6 +288,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); storm::storage::BitVector const& initialStates = mdp.getInitialStates(); storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); for (auto currentState : relevancyInformation.relevantStates) { for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { @@ -546,7 +547,7 @@ 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& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static void assertSymbolicCuts(storm::prism::Program& program, storm::models::sparse::Mdp const& mdp, 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; @@ -556,6 +557,7 @@ namespace storm { // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Compute the set of commands that may precede a given action. for (auto currentState : relevancyInformation.relevantStates) { @@ -888,7 +890,7 @@ 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& mdp, storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins, 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::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."; @@ -897,6 +899,7 @@ namespace storm { // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // 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) @@ -1356,7 +1359,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::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) { + 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) { storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); STORM_LOG_DEBUG("Analyzing solution with zero probability."); @@ -1372,8 +1375,10 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); + storm::storage::sparse::PrismChoiceOrigins const& subChoiceOrigins = subMdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Now determine which states and commands are actually reachable. + boost::container::flat_set reachableCommands; while (!stack.empty()) { uint_fast64_t currentState = stack.back(); @@ -1415,7 +1420,9 @@ namespace storm { 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> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, originalChoiceOrigins, statesThatCanReachTargetStates, locallyRelevantCommands); + storm::storage::sparse::PrismChoiceOrigins const& originalChoiceOrigins = originalMdp.getChoiceOrigins()->asPrismChoiceOrigins(); + + std::vector> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, 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 @@ -1480,7 +1487,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::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) { + 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) { STORM_LOG_DEBUG("Analyzing solution with insufficient probability."); @@ -1496,6 +1503,7 @@ namespace storm { storm::storage::SparseMatrix const& transitionMatrix = subMdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = subMdp.getNondeterministicChoiceIndices(); + storm::storage::sparse::PrismChoiceOrigins const& subChoiceOrigins = subMdp.getChoiceOrigins()->asPrismChoiceOrigins(); // Now determine which states and commands are actually reachable. boost::container::flat_set reachableCommands; @@ -1533,7 +1541,9 @@ namespace storm { 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> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, originalChoiceOrigins, statesThatCanReachTargetStates, locallyRelevantCommands); + storm::storage::sparse::PrismChoiceOrigins const& originalChoiceOrigins = originalMdp.getChoiceOrigins()->asPrismChoiceOrigins(); + + std::vector> guaranteedCommandSets = storm::utility::counterexamples::getGuaranteedCommandSets(originalMdp, statesThatCanReachTargetStates, locallyRelevantCommands); // Search for states for which we could enable another option and possibly improve the reachability probability. std::set> cutCommands; @@ -1578,13 +1588,12 @@ namespace storm { /*! * 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."); + static storm::models::sparse::Mdp restrictMdpToCommandSet(storm::models::sparse::Mdp const& mdp, boost::container::flat_set const& enabledCommands) { + STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origins."); + STORM_LOG_THROW(mdp.getChoiceOrigins()->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::sparse::PrismChoiceOrigins const& prismChoiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); storm::storage::SparseMatrixBuilder transitionMatrixBuilder(0, mdp.getTransitionMatrix().getColumnCount(), 0, true, true, mdp.getTransitionMatrix().getRowGroupCount()); std::vector subMdpChoiceIndexMapping; @@ -1619,10 +1628,10 @@ namespace storm { } } - 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)); + storm::storage::sparse::ModelComponents resultComponents(transitionMatrixBuilder.build()); + resultComponents.stateLabeling = mdp.getStateLabeling(); + resultComponents.choiceOrigins = prismChoiceOrigins.selectChoices(subMdpChoiceIndexMapping); + return storm::models::sparse::Mdp(std::move(resultComponents)); } /*! @@ -1631,7 +1640,6 @@ namespace storm { * @param program The program that was used to build the MDP. * @param constantDefinitionString A string defining the undefined constants in the given program. * @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. @@ -1640,7 +1648,7 @@ 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& 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) { + static boost::container::flat_set getMinimalCommandSet(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { #ifdef STORM_HAVE_Z3 @@ -1661,10 +1669,8 @@ 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_LOG_THROW(mdp.hasChoiceOrigins() && mdp.getChoiceOrigins()->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(); @@ -1683,7 +1689,7 @@ namespace storm { } // (2) Identify all states and commands that are relevant, because only these need to be considered later. - RelevancyInformation relevancyInformation = determineRelevantStatesAndCommands(mdp, prismChoiceOrigins, phiStates, psiStates); + RelevancyInformation relevancyInformation = determineRelevantStatesAndCommands(mdp, phiStates, psiStates); // (3) Create a solver. std::shared_ptr manager(new storm::expressions::ExpressionManager()); @@ -1701,12 +1707,12 @@ namespace storm { // (6) Add constraints that cut off a lot of suboptimal solutions. STORM_LOG_DEBUG("Asserting cuts."); - assertExplicitCuts(mdp, prismChoiceOrigins, psiStates, variableInformation, relevancyInformation, *solver); + assertExplicitCuts(mdp, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted explicit cuts."); - assertSymbolicCuts(preparedProgram, mdp, prismChoiceOrigins, variableInformation, relevancyInformation, *solver); + assertSymbolicCuts(preparedProgram, mdp, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted symbolic cuts."); if (includeReachabilityEncoding) { - assertReachabilityCuts(mdp, prismChoiceOrigins, psiStates, variableInformation, relevancyInformation, *solver); + assertReachabilityCuts(mdp, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } @@ -1735,10 +1741,8 @@ namespace storm { // 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.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::models::sparse::Mdp const& subMdp = restrictMdpToCommandSet(mdp, commandSet); + STORM_LOG_THROW(subMdp.hasChoiceOrigins() && subMdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Expected prism choice origins for submodel."); storm::modelchecker::helper::SparseMdpPrctlHelper modelCheckerHelper; STORM_LOG_DEBUG("Invoking model checker."); @@ -1759,11 +1763,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, subPrismChoiceOrigins, mdp, prismChoiceOrigins, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeZeroProbabilitySolution(*solver, subMdp, mdp, 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, subPrismChoiceOrigins, mdp, prismChoiceOrigins, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeInsufficientProbabilitySolution(*solver, subMdp, mdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); } } else { done = true; @@ -1801,7 +1805,7 @@ namespace storm { #endif } - 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) { + static void computeCounterexample(storm::prism::Program program, std::string const& constantDefinitionString, storm::models::sparse::Mdp const& mdp, std::shared_ptr const& formula) { #ifdef STORM_HAVE_Z3 std::cout << std::endl << "Generating minimal command set counterexample for formula " << *formula << std::endl; @@ -1843,7 +1847,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto commandSet = getMinimalCommandSet(program, constantDefinitionString, mdp, choiceOrigins, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); + auto commandSet = getMinimalCommandSet(program, constantDefinitionString, mdp, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule().isEncodeReachabilitySet()); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal command set of size " << commandSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index b22eb2baa..d52bc742e 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -9,26 +9,42 @@ 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) - : DeterministicModel(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { - exitRates = createExitRateVector(this->getTransitionMatrix()); + std::unordered_map const& rewardModels) + : Ctmc(storm::storage::sparse::ModelComponents(rateMatrix, stateLabeling, rewardModels, true)) { + // Intentionally left empty } template Ctmc::Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, - 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()); + std::unordered_map&& rewardModels) + : Ctmc(storm::storage::sparse::ModelComponents(std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), true)) { + // Intentionally left empty } 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) - : DeterministicModel(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)), exitRates(exitRates) { + Ctmc::Ctmc(storm::storage::sparse::ModelComponents const& components) + : DeterministicModel(storm::models::ModelType::Ctmc, components) { + + if (components.exitRates) { + exitRates = components.exitRates.get(); + } + + if (!components.rateTransitions) { + this->getTransitionMatrix().scaleRowsInPlace(exitRates); + } + } + + template + Ctmc::Ctmc(storm::storage::sparse::ModelComponents&& components) + : DeterministicModel(storm::models::ModelType::Ctmc, std::move(components)) { + + if (components.exitRates) { + exitRates = std::move(components.exitRates.get()); + } + + if (!components.rateTransitions) { + this->getTransitionMatrix().scaleRowsInPlace(exitRates); + } } template diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index 09da1d420..c6afaac16 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -20,36 +20,27 @@ namespace storm { * @param rateMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ 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::none); + std::unordered_map const& rewardModels = std::unordered_map()); /*! * Constructs a model by moving the given data. * - * @param transitionMatrix The matrix representing the transitions in the model. + * @param rateMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Ctmc(storm::storage::SparseMatrix&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); + std::unordered_map&& rewardModels = std::unordered_map()); /*! * Constructs a model from the given data. * - * @param rateMatrix The matrix representing the transitions in the model. - * @param exitRates The exit rates of all states. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + * @param components The components for this model. */ - 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::none); + Ctmc(storm::storage::sparse::ModelComponents const& components); + Ctmc(storm::storage::sparse::ModelComponents&& components); Ctmc(Ctmc const& ctmc) = default; diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 2cc082fac..836141891 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -6,24 +6,17 @@ namespace storm { namespace models { namespace sparse { + template - DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, - boost::optional const& optionalChoiceLabeling) - : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { - // Intentionally left empty. + DeterministicModel::DeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components) + : Model(modelType, components) { + // Intentionally left empty } template - DeterministicModel::DeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, - boost::optional&& optionalChoiceLabeling) - : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), std::move(optionalChoiceLabeling)) { - // Intentionally left empty. + DeterministicModel::DeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components) + : Model(modelType, std::move(components)) { + // Intentionally left empty } template diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index bba22eb09..f2dd82e12 100644 --- a/src/storm/models/sparse/DeterministicModel.h +++ b/src/storm/models/sparse/DeterministicModel.h @@ -17,32 +17,11 @@ namespace storm { /*! * Constructs a model from the given data. * - * @param modelType The type of the model. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + * @param modelType the type of this model + * @param components The components for this model. */ - DeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional const& optionalChoiceLabeling = boost::none); - - /*! - * Constructs a model by moving the given data. - * - * @param modelType The type of the model. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - */ - DeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); + DeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components); + DeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components); 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 222354b65..fa193d592 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -10,22 +10,31 @@ namespace storm { namespace sparse { template - Dtmc::Dtmc(storm::storage::SparseMatrix const& probabilityMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, - 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."); + Dtmc::Dtmc(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, + std::unordered_map const& rewardModels) + : Dtmc(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels)) { + // Intentionally left empty } template - Dtmc::Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - 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."); + Dtmc::Dtmc(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, + std::unordered_map&& rewardModels) + : Dtmc(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels))) { + // Intentionally left empty } - + template + Dtmc::Dtmc(storm::storage::sparse::ModelComponents const& components) + : DeterministicModel(storm::models::ModelType::Dtmc, components) { + // Intentionally left empty + } + + template + Dtmc::Dtmc(storm::storage::sparse::ModelComponents&& components) + : DeterministicModel(storm::models::ModelType::Dtmc, std::move(components)) { + // Intentionally left empty + } + template class Dtmc; diff --git a/src/storm/models/sparse/Dtmc.h b/src/storm/models/sparse/Dtmc.h index 291cfdf25..ecc3ecba8 100644 --- a/src/storm/models/sparse/Dtmc.h +++ b/src/storm/models/sparse/Dtmc.h @@ -13,18 +13,16 @@ namespace storm { template> class Dtmc : public DeterministicModel { public: - /*! + /*! * Constructs a model from the given data. * * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ - 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::none); + Dtmc(storm::storage::SparseMatrix const& transitionMatrix, + storm::models::sparse::StateLabeling const& stateLabeling, + std::unordered_map const& rewardModels = std::unordered_map()); /*! * Constructs a model by moving the given data. @@ -32,11 +30,19 @@ namespace storm { * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ - Dtmc(storm::storage::SparseMatrix&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); + Dtmc(storm::storage::SparseMatrix&& transitionMatrix, + storm::models::sparse::StateLabeling&& stateLabeling, + std::unordered_map&& rewardModels = std::unordered_map()); + + /*! + * Constructs a model from the given data. + * + * @param components The components for this model. + */ + Dtmc(storm::storage::sparse::ModelComponents const& components); + Dtmc(storm::storage::sparse::ModelComponents&& components); + Dtmc(Dtmc const& dtmc) = default; Dtmc& operator=(Dtmc const& dtmc) = default; diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp index 17a58ec44..b310b40e3 100644 --- a/src/storm/models/sparse/ItemLabeling.cpp +++ b/src/storm/models/sparse/ItemLabeling.cpp @@ -126,6 +126,10 @@ namespace storm { return labelings.size(); } + std::size_t ItemLabeling::getNumberOfItems() const { + return itemCount; + } + storm::storage::BitVector const& ItemLabeling::getItems(std::string const& label) const { STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "The label " << label << " is invalid for the labeling of the model."); return this->labelings[nameToLabelingIndexMap.at(label)]; diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h index 14e752031..746320afd 100644 --- a/src/storm/models/sparse/ItemLabeling.h +++ b/src/storm/models/sparse/ItemLabeling.h @@ -105,7 +105,14 @@ namespace storm { */ std::size_t getNumberOfLabels() const; + /*! + * Returns the number of items managed by this object. + * + * @return The number of labels. + */ + std::size_t getNumberOfItems() const; + /*! * Prints information about the labeling to the specified stream. diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 7a5d898e6..759f11051 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -16,61 +16,44 @@ namespace storm { template MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - storm::storage::BitVector const& markovianStates, - std::vector const& exitRates, - std::unordered_map const& rewardModels, - boost::optional const& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(this->checkIsClosed()) { - this->turnRatesToProbabilities(); - } - - template - MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - storm::storage::BitVector const& markovianStates, - std::vector const& exitRates, - std::unordered_map&& rewardModels, - 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(); - } - - - template - MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling, storm::storage::BitVector const& markovianStates, - std::unordered_map const& rewardModels, - boost::optional const& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates) { - turnRatesToProbabilities(); - this->closed = checkIsClosed(); + std::unordered_map const& rewardModels) + : MarkovAutomaton(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels, true, markovianStates)) { + // Intentionally left empty } template - MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& rateMatrix, + MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, storm::storage::BitVector&& markovianStates, - std::unordered_map&& rewardModels, - boost::optional&& optionalChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::MarkovAutomaton, rateMatrix, stateLabeling, rewardModels, optionalChoiceLabeling), markovianStates(markovianStates) { - turnRatesToProbabilities(); - this->closed = checkIsClosed(); + std::unordered_map&& rewardModels) + : MarkovAutomaton(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), true, std::move(markovianStates))) { + // Intentionally left empty } + template + MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents const& components) : NondeterministicModel(ModelType::MarkovAutomaton, components), markovianStates(components.markovianStates.get()) { + + if (components.exitRates) { + exitRates = components.exitRates.get(); + } + + if (components.rateTransitions) { + this->turnRatesToProbabilities(); + } + closed = this->checkIsClosed(); + } template - MarkovAutomaton::MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - storm::storage::BitVector const& markovianStates, - std::vector const& exitRates, - bool probabilities, - std::unordered_map&& rewardModels, - 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."); + MarkovAutomaton::MarkovAutomaton(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::MarkovAutomaton, std::move(components)), markovianStates(std::move(components.markovianStates.get())) { + + if (components.exitRates) { + exitRates = std::move(components.exitRates.get()); + } else { + this->turnRatesToProbabilities(); + } + closed = this->checkIsClosed(); } template @@ -157,15 +140,26 @@ namespace storm { template void MarkovAutomaton::turnRatesToProbabilities() { - this->exitRates.resize(this->getNumberOfStates()); + bool assertRates = (this->exitRates.size() == this->getNumberOfStates()); + if (!assertRates) { + STORM_LOG_THROW(this->exitRates.empty(), storm::exceptions::InvalidArgumentException, "The specified exit rate vector has an unexpected size."); + this->exitRates.reserve(this->getNumberOfStates()); + } + for (uint_fast64_t state = 0; state< this->getNumberOfStates(); ++state) { uint_fast64_t row = this->getTransitionMatrix().getRowGroupIndices()[state]; if (this->markovianStates.get(state)) { - this->exitRates[state] = this->getTransitionMatrix().getRowSum(row); + if (assertRates) { + STORM_LOG_THROW(this->exitRates[state] == this->getTransitionMatrix().getRowSum(row), storm::exceptions::InvalidArgumentException, "The specified exit rate is inconsistent with the rate matrix. Difference is " << (this->exitRates[state] - this->getTransitionMatrix().getRowSum(row)) << "."); + } else { + this->exitRates.push_back(this->getTransitionMatrix().getRowSum(row)); + } for (auto& transition : this->getTransitionMatrix().getRow(row)) { transition.setValue(transition.getValue() / this->exitRates[state]); } ++row; + } else { + this->exitRates.push_back(storm::utility::zero()); } for (; row < this->getTransitionMatrix().getRowGroupIndices()[state+1]; ++row) { STORM_LOG_THROW(storm::utility::isOne(this->getTransitionMatrix().getRowSum(row)), storm::exceptions::InvalidArgumentException, "Entries of transition matrix do not sum up to one for (non-Markovian) choice " << row << " of state " << state << " (sum is " << this->getTransitionMatrix().getRowSum(row) << ")."); @@ -250,6 +244,8 @@ namespace storm { 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."); + STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve choice labels."); + STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice labels."); 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 4ab1edaeb..249766b62 100644 --- a/src/storm/models/sparse/MarkovAutomaton.h +++ b/src/storm/models/sparse/MarkovAutomaton.h @@ -15,40 +15,22 @@ namespace storm { template> class MarkovAutomaton : public NondeterministicModel { public: - /*! - * Constructs a model from the given data. - * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates. - * @param stateLabeling The labeling of the states. - * @param markovianStates A bit vector indicating the Markovian states of the automaton. - * @param exitRates A vector storing the exit rates of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - */ - MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - storm::storage::BitVector const& markovianStates, - std::vector const& exitRates, - std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional const& optionalChoiceLabeling = boost::none); - + /*! * Constructs a model from the given data. * * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first * choice corresponds to the markovian transitions. * - * @param rateMatrix The matrix representing the transitions in the model in terms of rates. + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices). * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition). * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ - MarkovAutomaton(storm::storage::SparseMatrix const& rateMatrix, + MarkovAutomaton(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, storm::storage::BitVector const& markovianStates, - std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional const& optionalChoiceLabeling = boost::none); + std::unordered_map const& rewardModels = std::unordered_map()); /*! * Constructs a model from the given data. @@ -56,54 +38,24 @@ namespace storm { * For hybrid states (i.e., states with Markovian and probabilistic transitions), it is assumed that the first * choice corresponds to the markovian transitions. * - * @param rateMatrix The matrix representing the transitions in the model in terms of rates. + * @param transitionMatrix The matrix representing the transitions in the model in terms of rates (markocian choices) and probabilities (probabilistic choices). * @param stateLabeling The labeling of the states. * @param markovianStates A bit vector indicating the Markovian states of the automaton (i.e., states with at least one markovian transition). * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ - MarkovAutomaton(storm::storage::SparseMatrix&& rateMatrix, + MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, storm::storage::BitVector&& markovianStates, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); + std::unordered_map&& rewardModels = std::unordered_map()); /*! - * Constructs a model by moving the given data. - * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates. - * @param stateLabeling The labeling of the states. - * @param markovianStates A bit vector indicating the Markovian states of the automaton. - * @param exitRates A vector storing the exit rates of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - */ - MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - storm::storage::BitVector const& markovianStates, - std::vector const& exitRates, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); - - /*! - * Constructs a model by moving the given data. + * Constructs a model from the given data. * - * @param transitionMatrix The matrix representing the transitions in the model in terms of rates. - * @param stateLabeling The labeling of the states. - * @param markovianStates A bit vector indicating the Markovian states of the automaton. - * @param exitRates A vector storing the exit rates of the states. - * @param probabilities Flag if transitions matrix contains probabilities or rates - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + * @param components The components for this model. */ - MarkovAutomaton(storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - storm::storage::BitVector const& markovianStates, - std::vector const& exitRates, - bool probabilities, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); - + MarkovAutomaton(storm::storage::sparse::ModelComponents const& components); + MarkovAutomaton(storm::storage::sparse::ModelComponents&& components); + 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 5cfd36fa1..29690599a 100644 --- a/src/storm/models/sparse/Mdp.cpp +++ b/src/storm/models/sparse/Mdp.cpp @@ -12,36 +12,46 @@ namespace storm { namespace sparse { template - Mdp::Mdp(storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, - 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."); + Mdp::Mdp(storm::storage::SparseMatrix const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling, + std::unordered_map const& rewardModels) + : Mdp(storm::storage::sparse::ModelComponents(transitionMatrix, stateLabeling, rewardModels)) { + // Intentionally left empty } - - + template - Mdp::Mdp(storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, - 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."); + Mdp::Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, + std::unordered_map&& rewardModels) + : Mdp(storm::storage::sparse::ModelComponents(std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels))) { + // Intentionally left empty } - + + template + Mdp::Mdp(storm::storage::sparse::ModelComponents const& components) + : NondeterministicModel(storm::models::ModelType::Mdp, components) { + // Intentionally left empty + } + + template + Mdp::Mdp(storm::storage::sparse::ModelComponents&& components) + : NondeterministicModel(storm::models::ModelType::Mdp, std::move(components)) { + // Intentionally left empty + } + template Mdp Mdp::restrictChoices(storm::storage::BitVector const& enabledChoices) const { - storm::storage::SparseMatrix restrictedTransitions = this->getTransitionMatrix().restrictRows(enabledChoices); - std::unordered_map newRewardModels; + storm::storage::sparse::ModelComponents newComponents(this->getTransitionMatrix().restrictRows(enabledChoices)); + newComponents.stateLabeling = this->getStateLabeling(); for (auto const& rewardModel : this->getRewardModels()) { - newRewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); + newComponents.rewardModels.emplace(rewardModel.first, rewardModel.second.restrictActions(enabledChoices)); + } + if (this->hasChoiceLabeling()) { + newComponents.choiceLabeling = this->getChoiceLabeling().getSubLabeling(enabledChoices); } - if(this->hasChoiceLabeling()) { - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels, this->getChoiceLabeling().getSubLabeling(enabledChoices)); - } else { - return Mdp(restrictedTransitions, this->getStateLabeling(), newRewardModels); + newComponents.stateValuations = this->getOptionalStateValuations(); + if (this->hasChoiceOrigins()) { + newComponents.choiceOrigins = this->getChoiceOrigins()->selectChoices(enabledChoices); } + return Mdp(std::move(newComponents)); } template diff --git a/src/storm/models/sparse/Mdp.h b/src/storm/models/sparse/Mdp.h index 542b184af..e65770275 100644 --- a/src/storm/models/sparse/Mdp.h +++ b/src/storm/models/sparse/Mdp.h @@ -21,12 +21,10 @@ namespace storm { * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ 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::none); + std::unordered_map const& rewardModels = std::unordered_map()); /*! * Constructs a model by moving the given data. @@ -34,12 +32,18 @@ namespace storm { * @param transitionMatrix The matrix representing the transitions in the model. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. */ Mdp(storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); + std::unordered_map&& rewardModels = std::unordered_map()); + + /*! + * Constructs a model from the given data. + * + * @param components The components for this model. + */ + Mdp(storm::storage::sparse::ModelComponents const& components); + Mdp(storm::storage::sparse::ModelComponents&& components); Mdp(Mdp const& other) = default; Mdp& operator=(Mdp const& other) = default; diff --git a/src/storm/models/sparse/Model.cpp b/src/storm/models/sparse/Model.cpp index 85ada28b6..dde504e97 100644 --- a/src/storm/models/sparse/Model.cpp +++ b/src/storm/models/sparse/Model.cpp @@ -14,30 +14,66 @@ namespace storm { namespace models { namespace sparse { - template - Model::Model(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, - boost::optional const& optionalChoiceLabeling) - : ModelBase(modelType), transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), - rewardModels(rewardModels), choiceLabeling(optionalChoiceLabeling) { - for (auto const& rewardModel : this->getRewardModels()) { - STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); - } + + template + Model::Model(ModelType modelType, storm::storage::sparse::ModelComponents const& components) + : ModelBase(modelType), transitionMatrix(components.transitionMatrix), stateLabeling(components.stateLabeling), rewardModels(components.rewardModels), + choiceLabeling(components.choiceLabeling), stateValuations(components.stateValuations), choiceOrigins(components.choiceOrigins) { + assertValidityOfComponents(components); } - template - Model::Model(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, - boost::optional&& optionalChoiceLabeling) - : ModelBase(modelType), transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), - rewardModels(std::move(rewardModels)), choiceLabeling(std::move(optionalChoiceLabeling)) { + template + Model::Model(ModelType modelType, storm::storage::sparse::ModelComponents&& components) + : ModelBase(modelType), transitionMatrix(std::move(components.transitionMatrix)), stateLabeling(std::move(components.stateLabeling)), rewardModels(std::move(components.rewardModels)), + choiceLabeling(std::move(components.choiceLabeling)), stateValuations(std::move(components.stateValuations)), choiceOrigins(std::move(components.choiceOrigins)) { + assertValidityOfComponents(components); + } + + template + void Model::assertValidityOfComponents(storm::storage::sparse::ModelComponents const& components) const { + uint_fast64_t stateCount = this->getNumberOfStates(); + uint_fast64_t choiceCount = this->getTransitionMatrix().getRowCount(); + + // general components for all model types. + STORM_LOG_THROW(this->getTransitionMatrix().getColumnCount() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid column count of transition matrix."); + STORM_LOG_THROW(components.rateTransitions || this->getTransitionMatrix().isProbabilistic(), storm::exceptions::IllegalArgumentException, "The matrix is not probabilistic."); + STORM_LOG_THROW(this->getStateLabeling().getNumberOfItems() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid item count of state labeling."); for (auto const& rewardModel : this->getRewardModels()) { + STORM_LOG_THROW(!rewardModel.second.hasStateRewards() || rewardModel.second.getStateRewardVector().size() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid size of state reward vector."); + STORM_LOG_THROW(!rewardModel.second.hasStateActionRewards() || rewardModel.second.getStateActionRewardVector().size() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid size of state reward vector."); STORM_LOG_THROW(!rewardModel.second.hasTransitionRewards() || rewardModel.second.getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::IllegalArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist."); } + STORM_LOG_THROW(!this->hasChoiceLabeling() || this->getChoiceLabeling().getNumberOfItems() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid item count of choice labeling."); + STORM_LOG_THROW(!this->hasStateValuations() || this->getStateValuations().getNumberOfStates() == stateCount, storm::exceptions::IllegalArgumentException, "Invalid choice count for choice origins."); + STORM_LOG_THROW(!this->hasChoiceOrigins() || this->getChoiceOrigins()->getNumberOfChoices() == choiceCount, storm::exceptions::IllegalArgumentException, "Invalid choice count for choice origins."); + + // Branch on type of nondeterminism + if (this->isOfType(ModelType::Dtmc) || this->isOfType(ModelType::Ctmc)) { + STORM_LOG_THROW(this->getTransitionMatrix().hasTrivialRowGrouping(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Transition matrix has non-trivial row grouping."); + STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of rows of transition matrix does not match state count."); + STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create deterministic model: Number of columns of transition matrix does not match state count."); + STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored)."); + } else if (this->isOfType(ModelType::Mdp) || this->isOfType(ModelType::MarkovAutomaton)) { + STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of row groups of transition matrix does not match state count."); + STORM_LOG_THROW(stateCount == this->getTransitionMatrix().getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create nondeterministic model: Number of columns of transition matrix does not match state count."); + STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(), "Player 1 matrix given for a model that is no stochastic game (will be ignored)."); + } else { + STORM_LOG_THROW(this->isOfType(ModelType::S2pg), storm::exceptions::IllegalArgumentException, "Invalid model type."); + STORM_LOG_THROW(components.player1Matrix.is_initialized(), storm::exceptions::IllegalArgumentException, "No player 1 matrix given for stochastic game."); + STORM_LOG_THROW(components.player1Matrix->isProbabilistic(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry."); + STORM_LOG_THROW(stateCount == components.player1Matrix->getRowGroupCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p1 matrix does not match state count."); + STORM_LOG_THROW(this->getTransitionMatrix().getRowGroupCount() == components.player1Matrix->getColumnCount(), storm::exceptions::IllegalArgumentException, "Can not create stochastic game: Number of row groups of p2 matrix does not match column count of p1 matrix."); + } + + // Branch on continuous/discrete timing + if (this->isOfType(ModelType::Ctmc) || this->isOfType(ModelType::MarkovAutomaton)) { + STORM_LOG_THROW(components.rateTransitions || components.exitRates.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create continuous time model: no rates are given."); + STORM_LOG_THROW(!components.exitRates.is_initialized() || components.exitRates->size() == stateCount, storm::exceptions::IllegalArgumentException, "Size of exit rate vector does not match state count."); + STORM_LOG_THROW(this->isOfType(ModelType::Ctmc) || components.markovianStates.is_initialized(), storm::exceptions::IllegalArgumentException, "Can not create Markov Automaton: no Markovian states given."); + } else { + STORM_LOG_ERROR_COND(!components.rateTransitions && !components.exitRates.is_initialized(), "Rates specified for discrete-time model. The rates will be ignored."); + } + STORM_LOG_ERROR_COND(this->isOfType(ModelType::MarkovAutomaton) || !components.markovianStates.is_initialized(), "Markovian states given for a model that is not a Markov automaton (will be ignored)."); } template @@ -158,6 +194,20 @@ namespace storm { uint_fast64_t Model::getNumberOfRewardModels() const { return this->rewardModels.size(); } + template + storm::models::sparse::StateLabeling const& Model::getStateLabeling() const { + return stateLabeling; + } + + template + storm::models::sparse::StateLabeling& Model::getStateLabeling() { + return stateLabeling; + } + + template + bool Model::hasChoiceLabeling() const { + return static_cast(choiceLabeling); + } template storm::models::sparse::ChoiceLabeling const& Model::getChoiceLabeling() const { @@ -175,18 +225,43 @@ namespace storm { } template - storm::models::sparse::StateLabeling const& Model::getStateLabeling() const { - return stateLabeling; + bool Model::hasStateValuations() const { + return static_cast(stateValuations); } template - storm::models::sparse::StateLabeling& Model::getStateLabeling() { - return stateLabeling; + storm::storage::sparse::StateValuations const& Model::getStateValuations() const { + return stateValuations.get(); } template - bool Model::hasChoiceLabeling() const { - return static_cast(choiceLabeling); + boost::optional const& Model::getOptionalStateValuations() const { + return stateValuations; + } + + template + boost::optional& Model::getOptionalStateValuations() { + return stateValuations; + } + + template + bool Model::hasChoiceOrigins() const { + return static_cast(choiceOrigins); + } + + template + std::shared_ptr const& Model::getChoiceOrigins() const { + return choiceOrigins.get(); + } + + template + boost::optional> const& Model::getOptionalChoiceOrigins() const { + return choiceOrigins; + } + + template + boost::optional>& Model::getOptionalChoiceOrigins() { + return choiceOrigins; } template @@ -359,8 +434,6 @@ namespace storm { return storm::storage::getVariables(model.getTransitionMatrix()); } - - std::set getRewardParameters(Model const& model) { std::set result; for(auto rewModel : model.getRewardModels()) { diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 4b8959972..2659d5a46 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -8,8 +8,11 @@ #include "storm/models/ModelBase.h" #include "storm/models/sparse/StateLabeling.h" #include "storm/models/sparse/ChoiceLabeling.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/storage/sparse/StateType.h" #include "storm/storage/SparseMatrix.h" +#include "storm/storage/sparse/ChoiceOrigins.h" +#include "storm/storage/sparse/StateValuations.h" #include "storm/utility/OsDetection.h" namespace storm { @@ -17,11 +20,6 @@ namespace storm { class BitVector; } - namespace utility { - template - class ModelInstantiator; - } - namespace models { namespace sparse { @@ -33,9 +31,7 @@ namespace storm { */ template> class Model : public storm::models::ModelBase { - template - friend class storm::utility::ModelInstantiator; - + public: typedef CValueType ValueType; typedef CRewardModelType RewardModelType; @@ -43,37 +39,15 @@ namespace storm { Model(Model const& other) = default; Model& operator=(Model const& other) = default; - /*! * Constructs a model from the given data. * - * @param modelType The type of the model. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + * @param modelType the type of this model + * @param components The components for this model. */ - Model(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional const& optionalChoiceLabeling = boost::none); - - /*! - * Constructs a model by moving the given data. - * - * @param modelType The type of the model. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - */ - Model(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); - + Model(ModelType modelType, storm::storage::sparse::ModelComponents const& components); + Model(ModelType modelType, storm::storage::sparse::ModelComponents&& components); + /*! * Retrieves the backward transition relation of the model, i.e. a set of transitions between states * that correspond to the reversed transition relation of this model. @@ -218,6 +192,27 @@ namespace storm { */ bool removeRewardModel(std::string const& rewardModelName); + /*! + * Returns the state labeling associated with this model. + * + * @return The state labeling associated with this model. + */ + storm::models::sparse::StateLabeling const& getStateLabeling() const; + + /*! + * Returns the state labeling associated with this model. + * + * @return The state labeling associated with this model. + */ + storm::models::sparse::StateLabeling& getStateLabeling(); + + /*! + * Retrieves whether this model has a labeling of the choices. + * + * @return True iff this model has a labeling of the choices. + */ + bool hasChoiceLabeling() const; + /*! * Retrieves the labels for the choices of the model. Note that calling this method is only valid if the * model has a choice labeling. @@ -228,7 +223,7 @@ namespace storm { /*! * 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; @@ -241,25 +236,64 @@ namespace storm { boost::optional& getOptionalChoiceLabeling(); /*! - * Returns the state labeling associated with this model. + * Retrieves whether this model was build with state valuations. * - * @return The state labeling associated with this model. + * @return True iff this model has state valuations. */ - storm::models::sparse::StateLabeling const& getStateLabeling() const; + bool hasStateValuations() const; /*! - * Returns the state labeling associated with this model. + * Retrieves the valuations of the states of the model. Note that calling this method is only valid if the + * model has state valuations. * - * @return The state labeling associated with this model. + * @return The valuations of the states of the model. */ - storm::models::sparse::StateLabeling& getStateLabeling(); + storm::storage::sparse::StateValuations const& getStateValuations() const; /*! - * Retrieves whether this model has a labeling of the choices. + * Retrieves an optional value that contains the state valuations if there are some. * - * @return True iff this model has a labeling of the choices. + * @return The state valuations, if they're saved. */ - bool hasChoiceLabeling() const; + boost::optional const& getOptionalStateValuations() const; + + /*! + * Retrieves an optional value that contains the state valuations if there are some. + * + * @return The state valuations, if they're saved. + */ + boost::optional& getOptionalStateValuations(); + + + /*! + * Retrieves whether this model was build with choice origins. + * + * @return True iff this model has choice origins. + */ + bool hasChoiceOrigins() const; + + /*! + * Retrieves the origins of the choices of the model. Note that calling this method is only valid if the + * model has choice origins. + * + * @return The origins of the choices of the model. + */ + std::shared_ptr const& getChoiceOrigins() const; + + /*! + * Retrieves an optional value that contains the choice origins if there are some. + * + * @return The choice origins, if they're saved. + */ + boost::optional> const& getOptionalChoiceOrigins() const; + + /*! + * Retrieves an optional value that contains the choice origins if there are some. + * + * @return The choice origins, if they're saved. + */ + boost::optional>& getOptionalChoiceOrigins(); + /*! * Converts the transition rewards of all reward models to state-based rewards. For deterministic models, @@ -352,6 +386,10 @@ namespace storm { void printRewardModelsInformationToStream(std::ostream& out) const; private: + + // Upon construction of a model, this function asserts that the specified components are valid + void assertValidityOfComponents(storm::storage::sparse::ModelComponents const& components) const; + // A matrix representing transition relation. storm::storage::SparseMatrix transitionMatrix; @@ -363,6 +401,13 @@ namespace storm { // If set, a vector representing the labels of choices. boost::optional choiceLabeling; + + // if set, retrieves for each state the variable valuation that this state represents + boost::optional stateValuations; + + // if set, gives information about where each choice originates w.r.t. the input model description + boost::optional> choiceOrigins; + }; #ifdef STORM_HAVE_CARL diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 37e72c84a..ba0be43b7 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -11,25 +11,16 @@ namespace storm { namespace models { namespace sparse { - template - NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, - boost::optional const& optionalChoiceLabeling) - : Model(modelType, transitionMatrix, stateLabeling, rewardModels, optionalChoiceLabeling) { - // Intentionally left empty. + template + NondeterministicModel::NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components) + : Model(modelType, components) { + // Intentionally left empty } - template - NondeterministicModel::NondeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, - boost::optional&& optionalChoiceLabeling) - : Model(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(rewardModels), - std::move(optionalChoiceLabeling)) { - // Intentionally left empty. + template + NondeterministicModel::NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components) + : Model(modelType, std::move(components)) { + // Intentionally left empty } template diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index bb2443b05..1f2bd157a 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -14,41 +14,16 @@ namespace storm { template> class NondeterministicModel: public Model { public: - /*! - * Constructs a model from the given data. - * - * @param modelType The type of the model. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. - */ - NondeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix const& transitionMatrix, - storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional const& optionalChoiceLabeling = boost::none); + /*! - * Constructs a model by moving the given data. + * Constructs a model from the given data. * - * @param modelType The type of the model. - * @param transitionMatrix The matrix representing the transitions in the model. - * @param stateLabeling The labeling of the states. - * @param rewardModels A mapping of reward model names to reward models. - * @param optionalChoiceLabeling A vector that represents the labels associated with the choices of each state. + * @param modelType the type of this model + * @param components The components for this model. */ - NondeterministicModel(storm::models::ModelType const& modelType, - storm::storage::SparseMatrix&& transitionMatrix, - storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalChoiceLabeling = boost::none); - - NondeterministicModel(NondeterministicModel const& other) = default; - NondeterministicModel& operator=(NondeterministicModel const& other) = default; - - NondeterministicModel(NondeterministicModel&& other) = default; - NondeterministicModel& operator=(NondeterministicModel&& other) = default; + NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents const& components); + NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents&& components); /*! * Retrieves the number of (nondeterministic) choices in the model. diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h index 99afcc80d..d781fb4f4 100644 --- a/src/storm/models/sparse/StateLabeling.h +++ b/src/storm/models/sparse/StateLabeling.h @@ -58,8 +58,6 @@ namespace storm { */ std::set getLabelsOfState(storm::storage::sparse::state_type state) const; - - /*! * Adds a label to a given state. * diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp index e0b4576f1..0dbcb9283 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.cpp +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.cpp @@ -12,10 +12,8 @@ namespace storm { StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels, - boost::optional const& optionalPlayer1ChoiceLabeling, - boost::optional const& optionalPlayer2ChoiceLabeling) - : NondeterministicModel(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, rewardModels, optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1ChoiceLabeling(optionalPlayer1ChoiceLabeling) { + std::unordered_map const& rewardModels) + : StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents(player2Matrix, stateLabeling, rewardModels, false, boost::none, player1Matrix)) { // Intentionally left empty. } @@ -24,33 +22,31 @@ namespace storm { StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels, - 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)) { + std::unordered_map&& rewardModels) + : StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents(std::move(player2Matrix), std::move(stateLabeling), std::move(rewardModels), false, boost::none, std::move(player1Matrix))) { // Intentionally left empty. } template - storm::storage::SparseMatrix const& StochasticTwoPlayerGame::getPlayer1Matrix() const { - return player1Matrix; + StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents const& components) : NondeterministicModel(ModelType::S2pg, components), player1Matrix(components.player1Matrix.get()) { + // Intentionally left empty } - + template - storm::storage::SparseMatrix const& StochasticTwoPlayerGame::getPlayer2Matrix() const { - return this->getTransitionMatrix(); + StochasticTwoPlayerGame::StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents&& components) : NondeterministicModel(ModelType::S2pg, std::move(components)), player1Matrix(std::move(components.player1Matrix.get())) { + // Intentionally left empty } template - bool StochasticTwoPlayerGame::hasPlayer1ChoiceLabeling() const { - return static_cast(player1ChoiceLabeling); + storm::storage::SparseMatrix const& StochasticTwoPlayerGame::getPlayer1Matrix() const { + return player1Matrix; } template - storm::models::sparse::ChoiceLabeling const& StochasticTwoPlayerGame::getPlayer1ChoiceLabeling() const { - return player1ChoiceLabeling.get(); + storm::storage::SparseMatrix const& StochasticTwoPlayerGame::getPlayer2Matrix() const { + return this->getTransitionMatrix(); } - + template bool StochasticTwoPlayerGame::hasPlayer2ChoiceLabeling() const { return this->hasChoiceLabeling(); @@ -62,9 +58,9 @@ namespace storm { } template class StochasticTwoPlayerGame; -// template class StochasticTwoPlayerGame; #ifdef STORM_HAVE_CARL + template class StochasticTwoPlayerGame>; template class StochasticTwoPlayerGame; template class StochasticTwoPlayerGame; #endif diff --git a/src/storm/models/sparse/StochasticTwoPlayerGame.h b/src/storm/models/sparse/StochasticTwoPlayerGame.h index 9c850e83d..3485df4cb 100644 --- a/src/storm/models/sparse/StochasticTwoPlayerGame.h +++ b/src/storm/models/sparse/StochasticTwoPlayerGame.h @@ -22,15 +22,11 @@ namespace storm { * @param player2Matrix The matrix representing the choices of player 2. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalPlayer1ChoiceLabeling A vector that represents the labels associated with the choices of each player 1 state. - * @param optionalPlayer2ChoiceLabeling A vector that represents the labels associated with the choices of each player 2 state. */ StochasticTwoPlayerGame(storm::storage::SparseMatrix const& player1Matrix, storm::storage::SparseMatrix const& player2Matrix, storm::models::sparse::StateLabeling const& stateLabeling, - std::unordered_map const& rewardModels = std::unordered_map(), - boost::optional const& optionalPlayer1ChoiceLabeling = boost::none, - boost::optional const& optionalPlayer2ChoiceLabeling = boost::none); + std::unordered_map const& rewardModels = std::unordered_map()), /*! * Constructs a model by moving the given data. @@ -39,15 +35,20 @@ namespace storm { * @param player2Matrix The matrix representing the choices of player 2. * @param stateLabeling The labeling of the states. * @param rewardModels A mapping of reward model names to reward models. - * @param optionalPlayer1ChoiceLabeling A vector that represents the labels associated with the choices of each player 1 state. - * @param optionalPlayer2ChoiceLabeling A vector that represents the labels associated with the choices of each player 2 state. */ StochasticTwoPlayerGame(storm::storage::SparseMatrix&& player1Matrix, storm::storage::SparseMatrix&& player2Matrix, storm::models::sparse::StateLabeling&& stateLabeling, - std::unordered_map&& rewardModels = std::unordered_map(), - boost::optional&& optionalPlayer1ChoiceLabeling = boost::none, - boost::optional&& optionalPlayer2ChoiceLabeling = boost::none); + std::unordered_map&& rewardModels = std::unordered_map()), + + /*! + * Constructs a model from the given data. + * + * @param components The components for this model. + */ + StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents const& components); + StochasticTwoPlayerGame(storm::storage::sparse::ModelComponents&& components); + StochasticTwoPlayerGame(StochasticTwoPlayerGame const& other) = default; StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame const& other) = default; @@ -70,27 +71,13 @@ namespace storm { */ storm::storage::SparseMatrix const& getPlayer2Matrix() const; - /*! - * Retrieves the whether the game has labels attached to the choices in player 1 states. - * - * @return True if the game has player 1 choice labels. - */ - bool hasPlayer1ChoiceLabeling() const; - - /*! - * Retrieves the labels attached to the choices of player 1 states. - * - * @return A vector containing the labels of each player 1 choice. - */ - storm::models::sparse::ChoiceLabeling const& getPlayer1ChoiceLabeling() const; - /*! * Retrieves whether the game has labels attached to player 2 states. * * @return True if the game has player 2 labels. */ bool hasPlayer2ChoiceLabeling() const; - + /*! * Retrieves the labels attached to the choices of player 2 states. * @@ -105,11 +92,7 @@ namespace storm { // the index of a row group in the matrix for player 2). storm::storage::SparseMatrix player1Matrix; - // 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; - - // The matrix and labels for player 2 are stored in the superclass. + // The matrix for player 2 are stored in the superclass. }; } // namespace sparse diff --git a/src/storm/parser/DeterministicModelParser.cpp b/src/storm/parser/DeterministicModelParser.cpp index f6cf0180e..74bc6f1b0 100644 --- a/src/storm/parser/DeterministicModelParser.cpp +++ b/src/storm/parser/DeterministicModelParser.cpp @@ -15,7 +15,7 @@ namespace storm { namespace parser { template - typename DeterministicModelParser::Result DeterministicModelParser::parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { + storm::storage::sparse::ModelComponents> DeterministicModelParser::parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { // Parse the transitions. storm::storage::SparseMatrix transitions(std::move(storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitions(transitionsFilename))); @@ -26,22 +26,28 @@ namespace storm { storm::models::sparse::StateLabeling labeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)); // Construct the result. - DeterministicModelParser::Result result(std::move(transitions), std::move(labeling)); + storm::storage::sparse::ModelComponents> result(std::move(transitions), std::move(labeling)); // Only parse state rewards if a file is given. + boost::optional> stateRewards; if (stateRewardFilename != "") { - result.stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename); + stateRewards = storm::parser::SparseStateRewardParser::parseSparseStateReward(stateCount, stateRewardFilename); } // Only parse transition rewards if a file is given. + boost::optional> transitionRewards; if (transitionRewardFilename != "") { - result.transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFilename, result.transitionSystem); + transitionRewards = storm::parser::DeterministicSparseTransitionParser::parseDeterministicTransitionRewards(transitionRewardFilename, result.transitionMatrix); + } + + if (stateRewards || transitionRewards) { + result.rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(std::move(stateRewards), boost::none, std::move(transitionRewards)))); } // Only parse choice labeling if a file is given. boost::optional choiceLabeling; if (!choiceLabelingFilename.empty()) { - result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(result.transitionSystem.getRowCount(), choiceLabelingFilename); + result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(result.transitionMatrix.getRowCount(), choiceLabelingFilename); } return result; @@ -49,24 +55,17 @@ namespace storm { template storm::models::sparse::Dtmc> DeterministicModelParser::parseDtmc(std::string const & transitionsFilename, std::string const & labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { - typename DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))); - - std::unordered_map> rewardModels; - if (!stateRewardFilename.empty() || !transitionRewardFilename.empty()) { - rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); - } - return storm::models::sparse::Dtmc>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), std::move(parserResult.choiceLabeling)); + + auto parserResult = parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename); + return storm::models::sparse::Dtmc>(std::move(parserResult)); } template storm::models::sparse::Ctmc> DeterministicModelParser::parseCtmc(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { - typename DeterministicModelParser::Result parserResult(std::move(parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename))); - - std::unordered_map> rewardModels; - 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), std::move(parserResult.choiceLabeling)); + + auto parserResult = parseDeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename); + return storm::models::sparse::Ctmc>(std::move(parserResult)); + } template class DeterministicModelParser; diff --git a/src/storm/parser/DeterministicModelParser.h b/src/storm/parser/DeterministicModelParser.h index a30ef6d3c..8271ae482 100644 --- a/src/storm/parser/DeterministicModelParser.h +++ b/src/storm/parser/DeterministicModelParser.h @@ -3,6 +3,8 @@ #include "storm/models/sparse/Dtmc.h" #include "storm/models/sparse/Ctmc.h" +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace parser { @@ -16,49 +18,6 @@ namespace storm { template class DeterministicModelParser { public: - - /*! - * A structure containing the parsed components of a deterministic model. - */ - struct Result { - - /*! - * The copy constructor. - * - * @param transitionSystem The transition system to be contained in the Result. - * @param labeling The the labeling of the transition system to be contained in the Result. - */ - Result(storm::storage::SparseMatrix& transitionSystem, storm::models::sparse::StateLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { - // Intentionally left empty. - } - - /*! - * The move constructor. - * - * @param transitionSystem The transition system to be contained in the Result. - * @param labeling The the labeling of the transition system to be contained in the Result. - */ - Result(storm::storage::SparseMatrix&& transitionSystem, storm::models::sparse::StateLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { - // Intentionally left empty. - } - - //! A matrix representing the transitions of the model - storm::storage::SparseMatrix transitionSystem; - - //! The labels of each state. - storm::models::sparse::StateLabeling labeling; - - //! Optional rewards for each state. - boost::optional> stateRewards; - - //! Optional rewards for each transition. - boost::optional> transitionRewards; - - //! The labels of each choice. - boost::optional choiceLabeling; - }; - - /*! * Parse a Dtmc. * @@ -121,7 +80,7 @@ namespace storm { * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. * @return The parsed model encapsulated in a Result structure. */ - static Result parseDeterministicModel(std::string const& transitionsFilename, + static storm::storage::sparse::ModelComponents> parseDeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", diff --git a/src/storm/parser/DirectEncodingParser.cpp b/src/storm/parser/DirectEncodingParser.cpp index 110c9ca32..a2e551838 100644 --- a/src/storm/parser/DirectEncodingParser.cpp +++ b/src/storm/parser/DirectEncodingParser.cpp @@ -92,7 +92,7 @@ namespace storm { STORM_LOG_THROW(line == "@model", storm::exceptions::WrongFormatException, "Expected model declaration."); // Construct transition matrix - std::shared_ptr modelComponents = parseStates(file, type, nrStates, valueParser); + std::shared_ptr> modelComponents = parseStates(file, type, nrStates, valueParser); // Done parsing storm::utility::closeFile(file); @@ -105,7 +105,8 @@ namespace storm { } case storm::models::ModelType::Ctmc: { - return std::make_shared>(std::move(modelComponents->transitionMatrix), std::move(modelComponents->stateLabeling), std::move(modelComponents->rewardModels), std::move(modelComponents->choiceLabeling)); + modelComponents->rateTransitions = true; + return std::make_shared>(std::move(*modelComponents)); } case storm::models::ModelType::Mdp: { @@ -113,7 +114,8 @@ namespace storm { } case storm::models::ModelType::MarkovAutomaton: { - return std::make_shared>(std::move(modelComponents->transitionMatrix), std::move(modelComponents->stateLabeling), std::move(modelComponents->markovianStates), std::move(modelComponents->exitRates)); + modelComponents->rateTransitions = true; + return std::make_shared>(std::move(*modelComponents)); } default: STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Unknown/Unhandled model type " << type << " which cannot be parsed."); @@ -121,11 +123,11 @@ namespace storm { } template - std::shared_ptr::ModelComponents> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser) { + std::shared_ptr> DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser) { // Initialize - std::shared_ptr modelComponents = std::make_shared(); - modelComponents->nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton); - storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, modelComponents->nonDeterministic, 0); + auto modelComponents = std::make_shared>(); + bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton); + storm::storage::SparseMatrixBuilder builder = storm::storage::SparseMatrixBuilder(0, 0, 0, false, nonDeterministic, 0); modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); // Iterate over all lines @@ -177,7 +179,7 @@ namespace storm { } STORM_LOG_TRACE("New state " << state); STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond."); - if (modelComponents->nonDeterministic) { + if (nonDeterministic) { builder.newRowGroup(row); } } else if (boost::starts_with(line, "\taction ")) { diff --git a/src/storm/parser/DirectEncodingParser.h b/src/storm/parser/DirectEncodingParser.h index 1c7a6c3f0..43a5a6f8b 100644 --- a/src/storm/parser/DirectEncodingParser.h +++ b/src/storm/parser/DirectEncodingParser.h @@ -6,7 +6,7 @@ #include "storm/storage/expressions/ExpressionManager.h" #include "storm/parser/ExpressionParser.h" #include "storm/storage/expressions/ExpressionEvaluator.h" - +#include "storm/storage/sparse/ModelComponents.h" namespace storm { namespace parser { @@ -66,31 +66,6 @@ namespace storm { private: - // A structure holding the individual components of a model. - struct ModelComponents { - - // The transition matrix. - storm::storage::SparseMatrix transitionMatrix; - - // The state labeling. - storm::models::sparse::StateLabeling stateLabeling; - - // The reward models. - std::unordered_map rewardModels; - - // A vector that stores a labeling for each choice. - boost::optional choiceLabeling; - - // The exit rates for MAs. - std::vector exitRates; - - // The Markovian states for MA. - storm::storage::BitVector markovianStates; - - // A flag indicating if the model is non-deterministic. - bool nonDeterministic; - }; - /*! * Parse states and return transition matrix. * @@ -100,7 +75,7 @@ namespace storm { * * @return Transition matrix. */ - static std::shared_ptr parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser); + static std::shared_ptr> parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, ValueParser const& valueParser); }; } // namespace parser diff --git a/src/storm/parser/MarkovAutomatonParser.cpp b/src/storm/parser/MarkovAutomatonParser.cpp index a42c9c341..fbcc01f80 100644 --- a/src/storm/parser/MarkovAutomatonParser.cpp +++ b/src/storm/parser/MarkovAutomatonParser.cpp @@ -3,6 +3,7 @@ #include "SparseStateRewardParser.h" #include "NondeterministicSparseTransitionParser.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/models/sparse/StandardRewardModel.h" #include "storm/exceptions/WrongFormatException.h" @@ -24,6 +25,12 @@ namespace storm { // Parse the state labeling. storm::models::sparse::StateLabeling resultLabeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(transitionMatrix.getColumnCount(), labelingFilename)); + // Cunstruct the result components + storm::storage::sparse::ModelComponents> componets(std::move(transitionMatrix), std::move(resultLabeling)); + componets.rateTransitions = true; + componets.markovianStates = std::move(transitionResult.markovianStates); + componets.exitRates = std::move(transitionResult.exitRates); + // If given, parse the state rewards file. boost::optional> stateRewards; if (!stateRewardFilename.empty()) { @@ -36,19 +43,18 @@ namespace storm { transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitionMatrix)); } - std::unordered_map> rewardModels; - rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(std::move(stateRewards), boost::none, std::move(transitionRewards)))); + if (stateRewards || transitionRewards) { + componets.rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(std::move(stateRewards), boost::none, std::move(transitionRewards)))); + } // Only parse choice labeling if a file is given. boost::optional choiceLabeling; if (!choiceLabelingFilename.empty()) { - choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitionMatrix.getRowCount(), choiceLabelingFilename, transitionMatrix.getRowGroupIndices()); + componets.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitionMatrix.getRowCount(), choiceLabelingFilename, transitionMatrix.getRowGroupIndices()); } - // Put the pieces together to generate the Markov Automaton. - storm::models::sparse::MarkovAutomaton> resultingAutomaton(std::move(transitionMatrix), std::move(resultLabeling), std::move(transitionResult.markovianStates), std::move(transitionResult.exitRates), std::move(rewardModels), std::move(choiceLabeling)); - - return resultingAutomaton; + // generate the Markov Automaton. + return storm::models::sparse::MarkovAutomaton> (std::move(componets)); } template class MarkovAutomatonParser; diff --git a/src/storm/parser/NondeterministicModelParser.cpp b/src/storm/parser/NondeterministicModelParser.cpp index 152fa8943..b786a0d73 100644 --- a/src/storm/parser/NondeterministicModelParser.cpp +++ b/src/storm/parser/NondeterministicModelParser.cpp @@ -16,7 +16,7 @@ namespace storm { namespace parser { template - typename NondeterministicModelParser::Result NondeterministicModelParser::parseNondeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { + storm::storage::sparse::ModelComponents> NondeterministicModelParser::parseNondeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { // Parse the transitions. storm::storage::SparseMatrix transitions(std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitions(transitionsFilename))); @@ -25,6 +25,9 @@ namespace storm { // Parse the state labeling. storm::models::sparse::StateLabeling labeling(storm::parser::SparseItemLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)); + + // Initialize result. + storm::storage::sparse::ModelComponents> result(std::move(transitions), std::move(labeling)); // Only parse state rewards if a file is given. boost::optional> stateRewards; @@ -38,28 +41,24 @@ namespace storm { transitionRewards = std::move(storm::parser::NondeterministicSparseTransitionParser::parseNondeterministicTransitionRewards(transitionRewardFilename, transitions)); } + if (stateRewards || transitionRewards) { + result.rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(std::move(stateRewards), boost::none, std::move(transitionRewards)))); + } + // Only parse choice labeling if a file is given. boost::optional choiceLabeling; if (!choiceLabelingFilename.empty()) { - choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitions.getRowCount(), choiceLabelingFilename, transitions.getRowGroupIndices()); + result.choiceLabeling = storm::parser::SparseItemLabelingParser::parseChoiceLabeling(transitions.getRowCount(), choiceLabelingFilename, transitions.getRowGroupIndices()); } - // Construct the result. - Result result(std::move(transitions), std::move(labeling)); - result.stateRewards = std::move(stateRewards); - result.transitionRewards = std::move(transitionRewards); - result.choiceLabeling = std::move(choiceLabeling); - return result; } template storm::models::sparse::Mdp> NondeterministicModelParser::parseMdp(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename, std::string const& transitionRewardFilename, std::string const& choiceLabelingFilename) { - Result parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename); + auto parserResult = parseNondeterministicModel(transitionsFilename, labelingFilename, stateRewardFilename, transitionRewardFilename, choiceLabelingFilename); - std::unordered_map> rewardModels; - rewardModels.insert(std::make_pair("", storm::models::sparse::StandardRewardModel(parserResult.stateRewards, boost::optional>(), parserResult.transitionRewards))); - return storm::models::sparse::Mdp>(std::move(parserResult.transitionSystem), std::move(parserResult.labeling), std::move(rewardModels), std::move(parserResult.choiceLabeling)); + return storm::models::sparse::Mdp>(std::move(parserResult)); } template class NondeterministicModelParser; diff --git a/src/storm/parser/NondeterministicModelParser.h b/src/storm/parser/NondeterministicModelParser.h index 8ce22e13e..9be8a0432 100644 --- a/src/storm/parser/NondeterministicModelParser.h +++ b/src/storm/parser/NondeterministicModelParser.h @@ -2,6 +2,7 @@ #define STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ #include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace parser { @@ -16,57 +17,6 @@ namespace storm { class NondeterministicModelParser { public: - /*! - * A structure containing the parsed components of a nondeterministic model. - */ - struct Result { - - /*! - * The copy constructor. - * - * @param transitionSystem The transition system to be contained in the Result. - * @param labeling The the labeling of the transition system to be contained in the Result. - */ - Result(storm::storage::SparseMatrix& transitionSystem, storm::models::sparse::StateLabeling& labeling) : transitionSystem(transitionSystem), labeling(labeling) { - // Intentionally left empty. - } - - /*! - * The move constructor. - * - * @param transitionSystem The transition system to be contained in the Result. - * @param labeling The the labeling of the transition system to be contained in the Result. - */ - Result(storm::storage::SparseMatrix&& transitionSystem, storm::models::sparse::StateLabeling&& labeling) : transitionSystem(std::move(transitionSystem)), labeling(std::move(labeling)) { - // Intentionally left empty. - } - - /*! - * A matrix representing the transitions of the model - */ - storm::storage::SparseMatrix transitionSystem; - - /*! - * The labels of each state. - */ - storm::models::sparse::StateLabeling labeling; - - /*! - * Optional rewards for each state. - */ - boost::optional> stateRewards; - - /*! - * Optional rewards for each transition. - */ - boost::optional> transitionRewards; - - /*! - * Optional choice labeling. - */ - boost::optional choiceLabeling; - }; - /*! * Parse a Mdp. * @@ -101,7 +51,7 @@ namespace storm { * @param choiceLabelingFilename The path and name of the file containing the choice labeling of the model. This file is optional. * @return The parsed model encapsulated in a Result structure. */ - static Result parseNondeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", std::string const& choiceLabelingFilename = ""); + static storm::storage::sparse::ModelComponents> parseNondeterministicModel(std::string const& transitionsFilename, std::string const& labelingFilename, std::string const& stateRewardFilename = "", std::string const& transitionRewardFilename = "", std::string const& choiceLabelingFilename = ""); }; diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index d2bcead60..c42fa1bd0 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -1360,6 +1360,19 @@ namespace storm { } } + template + void SparseMatrix::scaleRowsInPlace(std::vector const& factors) { + STORM_LOG_ASSERT(factors.size() == this->getRowCount(), "Can not scale rows: Number of rows and number of scaling factors do not match."); + uint_fast64_t row = 0; + for (auto const& factor : factors) { + for (auto& entry : getRow(row)) { + entry.setValue(entry.getValue() * factor); + } + ++row; + } + } + + template typename SparseMatrix::const_rows SparseMatrix::getRows(index_type startRow, index_type endRow) const { return const_rows(this->columnsAndValues.begin() + this->rowIndications[startRow], this->rowIndications[endRow] - this->rowIndications[startRow]); diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index cf9211849..ba7d606a7 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -794,6 +794,11 @@ s * @param insertDiagonalEntries If set to true, the resulting matri */ void multiplyVectorWithMatrix(std::vector const& vector, std::vector& result) const; + /*! + * Scales each row of the matrix, i.e., multiplies each element in row i with factors[i] + */ + void scaleRowsInPlace(std::vector const& factors); + /*! * Performs one step of the successive over-relaxation technique. * diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp index f37e380f7..330091f9d 100644 --- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp +++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.cpp @@ -10,6 +10,7 @@ #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "storm/utility/constants.h" #include "storm/utility/macros.h" +#include "storm/utility/builder.h" #include "storm/exceptions/InvalidOperationException.h" @@ -53,6 +54,7 @@ namespace storm { // Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states. labeling.addLabel("init", initialStates % reachableStates); + return buildResult(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); } @@ -283,41 +285,37 @@ namespace storm { template std::shared_ptr> SparseModelMemoryProduct::buildResult(storm::storage::SparseMatrix&& matrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map>&& rewardModels) const { - switch (model.getType()) { - case storm::models::ModelType::Dtmc: - return std::make_shared> (std::move(matrix), std::move(labeling), std::move(rewardModels)); - case storm::models::ModelType::Mdp: - return std::make_shared> (std::move(matrix), std::move(labeling), std::move(rewardModels)); - case storm::models::ModelType::Ctmc: - return std::make_shared> (std::move(matrix), std::move(labeling), std::move(rewardModels)); - case storm::models::ModelType::MarkovAutomaton: - { - // We also need to translate the exit rates and the Markovian states - uint_fast64_t numResStates = matrix.getRowGroupCount(); - uint_fast64_t memoryStateCount = memory.getNumberOfStates(); - std::vector resultExitRates; - resultExitRates.reserve(matrix.getRowGroupCount()); - storm::storage::BitVector resultMarkovianStates(numResStates, false); - auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); - auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); + storm::storage::sparse::ModelComponents> components (std::move(matrix), std::move(labeling), std::move(rewardModels)); + + if (model.isOfType(storm::models::ModelType::Ctmc)) { + components.rateTransitions = true; + } else if (model.isOfType(storm::models::ModelType::MarkovAutomaton)) { + // We also need to translate the exit rates and the Markovian states + uint_fast64_t numResStates = matrix.getRowGroupCount(); + uint_fast64_t memoryStateCount = memory.getNumberOfStates(); + std::vector resultExitRates; + resultExitRates.reserve(matrix.getRowGroupCount()); + storm::storage::BitVector resultMarkovianStates(numResStates, false); + auto const& modelExitRates = dynamic_cast const&>(model).getExitRates(); + auto const& modelMarkovianStates = dynamic_cast const&>(model).getMarkovianStates(); - uint_fast64_t stateIndex = 0; - for (auto const& resState : toResultStateMapping) { - if (resState < numResStates) { - assert(resState == resultExitRates.size()); - uint_fast64_t modelState = stateIndex / memoryStateCount; - resultExitRates.push_back(modelExitRates[modelState]); - if (modelMarkovianStates.get(modelState)) { - resultMarkovianStates.set(resState, true); - } + uint_fast64_t stateIndex = 0; + for (auto const& resState : toResultStateMapping) { + if (resState < numResStates) { + assert(resState == resultExitRates.size()); + uint_fast64_t modelState = stateIndex / memoryStateCount; + resultExitRates.push_back(modelExitRates[modelState]); + if (modelMarkovianStates.get(modelState)) { + resultMarkovianStates.set(resState, true); } - ++stateIndex; } - return std::make_shared> (std::move(matrix), std::move(labeling), std::move(resultMarkovianStates), std::move(resultExitRates), true, std::move(rewardModels)); + ++stateIndex; } - default: - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Memory Structure Product for Model Type " << model.getType() << " is not supported"); + components.markovianStates = std::move(resultMarkovianStates); + components.exitRates = std::move(resultExitRates); } + + return storm::utility::builder::buildModelFromComponents(model.getType(), std::move(components)); } template class SparseModelMemoryProduct; diff --git a/src/storm/storage/sparse/ChoiceOrigins.cpp b/src/storm/storage/sparse/ChoiceOrigins.cpp index db6dcdd18..ac554af10 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.cpp +++ b/src/storm/storage/sparse/ChoiceOrigins.cpp @@ -47,12 +47,16 @@ namespace storm { return indexToIdentifier[choiceIndex]; } + uint_fast64_t ChoiceOrigins::getNumberOfChoices() const { + return indexToIdentifier.size(); + } + uint_fast64_t ChoiceOrigins::getIdentifierForChoicesWithNoOrigin() { return 0; } std::string const& ChoiceOrigins::getIdentifierInfo(uint_fast64_t identifier) const { - STORM_LOG_ASSERT(identifier <= this->getLargestIdentifier(), "Invalid choice origin identifier: " << identifier); + STORM_LOG_ASSERT(identifier < this->getNumberOfIdentifiers(), "Invalid choice origin identifier: " << identifier); if (identifierToInfo.empty()) { computeIdentifierInfos(); } @@ -84,7 +88,7 @@ namespace storm { storm::models::sparse::ChoiceLabeling ChoiceOrigins::toChoiceLabeling() const { storm::models::sparse::ChoiceLabeling result(indexToIdentifier.size()); - for (uint_fast64_t identifier = 0; identifier <= this->getLargestIdentifier(); ++identifier) { + for (uint_fast64_t identifier = 0; identifier < this->getNumberOfIdentifiers(); ++identifier) { storm::storage::BitVector choicesWithIdentifier = storm::utility::vector::filter(indexToIdentifier, [&identifier](uint_fast64_t i) -> bool { return i == identifier;}); if (!choicesWithIdentifier.empty()) { result.addLabel(getIdentifierInfo(identifier), std::move(choicesWithIdentifier)); diff --git a/src/storm/storage/sparse/ChoiceOrigins.h b/src/storm/storage/sparse/ChoiceOrigins.h index 15f29c1aa..0645ca466 100644 --- a/src/storm/storage/sparse/ChoiceOrigins.h +++ b/src/storm/storage/sparse/ChoiceOrigins.h @@ -37,10 +37,16 @@ namespace storm { uint_fast64_t getIdentifier(uint_fast64_t choiceIndex) const; /* - * Returns the largest identifier that is used by this object. + * Returns the number of considered identifier. * This can be used to, e.g., loop over all identifiers. */ - virtual uint_fast64_t getLargestIdentifier() const = 0; + virtual uint_fast64_t getNumberOfIdentifiers() const = 0; + + /* + * Returns the number of considered choice indices. + */ + uint_fast64_t getNumberOfChoices() const; + /* * Returns the identifier that is used for choices without an origin in the input specification * E.g., Selfloops introduced on deadlock states @@ -85,6 +91,8 @@ namespace storm { virtual void computeIdentifierInfos() const = 0; std::vector const indexToIdentifier; + + // cached identifier infos might be empty if identifiers have not been generated yet. mutable std::vector identifierToInfo; }; diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.cpp b/src/storm/storage/sparse/JaniChoiceOrigins.cpp index 35f8f92cc..4fce08388 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.cpp +++ b/src/storm/storage/sparse/JaniChoiceOrigins.cpp @@ -15,7 +15,7 @@ namespace storm { return true; } - uint_fast64_t JaniChoiceOrigins::getLargestIdentifier() const { + uint_fast64_t JaniChoiceOrigins::getNumberOfIdentifiers() const { return 0; } diff --git a/src/storm/storage/sparse/JaniChoiceOrigins.h b/src/storm/storage/sparse/JaniChoiceOrigins.h index 6d253fa68..3f0d09207 100644 --- a/src/storm/storage/sparse/JaniChoiceOrigins.h +++ b/src/storm/storage/sparse/JaniChoiceOrigins.h @@ -28,10 +28,10 @@ namespace storm { virtual bool isJaniChoiceOrigins() const override ; /* - * Returns the largest identifier that is used by this object. + * Returns the number of identifiers that are used by this object. * This can be used to, e.g., loop over all identifiers. */ - virtual uint_fast64_t getLargestIdentifier() const override; + virtual uint_fast64_t getNumberOfIdentifiers() const override; /* * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one. diff --git a/src/storm/storage/sparse/ModelComponents.h b/src/storm/storage/sparse/ModelComponents.h new file mode 100644 index 000000000..cf106b98a --- /dev/null +++ b/src/storm/storage/sparse/ModelComponents.h @@ -0,0 +1,89 @@ +#pragma once + +#include +#include +#include +#include + +#include "storm/models/ModelType.h" +#include "storm/models/sparse/StateLabeling.h" +#include "storm/models/sparse/ChoiceLabeling.h" +#include "storm/storage/sparse/StateType.h" +#include "storm/storage/sparse/StateValuations.h" +#include "storm/storage/sparse/ChoiceOrigins.h" +#include "storm/storage/SparseMatrix.h" +#include "storm/storage/BitVector.h" +#include "storm/models/sparse/StandardRewardModel.h" + +#include "storm/utility/macros.h" +#include "storm/exceptions/InvalidOperationException.h" + +namespace storm { + namespace storage { + namespace sparse { + + template> + struct ModelComponents { + + ModelComponents(storm::storage::SparseMatrix const& transitionMatrix, + storm::models::sparse::StateLabeling const& stateLabeling = storm::models::sparse::StateLabeling(), + std::unordered_map const& rewardModels = std::unordered_map(), + bool rateTransitions = false, + boost::optional const& markovianStates = boost::none, + boost::optional> const& player1Matrix = boost::none) + : transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), rewardModels(rewardModels), rateTransitions(rateTransitions), markovianStates(markovianStates), player1Matrix(player1Matrix) { + // Intentionally left empty + + // TODO: remove this output + std::cout << "Called copy constructor for model components (which should be avoided)" << std::endl; + } + + ModelComponents(storm::storage::SparseMatrix&& transitionMatrix = storm::storage::SparseMatrix(), + storm::models::sparse::StateLabeling&& stateLabeling = storm::models::sparse::StateLabeling(), + std::unordered_map&& rewardModels = std::unordered_map(), + bool rateTransitions = false, + boost::optional&& markovianStates = boost::none, + boost::optional>&& player1Matrix = boost::none) + : transitionMatrix(std::move(transitionMatrix)), stateLabeling(std::move(stateLabeling)), rewardModels(std::move(rewardModels)), rateTransitions(rateTransitions), markovianStates(std::move(markovianStates)), player1Matrix(std::move(player1Matrix)) { + // Intentionally left empty + } + + + + + // General components (applicable for all model types): + + // The transition matrix. + storm::storage::SparseMatrix transitionMatrix; + // The state labeling. + storm::models::sparse::StateLabeling stateLabeling; + // The reward models associated with the model. + std::unordered_map rewardModels; + // A vector that stores a labeling for each choice. + boost::optional choiceLabeling; + // stores for each state to which variable valuation it belongs + boost::optional stateValuations; + // stores for each choice from which parts of the input model description it originates + boost::optional> choiceOrigins; + + + // Continuous time specific components (CTMCs, Markov Automata): + + // True iff the transition values (for Markovian choices) are interpreted as rates. + bool rateTransitions; + + // The exit rate for each state. Must be given for CTMCs and MAs, if rateTransitions is false. Otherwise, it is optional. + boost::optional> exitRates; + + // A vector that stores which states are markovian (only for Markov Automata). + boost::optional markovianStates; + + + // Stochastic two player game specific components: + + // The matrix of player 1 choices (needed for stochastic two player games + boost::optional> player1Matrix; + }; + } + } +} \ No newline at end of file diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.cpp b/src/storm/storage/sparse/PrismChoiceOrigins.cpp index 6363841c7..5e19dc654 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.cpp +++ b/src/storm/storage/sparse/PrismChoiceOrigins.cpp @@ -22,7 +22,7 @@ namespace storm { return true; } - uint_fast64_t PrismChoiceOrigins::getLargestIdentifier() const { + uint_fast64_t PrismChoiceOrigins::getNumberOfIdentifiers() const { return identifierToCommandSet.size(); } @@ -43,7 +43,7 @@ namespace storm { void PrismChoiceOrigins::computeIdentifierInfos() const { this->identifierToInfo.clear(); - this->identifierToInfo.reserve(this->getLargestIdentifier() + 1); + this->identifierToInfo.reserve(this->getNumberOfIdentifiers()); for (CommandSet const& set : identifierToCommandSet) { // Get a string representation of this command set. std::stringstream setName; diff --git a/src/storm/storage/sparse/PrismChoiceOrigins.h b/src/storm/storage/sparse/PrismChoiceOrigins.h index 0a820d178..ad5e50444 100644 --- a/src/storm/storage/sparse/PrismChoiceOrigins.h +++ b/src/storm/storage/sparse/PrismChoiceOrigins.h @@ -35,10 +35,10 @@ namespace storm { virtual bool isPrismChoiceOrigins() const override ; /* - * Returns the largest identifier that is used by this object. + * Returns the number of identifier that are used by this object. * This can be used to, e.g., loop over all identifiers. */ - virtual uint_fast64_t getLargestIdentifier() const override; + virtual uint_fast64_t getNumberOfIdentifiers() const override; /* * Returns the prism program associated with this diff --git a/src/storm/storage/sparse/StateValuations.cpp b/src/storm/storage/sparse/StateValuations.cpp index 0ad9774b1..833ed9399 100644 --- a/src/storm/storage/sparse/StateValuations.cpp +++ b/src/storm/storage/sparse/StateValuations.cpp @@ -22,6 +22,10 @@ namespace storm { return valuations[state]; } + uint_fast64_t StateValuations::getNumberOfStates() const { + return valuations.size(); + } + StateValuations StateValuations::selectStates(storm::storage::BitVector const& selectedStates) const { return StateValuations(storm::utility::vector::filterVector(valuations, selectedStates)); } diff --git a/src/storm/storage/sparse/StateValuations.h b/src/storm/storage/sparse/StateValuations.h index e742505cb..84d5b7c2d 100644 --- a/src/storm/storage/sparse/StateValuations.h +++ b/src/storm/storage/sparse/StateValuations.h @@ -26,8 +26,12 @@ namespace storm { virtual ~StateValuations() = default; virtual std::string getStateInfo(storm::storage::sparse::state_type const& state) const override; + storm::expressions::SimpleValuation const& getStateValuation(storm::storage::sparse::state_type const& state) const; + // Returns the number of states that this object describes. + uint_fast64_t getNumberOfStates() const; + /* * Derive new state valuations from this by selecting the given states. */ @@ -38,7 +42,6 @@ namespace storm { * If an invalid state index is selected, the corresponding valuation will be empty. */ StateValuations selectStates(std::vector const& selectedStates) const; - private: diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index a6a0b21dc..49497237e 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -15,7 +15,6 @@ #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" - namespace storm { namespace transformer { @@ -248,30 +247,30 @@ namespace storm { template <> std::shared_ptr> GoalStateMerger>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map::RewardModelType>&& rewardModels) const { - + storm::storage::sparse::ModelComponents modelComponents(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % maybeStates; - markovianStates.resize(stateCount, true); + modelComponents.markovianStates = originalModel.getMarkovianStates() % maybeStates; + modelComponents.markovianStates->resize(stateCount, true); - std::vector exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); - exitRates.resize(stateCount, storm::utility::one()); + modelComponents.exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); + modelComponents.exitRates->resize(stateCount, storm::utility::one()); - return std::make_shared> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels)); + return std::make_shared> (std::move(modelComponents)); } template <> std::shared_ptr> GoalStateMerger>::buildOutputModel(storm::storage::BitVector const& maybeStates, ReturnType const& resultData, storm::storage::SparseMatrix&& transitionMatrix, storm::models::sparse::StateLabeling&& labeling, std::unordered_map::RewardModelType>&& rewardModels) const { - + storm::storage::sparse::ModelComponents modelComponents(std::move(transitionMatrix), std::move(labeling), std::move(rewardModels)); uint_fast64_t stateCount = maybeStates.getNumberOfSetBits() + (resultData.targetState ? 1 : 0) + (resultData.sinkState ? 1 : 0); - storm::storage::BitVector markovianStates = originalModel.getMarkovianStates() % maybeStates; - markovianStates.resize(stateCount, true); + modelComponents.markovianStates = originalModel.getMarkovianStates() % maybeStates; + modelComponents.markovianStates->resize(stateCount, true); - std::vector exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); - exitRates.resize(stateCount, storm::utility::one()); + modelComponents.exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), maybeStates); + modelComponents.exitRates->resize(stateCount, storm::utility::one()); - return std::make_shared> (std::move(transitionMatrix), std::move(labeling), std::move(markovianStates), std::move(exitRates), true, std::move(rewardModels)); + return std::make_shared> (std::move(modelComponents)); } template diff --git a/src/storm/transformer/StateDuplicator.h b/src/storm/transformer/StateDuplicator.h deleted file mode 100644 index b9c697b81..000000000 --- a/src/storm/transformer/StateDuplicator.h +++ /dev/null @@ -1,292 +0,0 @@ -#ifndef STORM_TRANSFORMER_STATEDUPLICATOR_H -#define STORM_TRANSFORMER_STATEDUPLICATOR_H - - -#include -#include - -#include "storm/models/sparse/StandardRewardModel.h" -#include "storm/utility/constants.h" -#include "storm/utility/graph.h" -#include "storm/utility/macros.h" -#include "storm/utility/vector.h" -#include "storm/models/sparse/Dtmc.h" -#include "storm/models/sparse/Mdp.h" -#include "storm/models/sparse/Ctmc.h" -#include "storm/models/sparse/MarkovAutomaton.h" - - -namespace storm { - namespace transformer { - - /* - * Duplicates the state space of the given model and redirects the incoming transitions of gateStates of the first copy to the gateStates of the second copy. - * Only states reachable from the initial states are kept. - */ - template - class StateDuplicator { - public: - - struct StateDuplicatorReturnType { - std::shared_ptr model; // The resulting model - storm::storage::BitVector firstCopy; // The states of the resulting model that correspond to the first copy - storm::storage::BitVector secondCopy; // The states of the resulting model that correspond to the second copy - storm::storage::BitVector gateStates; // The gate states of the resulting model - std::vector newToOldStateIndexMapping; // Gives for each state in the resulting model the corresponding state in the original model - std::vector firstCopyOldToNewStateIndexMapping; //Maps old indices of states in the first copy to their new indices - std::vector secondCopyOldToNewStateIndexMapping; //Maps old indices of states in the second copy to their new indices - storm::storage::BitVector duplicatedStates; // The states in the original model that have been duplicated - storm::storage::BitVector reachableStates; // The states in the original model that are reachable from the initial state - }; - - /* - * Duplicates the state space of the given model and redirects the incoming transitions of gateStates of the first copy to the gateStates of the second copy. - * - * Note that only reachable states are kept. - * Gate states will always belong to the second copy. - * Rewards and labels are duplicated accordingly. - * However, the non-gateStates in the second copy will not get the label for initial states. - * - * @param originalModel The model to be duplicated - * @param gateStates The states for which the incoming transitions are redirected - */ - static StateDuplicatorReturnType transform(SparseModelType const& originalModel, storm::storage::BitVector const& gateStates) { - STORM_LOG_DEBUG("Invoked state duplicator on model with " << originalModel.getNumberOfStates() << " states."); - StateDuplicatorReturnType result; - - // Collect some data for the result - initializeTransformation(originalModel, gateStates, result); - - // Transform the ingedients of the model - storm::storage::SparseMatrix matrix = transformMatrix(originalModel.getTransitionMatrix(), result, gateStates); - 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") { - newBitVectorForLabel &= (result.firstCopy | result.gateStates); - } - stateLabeling.addLabel(label, std::move(newBitVectorForLabel)); - } - - std::unordered_map rewardModels; - 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()) { - 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, 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; - } - - private: - - static void initializeTransformation(SparseModelType const& originalModel, storm::storage::BitVector const& gateStates, StateDuplicatorReturnType& result) { - - storm::storage::BitVector noStates(originalModel.getNumberOfStates(), false); - // Get the states that are reachable without visiting a gateState - storm::storage::BitVector statesForFirstCopy = storm::utility::graph::getReachableStates(originalModel.getTransitionMatrix(), originalModel.getInitialStates(), ~gateStates, noStates); - - // Get the states reachable from gateStates - storm::storage::BitVector statesForSecondCopy = storm::utility::graph::getReachableStates(originalModel.getTransitionMatrix(), gateStates, ~noStates, noStates); - - result.duplicatedStates = statesForFirstCopy & statesForSecondCopy; - result.reachableStates = statesForFirstCopy | statesForSecondCopy; - - uint_fast64_t numStates = statesForFirstCopy.getNumberOfSetBits() + statesForSecondCopy.getNumberOfSetBits(); - result.firstCopy = statesForFirstCopy % result.reachableStates; // only consider reachable states - result.firstCopy.resize(numStates, false); // the new states do NOT belong to the first copy - result.secondCopy = (statesForSecondCopy & (~statesForFirstCopy)) % result.reachableStates; // only consider reachable states - result.secondCopy.resize(numStates, true); // the new states DO belong to the second copy - STORM_LOG_ASSERT((result.firstCopy^result.secondCopy).full(), "firstCopy and secondCopy do not partition the state space."); - - // Get the state mappings. - // We initialize them with illegal values to assert that we don't get a valid - // state when given e.g. an unreachable state or a state from the other copy. - result.newToOldStateIndexMapping = std::vector(numStates, std::numeric_limits::max()); - 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) { - result.newToOldStateIndexMapping[newState] = oldState; - if (statesForFirstCopy.get(oldState)) { - result.firstCopyOldToNewStateIndexMapping[oldState] = newState; - } else { - result.secondCopyOldToNewStateIndexMapping[oldState] = newState; - } - ++newState; - } - // The remaining states are duplicates. All these states belong to the second copy. - - for (auto const& oldState : result.duplicatedStates) { - result.newToOldStateIndexMapping[newState] = oldState; - result.secondCopyOldToNewStateIndexMapping[oldState] = newState; - ++newState; - } - STORM_LOG_ASSERT(newState == numStates, "Unexpected state Indices"); - - result.gateStates = transformStateBitVector(gateStates, result); - } - - template - static typename std::enable_if>::value, RewardModelType>::type - transformRewardModel(RewardModelType const& originalRewardModel, std::vector const& originalRowGroupIndices, StateDuplicatorReturnType const& result, storm::storage::BitVector const& gateStates) { - boost::optional> stateRewardVector; - boost::optional> stateActionRewardVector; - boost::optional> transitionRewardMatrix; - if (originalRewardModel.hasStateRewards()) { - stateRewardVector = transformStateValueVector(originalRewardModel.getStateRewardVector(), result); - } - if (originalRewardModel.hasStateActionRewards()) { - stateActionRewardVector = transformActionValueVector(originalRewardModel.getStateActionRewardVector(), originalRowGroupIndices, result); - } - if (originalRewardModel.hasTransitionRewards()) { - transitionRewardMatrix = transformMatrix(originalRewardModel.getTransitionRewardMatrix(), result, gateStates); - } - return RewardModelType(std::move(stateRewardVector), std::move(stateActionRewardVector), std::move(transitionRewardMatrix)); - } - - template - static storm::storage::SparseMatrix transformMatrix(storm::storage::SparseMatrix const& originalMatrix, StateDuplicatorReturnType const& result, storm::storage::BitVector const& gateStates) { - // Build the builder - uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); - uint_fast64_t numRows = 0; - uint_fast64_t numEntries = 0; - for (auto const& oldState : result.newToOldStateIndexMapping) { - numRows += originalMatrix.getRowGroupSize(oldState); - numEntries += originalMatrix.getRowGroupEntryCount(oldState); - } - storm::storage::SparseMatrixBuilder builder(numRows, numStates, numEntries, true, !originalMatrix.hasTrivialRowGrouping(), originalMatrix.hasTrivialRowGrouping() ? 0 : numStates); - - // Fill in the data - uint_fast64_t newRow = 0; - 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())) { - builder.addNextValue(newRow, result.firstCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); - } 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())) { - builder.addNextValue(newRow, result.secondCopyOldToNewStateIndexMapping[entry.getColumn()], entry.getValue()); - } - } - ++newRow; - } - } - - return builder.build(); - } - - - 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) { - 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) { - v.push_back(originalVector[oldAction]); - } - } - STORM_LOG_ASSERT(v.size() == numActions, "Unexpected vector size."); - return v; - } - - template - static std::vector transformStateValueVector(std::vector const& originalVector, StateDuplicatorReturnType const& result) { - uint_fast64_t numStates = result.newToOldStateIndexMapping.size(); - std::vector v; - v.reserve(numStates); - 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 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) { - uint_fast64_t oldState = result.newToOldStateIndexMapping[newState]; - bv.set(newState, originalBitVector.get(oldState)); - } - return bv; - } - - - template - static typename std::enable_if< - std::is_same>::value || - std::is_same>::value || - std::is_same>::value, - MT>::type - createTransformedModel(MT const& /*originalModel*/, - StateDuplicatorReturnType const& /*result*/, - storm::storage::SparseMatrix& matrix, - storm::models::sparse::StateLabeling& stateLabeling, - std::unordered_map& rewardModels, - boost::optional& choiceLabeling ) { - return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); - } - - template - static typename std::enable_if< - std::is_same>::value, - MT>::type - createTransformedModel(MT const& originalModel, - StateDuplicatorReturnType const& result, - storm::storage::SparseMatrix& matrix, - storm::models::sparse::StateLabeling& stateLabeling, - std::unordered_map& rewardModels, - 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)); - } - - - }; - } -} -#endif // STORM_TRANSFORMER_STATEDUPLICATOR_H diff --git a/src/storm/transformer/SubsystemBuilder.h b/src/storm/transformer/SubsystemBuilder.h index 55dbb80fe..1b5e7bd53 100644 --- a/src/storm/transformer/SubsystemBuilder.h +++ b/src/storm/transformer/SubsystemBuilder.h @@ -14,6 +14,8 @@ #include "storm/models/sparse/Mdp.h" #include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/MarkovAutomaton.h" +#include "storm/storage/sparse/ModelComponents.h" +#include "storm/utility/builder.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" @@ -84,26 +86,33 @@ namespace storm { STORM_LOG_THROW(stateHasOneChoiceLeft, storm::exceptions::InvalidArgumentException, "The subsystem would contain a deadlock state."); } - // Transform the ingedients of the model - storm::storage::SparseMatrix matrix = originalModel.getTransitionMatrix().getSubmatrix(false, result.keptActions, subsystemStates); - storm::models::sparse::StateLabeling labeling = originalModel.getStateLabeling().getSubLabeling(subsystemStates); - std::unordered_map rewardModels; + // Transform the components of the model + storm::storage::sparse::ModelComponents components; + components.transitionMatrix = originalModel.getTransitionMatrix().getSubmatrix(false, result.keptActions, subsystemStates); + components.stateLabeling = originalModel.getStateLabeling().getSubLabeling(subsystemStates); for (auto const& rewardModel : originalModel.getRewardModels()){ - rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, result.keptActions))); + components.rewardModels.insert(std::make_pair(rewardModel.first, transformRewardModel(rewardModel.second, subsystemStates, result.keptActions))); } - boost::optional choiceLabeling; if (originalModel.hasChoiceLabeling()) { - choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(result.keptActions); + components.choiceLabeling = originalModel.getChoiceLabeling().getSubLabeling(result.keptActions); } - result.model = std::make_shared(createTransformedModel(originalModel, subsystemStates, matrix, labeling, rewardModels, choiceLabeling)); + if (originalModel.hasStateValuations()) { + components.stateValuations = originalModel.getStateValuations().selectStates(subsystemStateCount); + } + if (originalModel.hasChoiceOrigins()) { + components.choiceOrigins = originalModel.getChoiceOrigins().selectChoices(result.keptActions); + } + + transformModelSpecificComponents(originalModel, subsystemStates, components); + + result.model = storm::utility::builder::buildModelFromComponents(originalModel.getType(), std::move(components)); STORM_LOG_DEBUG("Subsystem Builder is done. Resulting model has " << result.model->getNumberOfStates() << " states."); return result; } private: - template - static typename std::enable_if>::value, RewardModelType>::type - transformRewardModel(RewardModelType const& originalRewardModel, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& subsystemActions) { + template + static RewardModelType transformRewardModel(RewardModelType const& originalRewardModel, storm::storage::BitVector const& subsystem, storm::storage::BitVector const& subsystemActions) { boost::optional> stateRewardVector; boost::optional> stateActionRewardVector; boost::optional> transitionRewardMatrix; @@ -122,32 +131,37 @@ namespace storm { template static typename std::enable_if< std::is_same>::value || - std::is_same>::value || - std::is_same>::value, + std::is_same>::value, MT>::type - createTransformedModel(MT const& /*originalModel*/, + transformModelSpecificComponents(MT const&, storm::storage::BitVector const& /*subsystem*/, - storm::storage::SparseMatrix& matrix, - storm::models::sparse::StateLabeling& stateLabeling, - std::unordered_map& rewardModels, - boost::optional& choiceLabeling ) { - return MT(std::move(matrix), std::move(stateLabeling), std::move(rewardModels), std::move(choiceLabeling)); + storm::storage::sparse::ModelComponents&) { + // Intentionally left empty } + template + static typename std::enable_if< + std::is_same>::value, + MT>::type + transformModelSpecificComponents(MT const& originalModel, + storm::storage::BitVector const& subsystem, + storm::storage::SparseMatrix& matrix, + storm::storage::sparse::ModelComponents& components) { + components.exitRates = storm::utility::vector::filterVector(originalModel.getExitRateVector(), subsystem); + components.rateTransitions = true; + } + template static typename std::enable_if< std::is_same>::value, MT>::type - createTransformedModel(MT const& originalModel, + transformModelSpecificComponents(MT const& originalModel, storm::storage::BitVector const& subsystem, storm::storage::SparseMatrix& matrix, - storm::models::sparse::StateLabeling& stateLabeling, - std::unordered_map& rewardModels, - 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)); + storm::storage::sparse::ModelComponents& components) { + components.markovianStates = originalModel.getMarkovianStates() % subsystem; + components.exitRates = storm::utility::vector::filterVector(originalModel.getExitRates(), subsystem); + components.rateTransitions = false; // Note that originalModel.getTransitionMatrix() contains probabilities } }; diff --git a/src/storm/utility/ModelInstantiator.h b/src/storm/utility/ModelInstantiator.h index d784c49ea..fa1ba8099 100644 --- a/src/storm/utility/ModelInstantiator.h +++ b/src/storm/utility/ModelInstantiator.h @@ -63,9 +63,12 @@ namespace storm { std::is_same>::value >::type initializeModelSpecificData(PMT const& parametricModel) { - auto stateLabelingCopy = parametricModel.getStateLabeling(); - auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); - this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + storm::storage::sparse::ModelComponents components(buildDummyMatrix(parametricModel.getTransitionMatrix())); + components.stateLabeling = parametricModel.getStateLabeling(); + components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels()); + components.choiceLabeling = parametricModel.getOptionalChoiceLabeling(); + + this->instantiatedModel = std::make_shared(std::move(components)); } template @@ -73,10 +76,13 @@ namespace storm { std::is_same>::value >::type initializeModelSpecificData(PMT const& parametricModel) { - auto stateLabelingCopy = parametricModel.getStateLabeling(); - auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); - std::vector exitRates(parametricModel.getExitRateVector().size(), storm::utility::one()); - this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(exitRates), std::move(stateLabelingCopy), buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); + storm::storage::sparse::ModelComponents components(buildDummyMatrix(parametricModel.getTransitionMatrix())); + components.stateLabeling = parametricModel.getStateLabeling(); + components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels()); + components.exitRates = std::vector(parametricModel.getExitRateVector().size(), storm::utility::one()); + components.rateTransitions = true; + components.choiceLabeling = parametricModel.getOptionalChoiceLabeling(); + this->instantiatedModel = std::make_shared(std::move(components)); initializeVectorMapping(this->instantiatedModel->getExitRateVector(), this->functions, this->vectorMapping, parametricModel.getExitRateVector()); } @@ -87,12 +93,14 @@ namespace storm { std::is_same>::value >::type initializeModelSpecificData(PMT const& parametricModel) { - auto stateLabelingCopy = parametricModel.getStateLabeling(); - auto markovianStatesCopy = parametricModel.getMarkovianStates(); - auto choiceLabelingCopy = parametricModel.getOptionalChoiceLabeling(); - std::vector exitRates(parametricModel.getExitRates().size(), storm::utility::one()); - this->instantiatedModel = std::make_shared(buildDummyMatrix(parametricModel.getTransitionMatrix()), std::move(stateLabelingCopy), std::move(markovianStatesCopy), std::move(exitRates), true, buildDummyRewardModels(parametricModel.getRewardModels()), std::move(choiceLabelingCopy)); - + storm::storage::sparse::ModelComponents components(buildDummyMatrix(parametricModel.getTransitionMatrix())); + components.stateLabeling = parametricModel.getStateLabeling(); + components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels()); + components.exitRates = std::vector(parametricModel.getExitRates().size(), storm::utility::one()); + components.markovianStates = parametricModel.getMarkovianStates(); + components.choiceLabeling = parametricModel.getOptionalChoiceLabeling(); + this->instantiatedModel = std::make_shared(std::move(components)); + initializeVectorMapping(this->instantiatedModel->getExitRates(), this->functions, this->vectorMapping, parametricModel.getExitRates()); } @@ -101,12 +109,13 @@ namespace storm { std::is_same>::value >::type initializeModelSpecificData(PMT const& parametricModel) { - auto player1MatrixCopy = parametricModel.getPlayer1Matrix(); - auto stateLabelingCopy = parametricModel.getStateLabeling(); - 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)); + storm::storage::sparse::ModelComponents components(buildDummyMatrix(parametricModel.getTransitionMatrix())); + components.stateLabeling = parametricModel.getStateLabeling(); + components.rewardModels = buildDummyRewardModels(parametricModel.getRewardModels()); + components.player1Matrix = parametricModel.getPlayer1Matrix(); + components.choiceLabeling = parametricModel.getOptionalChoiceLabeling(); + + this->instantiatedModel = std::make_shared(std::move(components)); } /*! diff --git a/src/storm/utility/builder.cpp b/src/storm/utility/builder.cpp new file mode 100644 index 000000000..9ace27060 --- /dev/null +++ b/src/storm/utility/builder.cpp @@ -0,0 +1,35 @@ +#include +#include "storm/utility/builder.h" + +#include "storm/models/sparse/Dtmc.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/models/sparse/Mdp.h" +#include "storm/models/sparse/MarkovAutomaton.h" + +namespace storm { + namespace utility { + namespace builder { + + template + std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components) { + switch (modelType) { + case storm::models::ModelType::Dtmc: + return std::make_shared>(std::move(components)); + case storm::models::ModelType::Ctmc: + return std::make_shared>(std::move(components)); + case storm::models::ModelType::Mdp: + return std::make_shared>(std::move(components)); + case storm::models::ModelType::MarkovAutomaton: + return std::make_shared>(std::move(components)); + case storm::models::ModelType::S2pg: + return std::make_shared>(std::move(components)); + } + } + + template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); + template std::shared_ptr>> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents>&& components); + template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); + template std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); + } + } +} \ No newline at end of file diff --git a/src/storm/utility/builder.h b/src/storm/utility/builder.h new file mode 100644 index 000000000..936191129 --- /dev/null +++ b/src/storm/utility/builder.h @@ -0,0 +1,19 @@ +#pragma once + +#include + +#include "storm/models/ModelType.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/sparse/ModelComponents.h" + +namespace storm { + namespace utility { + namespace builder { + + template> + std::shared_ptr> buildModelFromComponents(storm::models::ModelType modelType, storm::storage::sparse::ModelComponents&& components); + + } + } +} diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h index 19848b6b0..c77092923 100644 --- a/src/storm/utility/counterexamples.h +++ b/src/storm/utility/counterexamples.h @@ -16,11 +16,15 @@ namespace storm { * @return The set of Prism commands that is visited on all paths from any state to a target state. */ template - 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) { + std::vector> getGuaranteedCommandSets(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantCommands) { + STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without choice origns."); + STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins."); + // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins(); // 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); @@ -102,8 +106,8 @@ namespace storm { * @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 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 getGuaranteedCommandSet(storm::models::sparse::Mdp const& mdp, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantCommands) { + std::vector> guaranteedCommands = getGuaranteedCommandSets(mdp, psiStates, relevantCommands); boost::container::flat_set knownCommands(relevantCommands); boost::container::flat_set tempIntersection; diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 6dd2b758c..df73d87aa 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -146,7 +146,7 @@ namespace storm { std::vector filterProperties(std::vector const& properties, boost::optional> const& propertyFilter); template - storm::builder::ExplicitModelBuilderResult buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { + std::shared_ptr> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector> const& formulas) { storm::builder::BuilderOptions options(formulas); if (storm::settings::getModule().isBuildChoiceLabelsSet()) { @@ -302,7 +302,7 @@ namespace storm { } template - void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::shared_ptr choiceOrigins, std::shared_ptr const& formula) { + void generateCounterexample(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, 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."); @@ -314,9 +314,9 @@ namespace storm { bool useMILP = storm::settings::getModule().isUseMilpBasedMinimalCommandSetGenerationSet(); if (useMILP) { - storm::counterexamples::MILPMinimalCommandSetGenerator::computeCounterexample(program, *mdp, choiceOrigins, formula); + storm::counterexamples::MILPMinimalCommandSetGenerator::computeCounterexample(program, *mdp, formula); } else { - storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, choiceOrigins, formula); + storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, storm::settings::getModule().getConstantDefinitionString(), *mdp, formula); } } else { @@ -326,20 +326,20 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, std::shared_ptr> , std::shared_ptr, std::shared_ptr const& ) { + inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, 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, std::shared_ptr const& ) { + inline void generateCounterexample(storm::storage::SymbolicModelDescription const&, 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::shared_ptr choiceOrigins, std::vector> const& formulas) { + void generateCounterexamples(storm::storage::SymbolicModelDescription const& model, std::shared_ptr> markovModel, std::vector> const& formulas) { for (auto const& formula : formulas) { - generateCounterexample(model, markovModel, choiceOrigins, formula); + generateCounterexample(model, markovModel, formula); } } diff --git a/src/test/transformer/StateDuplicatorTest.cpp b/src/test/transformer/StateDuplicatorTest.cpp deleted file mode 100644 index d26eee055..000000000 --- a/src/test/transformer/StateDuplicatorTest.cpp +++ /dev/null @@ -1,100 +0,0 @@ -#include "gtest/gtest.h" - -#include "storm/transformer/StateDuplicator.h" - - -TEST(StateDuplicator, SimpleModelTest) { - - storm::storage::SparseMatrix matrix; - storm::storage::SparseMatrixBuilder builder(6, 4, 7, true, true, 4); - ASSERT_NO_THROW(builder.newRowGroup(0)); - ASSERT_NO_THROW(builder.addNextValue(0, 0, 0.3)); - ASSERT_NO_THROW(builder.addNextValue(0, 1, 0.7)); - ASSERT_NO_THROW(builder.addNextValue(1, 3, 1.0)); - ASSERT_NO_THROW(builder.newRowGroup(2)); - ASSERT_NO_THROW(builder.addNextValue(2, 1, 1.0)); - ASSERT_NO_THROW(builder.newRowGroup(3)); - ASSERT_NO_THROW(builder.addNextValue(3, 0, 1.0)); - ASSERT_NO_THROW(builder.newRowGroup(4)); - ASSERT_NO_THROW(builder.addNextValue(4, 0, 1.0)); - ASSERT_NO_THROW(builder.addNextValue(5, 3, 1.0)); - ASSERT_NO_THROW(matrix = builder.build()); - - storm::models::sparse::StateLabeling labeling(4); - storm::storage::BitVector initStates(4); - initStates.set(0); - labeling.addLabel("init", initStates); - storm::storage::BitVector gateStates(4); - gateStates.set(3); - labeling.addLabel("gate", gateStates); - storm::storage::BitVector aStates(4); - aStates.set(0); - aStates.set(2); - labeling.addLabel("a", aStates); - storm::storage::BitVector bStates(4); - bStates.set(1); - bStates.set(3); - labeling.addLabel("b", bStates); - - std::unordered_map> rewardModels; - std::vector stateReward = {1.0, 2.0, 3.0, 4.0}; - std::vector stateActionReward = {1.1, 1.2, 2.1, 3.1, 4.1, 4.2}; - rewardModels.insert(std::make_pair("rewards", storm::models::sparse::StandardRewardModel(stateReward, stateActionReward))); - - storm::models::sparse::Mdp model(matrix, labeling, rewardModels); - - auto res = storm::transformer::StateDuplicator>::transform(model, gateStates); - - storm::storage::SparseMatrixBuilder expectedBuilder(8, 5, 10, true, true, 5); - ASSERT_NO_THROW(expectedBuilder.newRowGroup(0)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(0, 0, 0.3)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(0, 1, 0.7)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(1, 2, 1.0)); - ASSERT_NO_THROW(expectedBuilder.newRowGroup(2)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(2, 1, 1.0)); - ASSERT_NO_THROW(expectedBuilder.newRowGroup(3)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(3, 3, 1.0)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(4, 2, 1.0)); - ASSERT_NO_THROW(expectedBuilder.newRowGroup(5)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(5, 3, 0.3)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(5, 4, 0.7)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(6, 2, 1.0)); - ASSERT_NO_THROW(expectedBuilder.newRowGroup(7)); - ASSERT_NO_THROW(expectedBuilder.addNextValue(7, 4, 1.0)); - ASSERT_NO_THROW(matrix = expectedBuilder.build()); - EXPECT_EQ(matrix, res.model->getTransitionMatrix()); - - initStates.resize(5); - EXPECT_EQ(initStates, res.model->getInitialStates()); - gateStates=storm::storage::BitVector(5); - gateStates.set(2); - EXPECT_EQ(gateStates, res.model->getStates("gate")); - aStates = initStates; - aStates.set(3); - EXPECT_EQ(aStates, res.model->getStates("a")); - bStates = ~aStates; - EXPECT_EQ(bStates, res.model->getStates("b")); - - EXPECT_TRUE(res.model->hasRewardModel("rewards")); - EXPECT_TRUE(res.model->getRewardModel("rewards").hasStateRewards()); - stateReward = {1.0, 2.0, 4.0, 1.0, 2.0}; - EXPECT_EQ(stateReward, res.model->getRewardModel("rewards").getStateRewardVector()); - EXPECT_TRUE(res.model->getRewardModel("rewards").hasStateActionRewards()); - stateActionReward = {1.1, 1.2, 2.1, 4.1, 4.2, 1.1, 1.2, 2.1}; - EXPECT_EQ(stateActionReward, res.model->getRewardModel("rewards").getStateActionRewardVector()); - - storm::storage::BitVector firstCopy(5); - firstCopy.set(0); - firstCopy.set(1); - EXPECT_EQ(firstCopy, res.firstCopy); - EXPECT_EQ(~firstCopy, res.secondCopy); - - std::vector mapping = {0,1,3,0,1}; - EXPECT_EQ(mapping, res.newToOldStateIndexMapping); - uint_fast64_t max = std::numeric_limits::max(); - mapping = {0, 1, max, max}; - EXPECT_EQ(mapping, res.firstCopyOldToNewStateIndexMapping); - mapping = {3, 4, max, 2}; - EXPECT_EQ(mapping, res.secondCopyOldToNewStateIndexMapping); - -}