diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 585bcfdfb..b10204e29 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -42,6 +42,8 @@ namespace storm { const std::string GeneralSettings::constantsOptionShortName = "const"; const std::string GeneralSettings::statisticsOptionName = "statistics"; const std::string GeneralSettings::statisticsOptionShortName = "stats"; + const std::string GeneralSettings::bisimulationOptionName = "bisimulation"; + const std::string GeneralSettings::bisimulationOptionShortName = "bisim"; GeneralSettings::GeneralSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, helpOptionName, false, "Shows all available options, arguments and descriptions.").setShortName(helpOptionShortName) @@ -72,7 +74,7 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the LTL formulas.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the counterexample is to be written.").setDefaultValueString("-").setIsOptional(true).build()).setShortName(counterexampleOptionShortName).build()); - + this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, true, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, transitionRewardsOptionName, "", "If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, stateRewardsOptionName, false, "If given, the state rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --" + explicitOptionName + ").") @@ -91,7 +93,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that Note that this requires the model to be given as an symbolic model (i.e., via --" + symbolicOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, statisticsOptionName, true, "Sets whether to display statistics if available.").setShortName(statisticsOptionShortName).build()); - } bool GeneralSettings::isHelpSet() const { @@ -278,6 +279,10 @@ namespace storm { return true; } + bool GeneralSettings::isBisimulationSet() const { + return this->getOption(bisimulationOptionName).getHasOptionBeenSet(); + } + } // namespace modules } // namespace settings } // namespace storm \ No newline at end of file diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index 75f48d8f1..f4cdf96d0 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -314,6 +314,13 @@ namespace storm { */ bool isShowStatisticsSet() const; + /*! + * Retrieves whether the option to perform bisimulation minimization is set. + * + * @return True iff the option was set. + */ + bool isBisimulationSet() const; + bool check() const override; // The name of the module. @@ -354,6 +361,8 @@ namespace storm { static const std::string constantsOptionShortName; static const std::string statisticsOptionName; static const std::string statisticsOptionShortName; + static const std::string bisimulationOptionName; + static const std::string bisimulationOptionShortName; }; } // namespace modules diff --git a/src/storage/BisimulationDecomposition.cpp b/src/storage/BisimulationDecomposition.cpp new file mode 100644 index 000000000..ba2e4111b --- /dev/null +++ b/src/storage/BisimulationDecomposition.cpp @@ -0,0 +1,50 @@ +#include "src/storage/BisimulationDecomposition.h" + +#include + +namespace storm { + namespace storage { + + template + BisimulationDecomposition::BisimulationDecomposition(storm::models::Dtmc const& model, bool weak) { + computeBisimulationEquivalenceClasses(model, weak); + } + + template + void BisimulationDecomposition::computeBisimulationEquivalenceClasses(storm::models::Dtmc const& model, bool weak) { + // We start by computing the initial partition. In particular, we also keep a mapping of states to their blocks. + std::vector stateToBlockMapping(model.getNumberOfStates()); + storm::storage::BitVector labeledStates = model.getLabeledStates("one"); + this->blocks.emplace_back(labeledStates.begin(), labeledStates.end()); + std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 0; } ); + labeledStates.complement(); + this->blocks.emplace_back(labeledStates.begin(), labeledStates.end()); + std::for_each(labeledStates.begin(), labeledStates.end(), [&] (storm::storage::sparse::state_type const& state) { stateToBlockMapping[state] = 1; } ); + + // Retrieve the backward transitions to allow for better checking of states that need to be re-examined. + storm::storage::SparseMatrix const& backwardTransitions = model.getBackwardTransitions(); + + // Initially, both blocks are potential splitters. + std::queue splitterQueue; + splitterQueue.push(0); + splitterQueue.push(1); + + // As long as there is a splitter, we keep refining the current partition. + while (!splitterQueue.empty()) { + + } + + // While there is a splitter... + // + // check the predecessors of the splitter: + // * if they still have the same signature as before, then they remain unsplit + // * otherwise, split off the states that now behave differently + // and mark the smaller block as a splitter + + // + + } + + template class BisimulationDecomposition; + } +} \ No newline at end of file diff --git a/src/storage/BisimulationDecomposition.h b/src/storage/BisimulationDecomposition.h new file mode 100644 index 000000000..1d2535b2e --- /dev/null +++ b/src/storage/BisimulationDecomposition.h @@ -0,0 +1,28 @@ +#ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ +#define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ + +#include "src/storage/Decomposition.h" +#include "src/models/Dtmc.h" + +namespace storm { + namespace storage { + + /*! + * This class represents the decomposition model into its bisimulation quotient. + */ + template + class BisimulationDecomposition : public Decomposition { + public: + /*! + * Decomposes the given DTMC into equivalence classes under weak or strong bisimulation. + */ + BisimulationDecomposition(storm::models::Dtmc const& model, bool weak); + + private: + void computeBisimulationEquivalenceClasses(storm::models::Dtmc const& model, bool weak); + }; + + } +} + +#endif /* STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp new file mode 100644 index 000000000..84bda0abf --- /dev/null +++ b/src/storage/Distribution.cpp @@ -0,0 +1,35 @@ +#include "src/storage/Distribution.h" + +#include + +namespace storm { + namespace storage { + template + void Distribution::addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability) { + this->distribution[state] += probability; + this->hash += static_cast(state); + } + + template + typename Distribution::iterator Distribution::begin() { + return this->distribution.begin(); + } + + template + typename Distribution::const_iterator Distribution::begin() const { + return this->distribution.begin(); + } + + template + typename Distribution::iterator Distribution::end() { + return this->distribution.end(); + } + + template + typename Distribution::const_iterator Distribution::end() const { + return this->distribution.end(); + } + + template class Distribution; + } +} \ No newline at end of file diff --git a/src/storage/Distribution.h b/src/storage/Distribution.h new file mode 100644 index 000000000..97639501c --- /dev/null +++ b/src/storage/Distribution.h @@ -0,0 +1,71 @@ +#ifndef STORM_STORAGE_DISTRIBUTION_H_ +#define STORM_STORAGE_DISTRIBUTION_H_ + +#include +#include + +#include "src/storage/sparse/StateType.h" + +namespace storm { + namespace storage { + + template + class Distribution { + public: + typedef boost::container::flat_map container_type; + typedef typename container_type::iterator iterator; + typedef typename container_type::const_iterator const_iterator; + + /*! + * Creates an empty distribution. + */ + Distribution() = default; + + /*! + * Assigns the given state the given probability under this distribution. + * + * @param state The state to which to assign the probability. + * @param probability The probability to assign. + */ + void addProbability(storm::storage::sparse::state_type const& state, ValueType const& probability); + + /*! + * Retrieves an iterator to the elements in this distribution. + * + * @return The iterator to the elements in this distribution. + */ + iterator begin(); + + /*! + * Retrieves an iterator to the elements in this distribution. + * + * @return The iterator to the elements in this distribution. + */ + const_iterator begin() const; + + /*! + * Retrieves an iterator past the elements in this distribution. + * + * @return The iterator past the elements in this distribution. + */ + iterator end(); + + /*! + * Retrieves an iterator past the elements in this distribution. + * + * @return The iterator past the elements in this distribution. + */ + const_iterator end() const; + + private: + // A list of states and the probabilities that are assigned to them. + container_type distribution; + + // A hash value that is maintained to allow for quicker equality comparison between distribution.s + std::size_t hash; + }; + + } +} + +#endif /* STORM_STORAGE_DISTRIBUTION_H_ */ \ No newline at end of file