diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp index ed65da9da..d5b8660b2 100644 --- a/src/builder/ExplicitPrismModelBuilder.cpp +++ b/src/builder/ExplicitPrismModelBuilder.cpp @@ -229,10 +229,10 @@ namespace storm { template StateType ExplicitPrismModelBuilder::getOrAddStateIndex(CompressedState const& state) { - uint32_t newIndex = stateStorage.numberOfStates; + StateType newIndex = static_cast(stateStorage.getNumberOfStates()); // Check, if the state was already registered. - std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); + std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); if (actualIndexBucketPair.first == newIndex) { if (options.explorationOrder == ExplorationOrder::Dfs) { @@ -245,7 +245,6 @@ namespace storm { } else { STORM_LOG_ASSERT(false, "Invalid exploration order."); } - ++stateStorage.numberOfStates; } return actualIndexBucketPair.first; @@ -467,7 +466,7 @@ namespace storm { // Finally -- if requested -- build the state information that can be retrieved from the outside. if (options.buildStateValuations) { - stateValuations = storm::storage::sparse::StateValuations(stateStorage.numberOfStates); + stateValuations = storm::storage::sparse::StateValuations(stateStorage.getNumberOfStates()); for (auto const& bitVectorIndexPair : stateStorage.stateToId) { stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation, program.getManager()); } diff --git a/src/modelchecker/exploration/Bounds.cpp b/src/modelchecker/exploration/Bounds.cpp index 32ad0cb92..9892c33f0 100644 --- a/src/modelchecker/exploration/Bounds.cpp +++ b/src/modelchecker/exploration/Bounds.cpp @@ -10,18 +10,14 @@ namespace storm { std::pair Bounds::getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const { ActionType index = explorationInformation.getRowGroup(state); if (index == explorationInformation.getUnexploredMarker()) { + std::cout << "state " << state << " is unexplored! retuning zero/one" << std::endl; return std::make_pair(storm::utility::zero(), storm::utility::one()); } else { + std::cout << "accessing at index " << index << " out of " << boundsPerState.size() << std::endl; return boundsPerState[index]; } } - - template - std::pair const& Bounds::getBoundsForExploredState(StateType const& state, ExplorationInformation const& explorationInformation) const { - ActionType index = explorationInformation.getRowGroup(state); - return boundsPerState[index]; - } - + template ValueType Bounds::getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const { ActionType index = explorationInformation.getRowGroup(state); @@ -78,7 +74,7 @@ namespace storm { template ValueType Bounds::getDifferenceOfStateBounds(StateType const& state, ExplorationInformation const& explorationInformation) const { - std::pair const& bounds = getBoundsForExploredState(state, explorationInformation); + std::pair bounds = getBoundsForState(state, explorationInformation); return bounds.second - bounds.first; } @@ -120,6 +116,7 @@ namespace storm { template void Bounds::setBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation, std::pair const& values) { StateType const& rowGroup = explorationInformation.getRowGroup(state); + std::cout << "setting " << values.first << ", " << values.second << " for state " << state << std::endl; setBoundsForRowGroup(rowGroup, values); } diff --git a/src/modelchecker/exploration/Bounds.h b/src/modelchecker/exploration/Bounds.h index 27e0979a5..816e8c923 100644 --- a/src/modelchecker/exploration/Bounds.h +++ b/src/modelchecker/exploration/Bounds.h @@ -21,8 +21,6 @@ namespace storm { typedef StateType ActionType; std::pair getBoundsForState(StateType const& state, ExplorationInformation const& explorationInformation) const; - - std::pair const& getBoundsForExploredState(StateType const& state, ExplorationInformation const& explorationInformation) const; ValueType getLowerBoundForState(StateType const& state, ExplorationInformation const& explorationInformation) const; diff --git a/src/modelchecker/exploration/ExplorationInformation.cpp b/src/modelchecker/exploration/ExplorationInformation.cpp index 12715f307..7f45eb6c6 100644 --- a/src/modelchecker/exploration/ExplorationInformation.cpp +++ b/src/modelchecker/exploration/ExplorationInformation.cpp @@ -10,7 +10,7 @@ namespace storm { namespace exploration_detail { template - ExplorationInformation::ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : stateStorage(bitsPerBucket), unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) { + ExplorationInformation::ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceWeightedProbability) { storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings(); localPrecomputation = settings.isLocalPrecomputationSet(); @@ -24,25 +24,24 @@ namespace storm { } template - void ExplorationInformation::setInitialStates(std::vector const& initialStates) { - stateStorage.initialStateIndices = initialStates; + typename ExplorationInformation::const_iterator ExplorationInformation::findUnexploredState(StateType const& state) const { + return unexploredStates.find(state); } template - StateType ExplorationInformation::getFirstInitialState() const { - return stateStorage.initialStateIndices.front(); + typename ExplorationInformation::const_iterator ExplorationInformation::unexploredStatesEnd() const { + return unexploredStates.end(); } template - std::size_t ExplorationInformation::getNumberOfInitialStates() const { - return stateStorage.initialStateIndices.size(); + void ExplorationInformation::removeUnexploredState(const_iterator it) { + unexploredStates.erase(it); } template - void ExplorationInformation::addUnexploredState(storm::generator::CompressedState const& compressedState) { + void ExplorationInformation::addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState) { stateToRowGroupMapping.push_back(unexploredMarker); - unexploredStates[stateStorage.numberOfStates] = compressedState; - ++stateStorage.numberOfStates; + unexploredStates[stateId] = compressedState; } template @@ -71,6 +70,21 @@ namespace storm { newRowGroup(matrix.size()); } + template + void ExplorationInformation::terminateCurrentRowGroup() { + rowGroupIndices.push_back(matrix.size()); + } + + template + void ExplorationInformation::moveActionToBackOfMatrix(ActionType const& action) { + matrix.emplace_back(std::move(matrix[action])); + } + + template + StateType ExplorationInformation::getActionCount() const { + return matrix.size(); + } + template std::size_t ExplorationInformation::getNumberOfUnexploredStates() const { return unexploredStates.size(); @@ -78,7 +92,7 @@ namespace storm { template std::size_t ExplorationInformation::getNumberOfDiscoveredStates() const { - return stateStorage.numberOfStates; + return stateToRowGroupMapping.size(); } template @@ -132,7 +146,7 @@ namespace storm { } template - void ExplorationInformation::addRowsToMatrix(std::size_t const& count) { + void ExplorationInformation::addActionsToMatrix(std::size_t const& count) { matrix.resize(matrix.size() + count); } diff --git a/src/modelchecker/exploration/ExplorationInformation.h b/src/modelchecker/exploration/ExplorationInformation.h index b073352cd..550b3d32c 100644 --- a/src/modelchecker/exploration/ExplorationInformation.h +++ b/src/modelchecker/exploration/ExplorationInformation.h @@ -13,7 +13,6 @@ #include "src/generator/CompressedState.h" #include "src/storage/SparseMatrix.h" -#include "src/storage/sparse/StateStorage.h" #include "src/settings/modules/ExplorationSettings.h" @@ -25,16 +24,19 @@ namespace storm { public: typedef StateType ActionType; typedef boost::container::flat_set StateSet; + typedef std::unordered_map IdToStateMap; + typedef typename IdToStateMap::const_iterator const_iterator; + typedef std::vector>> MatrixType; - ExplorationInformation(uint_fast64_t bitsPerBucket, storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits::max()); + ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits::max()); - void setInitialStates(std::vector const& initialStates); + const_iterator findUnexploredState(StateType const& state) const; - StateType getFirstInitialState() const; + const_iterator unexploredStatesEnd() const; - std::size_t getNumberOfInitialStates() const; + void removeUnexploredState(const_iterator it); - void addUnexploredState(storm::generator::CompressedState const& compressedState); + void addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState); void assignStateToRowGroup(StateType const& state, ActionType const& rowGroup); @@ -46,6 +48,12 @@ namespace storm { void newRowGroup(); + void terminateCurrentRowGroup(); + + void moveActionToBackOfMatrix(ActionType const& action); + + StateType getActionCount() const; + std::size_t getNumberOfUnexploredStates() const; std::size_t getNumberOfDiscoveredStates() const; @@ -70,7 +78,7 @@ namespace storm { std::vector> const& getRowOfMatrix(ActionType const& row) const; - void addRowsToMatrix(std::size_t const& count); + void addActionsToMatrix(std::size_t const& count); bool maximize() const; @@ -95,14 +103,12 @@ namespace storm { void setOptimizationDirection(storm::OptimizationDirection const& direction); private: - storm::storage::sparse::StateStorage stateStorage; - - std::vector>> matrix; + MatrixType matrix; std::vector rowGroupIndices; std::vector stateToRowGroupMapping; StateType unexploredMarker; - std::unordered_map unexploredStates; + IdToStateMap unexploredStates; storm::OptimizationDirection optimizationDirection; StateSet terminalStates; diff --git a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp index 4ad5b5613..9fd4c85f8 100644 --- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp @@ -52,45 +52,26 @@ namespace storm { storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula(); STORM_LOG_THROW(program.isDeterministicModel() || checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "For nondeterministic systems, an optimization direction (min/max) must be given in the property."); - std::map labelToExpressionMapping = program.getLabelToExpressionMapping(); - StateGeneration stateGeneration(program, variableInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); - - ExplorationInformation explorationInformation(variableInformation.getTotalBitOffset(true), checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize); - + ExplorationInformation explorationInformation(checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize); + // The first row group starts at action 0. explorationInformation.newRowGroup(0); - // Create a callback for the next-state generator to enable it to request the index of states. - stateGeneration.setStateToIdCallback(createStateToIdCallback(explorationInformation)); + std::map labelToExpressionMapping = program.getLabelToExpressionMapping(); + StateGeneration stateGeneration(program, variableInformation, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping)); + // Compute and return result. std::tuple boundsForInitialState = performExploration(stateGeneration, explorationInformation); return std::make_unique>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState)); } - - template - std::function::StateType (storm::generator::CompressedState const&)> SparseMdpExplorationModelChecker::createStateToIdCallback(ExplorationInformation& explorationInformation) const { - return [&explorationInformation,this] (storm::generator::CompressedState const& state) -> StateType { - StateType newIndex = explorationInformation.getNumberOfDiscoveredStates(); - // Check, if the state was already registered. - std::pair actualIndexBucketPair = explorationInformation.stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); - - if (actualIndexBucketPair.first == newIndex) { - explorationInformation.addUnexploredState(state); - } - - return actualIndexBucketPair.first; - }; - } - template std::tuple::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker::performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const { - // Generate the initial state so we know where to start the simulation. - explorationInformation.setInitialStates(stateGeneration.getInitialStates()); - STORM_LOG_THROW(explorationInformation.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); - StateType initialStateIndex = explorationInformation.getFirstInitialState(); + stateGeneration.computeInitialStates(); + STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine."); + StateType initialStateIndex = stateGeneration.getFirstInitialState(); // Create a structure that holds the bounds for the states and actions. Bounds bounds; @@ -141,7 +122,7 @@ namespace storm { template bool SparseMdpExplorationModelChecker::samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, Bounds& bounds, Statistics& stats) const { // Start the search from the initial state. - stack.push_back(std::make_pair(explorationInformation.getFirstInitialState(), 0)); + stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0)); // As long as we didn't find a terminal (accepting or rejecting) state in the search, sample a new successor. bool foundTerminalState = false; @@ -150,8 +131,8 @@ namespace storm { STORM_LOG_TRACE("State on top of stack is: " << currentStateId << "."); // If the state is not yet explored, we need to retrieve its behaviors. - auto unexploredIt = explorationInformation.unexploredStates.find(currentStateId); - if (unexploredIt != explorationInformation.unexploredStates.end()) { + auto unexploredIt = explorationInformation.findUnexploredState(currentStateId); + if (unexploredIt != explorationInformation.unexploredStatesEnd()) { STORM_LOG_TRACE("State was not yet explored."); // Explore the previously unexplored state. @@ -160,7 +141,7 @@ namespace storm { if (foundTerminalState) { STORM_LOG_TRACE("Aborting sampling of path, because a terminal state was reached."); } - explorationInformation.unexploredStates.erase(unexploredIt); + explorationInformation.removeUnexploredState(unexploredIt); } else { // If the state was already explored, we check whether it is a terminal state or not. if (explorationInformation.isTerminal(currentStateId)) { @@ -245,30 +226,31 @@ namespace storm { // need to store its behavior. if (!isTerminalState) { // Next, we insert the behavior into our matrix structure. - StateType startRow = explorationInformation.matrix.size(); - explorationInformation.addRowsToMatrix(behavior.getNumberOfChoices()); + StateType startAction = explorationInformation.getActionCount(); + explorationInformation.addActionsToMatrix(behavior.getNumberOfChoices()); - ActionType currentAction = 0; + ActionType localAction = 0; // Retrieve the lowest state bounds (wrt. to the current optimization direction). std::pair stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection()); for (auto const& choice : behavior) { for (auto const& entry : choice) { - explorationInformation.getRowOfMatrix(startRow + currentAction).emplace_back(entry.first, entry.second); + explorationInformation.getRowOfMatrix(startAction + localAction).emplace_back(entry.first, entry.second); + std::cout << "adding " << (startAction + localAction) << "x" << entry.first << " -> " << entry.second << std::endl; } - std::pair actionBounds = computeBoundsOfAction(startRow + currentAction, explorationInformation, bounds); + std::pair actionBounds = computeBoundsOfAction(startAction + localAction, explorationInformation, bounds); bounds.initializeBoundsForNextAction(actionBounds); stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); - STORM_LOG_TRACE("Initializing bounds of action " << (startRow + currentAction) << " to " << bounds.getLowerBoundForAction(startRow + currentAction) << " and " << bounds.getUpperBoundForAction(startRow + currentAction) << "."); + STORM_LOG_TRACE("Initializing bounds of action " << (startAction + localAction) << " to " << bounds.getLowerBoundForAction(startAction + localAction) << " and " << bounds.getUpperBoundForAction(startAction + localAction) << "."); - ++currentAction; + ++localAction; } // Terminate the row group. - explorationInformation.rowGroupIndices.push_back(explorationInformation.matrix.size()); + explorationInformation.terminateCurrentRowGroup(); bounds.setBoundsForState(currentStateId, explorationInformation, stateBounds); STORM_LOG_TRACE("Initializing bounds of state " << currentStateId << " to " << bounds.getLowerBoundForState(currentStateId, explorationInformation) << " and " << bounds.getUpperBoundForState(currentStateId, explorationInformation) << "."); @@ -292,7 +274,7 @@ namespace storm { } // Increase the size of the matrix, but leave the row empty. - explorationInformation.addRowsToMatrix(1); + explorationInformation.addActionsToMatrix(1); // Terminate the row group. explorationInformation.newRowGroup(); @@ -342,9 +324,9 @@ namespace storm { template typename SparseMdpExplorationModelChecker::StateType SparseMdpExplorationModelChecker::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation const& explorationInformation, Bounds const& bounds) const { std::vector> const& row = explorationInformation.getRowOfMatrix(chosenAction); -// if (row.size() == 1) { -// return row.front().getColumn(); -// } + if (row.size() == 1) { + return row.front().getColumn(); + } std::vector probabilities(row.size()); @@ -352,6 +334,7 @@ namespace storm { if (explorationInformation.useDifferenceWeightedProbabilityHeuristic()) { std::transform(row.begin(), row.end(), probabilities.begin(), [&bounds, &explorationInformation] (storm::storage::MatrixEntry const& entry) { + std::cout << entry.getColumn() << " with diff " << bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation) << std::endl; return entry.getValue() * bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation); }); } else if (explorationInformation.useProbabilityHeuristic()) { @@ -393,9 +376,8 @@ namespace storm { relevantStates.resize(std::distance(relevantStates.begin(), newEnd)); } else { for (StateType state = 0; state < explorationInformation.getNumberOfDiscoveredStates(); ++state) { - // Add the state to the relevant states if they are not unexplored. Additionally, if we are - // computing minimal probabilities, we only consider it relevant if it's not a target state. - if (!explorationInformation.isUnexplored(state) && (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(state, explorationInformation)))) { + // Add the state to the relevant states if they are not unexplored. + if (!explorationInformation.isUnexplored(state)) { relevantStates.push_back(state); } } @@ -408,8 +390,10 @@ namespace storm { storm::storage::BitVector targetStates(sink + 1); for (StateType index = 0; index < relevantStates.size(); ++index) { relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index); + std::cout << "lower bound for state " << relevantStates[index] << " is " << bounds.getLowerBoundForState(relevantStates[index], explorationInformation) << std::endl; if (storm::utility::isOne(bounds.getLowerBoundForState(relevantStates[index], explorationInformation))) { targetStates.set(index); + std::cout << relevantStates[index] << " was identified as a target state" << std::endl; } } @@ -425,9 +409,11 @@ namespace storm { if (it != relevantStateToNewRowGroupMapping.end()) { // If the entry is a relevant state, we copy it over (and compensate for the offset change). builder.addNextValue(currentRow, it->second, entry.getValue()); + std::cout << state << " to " << entry.getColumn() << " with prob " << entry.getValue() << std::endl; } else { // If the entry is an unexpanded state, we gather the probability to later redirect it to an unexpanded sink. unexpandedProbability += entry.getValue(); + std::cout << state << " has unexpanded prob " << unexpandedProbability << " to succ " << entry.getColumn() << std::endl; } } if (unexpandedProbability != storm::utility::zero()) { @@ -487,9 +473,13 @@ namespace storm { statesWithProbability1 = storm::utility::graph::performProb1A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates); } + std::cout << statesWithProbability0 << std::endl; + std::cout << statesWithProbability1 << std::endl; + // Set the bounds of the identified states. for (auto state : statesWithProbability0) { StateType originalState = relevantStates[state]; + std::cout << "determined " << originalState << " as a prob0 state" << std::endl; bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero()); explorationInformation.addTerminalState(originalState); } @@ -558,7 +548,7 @@ namespace storm { // the actions and the new state. std::pair stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection()); for (auto const& action : leavingActions) { - explorationInformation.matrix.emplace_back(std::move(explorationInformation.matrix[action])); + explorationInformation.moveActionToBackOfMatrix(action); std::pair const& actionBounds = bounds.getBoundsForAction(action); bounds.initializeBoundsForNextAction(actionBounds); stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds); @@ -566,7 +556,7 @@ namespace storm { bounds.setBoundsForRowGroup(nextRowGroup, stateBounds); // Terminate the row group of the newly introduced state. - explorationInformation.rowGroupIndices.push_back(explorationInformation.matrix.size()); + explorationInformation.terminateCurrentRowGroup(); } } diff --git a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h index 74e78cf0e..5db171722 100644 --- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h +++ b/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h @@ -44,8 +44,6 @@ namespace storm { virtual std::unique_ptr computeUntilProbabilities(CheckTask const& checkTask) override; private: - std::function createStateToIdCallback(ExplorationInformation& explorationInformation) const; - std::tuple performExploration(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation) const; bool samplePathFromInitialState(StateGeneration& stateGeneration, ExplorationInformation& explorationInformation, StateActionStack& stack, Bounds& bounds, Statistics& stats) const; diff --git a/src/modelchecker/exploration/StateGeneration.cpp b/src/modelchecker/exploration/StateGeneration.cpp index ae2343706..71fc4d416 100644 --- a/src/modelchecker/exploration/StateGeneration.cpp +++ b/src/modelchecker/exploration/StateGeneration.cpp @@ -1,17 +1,26 @@ #include "src/modelchecker/exploration/StateGeneration.h" +#include "src/modelchecker/exploration/ExplorationInformation.h" + namespace storm { namespace modelchecker { namespace exploration_detail { template - StateGeneration::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { - // Intentionally left empty. - } - - template - void StateGeneration::setStateToIdCallback(std::function const& stateToIdCallback) { - this->stateToIdCallback = stateToIdCallback; + StateGeneration::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), stateStorage(variableInformation.getTotalBitOffset(true)), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) { + + stateToIdCallback = [&explorationInformation, this] (storm::generator::CompressedState const& state) -> StateType { + StateType newIndex = stateStorage.getNumberOfStates(); + + // Check, if the state was already registered. + std::pair actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex); + + if (actualIndexBucketPair.first == newIndex) { + explorationInformation.addUnexploredState(newIndex, state); + } + + return actualIndexBucketPair.first; + }; } template @@ -21,7 +30,7 @@ namespace storm { template std::vector StateGeneration::getInitialStates() { - return generator.getInitialStates(stateToIdCallback); + return stateStorage.initialStateIndices; } template @@ -38,7 +47,22 @@ namespace storm { bool StateGeneration::isTargetState() const { return generator.satisfies(targetStateExpression); } - + + template + void StateGeneration::computeInitialStates() { + stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback); + } + + template + StateType StateGeneration::getFirstInitialState() const { + return stateStorage.initialStateIndices.front(); + } + + template + std::size_t StateGeneration::getNumberOfInitialStates() const { + return stateStorage.initialStateIndices.size(); + } + template class StateGeneration; } } diff --git a/src/modelchecker/exploration/StateGeneration.h b/src/modelchecker/exploration/StateGeneration.h index a10ff2883..f75211e54 100644 --- a/src/modelchecker/exploration/StateGeneration.h +++ b/src/modelchecker/exploration/StateGeneration.h @@ -4,6 +4,8 @@ #include "src/generator/CompressedState.h" #include "src/generator/PrismNextStateGenerator.h" +#include "src/storage/sparse/StateStorage.h" + namespace storm { namespace generator { template @@ -13,19 +15,26 @@ namespace storm { namespace modelchecker { namespace exploration_detail { + template + class ExplorationInformation; + template class StateGeneration { public: - StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression); - - void setStateToIdCallback(std::function const& stateToIdCallback); - + StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression); + void load(storm::generator::CompressedState const& state); std::vector getInitialStates(); storm::generator::StateBehavior expand(); + void computeInitialStates(); + + StateType getFirstInitialState() const; + + std::size_t getNumberOfInitialStates() const; + bool isConditionState() const; bool isTargetState() const; @@ -33,6 +42,9 @@ namespace storm { private: storm::generator::PrismNextStateGenerator generator; std::function stateToIdCallback; + + storm::storage::sparse::StateStorage stateStorage; + storm::expressions::Expression conditionStateExpression; storm::expressions::Expression targetStateExpression; }; diff --git a/src/settings/modules/ExplorationSettings.cpp b/src/settings/modules/ExplorationSettings.cpp index a890a1f9e..4a3a2796d 100644 --- a/src/settings/modules/ExplorationSettings.cpp +++ b/src/settings/modules/ExplorationSettings.cpp @@ -19,8 +19,8 @@ namespace storm { ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector types = { "local", "global" }; this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("global").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, false, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, false, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build()); std::vector nextStateHeuristics = { "probdiff", "prob" }; this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiff, prob } where 'prob' samples according to the probabilities in the system and 'probdiff' weights the probabilities with the differences between the current bounds.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiff").build()).build()); diff --git a/src/storage/sparse/StateStorage.cpp b/src/storage/sparse/StateStorage.cpp index 30c0eaace..60af49179 100644 --- a/src/storage/sparse/StateStorage.cpp +++ b/src/storage/sparse/StateStorage.cpp @@ -5,10 +5,15 @@ namespace storm { namespace sparse { template - StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() { + StateStorage::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState) { // Intentionally left empty. } + template + uint_fast64_t StateStorage::getNumberOfStates() const { + return stateToId.size(); + } + template class StateStorage; } } diff --git a/src/storage/sparse/StateStorage.h b/src/storage/sparse/StateStorage.h index 79c8483ab..eee1855c0 100644 --- a/src/storage/sparse/StateStorage.h +++ b/src/storage/sparse/StateStorage.h @@ -25,7 +25,7 @@ namespace storm { uint64_t bitsPerState; // The number of states that were found in the exploration so far. - uint_fast64_t numberOfStates; + uint_fast64_t getNumberOfStates() const; }; }