|
Storm 1.11.1.1
A Modern Probabilistic Model Checker
|
#include "storm/storage/dd/bisimulation/Partition.h"#include "storm/storage/dd/DdManager.h"#include "storm/storage/dd/bisimulation/PreservationInformation.h"#include "storm/logic/AtomicExpressionFormula.h"#include "storm/logic/AtomicLabelFormula.h"#include "storm/logic/Formulas.h"#include "storm/logic/FragmentSpecification.h"#include "storm/models/symbolic/Mdp.h"#include "storm/models/symbolic/StandardRewardModel.h"#include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"#include "storm/settings/SettingsManager.h"#include "storm/settings/modules/BisimulationSettings.h"#include "storm/exceptions/InvalidPropertyException.h"#include "storm/exceptions/NotSupportedException.h"#include "storm/utility/macros.h"#include "storm/adapters/RationalFunctionAdapter.h"
Go to the source code of this file.
Namespaces | |
| namespace | storm |
| LabParser.cpp. | |
| namespace | storm::dd |
| namespace | storm::dd::bisimulation |
Functions | |
| template<storm::dd::DdType DdType> | |
| void | storm::dd::bisimulation::enumerateBlocksRec (std::vector< storm::dd::Bdd< DdType > > const &stateSets, storm::dd::Bdd< DdType > const ¤tStateSet, uint64_t offset, storm::expressions::Variable const &blockVariable, std::function< void(storm::dd::Bdd< DdType > const &)> const &callback) |