diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index 94b1e0f46..e6da6ab7e 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -62,39 +62,24 @@ namespace storm { // The state-action reward vector. std::vector stateActionRewardVector; }; - - template - ExplicitPrismModelBuilder::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) { - // Intentionally left empty. - } - - template - ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation() : stateStorage(64, 10), initialStateIndices(), bitsPerState(64), numberOfStates() { - // Intentionally left empty. - } - - template - ExplicitPrismModelBuilder::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() { - // Intentionally left empty. - } - + template ExplicitPrismModelBuilder::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { // Intentionally left empty. } template - ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set()), expressionLabels(std::vector()), terminalStates(), negatedTerminalStates() { this->preserveFormula(formula); } template - ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { + ExplicitPrismModelBuilder::Options::Options(std::vector> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() { if (formulas.empty()) { this->buildAllRewardModels = true; this->buildAllLabels = true; @@ -182,19 +167,14 @@ namespace storm { } template - ExplicitPrismModelBuilder::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options) { - - // Create the variable information for the transformed program. - this->variableInformation = VariableInformation(this->program); - - // Create the internal state storage. - this->internalStateInformation = InternalStateInformation(variableInformation.getTotalBitOffset(true)); + ExplicitPrismModelBuilder::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options), variableInformation(this->program), stateStorage(variableInformation.getTotalBitOffset(true)) { + // Intentionally left empty. } template - typename ExplicitPrismModelBuilder::StateInformation const& ExplicitPrismModelBuilder::getStateInformation() const { - STORM_LOG_THROW(static_cast(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build."); - return stateInformation.get(); + storm::storage::sparse::StateValuations const& ExplicitPrismModelBuilder::getStateValuations() const { + STORM_LOG_THROW(static_cast(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build."); + return stateValuations.get(); } template @@ -261,10 +241,10 @@ namespace storm { template StateType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state) { - uint32_t newIndex = internalStateInformation.numberOfStates; + uint32_t newIndex = stateStorage.numberOfStates; // Check, if the state was already registered. - std::pair actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex); + std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); if (actualIndexBucketPair.first == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { @@ -277,7 +257,7 @@ namespace storm { } else { STORM_LOG_ASSERT(false, "Invalid exploration order."); } - ++internalStateInformation.numberOfStates; + ++stateStorage.numberOfStates; } return actualIndexBucketPair.first; @@ -311,7 +291,7 @@ namespace storm { } // Let the generator create all initial states. - this->internalStateInformation.initialStateIndices = generator.getInitialStates(stateToIdCallback); + this->stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback); // Now explore the current state until there is no more reachable state. uint_fast64_t currentRowGroup = 0; @@ -321,7 +301,7 @@ namespace storm { while (!statesToExplore.empty()) { // Get the first state in the queue. CompressedState currentState = statesToExplore.front(); - StateType currentIndex = internalStateInformation.stateStorage.getValue(currentState); + StateType currentIndex = stateStorage.stateToId.getValue(currentState); statesToExplore.pop_front(); // If the exploration order differs from breadth-first, we remember that this row group was actually @@ -426,13 +406,13 @@ namespace storm { transitionMatrixBuilder.replaceColumns(remapping, 0); // Fix (b). - std::vector newInitialStateIndices(this->internalStateInformation.initialStateIndices.size()); - std::transform(this->internalStateInformation.initialStateIndices.begin(), this->internalStateInformation.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } ); + std::vector newInitialStateIndices(this->stateStorage.initialStateIndices.size()); + std::transform(this->stateStorage.initialStateIndices.begin(), this->stateStorage.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } ); std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end()); - this->internalStateInformation.initialStateIndices = std::move(newInitialStateIndices); + this->stateStorage.initialStateIndices = std::move(newInitialStateIndices); // Fix (c). - this->internalStateInformation.stateStorage.remap([&remapping] (StateType const& state) { return remapping[state]; } ); + this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } ); } return choiceLabels; @@ -497,10 +477,10 @@ namespace storm { modelComponents.stateLabeling = buildStateLabeling(); // Finally -- if requested -- build the state information that can be retrieved from the outside. - if (options.buildStateInformation) { - stateInformation = StateInformation(internalStateInformation.numberOfStates); - for (auto const& bitVectorIndexPair : internalStateInformation.stateStorage) { - stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first); + if (options.buildStateValuations) { + stateValuations = storm::storage::sparse::StateValuations(stateStorage.numberOfStates); + for (auto const& bitVectorIndexPair : stateStorage.stateToId) { + stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first); } } @@ -510,7 +490,7 @@ namespace storm { template storm::models::sparse::StateLabeling ExplicitPrismModelBuilder::buildStateLabeling() { storm::generator::PrismStateLabelingGenerator generator(program, variableInformation); - return generator.generate(internalStateInformation.stateStorage, internalStateInformation.initialStateIndices); + return generator.generate(stateStorage.stateToId, stateStorage.initialStateIndices); } // Explicitly instantiate the class. diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index ab2eb9815..8cc724de2 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -20,6 +20,8 @@ #include "src/models/sparse/Model.h" #include "src/models/sparse/StateLabeling.h" #include "src/storage/SparseMatrix.h" +#include "src/storage/sparse/StateValuations.h" +#include "src/storage/sparse/StateStorage.h" #include "src/settings/SettingsManager.h" #include "src/utility/prism.h" @@ -45,42 +47,6 @@ namespace storm { template, typename StateType = uint32_t> class ExplicitPrismModelBuilder { public: - // A structure holding information about the reachable state space while building it. - struct InternalStateInformation { - // Builds an empty state information. - InternalStateInformation(); - - // Creates a state information structure for storing states of the given bit width. - InternalStateInformation(uint64_t bitsPerState); - - // This member stores all the states and maps them to their unique indices. - storm::storage::BitVectorHashMap stateStorage; - - // A list of initial states in terms of their global indices. - std::vector initialStateIndices; - - // The number of bits of each state. - uint64_t bitsPerState; - - // The number of states that were found in the exploration so far. - uint_fast64_t numberOfStates; - }; - - // A structure holding information about the reachable state space that can be retrieved from the outside. - struct StateInformation : public storm::models::sparse::StateAnnotation { - /*! - * Constructs a state information object for the given number of states. - */ - StateInformation(uint_fast64_t numberOfStates); - - // A mapping from state indices to their variable valuations. - std::vector valuations; - - std::string stateInfo(uint_fast64_t state) const override { - return valuations[state].toString(); - } - }; - // A structure holding the individual components of a model. struct ModelComponents { ModelComponents(); @@ -163,7 +129,7 @@ namespace storm { // A flag that indicates whether or not to store the state information after successfully building the // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful // call to translateProgram. - bool buildStateInformation; + bool buildStateValuations; // A list of reward models to be build in case not all reward models are to be build. std::set rewardModelsToBuild; @@ -214,7 +180,7 @@ namespace storm { * * @return A structure that stores information about all reachable states. */ - StateInformation const& getStateInformation() const; + storm::storage::sparse::StateValuations const& getStateValuations() const; /*! * Retrieves the program that was actually translated (i.e. including constant substitutions etc.). @@ -233,7 +199,6 @@ namespace storm { * used after invoking this method. * * @param state A pointer to a state for which to retrieve the index. This must not be used after the call. - * @param internalStateInformation The information about the already explored part of the reachable state space. * @return A pair indicating whether the state was already discovered before and the state id of the state. */ StateType getOrAddStateIndex(CompressedState const& state); @@ -245,7 +210,6 @@ namespace storm { * @param variableInformation A structure containing information about the variables in the program. * @param transitionRewards A list of transition rewards that are to be considered in the transition reward * matrix. - * @param internalStateInformation A structure containing information about the states of the program. * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not. * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this * function. @@ -270,9 +234,6 @@ namespace storm { /*! * Builds the state labeling for the given program. * - * @param program The program for which to build the state labeling. - * @param variableInformation Information about the variables in the program. - * @param internalStateInformation Information about the state space of the program. * @return The state labeling of the given program. */ storm::models::sparse::StateLabeling buildStateLabeling(); @@ -287,11 +248,11 @@ namespace storm { VariableInformation variableInformation; // Internal information about the states that were explored. - InternalStateInformation internalStateInformation; + storm::storage::sparse::StateStorage stateStorage; // This member holds information about reachable states that can be retrieved from the outside after a // successful build. - boost::optional stateInformation; + boost::optional stateValuations; // A set of states that still need to be explored. std::deque statesToExplore; diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp index 0316d6bc4..bdda7f3ed 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp @@ -2,27 +2,38 @@ #include "src/logic/FragmentSpecification.h" +#include "src/utility/prism.h" + #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" namespace storm { namespace modelchecker { - template - SparseMdpLearningModelChecker::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(program) { + template + SparseMdpLearningModelChecker::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(storm::utility::prism::preprocessProgram(program)), variableInformation(this->program), generator(program, variableInformation, false) { // Intentionally left empty. } - template - bool SparseMdpLearningModelChecker::canHandle(CheckTask const& checkTask) const { + template + bool SparseMdpLearningModelChecker::canHandle(CheckTask const& checkTask) const { storm::logic::Formula const& formula = checkTask.getFormula(); storm::logic::FragmentSpecification fragment = storm::logic::propositional().setProbabilityOperatorsAllowed(true).setReachabilityProbabilityFormulasAllowed(true); return formula.isInFragment(fragment); } - template - std::unique_ptr SparseMdpLearningModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { + template + std::unique_ptr SparseMdpLearningModelChecker::computeReachabilityProbabilities(CheckTask const& checkTask) { + + // Create a callback for the next-state generator to enable it to request the index of states. + std::function stateToIdCallback = std::bind(&SparseMdpLearningModelChecker::getOrAddStateIndex, this, std::placeholders::_1); + return nullptr; } + template + typename SparseMdpLearningModelChecker::StateType SparseMdpLearningModelChecker::getOrAddStateIndex(storm::generator::CompressedState const& state) { + + } + template class SparseMdpLearningModelChecker; } } \ No newline at end of file diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h index d398c6be3..02e53403b 100644 --- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h +++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h @@ -5,6 +5,9 @@ #include "src/storage/prism/Program.h" +#include "src/generator/PrismNextStateGenerator.h" +#include "src/generator/VariableInformation.h" + #include "src/utility/constants.h" namespace storm { @@ -13,6 +16,8 @@ namespace storm { template class SparseMdpLearningModelChecker : public AbstractModelChecker { public: + typedef uint32_t StateType; + SparseMdpLearningModelChecker(storm::prism::Program const& program); virtual bool canHandle(CheckTask const& checkTask) const override; @@ -20,8 +25,16 @@ namespace storm { virtual std::unique_ptr computeReachabilityProbabilities(CheckTask const& checkTask) override; private: + StateType getOrAddStateIndex(storm::generator::CompressedState const& state); + // The program that defines the model to check. storm::prism::Program program; + + // The variable information. + storm::generator::VariableInformation variableInformation; + + // A generator used to explore the model. + storm::generator::PrismNextStateGenerator generator; }; } } diff --git a/src/models/sparse/StateAnnotation.h b/src/models/sparse/StateAnnotation.h index 42067bf76..f608a5186 100644 --- a/src/models/sparse/StateAnnotation.h +++ b/src/models/sparse/StateAnnotation.h @@ -1,16 +1,19 @@ -#ifndef STORM_STATEANNOTATION_H -#define STORM_STATEANNOTATION_H +#ifndef STORM_MODELS_SPARSE_STATEANNOTATION_H_ +#define STORM_MODELS_SPARSE_STATEANNOTATION_H_ + +#include "src/storage/sparse/StateType.h" namespace storm { namespace models { namespace sparse { + class StateAnnotation { public: - virtual std::string stateInfo(uint_fast64_t s) const = 0; + virtual std::string stateInfo(storm::storage::sparse::state_type const& state) const = 0; }; + } } - } -#endif //STORM_STATEANNOTATION_H \ No newline at end of file +#endif /* STORM_MODELS_SPARSE_STATEANNOTATION_H_ */ \ No newline at end of file diff --git a/src/storage/sparse/StateStorage.cpp b/src/storage/sparse/StateStorage.cpp new file mode 100644 index 000000000..30c0eaace --- /dev/null +++ b/src/storage/sparse/StateStorage.cpp @@ -0,0 +1,15 @@ +#include "src/storage/sparse/StateStorage.h" + +namespace storm { + namespace storage { + namespace sparse { + + template + StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() { + // Intentionally left empty. + } + + template class StateStorage; + } + } +} \ No newline at end of file diff --git a/src/storage/sparse/StateStorage.h b/src/storage/sparse/StateStorage.h new file mode 100644 index 000000000..79c8483ab --- /dev/null +++ b/src/storage/sparse/StateStorage.h @@ -0,0 +1,35 @@ +#ifndef STORM_STORAGE_SPARSE_STATESTORAGE_H_ +#define STORM_STORAGE_SPARSE_STATESTORAGE_H_ + +#include + +#include "src/storage/BitVectorHashMap.h" + +namespace storm { + namespace storage { + namespace sparse { + + // A structure holding information about the reachable state space while building it. + template + struct StateStorage { + // Creates an empty state storage structure for storing states of the given bit width. + StateStorage(uint64_t bitsPerState); + + // This member stores all the states and maps them to their unique indices. + storm::storage::BitVectorHashMap stateToId; + + // A list of initial states in terms of their global indices. + std::vector initialStateIndices; + + // The number of bits of each state. + uint64_t bitsPerState; + + // The number of states that were found in the exploration so far. + uint_fast64_t numberOfStates; + }; + + } + } +} + +#endif /* STORM_STORAGE_SPARSE_STATESTORAGE_H_ */ \ No newline at end of file diff --git a/src/storage/sparse/StateValuations.cpp b/src/storage/sparse/StateValuations.cpp new file mode 100644 index 000000000..f3f98818f --- /dev/null +++ b/src/storage/sparse/StateValuations.cpp @@ -0,0 +1,17 @@ +#include "src/storage/sparse/StateValuations.h" + +namespace storm { + namespace storage { + namespace sparse { + + StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) { + // Intentionally left empty. + } + + std::string StateValuations::stateInfo(state_type const& state) const { + return valuations[state].toString(); + } + + } + } +} \ No newline at end of file diff --git a/src/storage/sparse/StateValuations.h b/src/storage/sparse/StateValuations.h new file mode 100644 index 000000000..b64620efd --- /dev/null +++ b/src/storage/sparse/StateValuations.h @@ -0,0 +1,33 @@ +#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ +#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ + +#include +#include + +#include "src/storage/sparse/StateType.h" +#include "src/storage/expressions/SimpleValuation.h" + +#include "src/models/sparse/StateAnnotation.h" + +namespace storm { + namespace storage { + namespace sparse { + + // A structure holding information about the reachable state space that can be retrieved from the outside. + struct StateValuations : public storm::models::sparse::StateAnnotation { + /*! + * Constructs a state information object for the given number of states. + */ + StateValuations(state_type const& numberOfStates); + + // A mapping from state indices to their variable valuations. + std::vector valuations; + + virtual std::string stateInfo(state_type const& state) const override; + }; + + } + } +} + +#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */ \ No newline at end of file