diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index ba863af43..d14f8848c 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -64,7 +64,7 @@ namespace storm {
storm::modelchecker::SparseMdpLearningModelChecker<ValueType> checker(program);
std::unique_ptr<storm::modelchecker::CheckResult> result;
if (checker.canHandle(task)) {
- std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(task);
+ result = checker.check(task);
} else {
std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
}
diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
index 46cf53011..f6ecc1055 100644
--- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.cpp
@@ -2,6 +2,7 @@
#include "src/storage/SparseMatrix.h"
#include "src/storage/sparse/StateStorage.h"
+#include "src/storage/MaximalEndComponentDecomposition.h"
#include "src/generator/PrismNextStateGenerator.h"
@@ -11,13 +12,16 @@
#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/GeneralSettings.h"
+
#include "src/utility/macros.h"
#include "src/exceptions/NotSupportedException.h"
namespace storm {
namespace modelchecker {
template<typename ValueType>
- SparseMdpLearningModelChecker<ValueType>::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(storm::utility::prism::preprocessProgram<ValueType>(program)), variableInformation(this->program) {
+ SparseMdpLearningModelChecker<ValueType>::SparseMdpLearningModelChecker(storm::prism::Program const& program) : program(storm::utility::prism::preprocessProgram<ValueType>(program)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(1e-9) {
// Intentionally left empty.
}
@@ -104,7 +108,6 @@ namespace storm {
max = std::max(max, current);
}
-// STORM_LOG_TRACE("Looking for action with value " << upperBoundsPerState[stateToRowGroupMapping[currentStateId]] << ".");
STORM_LOG_TRACE("Looking for action with value " << max << ".");
for (uint32_t row = rowGroupIndices[rowGroup]; row < rowGroupIndices[rowGroup + 1]; ++row) {
@@ -115,9 +118,7 @@ namespace storm {
STORM_LOG_TRACE("Computed (upper) bound " << current << " for row " << row << ".");
// If the action is one of the maximizing ones, insert it into our list.
- // TODO: should this need to be an approximate check?
-// if (current == upperBoundsPerState[stateToRowGroupMapping[currentStateId]]) {
- if (current == max) {
+ if (comparator.isEqual(current, max)) {
allMaxActions.push_back(row);
}
}
@@ -126,99 +127,128 @@ namespace storm {
// Now sample from all maximizing actions.
std::uniform_int_distribution<uint32_t> distribution(0, allMaxActions.size() - 1);
- return allMaxActions[distribution(generator)] - rowGroupIndices[rowGroup];
+ return allMaxActions[distribution(randomGenerator)] - rowGroupIndices[rowGroup];
}
template<typename ValueType>
typename SparseMdpLearningModelChecker<ValueType>::StateType SparseMdpLearningModelChecker<ValueType>::sampleSuccessorFromAction(StateType currentStateId, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping) {
uint32_t row = rowGroupIndices[stateToRowGroupMapping[currentStateId]];
- // TODO: this can be precomputed.
+ // TODO: precompute this?
std::vector<ValueType> probabilities(transitionMatrix[row].size());
std::transform(transitionMatrix[row].begin(), transitionMatrix[row].end(), probabilities.begin(), [] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) { return entry.getValue(); } );
// Now sample according to the probabilities.
std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end());
- StateType offset = distribution(generator);
+ StateType offset = distribution(randomGenerator);
STORM_LOG_TRACE("Sampled " << offset << " from " << probabilities.size() << " elements.");
return transitionMatrix[row][offset].getColumn();
}
template<typename ValueType>
- std::unique_ptr<CheckResult> SparseMdpLearningModelChecker<ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
- storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
- storm::logic::Formula const& subformula = eventuallyFormula.getSubformula();
- STORM_LOG_THROW(subformula.isAtomicExpressionFormula() || subformula.isAtomicLabelFormula(), storm::exceptions::NotSupportedException, "Learning engine can only deal with formulas of the form 'F \"label\"' or 'F expression'.");
- storm::expressions::Expression targetStateExpression;
+ storm::expressions::Expression SparseMdpLearningModelChecker<ValueType>::getTargetStateExpression(storm::logic::Formula const& subformula) {
+ storm::expressions::Expression result;
if (subformula.isAtomicExpressionFormula()) {
- targetStateExpression = subformula.asAtomicExpressionFormula().getExpression();
+ result = subformula.asAtomicExpressionFormula().getExpression();
} else {
- targetStateExpression = program.getLabelExpression(subformula.asAtomicLabelFormula().getLabel());
+ result = program.getLabelExpression(subformula.asAtomicLabelFormula().getLabel());
}
+ return result;
+ }
+
+ template<typename ValueType>
+ void SparseMdpLearningModelChecker<ValueType>::detectEndComponents(std::vector<std::pair<StateType, uint32_t>> const& stateActionStack, boost::container::flat_set<StateType> const& targetStates, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& lowerBoundsPerAction, std::vector<ValueType>& upperBoundsPerAction, std::vector<ValueType>& lowerBoundsPerState, std::vector<ValueType>& upperBoundsPerState, std::unordered_map<StateType, storm::generator::CompressedState>& unexploredStates, StateType const& unexploredMarker) const {
- // A container for the encountered states.
- storm::storage::sparse::StateStorage<StateType> stateStorage(variableInformation.getTotalBitOffset(true));
+ // Outline:
+ // 1. construct a sparse transition matrix of the relevant part of the state space.
+ // 2. use this matrix to compute an MEC decomposition.
+ // 3. if non-empty analyze the decomposition for accepting/rejecting MECs.
+ // 4. modify matrix to account for the findings of 3.
- // A generator used to explore the model.
- storm::generator::PrismNextStateGenerator<ValueType, StateType> generator(program, variableInformation, false);
+ // Start with 1.
+ storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0);
+ std::vector<StateType> relevantStates;
+ for (StateType state = 0; state < stateToRowGroupMapping.size(); ++state) {
+ if (stateToRowGroupMapping[state] != unexploredMarker) {
+ relevantStates.push_back(state);
+ }
+ }
+ StateType unexploredState = relevantStates.size();
- // A container that stores the transitions found so far.
- std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> matrix;
+ std::unordered_map<StateType, StateType> relevantStateToNewRowGroupMapping;
+ for (StateType index = 0; index < relevantStates.size(); ++index) {
+ relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index);
+ }
- // A vector storing where the row group of each state starts.
- std::vector<StateType> rowGroupIndices;
- rowGroupIndices.push_back(0);
+ StateType currentRow = 0;
+ for (auto const& state : relevantStates) {
+ builder.newRowGroup(currentRow);
+ StateType rowGroup = stateToRowGroupMapping[state];
+ for (auto row = rowGroupIndices[rowGroup]; row < rowGroupIndices[rowGroup + 1]; ++row) {
+ ValueType unexpandedProbability = storm::utility::zero<ValueType>();
+ for (auto const& entry : transitionMatrix[row]) {
+ auto it = relevantStateToNewRowGroupMapping.find(entry.getColumn());
+ 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());
+ } else {
+ // If the entry is an unexpanded state, we gather the probability to later redirect it to an unexpanded sink.
+ unexpandedProbability += entry.getValue();
+ }
+ }
+ builder.addNextValue(currentRow, unexploredState, unexpandedProbability);
+ ++currentRow;
+ }
+ }
+ builder.newRowGroup(currentRow);
- // A vector storing the mapping from state ids to row groups.
- std::vector<StateType> stateToRowGroupMapping;
- StateType unexploredMarker = std::numeric_limits<StateType>::max();
- // Vectors to store the lower/upper bounds for each action (in each state).
- std::vector<ValueType> lowerBoundsPerAction;
- std::vector<ValueType> upperBoundsPerAction;
- std::vector<ValueType> lowerBoundsPerState;
- std::vector<ValueType> upperBoundsPerState;
+ // Go on to step 2.
+ storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition;
- // A mapping of unexplored IDs to their actual compressed states.
- std::unordered_map<StateType, storm::generator::CompressedState> unexploredStates;
+ // 3. Analyze the MEC decomposition.
- // Create a callback for the next-state generator to enable it to request the index of states.
- std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback = [&stateStorage, &stateToRowGroupMapping, &unexploredStates, &unexploredMarker] (storm::generator::CompressedState const& state) -> StateType {
- StateType newIndex = stateStorage.numberOfStates;
-
- // Check, if the state was already registered.
- std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
-
- if (actualIndexBucketPair.first == newIndex) {
- ++stateStorage.numberOfStates;
- stateToRowGroupMapping.push_back(unexploredMarker);
- unexploredStates[newIndex] = state;
- }
-
- return actualIndexBucketPair.first;
- };
+ // 4. Finally modify the system
+ }
+
+ template<typename ValueType>
+ std::tuple<typename SparseMdpLearningModelChecker<ValueType>::StateType, ValueType, ValueType> SparseMdpLearningModelChecker<ValueType>::performLearningProcedure(storm::expressions::Expression const& targetStateExpression, storm::storage::sparse::StateStorage<StateType>& stateStorage, storm::generator::PrismNextStateGenerator<ValueType, StateType>& generator, std::function<StateType (storm::generator::CompressedState const&)> const& stateToIdCallback, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>>& matrix, std::vector<StateType>& rowGroupIndices, std::vector<StateType>& stateToRowGroupMapping, std::unordered_map<StateType, storm::generator::CompressedState>& unexploredStates, StateType const& unexploredMarker) {
+ // Generate the initial state so we know where to start the simulation.
stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
STORM_LOG_THROW(stateStorage.initialStateIndices.size() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the learning engine.");
+ StateType initialStateIndex = stateStorage.initialStateIndices.front();
+
+ // A set storing all target states.
+ boost::container::flat_set<StateType> targetStates;
+
+ // Vectors to store the lower/upper bounds for each action (in each state).
+ std::vector<ValueType> lowerBoundsPerAction;
+ std::vector<ValueType> upperBoundsPerAction;
+ std::vector<ValueType> lowerBoundsPerState;
+ std::vector<ValueType> upperBoundsPerState;
// Now perform the actual sampling.
std::vector<std::pair<StateType, uint32_t>> stateActionStack;
- uint_fast64_t iteration = 0;
+ std::size_t iterations = 0;
+ std::size_t maxPathLength = 0;
+ std::size_t pathLengthUntilEndComponentDetection = 27;
bool convergenceCriterionMet = false;
while (!convergenceCriterionMet) {
// Start the search from the initial state.
- stateActionStack.push_back(std::make_pair(stateStorage.initialStateIndices.front(), 0));
-
+ stateActionStack.push_back(std::make_pair(initialStateIndex, 0));
+
+ bool foundTerminalState = false;
bool foundTargetState = false;
- while (!foundTargetState) {
+ while (!foundTerminalState) {
StateType const& currentStateId = stateActionStack.back().first;
STORM_LOG_TRACE("State on top of stack is: " << currentStateId << ".");
// If the state is not yet expanded, we need to retrieve its behaviors.
auto unexploredIt = unexploredStates.find(currentStateId);
if (unexploredIt != unexploredStates.end()) {
- STORM_LOG_TRACE("State was not yet expanded.");
+ STORM_LOG_TRACE("State was not yet explored.");
// Map the unexplored state to a row group.
stateToRowGroupMapping[currentStateId] = rowGroupIndices.size() - 1;
@@ -235,60 +265,32 @@ namespace storm {
generator.load(currentState);
if (generator.satisfies(targetStateExpression)) {
STORM_LOG_TRACE("State does not need to be expanded, because it is a target state.");
-
- // If it's in fact a goal state, we need to go backwards in the stack and update the probabilities.
+ targetStates.insert(currentStateId);
foundTargetState = true;
- lowerBoundsPerState.back() = storm::utility::one<ValueType>();
-
- // Set the lower/upper bounds for the only (dummy) action.
- lowerBoundsPerAction.push_back(storm::utility::one<ValueType>());
- upperBoundsPerAction.push_back(storm::utility::one<ValueType>());
-
- // Increase the size of the matrix, but leave the row empty.
- matrix.resize(matrix.size() + 1);
-
- STORM_LOG_TRACE("Updating probabilities along states in stack.");
- updateProbabilitiesUsingStack(stateActionStack, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBoundsPerAction, upperBoundsPerAction, lowerBoundsPerState, upperBoundsPerState, unexploredMarker);
+ foundTerminalState = true;
} else {
- STORM_LOG_TRACE("Expanding state.");
+ STORM_LOG_TRACE("Exploring state.");
// If it needs to be expanded, we use the generator to retrieve the behavior of the new state.
storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(stateToIdCallback);
STORM_LOG_TRACE("State has " << behavior.getNumberOfChoices() << " choices.");
// Clumsily check whether we have found a state that forms a trivial BMEC.
- bool isNonacceptingTerminalState = false;
if (behavior.getNumberOfChoices() == 0) {
- isNonacceptingTerminalState = true;
+ foundTerminalState = true;
} else if (behavior.getNumberOfChoices() == 1) {
auto const& onlyChoice = *behavior.begin();
if (onlyChoice.size() == 1) {
auto const& onlyEntry = *onlyChoice.begin();
if (onlyEntry.first == currentStateId) {
- isNonacceptingTerminalState = true;
+ foundTerminalState = true;
}
}
}
- if (isNonacceptingTerminalState) {
- STORM_LOG_TRACE("State does not need to be expanded, because it forms a trivial BMEC.");
-
- foundTargetState = true;
- upperBoundsPerState.back() = storm::utility::zero<ValueType>();
-
- // Set the lower/upper bounds for the only (dummy) action.
- lowerBoundsPerAction.push_back(storm::utility::zero<ValueType>());
- upperBoundsPerAction.push_back(storm::utility::zero<ValueType>());
-
- // Increase the size of the matrix, but leave the row empty.
- matrix.resize(matrix.size() + 1);
-
- STORM_LOG_TRACE("Updating probabilities along states in stack.");
- updateProbabilitiesUsingStack(stateActionStack, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBoundsPerAction, upperBoundsPerAction, lowerBoundsPerState, upperBoundsPerState, unexploredMarker);
- }
- // If the state was neither a trivial (non-accepting) BMEC nor a target state, we need to store
- // its behavior.
- if (!foundTargetState) {
+ // If the state was neither a trivial (non-accepting) terminal state nor a target state, we
+ // need to store its behavior.
+ if (!foundTerminalState) {
// Next, we insert the behavior into our matrix structure.
StateType startRow = matrix.size();
matrix.resize(startRow + behavior.getNumberOfChoices());
@@ -297,10 +299,10 @@ namespace storm {
for (auto const& entry : choice) {
matrix[startRow + currentAction].emplace_back(entry.first, entry.second);
}
-
+
lowerBoundsPerAction.push_back(storm::utility::zero<ValueType>());
upperBoundsPerAction.push_back(storm::utility::one<ValueType>());
-
+
// Update the bounds for the explored states to initially let them have the correct value.
updateProbabilities(currentStateId, currentAction, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBoundsPerAction, upperBoundsPerAction, lowerBoundsPerState, upperBoundsPerState, unexploredMarker);
@@ -309,6 +311,26 @@ namespace storm {
}
}
+ if (foundTerminalState) {
+ STORM_LOG_TRACE("State does not need to be explored, because it is " << (foundTargetState ? "a target state" : "a rejecting terminal state") << ".");
+
+ if (foundTargetState) {
+ lowerBoundsPerState.back() = storm::utility::one<ValueType>();
+ lowerBoundsPerAction.push_back(storm::utility::one<ValueType>());
+ upperBoundsPerAction.push_back(storm::utility::one<ValueType>());
+ } else {
+ upperBoundsPerState.back() = storm::utility::zero<ValueType>();
+ lowerBoundsPerAction.push_back(storm::utility::zero<ValueType>());
+ upperBoundsPerAction.push_back(storm::utility::zero<ValueType>());
+ }
+
+ // Increase the size of the matrix, but leave the row empty.
+ matrix.resize(matrix.size() + 1);
+
+ STORM_LOG_TRACE("Updating probabilities along states in stack.");
+ updateProbabilitiesUsingStack(stateActionStack, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBoundsPerAction, upperBoundsPerAction, lowerBoundsPerState, upperBoundsPerState, unexploredMarker);
+ }
+
// Now that we have explored the state, we can dispose of it.
unexploredStates.erase(unexploredIt);
@@ -318,14 +340,14 @@ namespace storm {
// If the state was explored before, but determined to be a terminal state of the exploration,
// we need to determine this now.
if (matrix[rowGroupIndices[stateToRowGroupMapping[currentStateId]]].empty()) {
- foundTargetState = true;
+ foundTerminalState = true;
// Update the bounds along the path to the terminal state.
updateProbabilitiesUsingStack(stateActionStack, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBoundsPerAction, upperBoundsPerAction, lowerBoundsPerState, upperBoundsPerState, unexploredMarker);
}
}
- if (!foundTargetState) {
+ if (!foundTerminalState) {
// At this point, we can be sure that the state was expanded and that we can sample according to the
// probabilities in the matrix.
uint32_t chosenAction = sampleFromMaxActions(currentStateId, matrix, rowGroupIndices, stateToRowGroupMapping, upperBoundsPerAction, unexploredMarker);
@@ -337,20 +359,83 @@ namespace storm {
// Put the successor state and a dummy action on top of the stack.
stateActionStack.emplace_back(successor, 0);
+ maxPathLength = std::max(maxPathLength, stateActionStack.size());
+
+ // If the current path length exceeds the threshold, we perform an EC detection.
+ if (stateActionStack.size() > pathLengthUntilEndComponentDetection) {
+ detectEndComponents(stateActionStack, targetStates, matrix, rowGroupIndices, stateToRowGroupMapping, lowerBoundsPerAction, upperBoundsPerAction, lowerBoundsPerState, upperBoundsPerState, unexploredStates, unexploredMarker);
+ }
}
}
STORM_LOG_DEBUG("Discovered states: " << stateStorage.numberOfStates << " (" << unexploredStates.size() << " unexplored).");
- STORM_LOG_DEBUG("Lower bound is " << lowerBoundsPerState[0] << ".");
- STORM_LOG_DEBUG("Upper bound is " << upperBoundsPerState[0] << ".");
- ValueType difference = upperBoundsPerState[0] - lowerBoundsPerState[0];
- STORM_LOG_DEBUG("Difference after iteration " << iteration << " is " << difference << ".");
+ STORM_LOG_DEBUG("Lower bound is " << lowerBoundsPerState[initialStateIndex] << ".");
+ STORM_LOG_DEBUG("Upper bound is " << upperBoundsPerState[initialStateIndex] << ".");
+ ValueType difference = upperBoundsPerState[initialStateIndex] - lowerBoundsPerState[initialStateIndex];
+ STORM_LOG_DEBUG("Difference after iteration " << iterations << " is " << difference << ".");
convergenceCriterionMet = difference < 1e-6;
- ++iteration;
+ ++iterations;
}
- return nullptr;
+ if (storm::settings::generalSettings().isShowStatisticsSet()) {
+ std::cout << std::endl << "Learning summary -------------------------" << std::endl;
+ std::cout << "Discovered states: " << stateStorage.numberOfStates << " (" << unexploredStates.size() << " unexplored)" << std::endl;
+ std::cout << "Sampling iterations: " << iterations << std::endl;
+ std::cout << "Maximal path length: " << maxPathLength << std::endl;
+ }
+
+ return std::make_tuple(initialStateIndex, lowerBoundsPerState[initialStateIndex], upperBoundsPerState[initialStateIndex]);
+ }
+
+ template<typename ValueType>
+ std::unique_ptr<CheckResult> SparseMdpLearningModelChecker<ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
+ storm::logic::EventuallyFormula const& eventuallyFormula = checkTask.getFormula();
+ storm::logic::Formula const& subformula = eventuallyFormula.getSubformula();
+ STORM_LOG_THROW(subformula.isAtomicExpressionFormula() || subformula.isAtomicLabelFormula(), storm::exceptions::NotSupportedException, "Learning engine can only deal with formulas of the form 'F \"label\"' or 'F expression'.");
+
+ // Derive the expression for the target states, so we know when to abort the learning run.
+ storm::expressions::Expression targetStateExpression = getTargetStateExpression(subformula);
+
+ // A container for the encountered states.
+ storm::storage::sparse::StateStorage<StateType> stateStorage(variableInformation.getTotalBitOffset(true));
+
+ // A generator used to explore the model.
+ storm::generator::PrismNextStateGenerator<ValueType, StateType> generator(program, variableInformation, false);
+
+ // A container that stores the transitions found so far.
+ std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> matrix;
+
+ // A vector storing where the row group of each state starts.
+ std::vector<StateType> rowGroupIndices;
+ rowGroupIndices.push_back(0);
+
+ // A vector storing the mapping from state ids to row groups.
+ std::vector<StateType> stateToRowGroupMapping;
+ StateType unexploredMarker = std::numeric_limits<StateType>::max();
+
+ // A mapping of unexplored IDs to their actual compressed states.
+ std::unordered_map<StateType, storm::generator::CompressedState> unexploredStates;
+
+ // Create a callback for the next-state generator to enable it to request the index of states.
+ std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback = [&stateStorage, &stateToRowGroupMapping, &unexploredStates, &unexploredMarker] (storm::generator::CompressedState const& state) -> StateType {
+ StateType newIndex = stateStorage.numberOfStates;
+
+ // Check, if the state was already registered.
+ std::pair<uint32_t, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
+
+ if (actualIndexBucketPair.first == newIndex) {
+ ++stateStorage.numberOfStates;
+ stateToRowGroupMapping.push_back(unexploredMarker);
+ unexploredStates[newIndex] = state;
+ }
+
+ return actualIndexBucketPair.first;
+ };
+
+ // Compute and return result.
+ std::tuple<StateType, ValueType, ValueType> boundsForInitialState = performLearningProcedure(targetStateExpression, stateStorage, generator, stateToIdCallback, matrix, rowGroupIndices, stateToRowGroupMapping, unexploredStates, unexploredMarker);
+ return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
}
template class SparseMdpLearningModelChecker<double>;
diff --git a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h
index 1d91a5d14..60dc25bc2 100644
--- a/src/modelchecker/reachability/SparseMdpLearningModelChecker.h
+++ b/src/modelchecker/reachability/SparseMdpLearningModelChecker.h
@@ -10,9 +10,22 @@
#include "src/generator/CompressedState.h"
#include "src/generator/VariableInformation.h"
+#include "src/utility/ConstantsComparator.h"
#include "src/utility/constants.h"
namespace storm {
+ namespace storage {
+ namespace sparse {
+ template<typename StateType>
+ class StateStorage;
+ }
+ }
+
+ namespace generator {
+ template<typename ValueType, typename StateType>
+ class PrismNextStateGenerator;
+ }
+
namespace modelchecker {
template<typename ValueType>
@@ -27,6 +40,8 @@ namespace storm {
virtual std::unique_ptr<CheckResult> computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) override;
private:
+ std::tuple<StateType, ValueType, ValueType> performLearningProcedure(storm::expressions::Expression const& targetStateExpression, storm::storage::sparse::StateStorage<StateType>& stateStorage, storm::generator::PrismNextStateGenerator<ValueType, StateType>& generator, std::function<StateType (storm::generator::CompressedState const&)> const& stateToIdCallback, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>>& matrix, std::vector<StateType>& rowGroupIndices, std::vector<StateType>& stateToRowGroupMapping, std::unordered_map<StateType, storm::generator::CompressedState>& unexploredStates, StateType const& unexploredMarker);
+
void updateProbabilities(StateType const& sourceStateId, uint32_t action, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& lowerBounds, std::vector<ValueType>& upperBounds, std::vector<ValueType>& lowerBoundsPerState, std::vector<ValueType>& upperBoundsPerState, StateType const& unexploredMarker) const;
void updateProbabilitiesUsingStack(std::vector<std::pair<StateType, uint32_t>>& stateActionStack, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& lowerBounds, std::vector<ValueType>& upperBounds, std::vector<ValueType>& lowerBoundsPerState, std::vector<ValueType>& upperBoundsPerState, StateType const& unexploredMarker) const;
@@ -34,7 +49,11 @@ namespace storm {
uint32_t sampleFromMaxActions(StateType currentStateId, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& upperBounds, StateType const& unexploredMarker);
StateType sampleSuccessorFromAction(StateType currentStateId, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping);
-
+
+ void detectEndComponents(std::vector<std::pair<StateType, uint32_t>> const& stateActionStack, boost::container::flat_set<StateType> const& targetStates, std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> const& transitionMatrix, std::vector<StateType> const& rowGroupIndices, std::vector<StateType> const& stateToRowGroupMapping, std::vector<ValueType>& lowerBoundsPerAction, std::vector<ValueType>& upperBoundsPerAction, std::vector<ValueType>& lowerBoundsPerState, std::vector<ValueType>& upperBoundsPerState, std::unordered_map<StateType, storm::generator::CompressedState>& unexploredStates, StateType const& unexploredMarker) const;
+
+ storm::expressions::Expression getTargetStateExpression(storm::logic::Formula const& subformula);
+
// The program that defines the model to check.
storm::prism::Program program;
@@ -42,7 +61,10 @@ namespace storm {
storm::generator::VariableInformation variableInformation;
// The random number generator.
- std::default_random_engine generator;
+ std::default_random_engine randomGenerator;
+
+ // A comparator used to determine whether values are equal.
+ storm::utility::ConstantsComparator<ValueType> comparator;
};
}
}
diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp
index 18f14428a..2bc82362f 100644
--- a/src/parser/DeterministicModelParser.cpp
+++ b/src/parser/DeterministicModelParser.cpp
@@ -23,7 +23,7 @@ namespace storm {
uint_fast64_t stateCount = transitions.getColumnCount();
// Parse the state labeling.
- storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
+ storm::models::sparse::StateLabeling labeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename));
// Construct the result.
DeterministicModelParser<ValueType, RewardValueType>::Result result(std::move(transitions), std::move(labeling));
diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
index b2d539c3a..b703937fd 100644
--- a/src/parser/NondeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -25,7 +25,7 @@ namespace storm {
uint_fast64_t stateCount = transitions.getColumnCount();
// Parse the state labeling.
- storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
+ storm::models::sparse::StateLabeling labeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename));
// Only parse state rewards if a file is given.
boost::optional<std::vector<RewardValueType>> stateRewards;
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index da441214e..907f97081 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -106,14 +106,11 @@ namespace storm {
template<typename ValueType>
void SparseMatrixBuilder<ValueType>::addNextValue(index_type row, index_type column, ValueType const& value) {
// Check that we did not move backwards wrt. the row.
- if (row < lastRow) {
- throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.";
- }
+ STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException, "Adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.");
- // Check that we did not move backwards wrt. to column.
- if (row == lastRow && column < lastColumn) {
- throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row.";
- }
+ // If the element is in the same row, but was not inserted in the correct order, we need to fix the row after
+ // the insertion.
+ bool fixCurrentRow = row == lastRow && column < lastColumn;
// If we switched to another row, we have to adjust the missing entries in the row indices vector.
if (row != lastRow) {
@@ -132,6 +129,27 @@ namespace storm {
highestColumn = std::max(highestColumn, column);
++currentEntryCount;
+ // If we need to fix the row, do so now.
+ if (fixCurrentRow) {
+ // First, we sort according to columns.
+ std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
+ return a.getColumn() < b.getColumn();
+ });
+
+ // Then, we eliminate possible duplicate entries.
+ auto it = std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
+ return a.getColumn() == b.getColumn();
+ });
+
+ // Finally, remove the superfluous elements.
+ std::size_t elementsToRemove = std::distance(it, columnsAndValues.end());
+ if (elementsToRemove > 0) {
+ STORM_LOG_WARN("Unordered insertion into matrix builder caused duplicate entries.");
+ currentEntryCount -= elementsToRemove;
+ columnsAndValues.resize(columnsAndValues.size() - elementsToRemove);
+ }
+ }
+
// In case we did not expect this value, we throw an exception.
if (forceInitialDimensions) {
STORM_LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << ".");
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index c5c7133c6..f1debced1 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -229,7 +229,7 @@ namespace storm {
* @return True if replacement took place, False if nothing changed.
*/
bool replaceColumns(std::vector<index_type> const& replacements, index_type offset);
-
+
private:
// A flag indicating whether a row count was set upon construction.
bool initialRowCountSet;
diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp
index f3a89b2c5..c0cea43ac 100644
--- a/src/storage/expressions/ToExprtkStringVisitor.cpp
+++ b/src/storage/expressions/ToExprtkStringVisitor.cpp
@@ -10,7 +10,7 @@ namespace storm {
stream.str("");
stream.clear();
expression->accept(*this);
- return std::move(stream.str());
+ return stream.str();
}
boost::any ToExprtkStringVisitor::visit(IfThenElseExpression const& expression) {