diff --git a/CHANGELOG.md b/CHANGELOG.md index da86c5d73..3a5c36231 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -8,6 +8,7 @@ Version 1.4.x ------------- ## Version 1.4.2 (under development) +- DRN: support import of choice labelling - `storm-pomdp`: Only accept POMDPs that are canonical - `storm-pomdp`: Prism language extended with observable expressions - `storm-pomdp`: Various fixes that prevented usage. diff --git a/CMakeLists.txt b/CMakeLists.txt index 958e90983..5ef92dd45 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -493,7 +493,7 @@ include(CTest) # Compiles all tests add_custom_target(tests) # Compiles and runs all tests -add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND}) +add_custom_target(check COMMAND ${CMAKE_CTEST_COMMAND} --output-on-failure) set(CMAKE_CTEST_COMMAND_VERBOSE ${CMAKE_CTEST_COMMAND} -V) add_custom_target(check-verbose COMMAND ${CMAKE_CTEST_COMMAND_VERBOSE}) add_dependencies(check tests) diff --git a/resources/examples/testfiles/ma/chain_elimination1.drn b/resources/examples/testfiles/ma/chain_elimination1.drn new file mode 100644 index 000000000..4be37cb3a --- /dev/null +++ b/resources/examples/testfiles/ma/chain_elimination1.drn @@ -0,0 +1,155 @@ +// Exported by storm +// Original model type: Markov Automaton +@type: Markov Automaton +@parameters + +@reward_models + +@nr_states +43 +@model +state 0 !0 init + action 0 + 1 : 1 +state 1 !0.0003 + action 0 + 2 : 0.3333333333 + 3 : 0.3333333333 + 4 : 0.3333333333 +state 2 !0 + action 0 + 5 : 1 +state 3 !0 + action 0 + 6 : 1 +state 4 !0 + action 0 + 7 : 1 +state 5 !0 + action 0 + 8 : 1 +state 6 !0 + action 0 + 9 : 1 +state 7 !0 + action 0 + 10 : 1 +state 8 !0 + action 0 + 12 : 1 +state 9 !0 + action 0 + 14 : 1 +state 10 !0.1002 Fail + action 0 + 11 : 0.000998003992 + 13 : 0.000998003992 + 15 : 0.998003992 +state 11 !0 Fail + action 0 + 18 : 1 +state 12 !0.1002 Fail + action 0 + 16 : 0.000998003992 + 19 : 0.000998003992 + 20 : 0.998003992 +state 13 !0 Fail + action 0 + 21 : 1 +state 14 !0.1002 Fail + action 0 + 17 : 0.000998003992 + 22 : 0.000998003992 + 23 : 0.998003992 +state 15 !0 Fail + action 0 + 24 : 1 +state 16 !0 Fail + action 0 + 25 : 1 +state 17 !0 Fail + action 0 + 25 : 1 +state 18 !0 Fail + action 0 + 26 : 1 +state 19 !0 Fail + action 0 + 26 : 1 +state 20 !0 Fail + action 0 + 27 : 1 +state 21 !0 Fail + action 0 + 28 : 1 +state 22 !0 Fail + action 0 + 28 : 1 +state 23 !0 Fail + action 0 + 27 : 1 +state 24 !0 Fail + action 0 + 1 : 1 +state 25 !0.2001 Fail + action 0 + 31 : 0.0004997501249 + 32 : 0.4997501249 + 33 : 0.4997501249 +state 26 !0.2001 Fail + action 0 + 29 : 0.0004997501249 + 34 : 0.4997501249 + 35 : 0.4997501249 +state 27 !0 Fail + action 0 + 24 : 1 +state 28 !0.2001 Fail + action 0 + 30 : 0.0004997501249 + 36 : 0.4997501249 + 37 : 0.4997501249 +state 29 !0 Fail + action 0 + 38 : 1 +state 30 !0 Fail + action 0 + 38 : 1 +state 31 !0 Fail + action 0 + 38 : 1 +state 32 !0 Fail + action 0 + 14 : 1 +state 33 !0 Fail + action 0 + 12 : 1 +state 34 !0 Fail + action 0 + 12 : 1 +state 35 !0 Fail + action 0 + 39 : 1 +state 36 !0 Fail + action 0 + 14 : 1 +state 37 !0 Fail + action 0 + 39 : 1 +state 38 !0.3 Fail + action 0 + 40 : 0.3333333333 + 41 : 0.3333333333 + 42 : 0.3333333333 +state 39 !0 Fail + action 0 + 10 : 1 +state 40 !0 Fail + action 0 + 25 : 1 +state 41 !0 Fail + action 0 + 28 : 1 +state 42 !0 Fail + action 0 + 26 : 1 diff --git a/resources/examples/testfiles/ma/chain_elimination2.drn b/resources/examples/testfiles/ma/chain_elimination2.drn new file mode 100644 index 000000000..225843eec --- /dev/null +++ b/resources/examples/testfiles/ma/chain_elimination2.drn @@ -0,0 +1,34 @@ +// Exported by storm +// Original model type: Markov Automaton +@type: Markov Automaton +@parameters + +@reward_models + +@nr_states +10 +@model +state 0 !0.1 init + 1 : 1 +state 1 !0 + 2 : 1 +state 2 !0 + 3 : 1 +state 3 !0 + 4 : 0.1 + 5 : 0.9 +state 4 !0.2 Fail + 5 : 0.5 + 6 : 0.5 +state 5 !0.1 + 0 : 1 +state 6 !0.2 + 0 : 0.5 + 7 : 0.5 +state 7 !0.2 Fail + 6 : 0.5 + 8 : 0.5 +state 8 !0 Fail + 9 : 1 +state 9 !0 Fail + 3 : 1 diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 982dd0092..a49d244e5 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -292,12 +292,14 @@ namespace storm { } template - std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings) { + std::shared_ptr buildModelExplicit(storm::settings::modules::IOSettings const& ioSettings, storm::settings::modules::BuildSettings const& buildSettings) { std::shared_ptr result; if (ioSettings.isExplicitSet()) { result = storm::api::buildExplicitModel(ioSettings.getTransitionFilename(), ioSettings.getLabelingFilename(), ioSettings.isStateRewardsSet() ? boost::optional(ioSettings.getStateRewardsFilename()) : boost::none, ioSettings.isTransitionRewardsSet() ? boost::optional(ioSettings.getTransitionRewardsFilename()) : boost::none, ioSettings.isChoiceLabelingSet() ? boost::optional(ioSettings.getChoiceLabelingFilename()) : boost::none); } else if (ioSettings.isExplicitDRNSet()) { - result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename()); + storm::parser::DirectEncodingParserOptions options; + options.buildChoiceLabeling = buildSettings.isBuildChoiceLabelsSet(); + result = storm::api::buildExplicitDRNModel(ioSettings.getExplicitDRNFilename(), options); } else { STORM_LOG_THROW(ioSettings.isExplicitIMCASet(), storm::exceptions::InvalidSettingsException, "Unexpected explicit model input type."); result = storm::api::buildExplicitIMCAModel(ioSettings.getExplicitIMCAFilename()); @@ -320,7 +322,7 @@ namespace storm { } } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) { STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input."); - result = buildModelExplicit(ioSettings); + result = buildModelExplicit(ioSettings, buildSettings); } modelBuildingWatch.stop(); diff --git a/src/storm-dft/settings/DftSettings.cpp b/src/storm-dft/settings/DftSettings.cpp index 4ff3e2aaf..a3d0bf4ed 100644 --- a/src/storm-dft/settings/DftSettings.cpp +++ b/src/storm-dft/settings/DftSettings.cpp @@ -24,6 +24,7 @@ #include "storm-gspn/settings/modules/GSPNSettings.h" #include "storm-gspn/settings/modules/GSPNExportSettings.h" #include "storm/settings/modules/TransformationSettings.h" +#include "storm/settings/modules/HintSettings.h" namespace storm { @@ -39,6 +40,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); diff --git a/src/storm-pars/settings/ParsSettings.cpp b/src/storm-pars/settings/ParsSettings.cpp index c0aab397d..36a16e33a 100644 --- a/src/storm-pars/settings/ParsSettings.cpp +++ b/src/storm-pars/settings/ParsSettings.cpp @@ -26,6 +26,8 @@ #include "storm/settings/modules/JitBuilderSettings.h" #include "storm/settings/modules/MultiplierSettings.h" #include "storm/settings/modules/TransformationSettings.h" +#include "storm/settings/modules/HintSettings.h" + namespace storm { @@ -57,6 +59,8 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + + storm::settings::addModule(); } } diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp index d77415f72..4814c77f5 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.cpp +++ b/src/storm-parsers/parser/DirectEncodingParser.cpp @@ -28,7 +28,7 @@ namespace storm { namespace parser { template - std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename) { + std::shared_ptr> DirectEncodingParser::parseModel(std::string const& filename, DirectEncodingParserOptions const& options) { // Load file STORM_LOG_INFO("Reading from file " << filename); @@ -42,6 +42,7 @@ namespace storm { bool sawParameters = false; std::unordered_map placeholders; size_t nrStates = 0; + size_t nrChoices = 0; storm::models::ModelType type; std::vector rewardModelNames; std::shared_ptr> modelComponents; @@ -102,14 +103,19 @@ namespace storm { STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice"); std::getline(file, line); nrStates = parseNumber(line); + } else if (line == "@nr_choices") { + STORM_LOG_THROW(nrChoices == 0, storm::exceptions::WrongFormatException, "Number of actions declared twice"); + std::getline(file, line); + nrChoices = parseNumber(line); } else if (line == "@model") { // Parse rest of the model STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model."); STORM_LOG_THROW(sawParameters, storm::exceptions::WrongFormatException, "Parameters have to be declared before model."); STORM_LOG_THROW(nrStates != 0, storm::exceptions::WrongFormatException, "No. of states has to be declared before model."); - + STORM_LOG_THROW(!options.buildChoiceLabeling || nrChoices != 0, storm::exceptions::WrongFormatException, "No. of actions (@nr_choices) has to be declared before model."); + STORM_LOG_WARN_COND(nrChoices != 0, "No. of actions has to be declared. We may continue now, but future versions might not support this."); // Construct model components - modelComponents = parseStates(file, type, nrStates, placeholders, valueParser, rewardModelNames); + modelComponents = parseStates(file, type, nrStates, nrChoices, placeholders, valueParser, rewardModelNames, options); break; } else { STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse line '" << line << "'."); @@ -124,9 +130,9 @@ namespace storm { template std::shared_ptr> - DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, + DirectEncodingParser::parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices, std::unordered_map const& placeholders, ValueParser const& valueParser, - std::vector const& rewardModelNames) { + std::vector const& rewardModelNames, DirectEncodingParserOptions const& options) { // Initialize auto modelComponents = std::make_shared>(); bool nonDeterministic = (type == storm::models::ModelType::Mdp || type == storm::models::ModelType::MarkovAutomaton || type == storm::models::ModelType::Pomdp); @@ -135,6 +141,9 @@ namespace storm { modelComponents->stateLabeling = storm::models::sparse::StateLabeling(stateSize); modelComponents->observabilityClasses = std::vector(); modelComponents->observabilityClasses->resize(stateSize); + if (options.buildChoiceLabeling) { + modelComponents->choiceLabeling = storm::models::sparse::ChoiceLabeling(nrChoices); + } std::vector> stateRewards; std::vector> actionRewards; if (continuousTime) { @@ -296,8 +305,16 @@ namespace storm { } else { line = ""; } - size_t parsedId = parseNumber(curString); - STORM_LOG_ASSERT(row == firstRowOfState + parsedId, "Action ids do not correspond."); + + // curString contains action name. + if (options.buildChoiceLabeling) { + if (curString != "__NOLABEL__") { + if (!modelComponents->choiceLabeling.get().containsLabel(curString)) { + modelComponents->choiceLabeling.get().addLabel(curString); + } + modelComponents->choiceLabeling.get().addLabelToChoice(curString, row); + } + } // Check for rewards if (boost::starts_with(line, "[")) { // Rewards found @@ -323,7 +340,6 @@ namespace storm { } line = line.substr(posEndReward + 1); } - // TODO import choice labeling when the export works } else { // New transition diff --git a/src/storm-parsers/parser/DirectEncodingParser.h b/src/storm-parsers/parser/DirectEncodingParser.h index 5637a2f46..6c4254013 100644 --- a/src/storm-parsers/parser/DirectEncodingParser.h +++ b/src/storm-parsers/parser/DirectEncodingParser.h @@ -9,6 +9,9 @@ namespace storm { namespace parser { + struct DirectEncodingParserOptions { + bool buildChoiceLabeling = false; + }; /*! * Parser for models in the DRN format with explicit encoding. */ @@ -23,7 +26,7 @@ namespace storm { * * @return A sparse model */ - static std::shared_ptr> parseModel(std::string const& file); + static std::shared_ptr> parseModel(std::string const& fil, DirectEncodingParserOptions const& options = DirectEncodingParserOptions()); private: @@ -40,8 +43,8 @@ namespace storm { * @return Transition matrix. */ static std::shared_ptr> - parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, std::unordered_map const& placeholders, - ValueParser const& valueParser, std::vector const& rewardModelNames); + parseStates(std::istream& file, storm::models::ModelType type, size_t stateSize, size_t nrChoices, std::unordered_map const& placeholders, + ValueParser const& valueParser, std::vector const& rewardModelNames, DirectEncodingParserOptions const& options); /*! * Parse value from string while using placeholders. diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h index 5fc7898ee..0df66c7ff 100644 --- a/src/storm/api/builder.h +++ b/src/storm/api/builder.h @@ -144,8 +144,8 @@ namespace storm { } template - std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile) { - return storm::parser::DirectEncodingParser::parseModel(drnFile); + std::shared_ptr> buildExplicitDRNModel(std::string const& drnFile, storm::parser::DirectEncodingParserOptions const& options = storm::parser::DirectEncodingParserOptions()) { + return storm::parser::DirectEncodingParser::parseModel(drnFile, options); } template diff --git a/src/storm/models/sparse/ItemLabeling.cpp b/src/storm/models/sparse/ItemLabeling.cpp index 3cd32700b..5f5ffc548 100644 --- a/src/storm/models/sparse/ItemLabeling.cpp +++ b/src/storm/models/sparse/ItemLabeling.cpp @@ -64,6 +64,25 @@ namespace storm { addLabel(label, storage::BitVector(itemCount)); } + void ItemLabeling::removeLabel(std::string const& label) { + auto labelIt = nameToLabelingIndexMap.find(label); + STORM_LOG_THROW(labelIt != nameToLabelingIndexMap.end(), storm::exceptions::InvalidArgumentException, "Label '" << label << "' does not exist."); + uint64_t labelIndex = labelIt->second; + // Erase entry in map + nameToLabelingIndexMap.erase(labelIt); + // Erase label by 'swap and pop' + std::iter_swap(labelings.begin() + labelIndex, labelings.end() - 1); + labelings.pop_back(); + + // Update index of labeling we swapped from the end + for (auto& it: nameToLabelingIndexMap) { + if (it.second == labelings.size()) { + it.second = labelIndex; + break; + } + } + } + void ItemLabeling::join(ItemLabeling const& other) { STORM_LOG_THROW(this->itemCount == other.itemCount, storm::exceptions::InvalidArgumentException, "The item count of the two labelings does not match: " << this->itemCount << " vs. " << other.itemCount << "."); for (auto const& label : other.getLabels()) { @@ -123,11 +142,17 @@ namespace storm { } void ItemLabeling::addLabelToItem(std::string const& label, uint64_t item) { - STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::OutOfRangeException, "Label '" << label << "' unknown."); + STORM_LOG_THROW(this->containsLabel(label), storm::exceptions::InvalidArgumentException, "Label '" << label << "' unknown."); STORM_LOG_THROW(item < itemCount, storm::exceptions::OutOfRangeException, "Item index out of range."); this->labelings[nameToLabelingIndexMap.at(label)].set(item, true); } + void ItemLabeling::removeLabelFromItem(std::string const& label, uint64_t item) { + STORM_LOG_THROW(item < itemCount, storm::exceptions::OutOfRangeException, "Item index out of range."); + STORM_LOG_THROW(this->getItemHasLabel(label, item),storm::exceptions::InvalidArgumentException, "Item " << item << " does not have label '" << label << "'."); + this->labelings[nameToLabelingIndexMap.at(label)].set(item, false); + } + bool ItemLabeling::getItemHasLabel(std::string const& label, uint64_t item) 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)].get(item); diff --git a/src/storm/models/sparse/ItemLabeling.h b/src/storm/models/sparse/ItemLabeling.h index 0f774b792..7f6c9ce55 100644 --- a/src/storm/models/sparse/ItemLabeling.h +++ b/src/storm/models/sparse/ItemLabeling.h @@ -51,7 +51,6 @@ namespace storm { */ bool operator==(ItemLabeling const& other) const; - /*! * Adds a new label to the labelings. Initially, no item is labeled with this label. * @@ -59,6 +58,13 @@ namespace storm { */ void addLabel(std::string const& label); + /*! + * Removes a label from the labelings. + * + * @param label The name of the label to remove. + */ + void removeLabel(std::string const& label); + /*! * Retrieves the set of labels contained in this labeling. * @@ -191,7 +197,14 @@ namespace storm { */ virtual void addLabelToItem(std::string const& label, uint64_t item); - + /*! + * Removes a label from a given item. + * + * @param label The name of the label to remove. + * @param item The index of the item. + */ + virtual void removeLabelFromItem(std::string const& label, uint64_t item); + // The number of items for which this object can hold the labeling. uint64_t itemCount; diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 5a6f00466..6e7070546 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -272,8 +272,8 @@ namespace storm { //TODO update reward models and choice labels according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); 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."); + STORM_LOG_WARN_COND(!this->hasStateValuations(), "Conversion of MA to CTMC does not preserve state valuations."); + STORM_LOG_WARN_COND(!this->hasChoiceOrigins(), "Conversion of MA to CTMC does not preserve choice origins."); return std::make_shared>(std::move(rateMatrix), std::move(stateLabeling)); } diff --git a/src/storm/models/sparse/StateLabeling.cpp b/src/storm/models/sparse/StateLabeling.cpp index bcb00b7a9..1f0f88b8d 100644 --- a/src/storm/models/sparse/StateLabeling.cpp +++ b/src/storm/models/sparse/StateLabeling.cpp @@ -52,6 +52,10 @@ namespace storm { void StateLabeling::addLabelToState(std::string const& label, storm::storage::sparse::state_type state) { ItemLabeling::addLabelToItem(label, state); } + + void StateLabeling::removeLabelFromState(std::string const& label, storm::storage::sparse::state_type state) { + ItemLabeling::removeLabelFromItem(label, state); + } bool StateLabeling::getStateHasLabel(std::string const& label, storm::storage::sparse::state_type state) const { return ItemLabeling::getItemHasLabel(label, state); diff --git a/src/storm/models/sparse/StateLabeling.h b/src/storm/models/sparse/StateLabeling.h index d781fb4f4..ad431d0e2 100644 --- a/src/storm/models/sparse/StateLabeling.h +++ b/src/storm/models/sparse/StateLabeling.h @@ -65,6 +65,14 @@ namespace storm { * @param state The index of the state to label. */ void addLabelToState(std::string const& label, storm::storage::sparse::state_type state); + + /*! + * Removes a label from a given state. + * + * @param label The name of the label to remove. + * @param state The index of the state. + */ + void removeLabelFromState(std::string const& label, storm::storage::sparse::state_type state); /*! * Checks whether a given state is labeled with the given label. diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp index 058d92d99..8e278fecb 100644 --- a/src/storm/settings/SettingsManager.cpp +++ b/src/storm/settings/SettingsManager.cpp @@ -39,6 +39,7 @@ #include "storm/settings/modules/MultiObjectiveSettings.h" #include "storm/settings/modules/MultiplierSettings.h" #include "storm/settings/modules/TransformationSettings.h" +#include "storm/settings/modules/HintSettings.h" #include "storm/utility/macros.h" #include "storm/utility/file.h" #include "storm/utility/string.h" @@ -670,6 +671,7 @@ namespace storm { storm::settings::addModule(); storm::settings::addModule(); storm::settings::addModule(); + storm::settings::addModule(); } } diff --git a/src/storm/settings/modules/HintSettings.cpp b/src/storm/settings/modules/HintSettings.cpp new file mode 100644 index 000000000..4066c3fb1 --- /dev/null +++ b/src/storm/settings/modules/HintSettings.cpp @@ -0,0 +1,43 @@ +#include "storm/settings/modules/HintSettings.h" + +#include "storm/settings/Option.h" +#include "storm/settings/OptionBuilder.h" +#include "storm/settings/ArgumentBuilder.h" +#include "storm/exceptions/InvalidSettingsException.h" +#include "storm/exceptions/IllegalArgumentValueException.h" + +namespace storm { + namespace settings { + namespace modules { + + const std::string HintSettings::moduleName = "hints"; + + const std::string stateHintOption = "states"; + + + HintSettings::HintSettings() : ModuleSettings(moduleName) { + this->addOption(storm::settings::OptionBuilder(moduleName, stateHintOption, true, + "Estimate of the number of reachable states").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("number", "size.").build()).build()); + + } + + bool HintSettings::isNumberStatesSet() const { + return this->getOption(stateHintOption).getHasOptionBeenSet(); + } + + uint64_t HintSettings::getNumberStates() const { + return this->getOption(stateHintOption).getArgumentByName("number").getValueAsUnsignedInteger(); + } + + bool HintSettings::check() const { + return true; + } + + void HintSettings::finalize() { + //Intentionally left empty + } + + + } // namespace modules + } // namespace settings +} // namespace storm diff --git a/src/storm/settings/modules/HintSettings.h b/src/storm/settings/modules/HintSettings.h new file mode 100644 index 000000000..459c83443 --- /dev/null +++ b/src/storm/settings/modules/HintSettings.h @@ -0,0 +1,40 @@ +#pragma once + +#include "storm-config.h" +#include "storm/settings/modules/ModuleSettings.h" + +namespace storm { + namespace settings { + namespace modules { + + /*! + * This class represents the model transformer settings + */ + class HintSettings : public ModuleSettings { + public: + + /*! + * Creates a new set of transformer settings. + */ + HintSettings(); + + /*! + * Retrieves whether the option that estimates the number of states is set. + */ + bool isNumberStatesSet() const; + + uint64_t getNumberStates() const; + + bool check() const override; + + void finalize() override; + + // The name of the module. + static const std::string moduleName; + + }; + + } // namespace modules + } // namespace settings +} // namespace storm + diff --git a/src/storm/solver/stateelimination/NondeterministicModelStateEliminator.h b/src/storm/solver/stateelimination/NondeterministicModelStateEliminator.h index 1257d8df1..123d99a69 100644 --- a/src/storm/solver/stateelimination/NondeterministicModelStateEliminator.h +++ b/src/storm/solver/stateelimination/NondeterministicModelStateEliminator.h @@ -13,7 +13,7 @@ namespace storm { NondeterministicModelStateEliminator(storm::storage::FlexibleSparseMatrix& transitionMatrix, storm::storage::FlexibleSparseMatrix& backwardTransitions, std::vector& rowValues); - // Instantiaton of virtual methods. + // Instantiation of virtual methods. virtual void updateValue(storm::storage::sparse::state_type const& row, ValueType const& loopProbability) override; virtual void updatePredecessor(storm::storage::sparse::state_type const& predecessorRow, ValueType const& probability, storm::storage::sparse::state_type const& row) override; diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index 11abda87d..271568c7f 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -1,17 +1,14 @@ #include #include +#include #include "storm/storage/BitVector.h" -#include "storm/exceptions/InvalidArgumentException.h" -#include "storm/exceptions/OutOfRangeException.h" #include "storm/storage/BoostTypes.h" - #include "storm/utility/OsDetection.h" #include "storm/utility/Hash.h" #include "storm/utility/macros.h" -#include #ifdef STORM_DEV #define ASSERT_BITVECTOR diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index 2980c29cd..64b823652 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -10,7 +10,7 @@ namespace storm { namespace storage { - + /*! * A bit vector that is internally represented as a vector of 64-bit values. */ @@ -23,7 +23,7 @@ namespace storm { class const_iterator : public std::iterator { // Declare the BitVector class as a friend class to access its internal storage. friend class BitVector; - + public: /*! * Constructs an iterator over the indices of the set bits in the given bit vector, starting and @@ -36,21 +36,21 @@ namespace storm { * @param endIndex The index at which to abort the iteration process. */ const_iterator(uint64_t const* dataPtr, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit = true); - + /*! * Constructs an iterator by copying the given iterator. * * @param other The iterator to copy. */ const_iterator(const_iterator const& other); - + /*! * Assigns the contents of the given iterator to the current one via copying the former's contents. * * @param other The iterator from which to copy-assign. */ const_iterator& operator=(const_iterator const& other); - + /*! * Increases the position of the iterator to the position of the next bit that is set to true in the * underlying bit vector. @@ -64,14 +64,14 @@ namespace storm { * underlying bit vector. */ const_iterator& operator+=(size_t n); - + /*! * Returns the index of the current bit to which this iterator points. * * @return The index of the current bit to which this iterator points. */ uint_fast64_t operator*() const; - + /*! * Compares the iterator with another iterator for inequality. * @@ -79,7 +79,7 @@ namespace storm { * @return True if the two iterators are unequal. */ bool operator!=(const_iterator const& other) const; - + /*! * Compares the iterator with another iterator for equality. * @@ -87,28 +87,28 @@ namespace storm { * @return True if the two iterators are equal. */ bool operator==(const_iterator const& other) const; - + private: // The underlying bit vector of this iterator. uint64_t const* dataPtr; - + // The index of the bit this iterator currently points to. uint_fast64_t currentIndex; - + // The index of the bit that is past the end of the range of this iterator. uint_fast64_t endIndex; }; - - /* + + /*! * Constructs an empty bit vector of length 0. */ BitVector(); - - /* + + /*! * Deconstructs a bit vector by deleting the underlying storage. */ ~BitVector(); - + /*! * Constructs a bit vector which can hold the given number of bits and initializes all bits with the * provided truth value. @@ -117,7 +117,7 @@ namespace storm { * @param init The initial value of the first |length| bits. */ explicit BitVector(uint_fast64_t length, bool init = false); - + /*! * Creates a bit vector that has exactly the bits set that are given by the provided input iterator range * [first, last). @@ -128,26 +128,26 @@ namespace storm { */ template BitVector(uint_fast64_t length, InputIterator first, InputIterator last); - + /*! * Creates a bit vector that has exactly the bits set that are given by the vector */ BitVector(uint_fast64_t length, std::vector setEntries); - + /*! * Performs a deep copy of the given bit vector. * * @param other A reference to the bit vector to be copied. */ BitVector(BitVector const& other); - + /*! * Move constructs the bit vector from the given bit vector. * * @param other The bit vector from which to move-construct. */ BitVector(BitVector&& other); - + /*! * Compares the given bit vector with the current one. * @@ -155,7 +155,7 @@ namespace storm { * @return True iff the other bit vector is semantically the same as the current one. */ bool operator==(BitVector const& other) const; - + /*! * Compares the given bit vector with the current one. * @@ -163,7 +163,7 @@ namespace storm { * @return True iff the other bit vector is semantically not the same as the current one. */ bool operator!=(BitVector const& other) const; - + /*! * Assigns the contents of the given bit vector to the current bit vector via a deep copy. * @@ -172,7 +172,7 @@ namespace storm { * deep copy. */ BitVector& operator=(BitVector const& other); - + /*! * Move assigns the given bit vector to the current bit vector. * @@ -181,7 +181,7 @@ namespace storm { * into it. */ BitVector& operator=(BitVector&& other); - + /*! * Retrieves whether the current bit vector is (in some order) smaller than the given one. * @@ -189,15 +189,15 @@ namespace storm { * @return True iff the current bit vector is smaller than the given one. */ bool operator<(BitVector const& other) const; - + /*! * Sets the given truth value at the given index. * * @param index The index where to set the truth value. * @param value The truth value to set. */ - void set(const uint_fast64_t index, bool value = true); - + void set(uint_fast64_t index, bool value = true); + /*! * Sets all bits in the given iterator range [first, last). * @@ -206,7 +206,7 @@ namespace storm { */ template void set(InputIterator first, InputIterator last, bool value = true); - + /*! * Retrieves the truth value of the bit at the given index. Note: this does not check whether the given * index is within bounds. @@ -215,7 +215,7 @@ namespace storm { * @return True iff the bit at the given index is set. */ bool operator[](uint_fast64_t index) const; - + /*! * Retrieves the truth value of the bit at the given index and performs a bound check. If the access is * out-of-bounds an OutOfBoundsException is thrown. @@ -223,8 +223,8 @@ namespace storm { * @param index The index of the bit to access. * @return True iff the bit at the given index is set. */ - bool get(const uint_fast64_t index) const; - + bool get(uint_fast64_t index) const; + /*! * Resizes the bit vector to hold the given new number of bits. If the bit vector becomes smaller this way, * the bits are truncated. Otherwise, the new bits are initialized to the given value. @@ -246,7 +246,7 @@ namespace storm { * Expands the size to a multiple of 64. */ void expandSize(bool init = false); - + /*! * Enlarges the bit vector such that it holds at least the given number of bits (but possibly more). * This can be used to diminish reallocations when the final size of the bit vector is not known yet. @@ -257,7 +257,7 @@ namespace storm { * @param init The truth value to which to initialize newly created bits. */ void grow(uint_fast64_t minimumLength, bool init = false); - + /*! * Performs a logical "and" with the given bit vector. In case the sizes of the bit vectors do not match, * only the matching portion is considered and the overlapping bits are set to 0. @@ -266,7 +266,7 @@ namespace storm { * @return A bit vector corresponding to the logical "and" of the two bit vectors. */ BitVector operator&(BitVector const& other) const; - + /*! * Performs a logical "and" with the given bit vector and assigns the result to the current bit vector. * In case the sizes of the bit vectors do not match, only the matching portion is considered and the @@ -277,7 +277,7 @@ namespace storm { * of the two bit vectors. */ BitVector& operator&=(BitVector const& other); - + /*! * Performs a logical "or" with the given bit vector. In case the sizes of the bit vectors do not match, * only the matching portion is considered and the overlapping bits are set to 0. @@ -286,7 +286,7 @@ namespace storm { * @return A bit vector corresponding to the logical "or" of the two bit vectors. */ BitVector operator|(BitVector const& other) const; - + /*! * Performs a logical "or" with the given bit vector and assigns the result to the current bit vector. * In case the sizes of the bit vectors do not match, only the matching portion is considered and the @@ -297,7 +297,7 @@ namespace storm { * of the two bit vectors. */ BitVector& operator|=(BitVector const& other); - + /*! * Performs a logical "xor" with the given bit vector. In case the sizes of the bit vectors do not match, * only the matching portion is considered and the overlapping bits are set to 0. @@ -306,36 +306,39 @@ namespace storm { * @return A bit vector corresponding to the logical "xor" of the two bit vectors. */ BitVector operator^(BitVector const& other) const; - + /*! - * Computes a bit vector that is as long as the number of set bits in the given filter that has bit i is set - * iff the i-th set bit of the current bit vector is set in the filter. + * Computes a bit vector that contains only the values of the bits given by the filter. + * The returned bit vector is as long as the number of set bits in the given filter. + * Bit i is set in the returned bit vector iff the i-th set bit of the current bit vector is set in the filter. + * + * For example: 00100110 % 10101010 returns 0101 * - * @param filter A reference the bit vector to use as the filter. - * @return A bit vector that is as long as the number of set bits in the given filter that has bit i is set - * iff the i-th set bit of the current bit vector is set in the filter. + * @param filter A reference bit vector to use as the filter. + * @return A bit vector that is as long as the number of set bits in the given filter and + * contains only the values of the bits set in the filter. */ BitVector operator%(BitVector const& filter) const; - + /*! * Performs a logical "not" on the bit vector. * * @return A bit vector corresponding to the logical "not" of the bit vector. */ BitVector operator~() const; - + /*! * Negates all bits in the bit vector. */ void complement(); - + /*! * Increments the (unsigned) number represented by this BitVector by one. * @note Index 0 is assumed to be the least significant bit. * @note Wraps around, i.e., incrementing 11..1 yields 00..0. */ void increment(); - + /*! * Performs a logical "implies" with the given bit vector. In case the sizes of the bit vectors do not * match, only the matching portion is considered and the overlapping bits are set to 0. @@ -344,7 +347,7 @@ namespace storm { * @return A bit vector corresponding to the logical "implies" of the two bit vectors. */ BitVector implies(BitVector const& other) const; - + /*! * Checks whether all bits that are set in the current bit vector are also set in the given bit vector. * @@ -354,7 +357,7 @@ namespace storm { * vector. */ bool isSubsetOf(BitVector const& other) const; - + /*! * Checks whether none of the bits that are set in the current bit vector are also set in the given bit * vector. @@ -365,7 +368,7 @@ namespace storm { * given bit vector. */ bool isDisjointFrom(BitVector const& other) const; - + /*! * Checks whether the given bit vector matches the bits starting from the given index in the current bit * vector. Note: the given bit vector must be shorter than the current one minus the given index. @@ -375,7 +378,7 @@ namespace storm { * @return bool True iff the bits match exactly. */ bool matches(uint_fast64_t bitIndex, BitVector const& other) const; - + /*! * Sets the exact bit pattern of the given bit vector starting at the given bit index. Note: the given bit * vector must be shorter than the current one minus the given index. @@ -393,7 +396,7 @@ namespace storm { * TODO this operation is slow. */ BitVector permute(std::vector const& inversePermutation) const; - + /*! * Retrieves the content of the current bit vector at the given index for the given number of bits as a new * bit vector. @@ -403,7 +406,7 @@ namespace storm { * @return A new bit vector holding the selected bits. */ storm::storage::BitVector get(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const; - + /*! * Retrieves the content of the current bit vector at the given index for the given number of bits as an * unsigned integer value. @@ -412,14 +415,14 @@ namespace storm { * @param numberOfBits The number of bits to get. This value must be less or equal than 64. */ uint_fast64_t getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const; - + /*! * * @param bitIndex The index of the first of the two bits to get * @return A value between 0 and 3, encoded as a byte. */ uint_fast64_t getTwoBitsAligned(uint_fast64_t bitIndex) const; - + /*! * Sets the selected number of lowermost bits of the provided value at the given bit index. * @@ -428,14 +431,14 @@ namespace storm { * @param value The integer whose lowermost bits to set. */ void setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value); - + /*! * Retrieves whether no bits are set to true in this bit vector. * * @return False iff there is at least one bit set in this vector. */ bool empty() const; - + /*! * Retrieves whether all bits are set in this bit vector. * If the bit vector has size 0, this method always returns true. @@ -443,24 +446,24 @@ namespace storm { * @return True iff all bits in the bit vector are set. */ bool full() const; - + /*! * Removes all set bits from the bit vector. Calling empty() after this operation will yield true. */ void clear(); - + /*! * Sets all bits from the bit vector. Calling full() after this operation will yield true. */ void fill(); - + /*! * Returns the number of bits that are set to true in this bit vector. * * @return The number of bits that are set to true in this bit vector. */ uint_fast64_t getNumberOfSetBits() const; - + /*! * Retrieves the number of bits set in this bit vector with an index strictly smaller than the given one. * @@ -468,39 +471,39 @@ namespace storm { * @return The number of bits set in this bit vector with an index strictly smaller than the given one. */ uint_fast64_t getNumberOfSetBitsBeforeIndex(uint_fast64_t index) const; - + /*! * Retrieves a vector that holds at position i the number of bits set before index i. * * @return The resulting vector of 'offsets'. */ std::vector getNumberOfSetBitsBeforeIndices() const; - + /*! * Retrieves the number of bits this bit vector can store. * * @return The number of bits this bit vector can hold. */ size_t size() const; - + /*! * Returns (an approximation of) the size of the bit vector measured in bytes. * * @return The size of the bit vector measured in bytes. */ std::size_t getSizeInBytes() const; - + /*! * Returns an iterator to the indices of the set bits in the bit vector. */ const_iterator begin() const; - + /*! * Returns an iterator pointing at the element past the bit vector. */ const_iterator end() const; - - /* + + /*! * Retrieves the index of the bit that is the next bit set to true in the bit vector. If there is none, * this function returns the number of bits this vector holds in total. Put differently, if the return * value is equal to a call to size(), then there is no bit set after the specified position. @@ -510,8 +513,8 @@ namespace storm { * @return The index of the next bit that is set after the given index. */ uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const; - - /* + + /*! * Retrieves the index of the bit that is the next bit set to false in the bit vector. If there is none, * this function returns the number of bits this vector holds in total. Put differently, if the return * value is equal to a call to size(), then there is no unset bit after the specified position. @@ -521,8 +524,8 @@ namespace storm { * @return The index of the next bit that is set after the given index. */ uint_fast64_t getNextUnsetIndex(uint_fast64_t startingIndex) const; - - /* + + /*! * Compare two intervals [start1, start1+length] and [start2, start2+length] and swap them if the second * one is larger than the first one. After the method the intervals are sorted in decreasing order. * @@ -532,14 +535,15 @@ namespace storm { * @return True, if the intervals were swapped, false if nothing changed. */ bool compareAndSwap(uint_fast64_t start1, uint_fast64_t start2, uint_fast64_t length); - + friend std::ostream& operator<<(std::ostream& out, BitVector const& bitVector); + friend struct std::hash; friend struct FNV1aBitVectorHash; - + template friend struct Murmur3BitVectorHash; - + private: /*! * Creates an empty bit vector with the given number of buckets. @@ -548,7 +552,7 @@ namespace storm { * @param bitCount This must be the number of buckets times 64. */ BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount); - + /*! * Retrieves the index of the next bit that is set to the given value after (and including) the given starting index. * @@ -560,12 +564,12 @@ namespace storm { * in the given bit vector or endIndex in case the end index was reached. */ static uint_fast64_t getNextIndexWithValue(bool value, uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex); - + /*! * Truncate the last bucket so that no bits are set starting from bitCount. */ void truncateLastBucket(); - + /*! Retrieves the content of the current bit vector at the given index for the given number of bits as a new * bit vector. * @@ -574,7 +578,7 @@ namespace storm { * @return A new bit vector holding the selected bits. */ BitVector getAsBitVector(uint_fast64_t start, uint_fast64_t length) const; - + /*! * Sets the exact bit pattern of the given bit vector starting at the given bit index. Note: the given bit * vector must be shorter than the current one minus the given index. @@ -583,31 +587,31 @@ namespace storm { * @param other The bit vector whose pattern to set. */ void setFromBitVector(uint_fast64_t start, BitVector const& other); - + /*! * Print bit vector and display all bits. * * @param out Stream to print to. */ void printBits(std::ostream& out) const; - + /*! * Retrieves the number of buckets of the underlying storage. * * @return The number of buckets of the underlying storage. */ size_t bucketCount() const; - + // The number of bits that this bit vector can hold. uint_fast64_t bitCount; - + // The underlying storage of 64-bit buckets for all bits of this bit vector. uint64_t* buckets; - + // A bit mask that can be used to reduce a modulo 64 operation to a logical "and". static const uint_fast64_t mod64mask = (1 << 6) - 1; }; - + struct FNV1aBitVectorHash { std::size_t operator()(storm::storage::BitVector const& bv) const; }; @@ -621,7 +625,7 @@ namespace storm { } // namespace storm namespace std { - template <> + template<> struct hash { std::size_t operator()(storm::storage::BitVector const& bv) const; }; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index c05417ae2..224857989 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -676,6 +676,14 @@ namespace storm { return res; } + std::size_t Model::getTotalNumberOfNonTransientVariables() const { + std::size_t res = globalVariables.getNumberOfNontransientVariables(); + for (auto const& aut : getAutomata()) { + res += aut.getVariables().getNumberOfNontransientVariables(); + } + return res; + } + Variable const& Model::addVariable(Variable const& variable) { if (variable.isBooleanVariable()) { return addVariable(variable.asBooleanVariable()); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 3adbdd51c..41e205274 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -384,7 +384,13 @@ namespace storm { * Retrieves the total number of edges in this model. */ std::size_t getNumberOfEdges() const; - + + /*! + * Number of global and local variables. + */ + std::size_t getTotalNumberOfNonTransientVariables() const; + + /*! * Sets the system composition expression of the JANI model. */ @@ -547,7 +553,7 @@ namespace storm { * Determines whether this model is a discrete-time model. */ bool isDiscreteTimeModel() const; - + /*! * Retrieves a list of expressions that characterize the legal values of the variables in this model. * diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp index c3ba52a5a..10cdd7fba 100644 --- a/src/storm/storage/jani/VariableSet.cpp +++ b/src/storm/storage/jani/VariableSet.cpp @@ -76,7 +76,8 @@ namespace storm { } STORM_LOG_THROW(false, storm::exceptions::InvalidTypeException, "Cannot add variable of unknown type."); } - + + BooleanVariable const& VariableSet::addVariable(BooleanVariable const& variable) { STORM_LOG_THROW(!this->hasVariable(variable.getName()), storm::exceptions::WrongFormatException, "Cannot add variable with name '" << variable.getName() << "', because a variable with that name already exists."); std::shared_ptr newVariable = std::make_shared(variable); @@ -321,7 +322,16 @@ namespace storm { bool VariableSet::empty() const { return !(containsBooleanVariable() || containsBoundedIntegerVariable() || containsUnboundedIntegerVariables() || containsRealVariables() || containsArrayVariables() || containsClockVariables()); } - + + uint64_t VariableSet::getNumberOfVariables() const { + return variables.size(); + } + + + uint64_t VariableSet::getNumberOfNontransientVariables() const { + return getNumberOfVariables() - getNumberOfTransientVariables(); + } + uint_fast64_t VariableSet::getNumberOfTransientVariables() const { uint_fast64_t result = 0; for (auto const& variable : variables) { diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h index 612d2e992..53f45a359 100644 --- a/src/storm/storage/jani/VariableSet.h +++ b/src/storm/storage/jani/VariableSet.h @@ -228,26 +228,36 @@ namespace storm { * Retrieves whether this variable set is empty. */ bool empty() const; - + + /*! + * Total number of variables, including transient variables. + */ + uint64_t getNumberOfVariables() const; + + /* + * Total number of nontransient variables + */ + uint64_t getNumberOfNontransientVariables() const; + /*! * Retrieves the number of transient variables in this variable set. */ - uint_fast64_t getNumberOfTransientVariables() const; + uint64_t getNumberOfTransientVariables() const; /*! * Retrieves the number of real transient variables in this variable set. */ - uint_fast64_t getNumberOfRealTransientVariables() const; + uint64_t getNumberOfRealTransientVariables() const; /*! * Retrieves the number of unbounded integer transient variables in this variable set. */ - uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const; + uint64_t getNumberOfUnboundedIntegerTransientVariables() const; /*! * Retrieves the number of numerical (i.e. real, or integer) transient variables in this variable set. */ - uint_fast64_t getNumberOfNumericalTransientVariables() const; + uint64_t getNumberOfNumericalTransientVariables() const; /*! * Retrieves the transient variables in this variable set. diff --git a/src/storm/storage/jani/traverser/InformationCollector.cpp b/src/storm/storage/jani/traverser/InformationCollector.cpp new file mode 100644 index 000000000..6a7a42ebb --- /dev/null +++ b/src/storm/storage/jani/traverser/InformationCollector.cpp @@ -0,0 +1,20 @@ +#include "storm/storage/jani/traverser/InformationCollector.h" +#include "storm/storage/jani/traverser/JaniTraverser.h" +#include "storm/storage/jani/Model.h" + +namespace storm { + namespace jani { + namespace detail { + + } + + InformationObject collect(Model const& model) { + InformationObject result; + result.modelType = model.getModelType(); + result.nrAutomata = model.getNumberOfAutomata(); + result.nrEdges = model.getNumberOfEdges(); + result.nrVariables = model.getTotalNumberOfNonTransientVariables(); + return result; + } + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/traverser/InformationCollector.h b/src/storm/storage/jani/traverser/InformationCollector.h new file mode 100644 index 000000000..2c094d124 --- /dev/null +++ b/src/storm/storage/jani/traverser/InformationCollector.h @@ -0,0 +1,20 @@ +#pragma once +#include "storm/storage/jani/ModelType.h" + +namespace storm { + namespace jani { + + class Model; + + struct InformationObject { + storm::jani::ModelType modelType; + uint64_t nrVariables; + uint64_t nrAutomata; + uint64_t nrEdges; + uint64_t nrLocations; + }; + + InformationObject collect(Model const& model); + } +} + diff --git a/src/storm/transformer/NonMarkovianChainTransformer.cpp b/src/storm/transformer/NonMarkovianChainTransformer.cpp index 7f5bd61c4..b51bcc7a0 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.cpp +++ b/src/storm/transformer/NonMarkovianChainTransformer.cpp @@ -1,40 +1,35 @@ -#include - #include "NonMarkovianChainTransformer.h" -#include "storm/logic/Formulas.h" -#include "storm/logic/FragmentSpecification.h" +#include -#include "storm/storage/sparse/ModelComponents.h" #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/InvalidModelException.h" +#include "storm/logic/Formulas.h" +#include "storm/logic/FragmentSpecification.h" +#include "storm/models/sparse/Ctmc.h" #include "storm/models/sparse/StandardRewardModel.h" +#include +#include "storm/storage/FlexibleSparseMatrix.h" +#include "storm/storage/sparse/ModelComponents.h" #include "storm/utility/constants.h" -#include "storm/utility/ConstantsComparator.h" #include "storm/utility/vector.h" #include "storm/utility/macros.h" #include "storm/utility/graph.h" + namespace storm { namespace transformer { template std::shared_ptr> - NonMarkovianChainTransformer::eliminateNonmarkovianStates( - std::shared_ptr> ma, - EliminationLabelBehavior labelBehavior) { - // TODO reward models - + NonMarkovianChainTransformer::eliminateNonmarkovianStates(std::shared_ptr> ma, + EliminationLabelBehavior labelBehavior) { STORM_LOG_WARN_COND(labelBehavior == EliminationLabelBehavior::KeepLabels, "Labels are not preserved! Results may be incorrect. Continue at your own caution."); - if (labelBehavior == EliminationLabelBehavior::DeleteLabels) { - STORM_PRINT("Use Label Deletion" << std::endl) - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - STORM_PRINT("Use Label Merging" << std::endl) - } - STORM_LOG_WARN("Reward Models and Choice Labelings are ignored!"); - if (ma->isClosed() && ma->getMarkovianStates().full()) { - storm::storage::sparse::ModelComponents components( - ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); + STORM_LOG_THROW(ma->isClosed(), storm::exceptions::InvalidModelException, "MA should be closed first."); + + if (ma->getMarkovianStates().full()) { + // Is already a CTMC + storm::storage::sparse::ModelComponents components(ma->getTransitionMatrix(), ma->getStateLabeling(), ma->getRewardModels(), false); components.exitRates = ma->getExitRates(); if (ma->hasChoiceLabeling()) { components.choiceLabeling = ma->getChoiceLabeling(); @@ -45,243 +40,98 @@ namespace storm { if (ma->hasChoiceOrigins()) { components.choiceOrigins = ma->getChoiceOrigins(); } - return std::make_shared>( - std::move(components)); + return std::make_shared>(std::move(components)); } - std::map eliminationMapping; - std::set statesToKeep; - std::queue changedStates; - std::queue queue; - - storm::storage::SparseMatrix backwards = ma->getBackwardTransitions(); + // Initialize + storm::storage::FlexibleSparseMatrix flexibleMatrix(ma->getTransitionMatrix()); + storm::storage::FlexibleSparseMatrix flexibleBackwardTransitions(ma->getTransitionMatrix().transpose(), true); + storm::models::sparse::StateLabeling stateLabeling = ma->getStateLabeling(); + // TODO: update reward models and choice labels according to kept states + STORM_LOG_WARN_COND(ma->getRewardModels().empty(), "Reward models are not preserved in chain elimination."); + std::unordered_map rewardModels; + STORM_LOG_WARN_COND(!ma->hasChoiceLabeling(), "Choice labels are not preserved in chain elimination."); + STORM_LOG_WARN_COND(!ma->hasStateValuations(), "State valuations are not preserved in chain elimination."); + STORM_LOG_WARN_COND(!ma->hasChoiceOrigins(), "Choice origins are not preserved in chain elimination."); + + // Eliminate all probabilistic states by state elimination + auto actionRewards = std::vector(ma->getTransitionMatrix().getRowCount(), storm::utility::zero()); + storm::solver::stateelimination::NondeterministicModelStateEliminator stateEliminator(flexibleMatrix, flexibleBackwardTransitions, actionRewards); + storm::storage::BitVector keepStates(ma->getNumberOfStates(), true); - // Determine the state remapping - for (uint_fast64_t base_state = 0; base_state < ma->getNumberOfStates(); ++base_state) { - STORM_LOG_ASSERT(!ma->isHybridState(base_state), "Base state is hybrid."); - if (ma->isMarkovianState(base_state)) { - queue.push(base_state); - - while (!queue.empty()) { - auto currState = queue.front(); - queue.pop(); - - auto currLabels = ma->getLabelsOfState(currState); - - // Get predecessors from matrix - typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow(currState); - for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { - uint_fast64_t predecessor = entryIt->getColumn(); - if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { - if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels || - currLabels == ma->getLabelsOfState(predecessor)) { - // If labels are not to be preserved or states are labeled the same - if (!eliminationMapping.count(predecessor)) { - eliminationMapping[predecessor] = base_state; - queue.push(predecessor); - } else if (eliminationMapping[predecessor] != base_state) { - eliminationMapping.erase(predecessor); - statesToKeep.insert(predecessor); - changedStates.push(predecessor); - } - } else { - // Labels are to be preserved and states have different labels - if (eliminationMapping.count(predecessor)) { - eliminationMapping.erase(predecessor); - } - statesToKeep.insert(predecessor); - changedStates.push(predecessor); + for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { + STORM_LOG_ASSERT(!ma->isHybridState(state), "State is hybrid."); + if (ma->isProbabilisticState(state)) { + // Only eliminate immediate states (and no Markovian states) + if (ma->getNumberOfChoices(state) <= 1) { + // Eliminate only if no non-determinism occurs + STORM_LOG_ASSERT(ma->getNumberOfChoices(state) == 1, "State " << state << " has no choices."); + STORM_LOG_ASSERT(flexibleMatrix.getRowGroupSize(state) == 1, "State " << state << " has too many rows."); + + if (labelBehavior == EliminationLabelBehavior::KeepLabels) { + // Only eliminate if eliminated state and all its successors have the same labels + bool sameLabels = true; + auto currLabels = stateLabeling.getLabelsOfState(state); + typename storm::storage::FlexibleSparseMatrix::row_type entriesInRow = flexibleMatrix.getRow(state, 0); // Row group + for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { + if (currLabels != stateLabeling.getLabelsOfState(entryIt->getColumn())) { + STORM_LOG_TRACE("Do not eliminate state " << state << " because labels of state " << entryIt->getColumn() << " are different."); + sameLabels = false; + break; } } - } - } - } - } - - // Correct the mapping with the states which have to be kept - while (!changedStates.empty()) { - uint_fast64_t base_state = changedStates.front(); - queue.push(base_state); - - while (!queue.empty()) { - auto currState = queue.front(); - queue.pop(); - - auto currLabels = ma->getLabelsOfState(currState); + if (!sameLabels) { + continue; + } + } else { + // As helper for the labeling we create a bitvector representing all successor states + storm::storage::BitVector successors(stateLabeling.getNumberOfItems()); + typename storm::storage::FlexibleSparseMatrix::row_type entriesInRow = flexibleMatrix.getRow(state, 0); // Row group + for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { + successors.set(entryIt->getColumn()); + } - // Get predecessors from matrix - typename storm::storage::SparseMatrix::rows entriesInRow = backwards.getRow(currState); - for (auto entryIt = entriesInRow.begin(); entryIt != entriesInRow.end(); ++entryIt) { - uint_fast64_t predecessor = entryIt->getColumn(); - if (!ma->isMarkovianState(predecessor) && !statesToKeep.count(predecessor)) { - if (labelBehavior == EliminationLabelBehavior::DeleteLabels || labelBehavior == EliminationLabelBehavior::MergeLabels || - currLabels == ma->getLabelsOfState(predecessor)) { - // If labels are not to be preserved or states are labeled the same - if (!eliminationMapping.count(predecessor)) { - eliminationMapping[predecessor] = base_state; - queue.push(predecessor); - } else if (eliminationMapping[predecessor] != base_state) { - eliminationMapping.erase(predecessor); - statesToKeep.insert(predecessor); - changedStates.push(predecessor); + if (labelBehavior == EliminationLabelBehavior::MergeLabels) { + // Add labels from eliminated state to successors + for (std::string const& label : stateLabeling.getLabelsOfState(state)) { + storm::storage::BitVector states = stateLabeling.getStates(label); + // Add successor states for this label as well + stateLabeling.setStates(label, states | successors); } } else { - // Labels are to be preserved and states have different labels - if (eliminationMapping.count(predecessor)) { - eliminationMapping.erase(predecessor); + STORM_LOG_ASSERT(labelBehavior == EliminationLabelBehavior::DeleteLabels, "Unknown label behavior."); + if (stateLabeling.getStateHasLabel("init", state)) { + // Add "init" label of eliminated state to successor states + storm::storage::BitVector states = stateLabeling.getStates("init"); + // Add successor states for this label as well + stateLabeling.setStates("init", states | successors); } - statesToKeep.insert(predecessor); - changedStates.push(predecessor); } } - } - } - - changedStates.pop(); - } - - // At this point, we hopefully have a valid mapping which eliminates a lot of states - - STORM_LOG_TRACE("Elimination Mapping:"); - for (auto entry : eliminationMapping) { - STORM_LOG_TRACE(std::to_string(entry.first) << " -> " << std::to_string(entry.second)); - } - STORM_LOG_INFO("Eliminating " << eliminationMapping.size() << " states" << std::endl); - - // TODO explore if one can construct elimination mapping and state remapping in one step - uint64_t newStateCount = ma->getNumberOfStates() - eliminationMapping.size(); - - std::vector> labelMap(newStateCount, std::set()); - - // Construct a mapping of old state space to new one - std::vector stateRemapping(ma->getNumberOfStates(), -1); - uint_fast64_t currentNewState = 0; - for (uint_fast64_t state = 0; state < ma->getNumberOfStates(); ++state) { - if (eliminationMapping.count(state) > 0) { - if (stateRemapping[eliminationMapping[state]] == uint_fast64_t(-1)) { - stateRemapping[eliminationMapping[state]] = currentNewState; - stateRemapping[state] = currentNewState; - ++currentNewState; - queue.push(eliminationMapping[state]); - } else { - stateRemapping[state] = stateRemapping[eliminationMapping[state]]; - } - if (labelBehavior == EliminationLabelBehavior::DeleteLabels && ma->getInitialStates().get(state)) { - // Keep initial label for 'delete' behavior - labelMap[stateRemapping[eliminationMapping[state]]].insert("init"); - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - //add all labels to the label set for the representative - for (auto const &label : ma->getLabelsOfState(state)) { - labelMap[stateRemapping[eliminationMapping[state]]].insert(label); - } - } - } else { - if (stateRemapping[state] == uint_fast64_t(-1)) { - stateRemapping[state] = currentNewState; - queue.push(state); - ++currentNewState; - } - if (labelBehavior == EliminationLabelBehavior::DeleteLabels && ma->getInitialStates().get(state)) { - // Keep initial label for 'delete' behavior - labelMap[stateRemapping[state]].insert("init"); - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - for (auto const &label : ma->getLabelsOfState(state)) { - labelMap[stateRemapping[state]].insert(label); - } + // Eliminate this probabilistic state + stateEliminator.eliminateState(state, true); + keepStates.set(state, false); } } } - // Build the new MA - storm::storage::SparseMatrix newTransitionMatrix; - storm::models::sparse::StateLabeling newStateLabeling(newStateCount); - storm::storage::BitVector newMarkovianStates(ma->getNumberOfStates() - eliminationMapping.size(),false); - std::vector newExitRates; - //TODO choice labeling - boost::optional newChoiceLabeling; + // Create the new matrix + auto keptRows = ma->getTransitionMatrix().getRowFilter(keepStates); + storm::storage::SparseMatrix matrix = flexibleMatrix.createSparseMatrix(keptRows, keepStates); - // Initialize the matrix builder and helper variables - storm::storage::SparseMatrixBuilder matrixBuilder = storm::storage::SparseMatrixBuilder( - 0, 0, 0, false, true, 0); + // TODO: obtain the reward model for the resulting system - for (auto const &label : ma->getStateLabeling().getLabels()) { - if (!newStateLabeling.containsLabel(label)) { - newStateLabeling.addLabel(label); - } - } - uint_fast64_t currentRow = 0; - uint_fast64_t state = 0; - while (!queue.empty()) { - state = queue.front(); - queue.pop(); + // Prepare model components + storm::storage::BitVector markovianStates = ma->getMarkovianStates() % keepStates; + storm::models::sparse::StateLabeling labeling = stateLabeling.getSubLabeling(keepStates); + storm::storage::sparse::ModelComponents components(matrix, labeling, ma->getRewardModels(), false, markovianStates); + std::vector exitRates(markovianStates.size()); + storm::utility::vector::selectVectorValues(exitRates, keepStates, ma->getExitRates()); + components.exitRates = exitRates; - std::set labelSet = ma->getLabelsOfState(state); - if (labelBehavior == EliminationLabelBehavior::DeleteLabels) { - labelSet.insert(labelMap[stateRemapping[state]].begin(), labelMap[stateRemapping[state]].end()); - } - if (labelBehavior == EliminationLabelBehavior::MergeLabels) { - labelSet = labelMap[stateRemapping[state]]; - } - - for (auto const &label : labelSet) { - if (!newStateLabeling.containsLabel(label)) { - newStateLabeling.addLabel(label); - } - - newStateLabeling.addLabelToState(label, stateRemapping[state]); - } - - // Use a set to not include redundant rows - std::set> rowSet; - for (uint_fast64_t row = 0; row < ma->getTransitionMatrix().getRowGroupSize(state); ++row) { - std::map transitions; - for (typename storm::storage::SparseMatrix::const_iterator itEntry = ma->getTransitionMatrix().getRow( - state, row).begin(); - itEntry != ma->getTransitionMatrix().getRow(state, row).end(); ++itEntry) { - uint_fast64_t newId = stateRemapping[itEntry->getColumn()]; - if (transitions.count(newId) == 0) { - transitions[newId] = itEntry->getValue(); - } else { - transitions[newId] += itEntry->getValue(); - } - } - rowSet.insert(transitions); - } - - // correctly set rates - auto rate = storm::utility::zero(); - - if (ma->isMarkovianState(state)) { - newMarkovianStates.set(stateRemapping[state], true); - rate = ma->getExitRates().at(state); - } - - newExitRates.push_back(rate); - // Build matrix - matrixBuilder.newRowGroup(currentRow); - for (auto const &row : rowSet) { - for (auto const &transition : row) { - matrixBuilder.addNextValue(currentRow, transition.first, transition.second); - STORM_LOG_TRACE(stateRemapping[state] << "->" << transition.first << " : " << transition.second - << std::endl); - } - ++currentRow; - } - } - // explicitly force dimensions of the matrix in case a column is missing - newTransitionMatrix = matrixBuilder.build(newStateCount, newStateCount, newStateCount); - - storm::storage::sparse::ModelComponents newComponents = storm::storage::sparse::ModelComponents( - std::move(newTransitionMatrix), std::move(newStateLabeling)); - - newComponents.rateTransitions = false; - newComponents.markovianStates = std::move(newMarkovianStates); - newComponents.exitRates = std::move(newExitRates); - auto model = std::make_shared>( - std::move(newComponents)); + // Build transformed model + auto model = std::make_shared>(std::move(components)); if (model->isConvertibleToCtmc()) { return model->convertToCtmc(); } else { @@ -290,50 +140,49 @@ namespace storm { } template - bool NonMarkovianChainTransformer::preservesFormula( - storm::logic::Formula const &formula) { + bool NonMarkovianChainTransformer::preservesFormula(storm::logic::Formula const& formula) { storm::logic::FragmentSpecification fragment = storm::logic::propositional(); fragment.setProbabilityOperatorsAllowed(true); fragment.setGloballyFormulasAllowed(true); fragment.setReachabilityProbabilityFormulasAllowed(true); fragment.setUntilFormulasAllowed(true); + fragment.setBoundedUntilFormulasAllowed(true); fragment.setTimeBoundedUntilFormulasAllowed(true); + fragment.setNextFormulasAllowed(false); + fragment.setStepBoundedUntilFormulasAllowed(false); + return formula.isInFragment(fragment); } template std::vector> - NonMarkovianChainTransformer::checkAndTransformFormulas( - std::vector> const &formulas) { + NonMarkovianChainTransformer::checkAndTransformFormulas(std::vector> const& formulas) { std::vector> result; - for (auto const &f : formulas) { + for (auto const& f : formulas) { if (preservesFormula(*f)) { result.push_back(f); } else { - STORM_LOG_INFO("Non-Markovian chain elimination does not preserve formula " << *f); + STORM_LOG_WARN("Non-Markovian chain elimination does not preserve formula " << *f); } } return result; } - template - class NonMarkovianChainTransformer; + template class NonMarkovianChainTransformer; - template - class NonMarkovianChainTransformer>; -#ifdef STORM_HAVE_CARL + template class NonMarkovianChainTransformer>; - template - class NonMarkovianChainTransformer; +#ifdef STORM_HAVE_CARL + template class NonMarkovianChainTransformer; - template - class NonMarkovianChainTransformer; + template class NonMarkovianChainTransformer; #endif + } } diff --git a/src/storm/transformer/NonMarkovianChainTransformer.h b/src/storm/transformer/NonMarkovianChainTransformer.h index 691fcc9ee..64831ca70 100644 --- a/src/storm/transformer/NonMarkovianChainTransformer.h +++ b/src/storm/transformer/NonMarkovianChainTransformer.h @@ -21,13 +21,10 @@ namespace storm { * If no non-determinism occurs, a CTMC is generated. * * @param ma The input Markov Automaton. - * @param preserveLabels If set, the procedure considers the labels of non-Markovian states when eliminating states. + * @param labelBehavior How the labels of non-Markovian states should be treated when eliminating states. * @return A reference to the new model after eliminating non-Markovian states. */ - static std::shared_ptr> eliminateNonmarkovianStates( - std::shared_ptr> ma, - EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels - ); + static std::shared_ptr> eliminateNonmarkovianStates(std::shared_ptr> ma, EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels); /** * Check if the property specified by the given formula is preserved by the transformation. diff --git a/src/storm/utility/DirectEncodingExporter.cpp b/src/storm/utility/DirectEncodingExporter.cpp index b21b68a91..5e1ce3231 100644 --- a/src/storm/utility/DirectEncodingExporter.cpp +++ b/src/storm/utility/DirectEncodingExporter.cpp @@ -63,6 +63,7 @@ namespace storm { } os << std::endl; os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; + os << "@nr_choices" << std::endl << sparseModel->getNumberOfChoices() << std::endl; os << "@model" << std::endl; storm::storage::SparseMatrix const& matrix = sparseModel->getTransitionMatrix(); @@ -125,6 +126,9 @@ namespace storm { if (sparseModel->hasChoiceLabeling()) { os << "\taction "; bool lfirst = true; + if (sparseModel->getChoiceLabeling().getLabelsOfChoice(row).empty()) { + os << "__NOLABEL__"; + } for (auto const& label : sparseModel->getChoiceLabeling().getLabelsOfChoice(row)) { if (!lfirst) { os << "_"; diff --git a/src/test/storm/model/StateLabelingTest.cpp b/src/test/storm/model/StateLabelingTest.cpp new file mode 100644 index 000000000..f968480f8 --- /dev/null +++ b/src/test/storm/model/StateLabelingTest.cpp @@ -0,0 +1,37 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" + + +#include "storm/models/sparse/StateLabeling.h" + + + +TEST(StateLabelingTest, RemoveLabel) { + + storm::models::sparse::StateLabeling labeling(10); + EXPECT_EQ(10ul, labeling.getNumberOfItems()); + EXPECT_EQ(0ul, labeling.getNumberOfLabels()); + + storm::storage::BitVector statesTest1 = storm::storage::BitVector(10, {1, 4, 6, 7}); + labeling.addLabel("test1", statesTest1); + EXPECT_TRUE(labeling.containsLabel("test1")); + EXPECT_FALSE(labeling.containsLabel("abc")); + + storm::storage::BitVector statesTest2 = storm::storage::BitVector(10, {2, 6, 7, 8, 9}); + labeling.addLabel("test2", statesTest2); + + EXPECT_FALSE(labeling.getStateHasLabel("test2", 5)); + labeling.addLabelToState("test2", 5); + EXPECT_TRUE(labeling.getStateHasLabel("test2", 5)); + + EXPECT_TRUE(labeling.getStateHasLabel("test1", 4)); + labeling.removeLabelFromState("test1", 4); + EXPECT_FALSE(labeling.getStateHasLabel("test1", 4)); + + EXPECT_EQ(2ul, labeling.getNumberOfLabels()); + EXPECT_TRUE(labeling.getStateHasLabel("test1", 6)); + labeling.removeLabel("test1"); + EXPECT_FALSE(labeling.containsLabel("test1")); + EXPECT_EQ(1ul, labeling.getNumberOfLabels()); + EXPECT_TRUE(labeling.getStateHasLabel("test2", 5)); +} diff --git a/src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp b/src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp new file mode 100644 index 000000000..efe5acf5d --- /dev/null +++ b/src/test/storm/transformer/NonMarkovianChainTransformerTest.cpp @@ -0,0 +1,249 @@ +#include "test/storm_gtest.h" +#include "storm-config.h" +#include "storm/api/storm.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm-parsers/api/storm-parsers.h" +#include "storm-parsers/parser/PrismParser.h" +#include "storm/storage/jani/Property.h" + + +TEST(NonMarkovianChainTransformerTest, StreamExampleTest) { + storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/ma/stream2.ma"); + std::string formulasString = "Pmin=? [ F \"done\"];Pmin=? [ F<=1 \"done\"];Tmin=? [ F \"done\" ]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); + auto model = storm::api::buildSparseModel(program, formulas)->template as>(); + + EXPECT_EQ(12ul, model->getNumberOfStates()); + EXPECT_EQ(14ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + size_t initState = 0; + + auto labeling = model->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 10)); + + auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[2], true)); + EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Keep labels + auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels); + ASSERT_EQ(9ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 8)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Merge labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 7)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Delete labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("done", 7)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.6487584849, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(0.7888888889, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + +} + +TEST(NonMarkovianChainTransformerTest, ChainElimination1ExampleTest) { + auto model = storm::parser::DirectEncodingParser::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination1.drn")->template as>(); + std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString)); + + EXPECT_EQ(43ul, model->getNumberOfStates()); + EXPECT_EQ(59ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + size_t initState = 0; + + auto labeling = model->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + for (size_t i = 10; i < 43; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + + auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[2], true)); + EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Keep labels + auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels); + ASSERT_EQ(13ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(29ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + for (size_t i = 5; i < 13; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Merge labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + for (size_t i = 0; i < 8; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Delete labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels); + ASSERT_EQ(8ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(24ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 0)); + for (size_t i = 1; i < 8; ++i) { + ASSERT_TRUE(labeling.getStateHasLabel("Fail", i)); + } + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.08606881472, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(3333.333333, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); +} + +TEST(NonMarkovianChainTransformerTest, ChainElimination2ExampleTest) { + auto model = storm::parser::DirectEncodingParser::parseModel(STORM_TEST_RESOURCES_DIR "/ma/chain_elimination2.drn")->template as>(); + std::string formulasString = "Pmin=? [ F \"Fail\"];Pmin=? [ F<=300 \"Fail\"];Tmin=? [ F \"Fail\" ]"; + auto formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulasString)); + + EXPECT_EQ(10ul, model->getNumberOfStates()); + EXPECT_EQ(14ul, model->getNumberOfTransitions()); + ASSERT_TRUE(model->isOfType(storm::models::ModelType::MarkovAutomaton)); + size_t initState = 0; + + auto labeling = model->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 7)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 8)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 9)); + + auto result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(formulas[2], true)); + EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Keep labels + auto transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::KeepLabels); + ASSERT_EQ(7ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(11ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 5)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 6)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Merge labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::MergeLabels); + ASSERT_EQ(5ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 2)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + + + // Delete labels + transformed = storm::api::eliminateNonMarkovianChains(model, formulas, storm::transformer::EliminationLabelBehavior::DeleteLabels); + ASSERT_EQ(5ul, transformed.first->getNumberOfStates()); + ASSERT_EQ(10ul, transformed.first->getNumberOfTransitions()); + labeling = transformed.first->getStateLabeling(); + ASSERT_TRUE(labeling.getStateHasLabel("init", initState)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 1)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 2)); + ASSERT_FALSE(labeling.getStateHasLabel("Fail", 3)); + ASSERT_TRUE(labeling.getStateHasLabel("Fail", 4)); + EXPECT_EQ(2ul, transformed.second.size()); + + result = storm::api::verifyWithSparseEngine(transformed.first, storm::api::createTask(transformed.second[0], true)); + EXPECT_EQ(1, result->asExplicitQuantitativeCheckResult()[initState]); + result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[1], true)); + EXPECT_NEAR(0.791015319, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); + //result = storm::api::verifyWithSparseEngine(model, storm::api::createTask(transformed.second[2], true)); + //EXPECT_NEAR(190, result->asExplicitQuantitativeCheckResult()[initState], 1e-6); +}