#include "storm/modelchecker/exploration/SparseExplorationModelChecker.h"
#include "storm/modelchecker/exploration/ExplorationInformation.h"
#include "storm/modelchecker/exploration/StateGeneration.h"
#include "storm/modelchecker/exploration/Bounds.h"
#include "storm/modelchecker/exploration/Statistics.h"
#include "storm/generator/CompressedState.h"
#include "storm/storage/SparseMatrix.h"
#include "storm/storage/MaximalEndComponentDecomposition.h"
#include "storm/storage/prism/Program.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/settings/modules/ExplorationSettings.h"
#include "storm/utility/macros.h"
#include "storm/utility/constants.h"
#include "storm/utility/graph.h"
#include "storm/utility/prism.h"
#include "storm/exceptions/InvalidOperationException.h"
#include "storm/exceptions/InvalidPropertyException.h"
#include "storm/exceptions/NotSupportedException.h"
namespace storm {
namespace modelchecker {
template<typename ModelType, typename StateType>
SparseExplorationModelChecker<ModelType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program) : program(program.substituteConstantsFormulas()), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::getModule<storm::settings::modules::ExplorationSettings>().getPrecision()) {
// Intentionally left empty.
}
template<typename ModelType, typename StateType>
bool SparseExplorationModelChecker<ModelType, StateType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
storm::logic::Formula const& formula = checkTask.getFormula();
storm::logic::FragmentSpecification fragment = storm::logic::reachability();
return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
}
template<typename ModelType, typename StateType>
std::unique_ptr<CheckResult> SparseExplorationModelChecker<ModelType, StateType>::computeUntilProbabilities(Environment const& env, CheckTask<storm::logic::UntilFormula, ValueType> const& checkTask) {
storm::logic::UntilFormula const& untilFormula = checkTask.getFormula();
storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula();
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.");
ExplorationInformation<StateType, ValueType> explorationInformation(checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize);
// The first row group starts at action 0.
explorationInformation.newRowGroup(0);
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = program.getLabelToExpressionMapping();
StateGeneration<StateType, ValueType> stateGeneration(program, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping));
// Compute and return result.
std::tuple<StateType, ValueType, ValueType> boundsForInitialState = performExploration(stateGeneration, explorationInformation);
return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
}
template<typename ModelType, typename StateType>
std::tuple<StateType, typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, typename ModelType::ValueType>& explorationInformation) const {
// Generate the initial state so we know where to start the simulation.
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<StateType, ValueType> bounds;
// Create a stack that is used to track the path we sampled.
StateActionStack stack;
// Now perform the actual sampling.
Statistics<StateType, ValueType> stats;
bool convergenceCriterionMet = false;
while (!convergenceCriterionMet) {
bool result = samplePathFromInitialState(stateGeneration, explorationInformation, stack, bounds, stats);
stats.sampledPath();
stats.updateMaxPathLength(stack.size());
// If a terminal state was found, we update the probabilities along the path contained in the stack.
if (result) {
// Update the bounds along the path to the terminal state.
STORM_LOG_TRACE("Found terminal state, updating probabilities along path.");
updateProbabilityBoundsAlongSampledPath(stack, explorationInformation, bounds);
} else {
// If not terminal state was found, the search aborted, possibly because of an EC-detection. In this
// case, we cannot update the probabilities.
STORM_LOG_TRACE("Did not find terminal state.");
}
STORM_LOG_DEBUG("Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << stats.numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored).");
STORM_LOG_DEBUG("Value of initial state is in [" << bounds.getLowerBoundForState(initialStateIndex, explorationInformation) << ", " << bounds.getUpperBoundForState(initialStateIndex, explorationInformation) << "].");
ValueType difference = bounds.getDifferenceOfStateBounds(initialStateIndex, explorationInformation);
STORM_LOG_DEBUG("Difference after iteration " << stats.pathsSampled << " is " << difference << ".");
convergenceCriterionMet = comparator.isZero(difference);
// If the number of sampled paths exceeds a certain threshold, do a precomputation.
if (!convergenceCriterionMet && explorationInformation.performPrecomputationExcessiveSampledPaths(stats.pathsSampledSinceLastPrecomputation)) {
performPrecomputation(stack, explorationInformation, bounds, stats);
}
}
// Show statistics if required.
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
stats.printToStream(std::cout, explorationInformation);
}
return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation));
}
template<typename ModelType, typename StateType>
bool SparseExplorationModelChecker<ModelType, StateType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
// Start the search from the initial state.
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;
while (!foundTerminalState) {
StateType const& currentStateId = stack.back().first;
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.findUnexploredState(currentStateId);
if (unexploredIt != explorationInformation.unexploredStatesEnd()) {
STORM_LOG_TRACE("State was not yet explored.");
// Explore the previously unexplored state.
storm::generator::CompressedState const& compressedState = unexploredIt->second;
foundTerminalState = exploreState(stateGeneration, currentStateId, compressedState, explorationInformation, bounds, stats);
if (foundTerminalState) {
STORM_LOG_TRACE("Aborting sampling of path, because a terminal state was reached.");
}
explorationInformation.removeUnexploredState(unexploredIt);
} else {
// If the state was already explored, we check whether it is a terminal state or not.
if (explorationInformation.isTerminal(currentStateId)) {
STORM_LOG_TRACE("Found already explored terminal state: " << currentStateId << ".");
foundTerminalState = true;
}
}
// Notify the stats about the performed exploration step.
stats.explorationStep();
// If the state was not a terminal state, we continue the path search and sample the next state.
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 = sampleActionOfState(currentStateId, explorationInformation, bounds);
stack.back().second = chosenAction;
STORM_LOG_TRACE("Sampled action " << chosenAction << " in state " << currentStateId << ".");
StateType successor = sampleSuccessorFromAction(chosenAction, explorationInformation, bounds);
STORM_LOG_TRACE("Sampled successor " << successor << " according to action " << chosenAction << " of state " << currentStateId << ".");
// Put the successor state and a dummy action on top of the stack.
stack.emplace_back(successor, 0);
// If the number of exploration steps exceeds a certain threshold, do a precomputation.
if (explorationInformation.performPrecomputationExcessiveExplorationSteps(stats.explorationStepsSinceLastPrecomputation)) {
performPrecomputation(stack, explorationInformation, bounds, stats);
STORM_LOG_TRACE("Aborting the search after precomputation.");
stack.clear();
break;
}
}
}
return foundTerminalState;
}
template<typename ModelType, typename StateType>
bool SparseExplorationModelChecker<ModelType, StateType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
bool isTerminalState = false;
bool isTargetState = false;
++stats.numberOfExploredStates;
// Finally, map the unexplored state to the row group.
explorationInformation.assignStateToNextRowGroup(currentStateId);
STORM_LOG_TRACE("Assigning row group " << explorationInformation.getRowGroup(currentStateId) << " to state " << currentStateId << ".");
// Initialize the bounds, because some of the following computations depend on the values to be available for
// all states that have been assigned to a row-group.
bounds.initializeBoundsForNextState();
// Before generating the behavior of the state, we need to determine whether it's a target state that
// does not need to be expanded.
stateGeneration.load(currentState);
if (stateGeneration.isTargetState()) {
++stats.numberOfTargetStates;
isTargetState = true;
isTerminalState = true;
} else if (stateGeneration.isConditionState()) {
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 = stateGeneration.expand();
STORM_LOG_TRACE("State has " << behavior.getNumberOfChoices() << " choices.");
// Clumsily check whether we have found a state that forms a trivial BMEC.
bool otherSuccessor = false;
for (auto const& choice : behavior) {
for (auto const& entry : choice) {
if (entry.first != currentStateId) {
otherSuccessor = true;
break;
}
}
}
isTerminalState = !otherSuccessor;
// If the state was neither a trivial (non-accepting) terminal state nor a target state, we
// need to store its behavior.
if (!isTerminalState) {
// Next, we insert the behavior into our matrix structure.
StateType startAction = explorationInformation.getActionCount();
explorationInformation.addActionsToMatrix(behavior.getNumberOfChoices());
ActionType localAction = 0;
// Retrieve the lowest state bounds (wrt. to the current optimization direction).
std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
for (auto const& choice : behavior) {
for (auto const& entry : choice) {
explorationInformation.getRowOfMatrix(startAction + localAction).emplace_back(entry.first, entry.second);
STORM_LOG_TRACE("Found transition " << currentStateId << "-[" << (startAction + localAction) << ", " << entry.second << "]-> " << entry.first << ".");
}
std::pair<ValueType, ValueType> actionBounds = computeBoundsOfAction(startAction + localAction, explorationInformation, bounds);
bounds.initializeBoundsForNextAction(actionBounds);
stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds);
STORM_LOG_TRACE("Initializing bounds of action " << (startAction + localAction) << " to " << bounds.getLowerBoundForAction(startAction + localAction) << " and " << bounds.getUpperBoundForAction(startAction + localAction) << ".");
++localAction;
}
// Terminate the row group.
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) << ".");
}
} else {
// In this case, the state is neither a target state nor a condition state and therefore a rejecting
// terminal state.
isTerminalState = true;
}
if (isTerminalState) {
STORM_LOG_TRACE("State does not need to be explored, because it is " << (isTargetState ? "a target state" : "a rejecting terminal state") << ".");
explorationInformation.addTerminalState(currentStateId);
if (isTargetState) {
bounds.setBoundsForState(currentStateId, explorationInformation, std::make_pair(storm::utility::one<ValueType>(), storm::utility::one<ValueType>()));
bounds.initializeBoundsForNextAction(std::make_pair(storm::utility::one<ValueType>(), storm::utility::one<ValueType>()));
} else {
bounds.setBoundsForState(currentStateId, explorationInformation, std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()));
bounds.initializeBoundsForNextAction(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()));
}
// Increase the size of the matrix, but leave the row empty.
explorationInformation.addActionsToMatrix(1);
// Terminate the row group.
explorationInformation.newRowGroup();
}
return isTerminalState;
}
template<typename ModelType, typename StateType>
typename SparseExplorationModelChecker<ModelType, StateType>::ActionType SparseExplorationModelChecker<ModelType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
// Determine the values of all available actions.
std::vector<std::pair<ActionType, ValueType>> actionValues;
StateType rowGroup = explorationInformation.getRowGroup(currentStateId);
// Check for cases in which we do not need to perform more work.
if (explorationInformation.onlyOneActionAvailable(rowGroup)) {
return explorationInformation.getStartRowOfGroup(rowGroup);
}
// If there are more choices to consider, start by gathering the values of relevant actions.
STORM_LOG_TRACE("Sampling from actions leaving the state.");
for (uint32_t row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) {
actionValues.push_back(std::make_pair(row, bounds.getBoundForAction(explorationInformation.getOptimizationDirection(), row)));
}
STORM_LOG_ASSERT(!actionValues.empty(), "Values for actions must not be empty.");
// Sort the actions wrt. to the optimization direction.
if (explorationInformation.maximize()) {
std::sort(actionValues.begin(), actionValues.end(), [] (std::pair<ActionType, ValueType> const& a, std::pair<ActionType, ValueType> const& b) { return a.second > b.second; } );
} else {
std::sort(actionValues.begin(), actionValues.end(), [] (std::pair<ActionType, ValueType> const& a, std::pair<ActionType, ValueType> const& b) { return a.second < b.second; } );
}
// Determine the first elements of the sorted range that agree on their value.
auto end = ++actionValues.begin();
while (end != actionValues.end() && comparator.isEqual(actionValues.begin()->second, end->second)) {
++end;
}
// Now sample from all maximizing actions.
std::uniform_int_distribution<ActionType> distribution(0, std::distance(actionValues.begin(), end) - 1);
return actionValues[distribution(randomGenerator)].first;
}
template<typename ModelType, typename StateType>
StateType SparseExplorationModelChecker<ModelType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
if (row.size() == 1) {
return row.front().getColumn();
}
// Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen.
if (explorationInformation.useDifferenceProbabilitySumHeuristic() || explorationInformation.useProbabilityHeuristic()) {
std::vector<ValueType> probabilities(row.size());
if (explorationInformation.useDifferenceProbabilitySumHeuristic()) {
std::transform(row.begin(), row.end(), probabilities.begin(),
[&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) {
return entry.getValue() + bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation);
});
} else if (explorationInformation.useProbabilityHeuristic()) {
std::transform(row.begin(), 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());
return row[distribution(randomGenerator)].getColumn();
} else {
STORM_LOG_ASSERT(explorationInformation.useUniformHeuristic(), "Illegal next-state heuristic.");
std::uniform_int_distribution<ActionType> distribution(0, row.size() - 1);
return row[distribution(randomGenerator)].getColumn();
}
}
template<typename ModelType, typename StateType>
bool SparseExplorationModelChecker<ModelType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
++stats.numberOfPrecomputations;
// Outline:
// 1. construct a sparse transition matrix of the relevant part of the state space.
// 2. use this matrix to compute states with probability 0/1 and an MEC decomposition (in the max case).
// 3. use MEC decomposition to collapse MECs.
STORM_LOG_TRACE("Starting " << (explorationInformation.useLocalPrecomputation() ? "local" : "global") << " precomputation.");
// Construct the matrix that represents the fragment of the system contained in the currently sampled path.
storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0);
// Determine the set of states that was expanded.
std::vector<StateType> relevantStates;
if (explorationInformation.useLocalPrecomputation()) {
for (auto const& stateActionPair : stack) {
if (explorationInformation.maximize() || !storm::utility::isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
relevantStates.push_back(stateActionPair.first);
}
}
std::sort(relevantStates.begin(), relevantStates.end());
auto newEnd = std::unique(relevantStates.begin(), relevantStates.end());
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.
if (!explorationInformation.isUnexplored(state)) {
relevantStates.push_back(state);
}
}
}
StateType sink = relevantStates.size();
// Create a mapping for faster look-up during the translation of flexible matrix to the real sparse matrix.
// While doing so, record all target states.
std::unordered_map<StateType, StateType> relevantStateToNewRowGroupMapping;
storm::storage::BitVector targetStates(sink + 1);
for (StateType index = 0; index < relevantStates.size(); ++index) {
relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index);
if (storm::utility::isOne(bounds.getLowerBoundForState(relevantStates[index], explorationInformation))) {
targetStates.set(index);
}
}
// Do the actual translation.
StateType currentRow = 0;
for (auto const& state : relevantStates) {
builder.newRowGroup(currentRow);
StateType rowGroup = explorationInformation.getRowGroup(state);
for (auto row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) {
ValueType unexpandedProbability = storm::utility::zero<ValueType>();
for (auto const& entry : explorationInformation.getRowOfMatrix(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();
}
}
if (unexpandedProbability != storm::utility::zero<ValueType>()) {
builder.addNextValue(currentRow, sink, unexpandedProbability);
}
++currentRow;
}
}
// Then, make the unexpanded state absorbing.
builder.newRowGroup(currentRow);
builder.addNextValue(currentRow, sink, storm::utility::one<ValueType>());
storm::storage::SparseMatrix<ValueType> relevantStatesMatrix = builder.build();
storm::storage::SparseMatrix<ValueType> transposedMatrix = relevantStatesMatrix.transpose(true);
STORM_LOG_TRACE("Successfully built matrix for precomputation.");
storm::storage::BitVector allStates(sink + 1, true);
storm::storage::BitVector statesWithProbability0;
storm::storage::BitVector statesWithProbability1;
if (explorationInformation.maximize()) {
// If we are computing maximal probabilities, we first perform a detection of states that have
// probability 01 and then additionally perform an MEC decomposition. The reason for this somewhat
// duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need
// it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states
// (not contained in MECs) also have probability 0/1.
targetStates.set(sink, true);
statesWithProbability0 = storm::utility::graph::performProb0A(transposedMatrix, allStates, targetStates);
targetStates.set(sink, false);
statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true));
++stats.ecDetections;
STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s).");
// If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'.
STORM_LOG_ASSERT(mecDecomposition.size() > 0, "Expected at least one MEC (the trivial sink MEC).");
if (mecDecomposition.size() == 1) {
++stats.failedEcDetections;
} else {
stats.totalNumberOfEcDetected += mecDecomposition.size() - 1;
// 3. Analyze the MEC decomposition.
for (auto const& mec : mecDecomposition) {
// Ignore the (expected) MEC of the sink state.
if (mec.containsState(sink)) {
continue;
}
collapseMec(mec, relevantStates, relevantStatesMatrix, explorationInformation, bounds);
}
}
} else {
// If we are computing minimal probabilities, we do not need to perform an EC-detection. We rather
// compute all states (of the considered fragment) that have probability 0/1. For states with
// probability 0, we have to mark the sink as being a target. For states with probability 1, however,
// we must treat the sink as being rejecting.
targetStates.set(sink, true);
statesWithProbability0 = storm::utility::graph::performProb0E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
targetStates.set(sink, false);
statesWithProbability1 = storm::utility::graph::performProb1A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
}
// Set the bounds of the identified states.
STORM_LOG_ASSERT((statesWithProbability0 & statesWithProbability1).empty(), "States with probability 0 and 1 overlap.");
for (auto state : statesWithProbability0) {
// Skip the sink state as it is not contained in the original system.
if (state == sink) {
continue;
}
StateType originalState = relevantStates[state];
bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
explorationInformation.addTerminalState(originalState);
}
for (auto state : statesWithProbability1) {
// Skip the sink state as it is not contained in the original system.
if (state == sink) {
continue;
}
StateType originalState = relevantStates[state];
bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one<ValueType>());
explorationInformation.addTerminalState(originalState);
}
return true;
}
template<typename ModelType, typename StateType>
void SparseExplorationModelChecker<ModelType, StateType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
bool containsTargetState = false;
// Now we record all actions leaving the EC.
std::vector<ActionType> leavingActions;
for (auto const& stateAndChoices : mec) {
// Compute the state of the original model that corresponds to the current state.
StateType originalState = relevantStates[stateAndChoices.first];
StateType originalRowGroup = explorationInformation.getRowGroup(originalState);
// Check whether a target state is contained in the MEC.
if (!containsTargetState && storm::utility::isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) {
containsTargetState = true;
}
// For each state, compute the actions that leave the MEC.
auto includedChoicesIt = stateAndChoices.second.begin();
auto includedChoicesIte = stateAndChoices.second.end();
for (auto action = explorationInformation.getStartRowOfGroup(originalRowGroup); action < explorationInformation.getStartRowOfGroup(originalRowGroup + 1); ++action) {
if (includedChoicesIt != includedChoicesIte) {
STORM_LOG_TRACE("Next (local) choice contained in MEC is " << (*includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first]));
STORM_LOG_TRACE("Current (local) choice iterated is " << (action - explorationInformation.getStartRowOfGroup(originalRowGroup)));
if (action - explorationInformation.getStartRowOfGroup(originalRowGroup) != *includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first]) {
STORM_LOG_TRACE("Choice leaves the EC.");
leavingActions.push_back(action);
} else {
STORM_LOG_TRACE("Choice stays in the EC.");
++includedChoicesIt;
}
} else {
STORM_LOG_TRACE("Choice leaves the EC, because there is no more choice staying in the EC.");
leavingActions.push_back(action);
}
}
}
// Now, we need to collapse the EC only if it does not contain a target state and the leaving actions are
// non-empty, because only then have the states a (potentially) non-zero, non-one probability.
if (!containsTargetState && !leavingActions.empty()) {
// In this case, no target state is contained in the MEC, but there are actions leaving the MEC. To
// prevent the simulation getting stuck in this MEC again, we replace all states in the MEC by a new
// state whose outgoing actions are the ones leaving the MEC. We do this, by assigning all states in the
// MEC to a new row group, which will then hold all the outgoing choices.
// Remap all contained states to the new row group.
StateType nextRowGroup = explorationInformation.getNextRowGroup();
for (auto const& stateAndChoices : mec) {
explorationInformation.assignStateToRowGroup(stateAndChoices.first, nextRowGroup);
}
bounds.initializeBoundsForNextState();
// Add to the new row group all leaving actions of contained states and set the appropriate bounds for
// the actions and the new state.
std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
for (auto const& action : leavingActions) {
explorationInformation.moveActionToBackOfMatrix(action);
std::pair<ValueType, ValueType> const& actionBounds = bounds.getBoundsForAction(action);
bounds.initializeBoundsForNextAction(actionBounds);
stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds);
}
bounds.setBoundsForRowGroup(nextRowGroup, stateBounds);
// Terminate the row group of the newly introduced state.
explorationInformation.terminateCurrentRowGroup();
}
}
template<typename ModelType, typename StateType>
typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
}
return result;
}
template<typename ModelType, typename StateType>
typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType result = storm::utility::zero<ValueType>();
for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
}
return result;
}
template<typename ModelType, typename StateType>
std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
// TODO: take into account self-loops?
std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
result.first += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
result.second += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
}
return result;
}
template<typename ModelType, typename StateType>
std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
StateType group = explorationInformation.getRowGroup(currentStateId);
std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection());
for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) {
std::pair<ValueType, ValueType> actionValues = computeBoundsOfAction(action, explorationInformation, bounds);
result = combineBounds(explorationInformation.getOptimizationDirection(), result, actionValues);
}
return result;
}
template<typename ModelType, typename StateType>
void SparseExplorationModelChecker<ModelType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
stack.pop_back();
while (!stack.empty()) {
updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds);
stack.pop_back();
}
}
template<typename ModelType, typename StateType>
void SparseExplorationModelChecker<ModelType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
// Compute the new lower/upper values of the action.
std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds);
// And set them as the current value.
bounds.setBoundsForAction(action, newBoundsForAction);
// Check if we need to update the values for the states.
if (explorationInformation.maximize()) {
bounds.setLowerBoundOfStateIfGreaterThanOld(state, explorationInformation, newBoundsForAction.first);
StateType rowGroup = explorationInformation.getRowGroup(state);
if (newBoundsForAction.second < bounds.getUpperBoundForRowGroup(rowGroup)) {
if (explorationInformation.getRowGroupSize(rowGroup) > 1) {
newBoundsForAction.second = std::max(newBoundsForAction.second, computeBoundOverAllOtherActions(storm::OptimizationDirection::Maximize, state, action, explorationInformation, bounds));
}
bounds.setUpperBoundForRowGroup(rowGroup, newBoundsForAction.second);
}
} else {
bounds.setUpperBoundOfStateIfLessThanOld(state, explorationInformation, newBoundsForAction.second);
StateType rowGroup = explorationInformation.getRowGroup(state);
if (bounds.getLowerBoundForRowGroup(rowGroup) < newBoundsForAction.first) {
if (explorationInformation.getRowGroupSize(rowGroup) > 1) {
ValueType min = computeBoundOverAllOtherActions(storm::OptimizationDirection::Minimize, state, action, explorationInformation, bounds);
newBoundsForAction.first = std::min(newBoundsForAction.first, min);
}
bounds.setLowerBoundForRowGroup(rowGroup, newBoundsForAction.first);
}
}
}
template<typename ModelType, typename StateType>
typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection());
ActionType group = explorationInformation.getRowGroup(state);
for (auto currentAction = explorationInformation.getStartRowOfGroup(group); currentAction < explorationInformation.getStartRowOfGroup(group + 1); ++currentAction) {
if (currentAction == action) {
continue;
}
if (direction == storm::OptimizationDirection::Maximize) {
bound = std::max(bound, computeUpperBoundOfAction(currentAction, explorationInformation, bounds));
} else {
bound = std::min(bound, computeLowerBoundOfAction(currentAction, explorationInformation, bounds));
}
}
return bound;
}
template<typename ModelType, typename StateType>
std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const {
ValueType val = getLowestBound(direction);
return std::make_pair(val, val);
}
template<typename ModelType, typename StateType>
typename ModelType::ValueType SparseExplorationModelChecker<ModelType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const {
if (direction == storm::OptimizationDirection::Maximize) {
return storm::utility::zero<ValueType>();
} else {
return storm::utility::one<ValueType>();
}
}
template<typename ModelType, typename StateType>
std::pair<typename ModelType::ValueType, typename ModelType::ValueType> SparseExplorationModelChecker<ModelType, StateType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const {
if (direction == storm::OptimizationDirection::Maximize) {
return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second));
} else {
return std::make_pair(std::min(bounds1.first, bounds2.first), std::min(bounds1.second, bounds2.second));
}
}
template class SparseExplorationModelChecker<storm::models::sparse::Dtmc<double>, uint32_t>;
template class SparseExplorationModelChecker<storm::models::sparse::Mdp<double>, uint32_t>;
}
}