From b2b692b8aeafe5914997c34fba3aae670c4d1928 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 29 Apr 2017 10:50:30 +0200 Subject: [PATCH 01/22] extended JANI next-state generator to be able to deal with custom system compositions --- .../generator/JaniNextStateGenerator.cpp | 499 ++++++++++-------- src/storm/generator/JaniNextStateGenerator.h | 45 +- src/storm/generator/VariableInformation.cpp | 50 +- src/storm/generator/VariableInformation.h | 8 +- 4 files changed, 339 insertions(+), 263 deletions(-) diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 9ff5974c3..fbcf93c0a 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -34,12 +34,9 @@ namespace storm { template JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) { - STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); - STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition"); - // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway). if (this->model.hasTransientEdgeDestinationAssignments()) { @@ -47,9 +44,12 @@ namespace storm { } STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); - // Only after checking validity of the program, we initialize the variable information. + // Create all synchronization-related information, e.g. the automata that are put in parallel. + this->createSynchronizationInformation(); + + // Now we are ready to initialize the variable information. this->checkValid(); - this->variableInformation = VariableInformation(model); + this->variableInformation = VariableInformation(model, this->parallelAutomata); // Create a proper evalator. this->evaluator = std::make_unique>(model.getManager()); @@ -92,11 +92,6 @@ namespace storm { // If there are terminal states we need to handle, we now need to translate all labels to expressions. if (this->options.hasTerminalStates()) { - std::vector> composedAutomata; - for (auto const& automaton : this->model.getAutomata()) { - composedAutomata.emplace_back(automaton); - } - for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) { if (expressionOrLabelAndBool.first.isExpression()) { this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second)); @@ -110,7 +105,7 @@ namespace storm { STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'."); - this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), composedAutomata), expressionOrLabelAndBool.second)); + this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata), expressionOrLabelAndBool.second)); } } } @@ -177,15 +172,11 @@ namespace storm { storm::utility::solver::SmtSolverFactory factory; std::unique_ptr solver = factory.create(model.getExpressionManager()); - std::vector> allAutomata; - for (auto const& automaton : model.getAutomata()) { - allAutomata.push_back(automaton); - } - std::vector rangeExpressions = model.getAllRangeExpressions(allAutomata); + std::vector rangeExpressions = model.getAllRangeExpressions(this->parallelAutomata); for (auto const& expression : rangeExpressions) { solver->add(expression); } - solver->add(model.getInitialStatesExpression(allAutomata)); + solver->add(model.getInitialStatesExpression(this->parallelAutomata)); // Proceed as long as the solver can still enumerate initial states. std::vector initialStateIndices; @@ -213,9 +204,10 @@ namespace storm { // Gather iterators to the initial locations of all the automata. std::vector::const_iterator> initialLocationsIts; std::vector::const_iterator> initialLocationsItes; - for (auto const& automaton : allAutomata) { - initialLocationsIts.push_back(automaton.get().getInitialLocationIndices().cbegin()); - initialLocationsItes.push_back(automaton.get().getInitialLocationIndices().cend()); + for (auto const& automatonRef : this->parallelAutomata) { + auto const& automaton = automatonRef.get(); + initialLocationsIts.push_back(automaton.getInitialLocationIndices().cbegin()); + initialLocationsItes.push_back(automaton.getInitialLocationIndices().cend()); } storm::utility::combinatorics::forEach(initialLocationsIts, initialLocationsItes, [this,&initialState] (uint64_t index, uint64_t value) { setLocation(initialState, this->variableInformation.locationVariables[index], value); }, [&stateToIdCallback,&initialStateIndices,&initialState] () { // Register initial state. @@ -287,7 +279,8 @@ namespace storm { // need the state rewards then. std::vector stateRewards(this->rewardVariables.size(), storm::utility::zero()); uint64_t automatonIndex = 0; - for (auto const& automaton : model.getAutomata()) { + for (auto const& automatonRef : this->parallelAutomata) { + auto const& automaton = automatonRef.get(); uint64_t currentLocationIndex = locations[automatonIndex]; storm::jani::Location const& location = automaton.getLocation(currentLocationIndex); auto valueIt = stateRewards.begin(); @@ -307,12 +300,7 @@ namespace storm { // Get all choices for the state. result.setExpanded(); - std::vector> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback); - std::vector> allLabeledChoices = getNonsilentActionChoices(locations, *this->state, stateToIdCallback); - for (auto& choice : allLabeledChoices) { - allChoices.push_back(std::move(choice)); - } - + std::vector> allChoices = getActionChoices(locations, *this->state, stateToIdCallback); std::size_t totalNumberOfChoices = allChoices.size(); // If there is not a single choice, we return immediately, because the state has no behavior (other than @@ -370,239 +358,235 @@ namespace storm { return result; } - + template - std::vector> JaniNextStateGenerator::getSilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { - std::vector> result; + Choice JaniNextStateGenerator::expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex, CompressedState const& state, StateToIdCallback stateToIdCallback) { + // Determine the exit rate if it's a Markovian edge. + boost::optional exitRate = boost::none; + if (edge.hasRate()) { + exitRate = this->evaluator->asRational(edge.getRate()); + } - // Iterate over all automata. - uint64_t automatonIndex = 0; + Choice choice(edge.getActionIndex(), static_cast(exitRate)); - for (auto const& automaton : model.getAutomata()) { - uint64_t location = locations[automatonIndex]; + // Iterate over all updates of the current command. + ValueType probabilitySum = storm::utility::zero(); + for (auto const& destination : edge.getDestinations()) { + ValueType probability = this->evaluator->asRational(destination.getProbability()); - // Iterate over all edges from the source location. - for (auto const& edge : automaton.getEdgesFromLocation(location)) { - // Skip the edge if it is labeled with a non-silent action. - if (edge.getActionIndex() != storm::jani::Model::SILENT_ACTION_INDEX) { - continue; - } + if (probability != storm::utility::zero()) { + // Obtain target state index and add it to the list of known states. If it has not yet been + // seen, we also add it to the set of states that have yet to be explored. + auto newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]); - // Skip the command, if it is not enabled. - if (!this->evaluator->asBool(edge.getGuard())) { - continue; - } + StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex])); - // Determine the exit rate if it's a Markovian edge. - boost::optional exitRate = boost::none; - if (edge.hasRate()) { - exitRate = this->evaluator->asRational(edge.getRate()); - } + // Update the choice by adding the probability/target state to it. + probability = exitRate ? exitRate.get() * probability : probability; + choice.addProbability(stateIndex, probability); - result.push_back(Choice(edge.getActionIndex(), static_cast(exitRate))); - Choice& choice = result.back(); + if (this->options.isExplorationChecksSet()) { + probabilitySum += probability; + } + } + } + + // Create the state-action reward for the newly created choice. + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } ); + + if (this->options.isExplorationChecksSet()) { + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); + } + + return choice; + } + + template + std::vector> JaniNextStateGenerator::expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> result; + + if (this->options.isExplorationChecksSet()) { + // Check whether a global variable is written multiple times in any combination. + checkGlobalVariableWritesValid(edgeCombination); + } + + std::vector iteratorList(edgeCombination.size()); + + // Initialize the list of iterators. + for (size_t i = 0; i < edgeCombination.size(); ++i) { + iteratorList[i] = edgeCombination[i].second.cbegin(); + } + + // As long as there is one feasible combination of commands, keep on expanding it. + bool done = false; + while (!done) { + boost::container::flat_map* currentTargetStates = new boost::container::flat_map(); + boost::container::flat_map* newTargetStates = new boost::container::flat_map(); + std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); + + currentTargetStates->emplace(state, storm::utility::one()); + + for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { + storm::jani::Edge const& edge = **iteratorList[i]; - // Iterate over all updates of the current command. - ValueType probabilitySum = storm::utility::zero(); for (auto const& destination : edge.getDestinations()) { - ValueType probability = this->evaluator->asRational(destination.getProbability()); - - if (probability != storm::utility::zero()) { - // Obtain target state index and add it to the list of known states. If it has not yet been - // seen, we also add it to the set of states that have yet to be explored. - StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex])); - - // Update the choice by adding the probability/target state to it. - probability = exitRate ? exitRate.get() * probability : probability; - choice.addProbability(stateIndex, probability); + for (auto const& stateProbabilityPair : *currentTargetStates) { + // Compute the new state under the current update and add it to the set of new target states. + CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, this->variableInformation.locationVariables[edgeCombination[i].first]); - if (this->options.isExplorationChecksSet()) { - probabilitySum += probability; + // If the new state was already found as a successor state, update the probability + // and otherwise insert it. + ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); + if (edge.hasRate()) { + probability *= this->evaluator->asRational(edge.getRate()); + } + if (probability != storm::utility::zero()) { + auto targetStateIt = newTargetStates->find(newTargetState); + if (targetStateIt != newTargetStates->end()) { + targetStateIt->second += probability; + } else { + newTargetStates->emplace(newTargetState, probability); + } } } + + // Create the state-action reward for the newly created choice. + auto valueIt = stateActionRewards.begin(); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); } - // Create the state-action reward for the newly created choice. - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&choice] (ValueType const& value) { choice.addReward(value); } ); + // If there is one more command to come, shift the target states one time step back. + if (i < iteratorList.size() - 1) { + delete currentTargetStates; + currentTargetStates = newTargetStates; + newTargetStates = new boost::container::flat_map(); + } + } + + // At this point, we applied all commands of the current command combination and newTargetStates + // contains all target states and their respective probabilities. That means we are now ready to + // add the choice to the list of transitions. + result.emplace_back(outputActionIndex); + + // Now create the actual distribution. + Choice& choice = result.back(); + + // Add the rewards to the choice. + choice.addRewards(std::move(stateActionRewards)); + + // Add the probabilities/rates to the newly created choice. + ValueType probabilitySum = storm::utility::zero(); + for (auto const& stateProbabilityPair : *newTargetStates) { + StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); + choice.addProbability(actualIndex, stateProbabilityPair.second); if (this->options.isExplorationChecksSet()) { - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ")."); + probabilitySum += stateProbabilityPair.second; } } - ++automatonIndex; + if (this->options.isExplorationChecksSet()) { + // Check that the resulting distribution is in fact a distribution. + STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ")."); + } + + // Dispose of the temporary maps. + delete currentTargetStates; + delete newTargetStates; + + // Now, check whether there is one more command combination to consider. + bool movedIterator = false; + for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) { + ++iteratorList[j]; + if (iteratorList[j] != edgeCombination[j].second.end()) { + movedIterator = true; + } else { + // Reset the iterator to the beginning of the list. + iteratorList[j] = edgeCombination[j].second.begin(); + } + } + + done = !movedIterator; } return result; } template - std::vector> JaniNextStateGenerator::getNonsilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { + std::vector> JaniNextStateGenerator::getActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) { std::vector> result; - for (uint64_t actionIndex : model.getNonsilentActionIndices()) { - std::vector> enabledEdges = getEnabledEdges(locations, actionIndex); - - // Only process this action, if there is at least one feasible solution. - if (!enabledEdges.empty()) { - if (this->options.isExplorationChecksSet()) { - // Check whether a global variable is written multiple times in any combination. - checkGlobalVariableWritesValid(enabledEdges); + for (auto const& outputAndEdges : edges) { + auto const& edges = outputAndEdges.second; + if (edges.size() == 1) { + // If the synch consists of just one element, it's non-synchronizing. + auto const& nonsychingEdges = edges.front(); + uint64_t automatonIndex = nonsychingEdges.first; + + auto edgesIt = nonsychingEdges.second.find(locations[automatonIndex]); + if (edgesIt != nonsychingEdges.second.end()) { + for (auto const& edge : edgesIt->second) { + if (!this->evaluator->asBool(edge->getGuard())) { + continue; + } + + Choice choice = expandNonSynchronizingEdge(*edge, outputAndEdges.first ? outputAndEdges.first.get() : edge->getActionIndex(), automatonIndex, state, stateToIdCallback); + result.emplace_back(std::move(choice)); + } } + } else { + // If the element has more than one set of edges, we need to perform a synchronization. + STORM_LOG_ASSERT(outputAndEdges.first, "Need output action index for synchronization."); - std::vector::const_iterator> iteratorList(enabledEdges.size()); - - // Initialize the list of iterators. - for (size_t i = 0; i < enabledEdges.size(); ++i) { - iteratorList[i] = enabledEdges[i].cbegin(); - } + AutomataEdgeSets automataEdgeSets; + uint64_t outputActionIndex = outputAndEdges.first.get(); - // As long as there is one feasible combination of commands, keep on expanding it. - bool done = false; - while (!done) { - boost::container::flat_map* currentTargetStates = new boost::container::flat_map(); - boost::container::flat_map* newTargetStates = new boost::container::flat_map(); - std::vector stateActionRewards(rewardVariables.size(), storm::utility::zero()); + bool productiveCombination = true; + for (auto const& automatonAndEdges : outputAndEdges.second) { + uint64_t automatonIndex = automatonAndEdges.first; + EdgeSet enabledEdgesOfAutomaton; - currentTargetStates->emplace(state, storm::utility::one()); - - auto locationVariableIt = this->variableInformation.locationVariables.cbegin(); - for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) { - storm::jani::Edge const& edge = **iteratorList[i]; - - for (auto const& destination : edge.getDestinations()) { - for (auto const& stateProbabilityPair : *currentTargetStates) { - // Compute the new state under the current update and add it to the set of new target states. - CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination, *locationVariableIt); - - // If the new state was already found as a successor state, update the probability - // and otherwise insert it. - ValueType probability = stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()); - if (edge.hasRate()) { - probability *= this->evaluator->asRational(edge.getRate()); - } - if (probability != storm::utility::zero()) { - auto targetStateIt = newTargetStates->find(newTargetState); - if (targetStateIt != newTargetStates->end()) { - targetStateIt->second += probability; - } else { - newTargetStates->emplace(newTargetState, probability); - } - } + bool atLeastOneEdge = false; + auto edgesIt = automatonAndEdges.second.find(locations[automatonIndex]); + if (edgesIt != automatonAndEdges.second.end()) { + for (auto const& edge : edgesIt->second) { + if (!this->evaluator->asBool(edge->getGuard())) { + continue; } - - // Create the state-action reward for the newly created choice. - auto valueIt = stateActionRewards.begin(); - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } ); - } - - // If there is one more command to come, shift the target states one time step back. - if (i < iteratorList.size() - 1) { - delete currentTargetStates; - currentTargetStates = newTargetStates; - newTargetStates = new boost::container::flat_map(); - } - ++locationVariableIt; - } - - // At this point, we applied all commands of the current command combination and newTargetStates - // contains all target states and their respective probabilities. That means we are now ready to - // add the choice to the list of transitions. - result.push_back(Choice(actionIndex)); - - // Now create the actual distribution. - Choice& choice = result.back(); - - // Add the rewards to the choice. - choice.addRewards(std::move(stateActionRewards)); - - // Add the probabilities/rates to the newly created choice. - ValueType probabilitySum = storm::utility::zero(); - for (auto const& stateProbabilityPair : *newTargetStates) { - StateType actualIndex = stateToIdCallback(stateProbabilityPair.first); - choice.addProbability(actualIndex, stateProbabilityPair.second); - - if (this->options.isExplorationChecksSet()) { - probabilitySum += stateProbabilityPair.second; + atLeastOneEdge = true; + enabledEdgesOfAutomaton.emplace_back(edge); } } - - if (this->options.isExplorationChecksSet()) { - // Check that the resulting distribution is in fact a distribution. - STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not sum to one for some command (actually sum to " << probabilitySum << ")."); - } - - // Dispose of the temporary maps. - delete currentTargetStates; - delete newTargetStates; - - // Now, check whether there is one more command combination to consider. - bool movedIterator = false; - for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) { - ++iteratorList[j]; - if (iteratorList[j] != enabledEdges[j].end()) { - movedIterator = true; - } else { - // Reset the iterator to the beginning of the list. - iteratorList[j] = enabledEdges[j].begin(); - } + + // If there is no enabled edge of this automaton, the whole combination is not productive. + if (!atLeastOneEdge) { + productiveCombination = false; + break; } - done = !movedIterator; + automataEdgeSets.emplace_back(std::make_pair(automatonIndex, std::move(enabledEdgesOfAutomaton))); } - } - } - - return result; - } - - template - std::vector> JaniNextStateGenerator::getEnabledEdges(std::vector const& locationIndices, uint64_t actionIndex) { - std::vector> result; - - // Iterate over all automata. - uint64_t automatonIndex = 0; - for (auto const& automaton : model.getAutomata()) { - // If the automaton has no edge labeled with the given action, we can skip it. - if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { - continue; - } - - auto edges = automaton.getEdgesFromLocation(locationIndices[automatonIndex], actionIndex); - - // If the automaton contains the action, but there is no edge available labeled with - // this action, we don't have any feasible command combinations. - if (edges.empty()) { - return std::vector>(); - } - - std::vector edgePointers; - for (auto const& edge : edges) { - if (this->evaluator->asBool(edge.getGuard())) { - edgePointers.push_back(&edge); + + if (productiveCombination) { + std::vector> choices = expandSynchronizingEdgeCombination(automataEdgeSets, outputActionIndex, state, stateToIdCallback); + + for (auto const& choice : choices) { + result.emplace_back(std::move(choice)); + } } - } - - // If there was no enabled edge although the automaton has some edge with the required action, we must - // not return anything. - if (edgePointers.empty()) { - return std::vector>(); - } - - result.emplace_back(std::move(edgePointers)); - ++automatonIndex; + } } - + return result; } template - void JaniNextStateGenerator::checkGlobalVariableWritesValid(std::vector> const& enabledEdges) const { + void JaniNextStateGenerator::checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const { std::map writtenGlobalVariables; for (auto edgeSetIt = enabledEdges.begin(), edgeSetIte = enabledEdges.end(); edgeSetIt != edgeSetIte; ++edgeSetIt) { - for (auto const& edge : *edgeSetIt) { + for (auto const& edge : edgeSetIt->second) { for (auto const& globalVariable : edge->getWrittenGlobalVariables()) { auto it = writtenGlobalVariables.find(globalVariable); @@ -629,20 +613,13 @@ namespace storm { template storm::models::sparse::StateLabeling JaniNextStateGenerator::label(storm::storage::BitVectorHashMap const& states, std::vector const& initialStateIndices, std::vector const& deadlockStateIndices) { - - // Prepare a mapping from automata names to the location variables. - std::vector> composedAutomata; - for (auto const& automaton : model.getAutomata()) { - composedAutomata.emplace_back(automaton); - } - // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to // create a list of boolean transient variables and the expressions that define them. std::unordered_map transientVariableToExpressionMap; for (auto const& variable : model.getGlobalVariables().getTransientVariables()) { if (variable.isBooleanVariable()) { if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable.getName()) != this->options.getLabelNames().end()) { - transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), composedAutomata); + transientVariableToExpressionMap[variable.getExpressionVariable()] = model.getLabelExpression(variable.asBooleanVariable(), this->parallelAutomata); } } } @@ -691,7 +668,8 @@ namespace storm { } // Then fill them. - for (auto const& automaton : model.getAutomata()) { + for (auto const& automatonRef : this->parallelAutomata) { + auto const& automaton = automatonRef.get(); for (auto const& location : automaton.getLocations()) { auto rewardVariableIt = rewardVariables.begin(); auto rewardVariableIte = rewardVariables.end(); @@ -731,6 +709,81 @@ namespace storm { } } + template + void JaniNextStateGenerator::createSynchronizationInformation() { + // Create synchronizing edges information. + storm::jani::Composition const& topLevelComposition = this->model.getSystemComposition(); + if (topLevelComposition.isAutomatonComposition()) { + auto const& automaton = this->model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName()); + this->parallelAutomata.push_back(automaton); + + LocationsAndEdges locationsAndEdges; + for (auto const& edge : automaton.getEdges()) { + locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge); + } + + AutomataAndEdges automataAndEdges; + automataAndEdges.emplace_back(std::make_pair(0, std::move(locationsAndEdges))); + + this->edges.emplace_back(std::make_pair(boost::none, std::move(automataAndEdges))); + } else { + STORM_LOG_THROW(topLevelComposition.isParallelComposition(), storm::exceptions::WrongFormatException, "Expected parallel composition."); + storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition(); + + uint64_t automatonIndex = 0; + for (auto const& composition : parallelComposition.getSubcompositions()) { + STORM_LOG_THROW(composition->isAutomatonComposition(), storm::exceptions::WrongFormatException, "Expected flat parallel composition."); + this->parallelAutomata.push_back(this->model.getAutomaton(composition->asAutomatonComposition().getAutomatonName())); + + // Add edges with silent action. + LocationsAndEdges locationsAndEdges; + for (auto const& edge : parallelAutomata.back().get().getEdges()) { + if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) { + locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge); + } + } + + if (!locationsAndEdges.empty()) { + AutomataAndEdges automataAndEdges; + automataAndEdges.emplace_back(std::make_pair(automatonIndex, std::move(locationsAndEdges))); + this->edges.emplace_back(std::make_pair(boost::none, std::move(automataAndEdges))); + } + ++automatonIndex; + } + + for (auto const& vector : parallelComposition.getSynchronizationVectors()) { + uint64_t outputActionIndex = this->model.getActionIndex(vector.getOutput()); + + AutomataAndEdges automataAndEdges; + bool atLeastOneEdge = true; + uint64_t automatonIndex = 0; + for (auto const& element : vector.getInput()) { + if (!storm::jani::SynchronizationVector::isNoActionInput(element)) { + LocationsAndEdges locationsAndEdges; + uint64_t actionIndex = this->model.getActionIndex(element); + for (auto const& edge : parallelAutomata[automatonIndex].get().getEdges()) { + if (edge.getActionIndex() == actionIndex) { + locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge); + } + } + if (locationsAndEdges.empty()) { + atLeastOneEdge = false; + break; + } + automataAndEdges.emplace_back(std::make_pair(automatonIndex, std::move(locationsAndEdges))); + } + ++automatonIndex; + } + + if (atLeastOneEdge) { + this->edges.emplace_back(std::make_pair(outputActionIndex, std::move(automataAndEdges))); + } + } + } + + STORM_LOG_TRACE("Number of synchronizations: " << this->edges.size() << "."); + } + template void JaniNextStateGenerator::checkValid() const { // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message. diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h index 2d15e887b..3fcfc2777 100644 --- a/src/storm/generator/JaniNextStateGenerator.h +++ b/src/storm/generator/JaniNextStateGenerator.h @@ -66,35 +66,33 @@ namespace storm { CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable); /*! - * Retrieves all choices labeled with the silent action possible from the given state. + * Retrieves all choices possible from the given state. * * @param locations The current locations of all automata. * @param state The state for which to retrieve the silent choices. - * @return The silent action choices of the state. + * @return The action choices of the state. */ - std::vector> getSilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback); + std::vector> getActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback); /*! - * Retrieves all choices labeled with some non-silent action possible from the given state. - * - * @param locations THe current locations of all automata. - * @param state The state for which to retrieve the non-silent choices. - * @return The non-silent action choices of the state. + * Retrieves the choice generated by the given edge. */ - std::vector> getNonsilentActionChoices(std::vector const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback); + Choice expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex, CompressedState const& state, StateToIdCallback stateToIdCallback); - /*! - * Retrieves a list of lists of edges such that the list at index i are all edges of automaton i enabled in - * the current state. If the list is empty, it means there was at least one automaton containing edges with - * the desired action, but none of them were enabled. - */ - std::vector> getEnabledEdges(std::vector const& locationIndices, uint64_t actionIndex); + typedef std::vector EdgeSet; + typedef std::unordered_map LocationsAndEdges; + typedef std::vector> AutomataAndEdges; + typedef std::pair, AutomataAndEdges> OutputAndEdges; + + typedef std::pair AutomatonAndEdgeSet; + typedef std::vector AutomataEdgeSets; + + std::vector> expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback); /*! - * Checks the list of enabled edges (obtained by a call to getEnabledEdges) for multiple - * synchronized writes to the same global variable. + * Checks the list of enabled edges for multiple synchronized writes to the same global variable. */ - void checkGlobalVariableWritesValid(std::vector> const& enabledEdges) const; + void checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const; /*! * Treats the given transient assignments by calling the callback function whenever a transient assignment @@ -107,6 +105,11 @@ namespace storm { */ void buildRewardModelInformation(); + /*! + * Creates the internal information about synchronizing edges. + */ + void createSynchronizationInformation(); + /*! * Checks the underlying model for validity for this next-state generator. */ @@ -115,6 +118,12 @@ namespace storm { /// The model used for the generation of next states. storm::jani::Model model; + /// The automata that are put into parallel by this generator. + std::vector> parallelAutomata; + + /// The vector storing the edges that need to be explored (synchronously or asynchronously). + std::vector edges; + /// The transient variables of reward models that need to be considered. std::vector rewardVariables; diff --git a/src/storm/generator/VariableInformation.cpp b/src/storm/generator/VariableInformation.cpp index 2cfd5911c..e691300c6 100644 --- a/src/storm/generator/VariableInformation.cpp +++ b/src/storm/generator/VariableInformation.cpp @@ -4,10 +4,13 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/Automaton.h" +#include "storm/storage/jani/AutomatonComposition.h" +#include "storm/storage/jani/ParallelComposition.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" +#include "storm/exceptions/WrongFormatException.h" #include @@ -55,7 +58,7 @@ namespace storm { sortVariables(); } - VariableInformation::VariableInformation(storm::jani::Model const& model) : totalBitOffset(0) { + VariableInformation::VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata) : totalBitOffset(0) { // Check that the model does not contain non-transient unbounded integer or non-transient real variables. STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientRealVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains global non-transient real variables."); STORM_LOG_THROW(!model.getGlobalVariables().containsNonTransientUnboundedIntegerVariables(), storm::exceptions::InvalidArgumentException, "Cannot build model from JANI model that contains non-transient unbounded integer variables."); @@ -79,29 +82,34 @@ namespace storm { totalBitOffset += bitwidth; } } - for (auto const& automaton : model.getAutomata()) { - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); - locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); - totalBitOffset += bitwidth; - - for (auto const& variable : automaton.getVariables().getBooleanVariables()) { - if (!variable.isTransient()) { - booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); - ++totalBitOffset; - } + + for (auto const& automatonRef : parallelAutomata) { + createVariablesForAutomaton(automatonRef.get()); + } + + sortVariables(); + } + + void VariableInformation::createVariablesForAutomaton(storm::jani::Automaton const& automaton) { + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(automaton.getNumberOfLocations()))); + locationVariables.emplace_back(automaton.getLocationExpressionVariable(), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; + + for (auto const& variable : automaton.getVariables().getBooleanVariables()) { + if (!variable.isTransient()) { + booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset); + ++totalBitOffset; } - for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { - if (!variable.isTransient()) { - int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); - int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); - uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); - integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); - totalBitOffset += bitwidth; - } + } + for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) { + if (!variable.isTransient()) { + int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt(); + int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt(); + uint_fast64_t bitwidth = static_cast(std::ceil(std::log2(upperBound - lowerBound + 1))); + integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth); + totalBitOffset += bitwidth; } } - - sortVariables(); } uint_fast64_t VariableInformation::getTotalBitOffset(bool roundTo64Bit) const { diff --git a/src/storm/generator/VariableInformation.h b/src/storm/generator/VariableInformation.h index 4f2d6f632..764881e80 100644 --- a/src/storm/generator/VariableInformation.h +++ b/src/storm/generator/VariableInformation.h @@ -13,6 +13,7 @@ namespace storm { namespace jani { class Model; + class Automaton; } namespace generator { @@ -74,7 +75,7 @@ namespace storm { // A structure storing information about the used variables of the program. struct VariableInformation { VariableInformation(storm::prism::Program const& program); - VariableInformation(storm::jani::Model const& model); + VariableInformation(storm::jani::Model const& model, std::vector> const& parallelAutomata); VariableInformation() = default; uint_fast64_t getTotalBitOffset(bool roundTo64Bit = false) const; @@ -96,6 +97,11 @@ namespace storm { * Sorts the variables to establish a known ordering. */ void sortVariables(); + + /*! + * Creates all necessary variables for a JANI automaton. + */ + void createVariablesForAutomaton(storm::jani::Automaton const& automaton); }; } From 6d86df0ead0b84b12f96c3910ff5ca3133a3d602 Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 30 Apr 2017 14:50:16 +0200 Subject: [PATCH 02/22] fixed doing the end component analysis in multi objective model checking multiple times --- .../modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 9e5474362..58edc68a8 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -81,6 +81,7 @@ namespace storm { auto backwardTransitions = result.preprocessedModel.getBackwardTransitions(); analyzeEndComponents(result, backwardTransitions); ensureRewardFiniteness(result, backwardTransitions); + break; } } return result; From e8adc21fdb3e57b8e04a7e9d5eeea695e6c3a3a3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 2 May 2017 17:52:07 +0200 Subject: [PATCH 03/22] version is now updated to a dev version when committing after a tagged version --- CMakeLists.txt | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index b24322d49..64c2c6ac7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -397,9 +397,18 @@ else() else() set(STORM_VERSION_DIRTY "false") endif() - message(STATUS "Storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} (${STORM_VERSION_COMMITS_AHEAD} commits ahead of tag), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") + + set(STORM_VERSION_DEV_STRING "") + if(STORM_VERSION_COMMITS_AHEAD) + MATH(EXPR STORM_VERSION_DEV_PATCH "${STORM_VERSION_PATCH}+1") + + set(STORM_VERSION_DEV_STRING "(dev)") + else() + set(STORM_VERSION_DEV_PATCH ${STORM_VERSION_PATCH}) + endif() + message(STATUS "Storm - version is ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_DEV_PATCH}${STORM_VERSION_DEV_STRING} (version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH} + ${STORM_VERSION_COMMITS_AHEAD} commits), building from git: ${STORM_VERSION_GIT_HASH} (dirty: ${STORM_VERSION_DIRTY}).") endif() -set(STORM_VERSION "${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}") +set(STORM_VERSION "${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_DEV_PATCH}") # Configure a header file to pass some of the CMake settings to the source code From b82e0608e513831b0f7c5ff345f6fbcd40cc12c2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 5 May 2017 08:24:31 +0200 Subject: [PATCH 04/22] Fix for CheckTask: now properly updating uperator information to make nested formulas work again (pointed out by Matt S Bauer) --- src/storm/modelchecker/CheckTask.h | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 32063b293..4440f1ba3 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/src/storm/modelchecker/CheckTask.h @@ -52,7 +52,6 @@ namespace storm { template CheckTask substituteFormula(NewFormulaType const& newFormula) const { CheckTask result(newFormula, this->optimizationDirection, this->rewardModel, this->onlyInitialStatesRelevant, this->bound, this->qualitative, this->produceSchedulers, this->hint); - result.updateOperatorInformation(); return result; } @@ -68,13 +67,13 @@ namespace storm { } if (operatorFormula.hasBound()) { - if (onlyInitialStatesRelevant) { - this->bound = operatorFormula.getBound(); - } - - if (!optimizationDirection) { - this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; - } + this->bound = operatorFormula.getBound(); + } + + if (operatorFormula.hasOptimalityType()) { + this->optimizationDirection = operatorFormula.getOptimalityType(); + } else if (operatorFormula.hasBound()) { + this->optimizationDirection = operatorFormula.getComparisonType() == storm::logic::ComparisonType::Less || operatorFormula.getComparisonType() == storm::logic::ComparisonType::LessEqual ? OptimizationDirection::Maximize : OptimizationDirection::Minimize; } if (formula.get().isProbabilityOperatorFormula()) { From 748e100aadaaa91d0c0833b8c525754b9715eb33 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 May 2017 15:54:04 +0200 Subject: [PATCH 05/22] fixed/improved .dot output for MAs and Mdps. We now also display the index of each choice. --- src/storm/models/sparse/MarkovAutomaton.cpp | 13 +++++++------ src/storm/models/sparse/NondeterministicModel.cpp | 11 ++++++----- 2 files changed, 13 insertions(+), 11 deletions(-) diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index 069ed1936..f0eb0fc39 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -157,7 +157,7 @@ namespace storm { template void MarkovAutomaton::writeDotToStream(std::ostream& outStream, bool includeLabeling, storm::storage::BitVector const* subsystem, std::vector const* firstValue, std::vector const* secondValue, std::vector const* stateColoring, std::vector const* colors, std::vector* scheduler, bool finalizeOutput) const { - NondeterministicModel::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); + Model::writeDotToStream(outStream, includeLabeling, subsystem, firstValue, secondValue, stateColoring, colors, scheduler, false); // Write the probability distributions for all the states. for (uint_fast64_t state = 0; state < this->getNumberOfStates(); ++state) { @@ -166,7 +166,8 @@ namespace storm { // For this, we need to iterate over all available nondeterministic choices in the current state. for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { - typename storm::storage::SparseMatrix::const_rows row = this->getTransitionMatrix().getRow(this->getTransitionMatrix().getRowGroupIndices()[state] + choice); + uint_fast64_t rowIndex = this->getTransitionMatrix().getRowGroupIndices()[state] + choice; + typename storm::storage::SparseMatrix::const_rows row = this->getTransitionMatrix().getRow(rowIndex); if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. @@ -192,17 +193,17 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\" [ label= \"" << rowIndex << "\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; + outStream << ", color=\"red\", penwidth = 2"; } else { - outStream << " [style = \"dotted\"]"; + outStream << ", style = \"dotted\""; } } - outStream << ";" << std::endl; + outStream << "];" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. for (auto const& transition : row) { diff --git a/src/storm/models/sparse/NondeterministicModel.cpp b/src/storm/models/sparse/NondeterministicModel.cpp index 8a7a82485..7f221cabe 100644 --- a/src/storm/models/sparse/NondeterministicModel.cpp +++ b/src/storm/models/sparse/NondeterministicModel.cpp @@ -108,7 +108,8 @@ namespace storm { // For this, we need to iterate over all available nondeterministic choices in the current state. for (uint_fast64_t choice = 0; choice < rowCount; ++choice) { - typename storm::storage::SparseMatrix::const_rows row = this->getTransitionMatrix().getRow(this->getNondeterministicChoiceIndices()[state] + choice); + uint_fast64_t rowIndex = this->getNondeterministicChoiceIndices()[state] + choice; + typename storm::storage::SparseMatrix::const_rows row = this->getTransitionMatrix().getRow(rowIndex); if (scheduler != nullptr) { // If the scheduler picked the current choice, we will not make it dotted, but highlight it. @@ -131,17 +132,17 @@ namespace storm { } outStream << "];" << std::endl; - outStream << "\t" << state << " -> \"" << state << "c" << choice << "\""; + outStream << "\t" << state << " -> \"" << state << "c" << choice << "\" [ label= \"" << rowIndex << "\""; // If we were given a scheduler to highlight, we do so now. if (scheduler != nullptr) { if (highlightChoice) { - outStream << " [color=\"red\", penwidth = 2]"; + outStream << ", color=\"red\", penwidth = 2"; } else { - outStream << " [style = \"dotted\"]"; + outStream << ", style = \"dotted\""; } } - outStream << ";" << std::endl; + outStream << "];" << std::endl; // Now draw all probabilitic arcs that belong to this nondeterminstic choice. for (auto const& transition : row) { From 3d4d23691c33ea439dfbf7b4b1038b704f1003d5 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 May 2017 15:58:13 +0200 Subject: [PATCH 06/22] fixed translation of mathsat's rational number expressions to storm's rational number expressions --- src/storm/adapters/MathsatExpressionAdapter.h | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index 63edcc371..1e70d546a 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -13,6 +13,7 @@ #include "storage/expressions/Expressions.h" #include "storage/expressions/ExpressionVisitor.h" #include "storm/utility/macros.h" +#include "storm/utility/constants.h" #include "storm/exceptions/ExpressionEvaluationException.h" #include "storm/exceptions/InvalidTypeException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -250,10 +251,13 @@ namespace storm { msat_free(name); return result; } else if (msat_term_is_number(env, term)) { + char* termAsCString = msat_term_repr(term); + std::string termString(termAsCString); + msat_free(termAsCString); if (msat_is_integer_type(env, msat_term_get_type(term))) { return manager.integer(std::stoll(msat_term_repr(term))); } else if (msat_is_rational_type(env, msat_term_get_type(term))) { - return manager.rational(std::stod(msat_term_repr(term))); + return manager.rational(storm::utility::convertNumber(termString)); } } From f6963f5bd170b5ab3defb987dea6bb15420612b2 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 May 2017 15:59:26 +0200 Subject: [PATCH 07/22] Fixed translation of z3 expressions using the distinct operator (n-ary !=) to storm expressions --- src/storm/adapters/Z3ExpressionAdapter.cpp | 20 +++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/src/storm/adapters/Z3ExpressionAdapter.cpp b/src/storm/adapters/Z3ExpressionAdapter.cpp index c4fbff3cd..d715f4599 100644 --- a/src/storm/adapters/Z3ExpressionAdapter.cpp +++ b/src/storm/adapters/Z3ExpressionAdapter.cpp @@ -54,6 +54,24 @@ namespace storm { return manager.boolean(false); case Z3_OP_EQ: return this->translateExpression(expr.arg(0)) == this->translateExpression(expr.arg(1)); + case Z3_OP_DISTINCT: { + unsigned args = expr.num_args(); + STORM_LOG_THROW(args != 0, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. DISTINCT (mutual != ) operator with 0-arity is assumed to be an error."); + if (args == 1) { + return manager.boolean(true); + } else { + storm::expressions::Expression retVal = this->translateExpression(expr.arg(0)) != this->translateExpression(expr.arg(1)); + for (unsigned arg2 = 2; arg2 < args; ++arg2) { + retVal = retVal && (this->translateExpression(expr.arg(0)) != this->translateExpression(expr.arg(arg2))); + } + for (unsigned arg1 = 1; arg1 < args; ++arg1) { + for (unsigned arg2 = arg1 + 1; arg2 < args; ++arg2) { + retVal = retVal && (this->translateExpression(expr.arg(arg1)) != this->translateExpression(expr.arg(arg2))); + } + } + return retVal; + } + } case Z3_OP_ITE: return storm::expressions::ite(this->translateExpression(expr.arg(0)), this->translateExpression(expr.arg(1)), this->translateExpression(expr.arg(2))); case Z3_OP_AND: { @@ -133,7 +151,7 @@ namespace storm { STORM_LOG_THROW(expr.is_const(), storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered non-constant uninterpreted function."); return manager.getVariable(expr.decl().name().str()).getExpression(); default: - STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().kind() <<"."); + STORM_LOG_THROW(false, storm::exceptions::ExpressionEvaluationException, "Failed to convert Z3 expression. Encountered unhandled Z3_decl_kind " << expr.decl().decl_kind() <<"."); break; } } else { From 267768a5b66f58a3d655d4060fd5b15ca719dcd8 Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 5 May 2017 19:24:34 +0200 Subject: [PATCH 08/22] enabled markov automata with rationals --- .../SparseMarkovAutomatonCslModelChecker.cpp | 11 ++- .../helper/SparseMarkovAutomatonCslHelper.cpp | 95 +++++++++++++------ .../helper/SparseMarkovAutomatonCslHelper.h | 22 ++++- .../modelchecker/multiobjective/pcaa.cpp | 2 +- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 26 +++-- .../pcaa/SparseMaPcaaWeightVectorChecker.h | 6 +- .../pcaa/SparsePcaaAchievabilityQuery.cpp | 2 +- .../pcaa/SparsePcaaParetoQuery.cpp | 2 +- .../pcaa/SparsePcaaQuantitativeQuery.cpp | 2 +- .../multiobjective/pcaa/SparsePcaaQuery.cpp | 6 ++ src/storm/utility/storm.h | 4 +- 11 files changed, 127 insertions(+), 51 deletions(-) diff --git a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 03789fe53..8f2fd22ce 100644 --- a/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -66,7 +66,7 @@ namespace storm { upperBound = storm::utility::infinity(); } - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), rightResult.getTruthValuesVector(), std::make_pair(lowerBound, upperBound), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -78,7 +78,7 @@ namespace storm { std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult(); ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeUntilProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -90,7 +90,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityRewards(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -103,7 +103,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(stateFormula); ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -115,7 +115,7 @@ namespace storm { std::unique_ptr subResultPointer = this->check(eventuallyFormula.getSubformula()); ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult(); - std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); + std::vector result = storm::modelchecker::helper::SparseMarkovAutomatonCslHelper::computeReachabilityTimes(checkTask.getOptimizationDirection(), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), this->getModel().getExitRates(), this->getModel().getMarkovianStates(), subResult.getTruthValuesVector(), *minMaxLinearEquationSolverFactory); return std::unique_ptr(new ExplicitQuantitativeCheckResult(std::move(result))); } @@ -125,5 +125,6 @@ namespace storm { } template class SparseMarkovAutomatonCslModelChecker>; + template class SparseMarkovAutomatonCslModelChecker>; } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index a76916519..c555fd0e8 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -16,22 +16,23 @@ #include "storm/storage/expressions/Variable.h" #include "storm/storage/expressions/Expression.h" +#include "storm/storage/expressions/ExpressionManager.h" #include "storm/utility/numerical.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/solver/LpSolver.h" - #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/InvalidOperationException.h" namespace storm { namespace modelchecker { namespace helper { - template - void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template ::SupportsExponential, int>::type> + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { // Start by computing four sparse matrices: // * a matrix aMarkovian with all (discretized) transitions from Markovian non-goal states to all Markovian non-goal states. @@ -116,9 +117,14 @@ namespace storm { storm::utility::vector::addVectors(bProbabilistic, bProbabilisticFixed, bProbabilistic); solver->solveEquations(dir, probabilisticNonGoalValues, bProbabilistic); } - - template - std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + + template ::SupportsExponential, int>::type> + void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded reachability probabilities is unsupported for this value type."); + } + + template ::SupportsExponential, int>::type> + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); @@ -180,16 +186,20 @@ namespace storm { return result; } } - + + template ::SupportsExponential, int>::type> + std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded until probabilities is unsupported for this value type."); + } + template - std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { return std::move(storm::modelchecker::helper::SparseMdpPrctlHelper::computeUntilProbabilities(dir, transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, false, minMaxLinearEquationSolverFactory).values); } - template - template - std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + template + std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { std::vector stateRewardWeights(transitionMatrix.getRowGroupCount()); for (auto const markovianState : markovianStates) { stateRewardWeights[markovianState] = storm::utility::one() / exitRateVector[markovianState]; @@ -199,7 +209,7 @@ namespace storm { } template - std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { uint_fast64_t numberOfStates = transitionMatrix.getRowGroupCount(); // If there are no goal states, we avoid the computation and directly return zero. @@ -213,7 +223,7 @@ namespace storm { } // Start by decomposing the Markov automaton into its MECs. - storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions); + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions); // Get some data members for convenience. std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); @@ -354,7 +364,7 @@ namespace storm { } template - std::vector SparseMarkovAutomatonCslHelper::computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { + std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory) { std::vector rewardValues(transitionMatrix.getRowCount(), storm::utility::zero()); for (auto const markovianState : markovianStates) { rewardValues[transitionMatrix.getRowGroupIndices()[markovianState]] = storm::utility::one() / exitRateVector[markovianState]; @@ -363,8 +373,7 @@ namespace storm { } template - std::vector - SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, + std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const &transitionMatrix, storm::storage::SparseMatrix const &backwardTransitions, storm::storage::BitVector const &goalStates, @@ -380,7 +389,7 @@ namespace storm { // reach a bottom SCC without a goal state. // So we start by computing all bottom SCCs without goal states. - storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, + storm::storage::StronglyConnectedComponentDecomposition sccDecomposition(transitionMatrix, ~goalStates, true, true); @@ -408,7 +417,7 @@ namespace storm { // If we maximize the property, the expected time of a state is infinite, if an end-component without any goal state is reachable. // So we start by computing all MECs that have no goal state. - storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, + storm::storage::MaximalEndComponentDecomposition mecDecomposition(transitionMatrix, backwardTransitions, ~goalStates); @@ -463,10 +472,9 @@ namespace storm { return result; } - template - ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { + ValueType SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) { std::unique_ptr lpSolverFactory(new storm::utility::solver::LpSolverFactory()); std::unique_ptr solver = lpSolverFactory->create("LRA for MEC"); solver->setOptimizationDirection(invert(dir)); @@ -490,11 +498,11 @@ namespace storm { storm::expressions::Expression constraint = stateToVariableMap.at(state); for (auto element : transitionMatrix.getRow(nondeterministicChoiceIndices[state])) { - constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); + constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getManager().rational((element.getValue())); } - constraint = constraint + solver->getConstant(storm::utility::one() / exitRateVector[state]) * k; - storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getConstant(storm::utility::one() / exitRateVector[state]) : solver->getConstant(0); + constraint = constraint + solver->getManager().rational(storm::utility::one() / exitRateVector[state]) * k; + storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getManager().rational(storm::utility::one() / exitRateVector[state]) : solver->getManager().rational(storm::utility::zero()); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -508,10 +516,10 @@ namespace storm { storm::expressions::Expression constraint = stateToVariableMap.at(state); for (auto element : transitionMatrix.getRow(choice)) { - constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getConstant(element.getValue()); + constraint = constraint - stateToVariableMap.at(element.getColumn()) * solver->getManager().rational(element.getValue()); } - storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::zero()); + storm::expressions::Expression rightHandSide = solver->getManager().rational(storm::utility::zero()); if (dir == OptimizationDirection::Minimize) { constraint = constraint <= rightHandSide; } else { @@ -523,12 +531,43 @@ namespace storm { } solver->optimize(); - return solver->getContinuousValue(k); + return storm::utility::convertNumber(solver->getContinuousValue(k)); } + - template class SparseMarkovAutomatonCslHelper; - template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, double delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template double SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + + template std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::models::sparse::StandardRewardModel const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template std::vector SparseMarkovAutomatonCslHelper::computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template void SparseMarkovAutomatonCslHelper::computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, storm::RationalNumber delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template storm::RationalNumber SparseMarkovAutomatonCslHelper::computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); + + template std::vector SparseMarkovAutomatonCslHelper::computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + } } } diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h index f0ab29ebc..d61baf0c2 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.h @@ -5,28 +5,40 @@ #include "storm/storage/MaximalEndComponent.h" #include "storm/solver/OptimizationDirection.h" #include "storm/solver/MinMaxLinearEquationSolver.h" +#include "storm/utility/NumberTraits.h" namespace storm { namespace modelchecker { namespace helper { - template class SparseMarkovAutomatonCslHelper { public: + + template ::SupportsExponential, int>::type = 0> + static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template ::SupportsExponential, int>::type = 0> static std::vector computeBoundedUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template static std::vector computeUntilProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - template + template static std::vector computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, RewardModelType const& rewardModel, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template static std::vector computeLongRunAverageProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); - static std::vector computeTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + template + static std::vector computeReachabilityTimes(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& psiStates, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); private: + template ::SupportsExponential, int>::type = 0> + static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); + + template ::SupportsExponential, int>::type = 0> static void computeBoundedReachabilityProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector& markovianNonGoalValues, std::vector& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); /*! @@ -35,12 +47,13 @@ namespace storm { * @param dir Sets whether the long-run average is to be minimized or maximized. * @param transitionMatrix The transition matrix of the underlying Markov automaton. * @param markovianStates A bit vector storing all markovian states. - * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are + * @param exitRateVector A vector with exit rates for all states. Exit rates of probabilistic states are * assumed to be zero. * @param goalStates A bit vector indicating which states are to be considered as goal states. * @param mec The maximal end component to consider for computing the long-run average. * @return The long-run average of being in a goal state for the given MEC. */ + template static ValueType computeLraForMaximalEndComponent(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec); /*! @@ -56,6 +69,7 @@ namespace storm { * of the state. * @return A vector that contains the expected reward for each state of the model. */ + template static std::vector computeExpectedRewards(OptimizationDirection dir, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& goalStates, std::vector const& stateRewards, storm::solver::MinMaxLinearEquationSolverFactory const& minMaxLinearEquationSolverFactory); }; diff --git a/src/storm/modelchecker/multiobjective/pcaa.cpp b/src/storm/modelchecker/multiobjective/pcaa.cpp index 6019c19cd..421cbb566 100644 --- a/src/storm/modelchecker/multiobjective/pcaa.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa.cpp @@ -80,7 +80,7 @@ namespace storm { template std::unique_ptr performPcaa>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); #ifdef STORM_HAVE_CARL template std::unique_ptr performPcaa>(storm::models::sparse::Mdp const& model, storm::logic::MultiObjectiveFormula const& formula); - // template std::unique_ptr performPcaa>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); + template std::unique_ptr performPcaa>(storm::models::sparse::MarkovAutomaton const& model, storm::logic::MultiObjectiveFormula const& formula); #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 8ae1c8498..45d99f003 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -7,6 +7,7 @@ #include "storm/models/sparse/StandardRewardModel.h" #include "storm/utility/macros.h" #include "storm/utility/vector.h" +#include "storm/solver/GmmxxLinearEquationSolver.h" #include "storm/exceptions/InvalidOperationException.h" #include "storm/exceptions/InvalidPropertyException.h" @@ -298,14 +299,23 @@ namespace storm { } template + template ::SupportsExponential, int>::type> std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(SubModel const& PS) const { std::unique_ptr result(new LinEqSolverData()); + auto factory = std::make_unique>(); // We choose Jacobi since we call the solver very frequently on 'easy' inputs (note that jacobi without preconditioning has very little overhead). - result->factory.getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi); - result->factory.getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); + factory->getSettings().setSolutionMethod(storm::solver::GmmxxLinearEquationSolverSettings::SolutionMethod::Jacobi); + factory->getSettings().setPreconditioner(storm::solver::GmmxxLinearEquationSolverSettings::Preconditioner::None); + result->factory = std::move(factory); result->b.resize(PS.getNumberOfStates()); return result; } + + template + template ::SupportsExponential, int>::type> + std::unique_ptr::LinEqSolverData> SparseMaPcaaWeightVectorChecker::initLinEqSolver(SubModel const& PS) const { + STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Computing bounded probabilities of MAs is unsupported for this value type."); + } template void SparseMaPcaaWeightVectorChecker::updateDataToCurrentEpoch(SubModel& MS, SubModel& PS, MinMaxSolverData& minMax, storm::storage::BitVector& consideredObjectives, uint_fast64_t const& currentEpoch, std::vector const& weightVector, TimeBoundMap::iterator& upperTimeBoundIt, TimeBoundMap const& upperTimeBounds) { @@ -341,7 +351,7 @@ namespace storm { linEq.solver = nullptr; storm::storage::SparseMatrix linEqMatrix = PS.toPS.selectRowsFromRowGroups(optimalChoicesAtCurrentEpoch, true); linEqMatrix.convertToEquationSystem(); - linEq.solver = linEq.factory.create(std::move(linEqMatrix)); + linEq.solver = linEq.factory->create(std::move(linEqMatrix)); linEq.solver->setCachingEnabled(true); } @@ -393,11 +403,13 @@ namespace storm { template double SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, double const& digitizationConstant) const; template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds( SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, double const& digitizationConstant); + template std::unique_ptr>::LinEqSolverData> SparseMaPcaaWeightVectorChecker>::initLinEqSolver( SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; #ifdef STORM_HAVE_CARL -// template class SparseMaPcaaWeightVectorChecker>; - // template storm::RationalNumber SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; - // template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; -// template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); + template class SparseMaPcaaWeightVectorChecker>; + template storm::RationalNumber SparseMaPcaaWeightVectorChecker>::getDigitizationConstant(std::vector const& direction) const; + template void SparseMaPcaaWeightVectorChecker>::digitize(SparseMaPcaaWeightVectorChecker>::SubModel& subModel, storm::RationalNumber const& digitizationConstant) const; + template void SparseMaPcaaWeightVectorChecker>::digitizeTimeBounds(SparseMaPcaaWeightVectorChecker>::TimeBoundMap& upperTimeBounds, storm::RationalNumber const& digitizationConstant); + template std::unique_ptr>::LinEqSolverData> SparseMaPcaaWeightVectorChecker>::initLinEqSolver( SparseMaPcaaWeightVectorChecker>::SubModel const& PS ) const; #endif } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h index 827f1701e..ef3c6ea72 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.h @@ -6,7 +6,6 @@ #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaWeightVectorChecker.h" #include "storm/solver/LinearEquationSolver.h" -#include "storm/solver/GmmxxLinearEquationSolver.h" #include "storm/solver/MinMaxLinearEquationSolver.h" #include "storm/utility/NumberTraits.h" @@ -71,7 +70,7 @@ namespace storm { }; struct LinEqSolverData { - storm::solver::GmmxxLinearEquationSolverFactory factory; + std::unique_ptr> factory; std::unique_ptr> solver; std::vector b; }; @@ -124,6 +123,9 @@ namespace storm { /*! * Initializes the data for the LinEq solver */ + template ::SupportsExponential, int>::type = 0> + std::unique_ptr initLinEqSolver(SubModel const& PS) const; + template ::SupportsExponential, int>::type = 0> std::unique_ptr initLinEqSolver(SubModel const& PS) const; /* diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp index fec46a006..db0c2da9d 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.cpp @@ -105,7 +105,7 @@ namespace storm { template class SparsePcaaAchievabilityQuery, storm::RationalNumber>; template class SparsePcaaAchievabilityQuery, storm::RationalNumber>; - // template class SparsePcaaAchievabilityQuery, storm::RationalNumber>; + template class SparsePcaaAchievabilityQuery, storm::RationalNumber>; #endif } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp index 9caf36d04..92717febb 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp @@ -95,7 +95,7 @@ namespace storm { template class SparsePcaaParetoQuery, storm::RationalNumber>; template class SparsePcaaParetoQuery, storm::RationalNumber>; - // template class SparsePcaaParetoQuery, storm::RationalNumber>; + template class SparsePcaaParetoQuery, storm::RationalNumber>; #endif } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp index 48448f968..9dd81014b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.cpp @@ -201,7 +201,7 @@ namespace storm { template class SparsePcaaQuantitativeQuery, storm::RationalNumber>; template class SparsePcaaQuantitativeQuery, storm::RationalNumber>; - // template class SparsePcaaQuantitativeQuery, storm::RationalNumber>; + template class SparsePcaaQuantitativeQuery, storm::RationalNumber>; #endif } } diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp index 5bc096c93..10652dd07 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaQuery.cpp @@ -46,6 +46,11 @@ namespace storm { this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); } + template<> + void SparsePcaaQuery, storm::RationalNumber>::initializeWeightVectorChecker(storm::models::sparse::MarkovAutomaton const& model, std::vector> const& objectives, storm::storage::BitVector const& actionsWithNegativeReward, storm::storage::BitVector const& ecActions, storm::storage::BitVector const& possiblyRecurrentStates) { + this->weightVectorChecker = std::unique_ptr>>(new SparseMaPcaaWeightVectorChecker>(model, objectives, actionsWithNegativeReward, ecActions, possiblyRecurrentStates)); + } + template typename SparsePcaaQuery::WeightVector SparsePcaaQuery::findSeparatingVector(Point const& pointToBeSeparated) { STORM_LOG_DEBUG("Searching a weight vector to seperate the point given by " << storm::utility::vector::toString(storm::utility::vector::convertNumericVector(pointToBeSeparated)) << "."); @@ -239,6 +244,7 @@ namespace storm { template class SparsePcaaQuery, storm::RationalNumber>; template class SparsePcaaQuery, storm::RationalNumber>; + template class SparsePcaaQuery, storm::RationalNumber>; #endif } } diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index 368a09618..c2230c87c 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -526,7 +526,7 @@ namespace storm { } template - std::unique_ptr verifySparseMarkovAutomaton(std::shared_ptr> ma, storm::modelchecker::CheckTask const& task) { + std::unique_ptr verifySparseMarkovAutomaton(std::shared_ptr> ma, storm::modelchecker::CheckTask const& task) { std::unique_ptr result; // Close the MA, if it is not already closed. if (!ma->isClosed()) { @@ -572,6 +572,8 @@ namespace storm { result = verifySparseCtmc(model->template as>(), task); } else if (model->getType() == storm::models::ModelType::Mdp) { result = verifySparseMdp(model->template as>(), task); + } else if (model->getType() == storm::models::ModelType::MarkovAutomaton) { + result = verifySparseMarkovAutomaton(model->template as>(), task); } else { STORM_LOG_ASSERT(false, "Illegal model type."); } From 927a8f93cceb3cf0a4a2e4ed57ed0f22ed621349 Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 10 May 2017 16:33:06 +0200 Subject: [PATCH 09/22] fixed translation of rational numbers to mathsat expressions --- src/storm/adapters/MathsatExpressionAdapter.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h index 1e70d546a..357c482b3 100644 --- a/src/storm/adapters/MathsatExpressionAdapter.h +++ b/src/storm/adapters/MathsatExpressionAdapter.h @@ -182,7 +182,9 @@ namespace storm { } virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) override { - return msat_make_number(env, std::to_string(expression.getValueAsDouble()).c_str()); + std::stringstream fractionStream; + fractionStream << expression.getValue(); + return msat_make_number(env, fractionStream.str().c_str()); } virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) override { From d655621ea1a44aa54dcb82ff9779963c99b303ab Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 11 May 2017 13:13:13 +0200 Subject: [PATCH 10/22] Fixed seg fault when building model valuations --- src/storm/builder/ExplicitModelBuilder.h | 2 +- src/storm/storage/expressions/SimpleValuation.cpp | 8 ++++---- src/storm/storage/expressions/Valuation.cpp | 4 ++++ src/storm/storage/expressions/Valuation.h | 8 ++++++++ 4 files changed, 17 insertions(+), 5 deletions(-) diff --git a/src/storm/builder/ExplicitModelBuilder.h b/src/storm/builder/ExplicitModelBuilder.h index 25acb684c..0141b2d68 100644 --- a/src/storm/builder/ExplicitModelBuilder.h +++ b/src/storm/builder/ExplicitModelBuilder.h @@ -79,7 +79,7 @@ namespace storm { // A flag that indicates whether or not to store the state information after successfully building the // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful - // call to translateProgram. + // call to build. bool buildStateValuations; }; diff --git a/src/storm/storage/expressions/SimpleValuation.cpp b/src/storm/storage/expressions/SimpleValuation.cpp index f0dd7deef..e60556305 100644 --- a/src/storm/storage/expressions/SimpleValuation.cpp +++ b/src/storm/storage/expressions/SimpleValuation.cpp @@ -19,7 +19,7 @@ namespace storm { // Intentionally left empty. } - SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManager().getSharedPointer()) { + SimpleValuation::SimpleValuation(SimpleValuation const& other) : Valuation(other.getManagerAsSharedPtr()) { if (this != &other) { booleanValues = other.booleanValues; integerValues = other.integerValues; @@ -29,7 +29,7 @@ namespace storm { SimpleValuation& SimpleValuation::operator=(SimpleValuation const& other) { if (this != &other) { - this->setManager(other.getManager().getSharedPointer()); + this->setManager(other.getManagerAsSharedPtr()); booleanValues = other.booleanValues; integerValues = other.integerValues; rationalValues = other.rationalValues; @@ -37,7 +37,7 @@ namespace storm { return *this; } - SimpleValuation::SimpleValuation(SimpleValuation&& other) : Valuation(other.getManager().getSharedPointer()) { + SimpleValuation::SimpleValuation(SimpleValuation&& other) : Valuation(other.getManagerAsSharedPtr()) { if (this != &other) { booleanValues = std::move(other.booleanValues); integerValues = std::move(other.integerValues); @@ -47,7 +47,7 @@ namespace storm { SimpleValuation& SimpleValuation::operator=(SimpleValuation&& other) { if (this != &other) { - this->setManager(other.getManager().getSharedPointer()); + this->setManager(other.getManagerAsSharedPtr()); booleanValues = std::move(other.booleanValues); integerValues = std::move(other.integerValues); rationalValues = std::move(other.rationalValues); diff --git a/src/storm/storage/expressions/Valuation.cpp b/src/storm/storage/expressions/Valuation.cpp index 81ab20467..912617a18 100644 --- a/src/storm/storage/expressions/Valuation.cpp +++ b/src/storm/storage/expressions/Valuation.cpp @@ -15,6 +15,10 @@ namespace storm { return *manager; } + std::shared_ptr const& Valuation::getManagerAsSharedPtr() const { + return manager; + } + void Valuation::setManager(std::shared_ptr const& manager) { this->manager = manager; } diff --git a/src/storm/storage/expressions/Valuation.h b/src/storm/storage/expressions/Valuation.h index 0ce691db4..fbe6e4470 100644 --- a/src/storm/storage/expressions/Valuation.h +++ b/src/storm/storage/expressions/Valuation.h @@ -101,6 +101,14 @@ namespace storm { ExpressionManager const& getManager() const; protected: + + /*! + * Retrieves the manager responsible for the variables of this valuation. + * + * @return The manager. + */ + std::shared_ptr const& getManagerAsSharedPtr() const; + /*! * Sets the manager responsible for the variables in this valuation. * From 87f494627c33a4edeae0afc74b4970e2fdbb4344 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 11 May 2017 22:31:13 +0200 Subject: [PATCH 11/22] Fixes after carl update in order to get ginac from carl. --- resources/3rdparty/CMakeLists.txt | 21 ++++++++++++++++----- 1 file changed, 16 insertions(+), 5 deletions(-) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 17e433ff3..9ede52524 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -213,15 +213,17 @@ if(USE_CARL) set(STORM_SHIPPED_CARL OFF) set(STORM_HAVE_CARL ON) message(STATUS "Storm - Use system version of carl.") - message(STATUS "Storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}).") + message(STATUS "Storm - Linking with carl ${carl_VERSION} (CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).") set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) + set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) + else() set(STORM_SHIPPED_CARL ON) # The first external project will be built at *configure stage* message("START CARL CONFIG PROCESS") file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) execute_process( - COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DCARL_USE_CLN_NUMBERS=ON" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON" + COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DUSE_CLN_NUMBERS=ON" "-DUSE_GINAC=ON" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON" WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download OUTPUT_VARIABLE carlconfig_out RESULT_VARIABLE carlconfig_result) @@ -253,8 +255,12 @@ if(USE_CARL) BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT} ) include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlConfig.cmake) - message("CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}") - set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) + message("CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}") + + + set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS}) + set(STORM_HAVE_GINAC ${CARL_USE_GINAC}) + add_dependencies(resources carl) set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include/") set(carl_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}) @@ -263,15 +269,20 @@ if(USE_CARL) # install the carl dynamic library if we build it install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.1.0.0${DYNAMIC_EXT} DESTINATION lib) endif() + if(STORM_USE_CLN_RF AND NOT STORM_HAVE_CLN) message(FATAL_ERROR "Cannot use CLN numbers if carl is build without.") endif() + if(STORM_USE_CLN_RF AND NOT STORM_HAVE_GINAC) + message(FATAL_ERROR "Cannot use CLN numbers if carl is build without ginac.") + endif() + #The library that needs symbols must be first, then the library that resolves the symbol. list(APPEND STORM_DEP_IMP_TARGETS lib_carl) if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF) - list(APPEND STORM_DEP_IMP_TARGETS CLN_SHARED) + list(APPEND STORM_DEP_IMP_TARGETS GINAC_SHARED CLN_SHARED) endif() list(APPEND STORM_DEP_IMP_TARGETS GMPXX_SHARED GMP_SHARED) From 18798f79509cde8f8badc3d04afb79ed05081d33 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 12 May 2017 11:23:44 +0200 Subject: [PATCH 12/22] An existing file is also writable --- src/storm/settings/ArgumentValidators.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/storm/settings/ArgumentValidators.cpp b/src/storm/settings/ArgumentValidators.cpp index 13a1792b5..b8896590d 100644 --- a/src/storm/settings/ArgumentValidators.cpp +++ b/src/storm/settings/ArgumentValidators.cpp @@ -86,9 +86,6 @@ namespace storm { return true; } else if (mode == Mode::Writable) { - struct stat info; - STORM_LOG_THROW(stat (filename.c_str(), &info) != 0, storm::exceptions::IllegalArgumentValueException , "Could not open file '" << filename << "' for writing because file or directory already exists."); - std::ofstream filestream(filename); STORM_LOG_THROW(filestream.is_open(), storm::exceptions::IllegalArgumentValueException , "Could not open file '" << filename << "' for writing."); filestream.close(); From cb5aff10aea5c80b7c0b7fbe847e660055f51776 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 15 May 2017 21:41:06 +0200 Subject: [PATCH 13/22] Fix ambigious isspace that was preventing compilation, introduced by some earlier commit. --- .../parser/GreatSpnEditorProjectParser.cpp | 26 +++++++++++---- src/storm-gspn/parser/PnmlParser.cpp | 33 ++++++++++++------- 2 files changed, 41 insertions(+), 18 deletions(-) diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp index 826124f25..2ab73ac91 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp +++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp @@ -2,6 +2,8 @@ #ifdef STORM_HAVE_XERCES #include +#include + #include "storm-gspn/adapters/XercesAdapter.h" @@ -9,8 +11,18 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/macros.h" +namespace { + bool isOnlyWhitespace(std::string const& in) { + return std::all_of(in.begin(), in.end(), [](char c){ + return std::isspace(static_cast(c)); + }); + } +} + namespace storm { namespace parser { + + storm::gspn::GSPN* GreatSpnEditorProjectParser::parse(xercesc::DOMElement const* elementRoot) { if (storm::adapters::XMLtoString(elementRoot->getTagName()) == "project") { traverseProjectElement(elementRoot); @@ -46,7 +58,7 @@ namespace storm { if (name.compare("gspn") == 0) { traverseGspnElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -84,7 +96,7 @@ namespace storm { traverseNodesElement(child); } else if (name.compare("edges") == 0) { traverseEdgesElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -114,7 +126,7 @@ namespace storm { traversePlaceElement(child); } else if(name.compare("transition") == 0) { traverseTransitionElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -144,7 +156,7 @@ namespace storm { if (name.compare("arc") == 0) { traverseArcElement(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -192,7 +204,7 @@ namespace storm { auto child = node->getChildNodes()->item(i); auto name = storm::adapters::getName(child); - if (std::all_of(name.begin(), name.end(), isspace)) { + if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -252,7 +264,7 @@ namespace storm { auto child = node->getChildNodes()->item(i); auto name = storm::adapters::getName(child); - if (std::all_of(name.begin(), name.end(), isspace)) { + if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -325,7 +337,7 @@ namespace storm { auto child = node->getChildNodes()->item(i); auto name = storm::adapters::getName(child); - if (std::all_of(name.begin(), name.end(), isspace)) { + if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else if(ignoreArcChild(name)) { // ignore diff --git a/src/storm-gspn/parser/PnmlParser.cpp b/src/storm-gspn/parser/PnmlParser.cpp index 3dfd9e2a6..71757defc 100644 --- a/src/storm-gspn/parser/PnmlParser.cpp +++ b/src/storm-gspn/parser/PnmlParser.cpp @@ -9,8 +9,19 @@ #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/macros.h" + +namespace { + bool isOnlyWhitespace(std::string const& in) { + return std::all_of(in.begin(), in.end(), [](char c){ + return std::isspace(static_cast(c)); + }); + } +} namespace storm { namespace parser { + + + storm::gspn::GSPN * PnmlParser::parse(xercesc::DOMElement const* elementRoot ) { if (storm::adapters::getName(elementRoot) == "pnml") { traversePnmlElement(elementRoot); @@ -39,7 +50,7 @@ namespace storm { if (name == "net") { traverseNetOrPage(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -79,7 +90,7 @@ namespace storm { // Some pnml files have a child named page. // The page node has the same children like the net node (e.g., place, transition, arc) traverseNetOrPage(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -120,7 +131,7 @@ namespace storm { } else if(name == "capacity") { capacity.first = true; capacity.second = traverseCapacity(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else if (name == "name" || name == "graphics") { @@ -179,7 +190,7 @@ namespace storm { timed.second = traverseTransitionType(child); } else if (name == "priority") { priority = traversePriority(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else if (name == "graphics" || name == "name" || @@ -255,7 +266,7 @@ namespace storm { } else if(name == "inscription") { multiplicity.first = true; multiplicity.second = traverseMultiplicity(child); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else if (name == "graphics" || name == "arcpath" || name == "tagged") { // ignore these tags @@ -304,7 +315,7 @@ namespace storm { auto value = storm::adapters::getName(child->getFirstChild()); value = value.substr(std::string("Default,").length()); result = std::stoull(value); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else if (name == "graphics") { // ignore these tags @@ -330,7 +341,7 @@ namespace storm { result = std::stoull(value); } else if (name == "graphics") { // ignore these nodes - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -354,7 +365,7 @@ namespace storm { result = std::stoull(value); } else if (name == "graphics") { // ignore these nodes - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -373,7 +384,7 @@ namespace storm { auto name = storm::adapters::getName(child); if (name == "value") { result = storm::adapters::getName(child->getFirstChild()); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -391,7 +402,7 @@ namespace storm { auto name = storm::adapters::getName(child); if (name == "value") { result = storm::adapters::getName(child->getFirstChild()) == "true" ? true : false; - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else { // Found node or attribute which is at the moment nod handled by this parser. @@ -428,7 +439,7 @@ namespace storm { auto value = storm::adapters::getName(child->getFirstChild()); value = value.substr(std::string("Default,").length()); result = std::stoull(value); - } else if (std::all_of(name.begin(), name.end(), isspace)) { + } else if (isOnlyWhitespace(name)) { // ignore node (contains only whitespace) } else if (name == "graphics") { // ignore these tags From 5c7d3db7437a2d488b8fd5df678251c6d7eeb8d3 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 15 May 2017 21:42:16 +0200 Subject: [PATCH 14/22] towards proper side constraints for parametetric systems --- src/storm/adapters/CarlAdapter.h | 1 + src/storm/analysis/GraphConditions.cpp | 63 ++++++++++++++++++++++ src/storm/analysis/GraphConditions.h | 75 ++++++++++++++++++++++++++ src/storm/cli/entrypoints.h | 8 ++- src/storm/models/sparse/Dtmc.cpp | 42 +-------------- src/storm/models/sparse/Dtmc.h | 54 +------------------ src/storm/utility/storm.h | 14 +++-- 7 files changed, 154 insertions(+), 103 deletions(-) create mode 100644 src/storm/analysis/GraphConditions.cpp create mode 100644 src/storm/analysis/GraphConditions.h diff --git a/src/storm/adapters/CarlAdapter.h b/src/storm/adapters/CarlAdapter.h index 27aa37960..642822b68 100644 --- a/src/storm/adapters/CarlAdapter.h +++ b/src/storm/adapters/CarlAdapter.h @@ -9,6 +9,7 @@ #include #include #include +#include namespace carl { // Define hash values for all polynomials and rational function. diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp new file mode 100644 index 000000000..063c963b1 --- /dev/null +++ b/src/storm/analysis/GraphConditions.cpp @@ -0,0 +1,63 @@ + +#include "GraphConditions.h" +#include "storm/utility/constants.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace analysis { + template + ConstraintCollector::ConstraintCollector(storm::models::sparse::Dtmc const& dtmc) { + process(dtmc); + } + + template + std::unordered_set::val> const& ConstraintCollector::getWellformedConstraints() const { + return this->wellformedConstraintSet; + } + + template + std::unordered_set::val> const& ConstraintCollector::getGraphPreservingConstraints() const { + return this->graphPreservingConstraintSet; + } + + template + void ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { + for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { + ValueType sum = storm::utility::zero(); + for (auto const& transition : dtmc.getRows(state)) { + sum += transition.getValue(); + if (!storm::utility::isConstant(transition.getValue())) { + if (transition.getValue().denominator().isConstant()) { + if (transition.getValue().denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::LEQ); + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (transition.getValue().denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace((transition.getValue().nominator() - transition.getValue().denominator()).polynomial(), storm::CompareRelation::GEQ); + wellformedConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at edges not yet supported."); + } + graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); + } + } + STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); + if(!storm::utility::isConstant(sum)) { + wellformedConstraintSet.emplace((sum.nominator() - sum.denominator()).polynomial(), storm::CompareRelation::EQ); + } + + } + } + + template + void ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { + process(dtmc); + } + + + template class ConstraintCollector; + } +} \ No newline at end of file diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h new file mode 100644 index 000000000..14bdd994f --- /dev/null +++ b/src/storm/analysis/GraphConditions.h @@ -0,0 +1,75 @@ +#pragma once + +#include +#include +#include "storm/adapters/CarlAdapter.h" +#include "storm/models/sparse/Dtmc.h" + +namespace storm { + namespace analysis { + +template +struct ConstraintType { + typedef storm::ArithConstraint val; +}; + +template +struct ConstraintType::value>::type> { + typedef carl::Formula val; +}; + +/** + * Class to collect constraints on parametric Markov chains. + */ +template +class ConstraintCollector { +private: + // A set of constraints that says that the DTMC actually has valid probability distributions in all states. + std::unordered_set::val> wellformedConstraintSet; + + // A set of constraints that makes sure that the underlying graph of the model does not change depending + // on the parameter values. + std::unordered_set::val> graphPreservingConstraintSet; + +public: + /*! + * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for + * retrieval after the construction. + * + * @param dtmc The DTMC for which to create the constraints. + */ + ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); + + /*! + * Returns the set of wellformed-ness constraints. + * + * @return The set of wellformed-ness constraints. + */ + std::unordered_set::val> const& getWellformedConstraints() const; + + /*! + * Returns the set of graph-preserving constraints. + * + * @return The set of graph-preserving constraints. + */ + std::unordered_set::val> const& getGraphPreservingConstraints() const; + + /*! + * Constructs the constraints for the given DTMC. + * + * @param dtmc The DTMC for which to create the constraints. + */ + void process(storm::models::sparse::Dtmc const& dtmc); + + /*! + * Constructs the constraints for the given DTMC by calling the process method. + * + * @param dtmc The DTMC for which to create the constraints. + */ + void operator()(storm::models::sparse::Dtmc const& dtmc); + +}; + + + } +} \ No newline at end of file diff --git a/src/storm/cli/entrypoints.h b/src/storm/cli/entrypoints.h index c5baa8287..b43db8bd9 100644 --- a/src/storm/cli/entrypoints.h +++ b/src/storm/cli/entrypoints.h @@ -1,10 +1,10 @@ -#ifndef STORM_ENTRYPOINTS_H_H -#define STORM_ENTRYPOINTS_H_H +#pragma once #include #include "storm/utility/storm.h" +#include "storm/analysis/GraphConditions.h" #include "storm/storage/SymbolicModelDescription.h" #include "storm/utility/DirectEncodingExporter.h" #include "storm/utility/Stopwatch.h" @@ -112,7 +112,7 @@ namespace storm { } if (storm::settings::getModule().exportResultToFile()) { - exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()], storm::models::sparse::Dtmc::ConstraintCollector(*(model->template as>())), storm::settings::getModule().exportResultPath()); + exportParametricResultToFile(result->asExplicitQuantitativeCheckResult()[*model->getInitialStates().begin()], storm::analysis::ConstraintCollector(*(model->template as>())), storm::settings::getModule().exportResultPath()); } } } @@ -469,5 +469,3 @@ namespace storm { } } - -#endif //STORM_ENTRYPOINTS_H_H diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index c61afdaf9..319a06ee9 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -25,47 +25,7 @@ namespace storm { STORM_LOG_THROW(probabilityMatrix.isProbabilistic(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid."); } -#ifdef STORM_HAVE_CARL - template - Dtmc::ConstraintCollector::ConstraintCollector(Dtmc const& dtmc) { - process(dtmc); - } - - template - std::unordered_set> const& Dtmc::ConstraintCollector::getWellformedConstraints() const { - return this->wellformedConstraintSet; - } - - template - std::unordered_set> const& Dtmc::ConstraintCollector::getGraphPreservingConstraints() const { - return this->graphPreservingConstraintSet; - } - - template - void Dtmc::ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { - for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { - ValueType sum = storm::utility::zero(); - for (auto const& transition : dtmc.getRows(state)) { - sum += transition.getValue(); - if (!storm::utility::isConstant(transition.getValue())) { - wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ); - wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ); - graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GREATER); - } - } - STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1."); - if(!storm::utility::isConstant(sum)) { - wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ); - } - - } - } - - template - void Dtmc::ConstraintCollector::operator()(storm::models::sparse::Dtmc const& dtmc) { - process(dtmc); - } -#endif + template class Dtmc; template class Dtmc; diff --git a/src/storm/models/sparse/Dtmc.h b/src/storm/models/sparse/Dtmc.h index 25002856c..4f2d0dfb1 100644 --- a/src/storm/models/sparse/Dtmc.h +++ b/src/storm/models/sparse/Dtmc.h @@ -1,10 +1,7 @@ #ifndef STORM_MODELS_SPARSE_DTMC_H_ #define STORM_MODELS_SPARSE_DTMC_H_ -#include #include "storm/models/sparse/DeterministicModel.h" -#include "storm/utility/OsDetection.h" -#include "storm/adapters/CarlAdapter.h" namespace storm { namespace models { @@ -47,56 +44,7 @@ namespace storm { Dtmc(Dtmc&& dtmc) = default; Dtmc& operator=(Dtmc&& dtmc) = default; - -#ifdef STORM_HAVE_CARL - class ConstraintCollector { - private: - // A set of constraints that says that the DTMC actually has valid probability distributions in all states. - std::unordered_set> wellformedConstraintSet; - - // A set of constraints that makes sure that the underlying graph of the model does not change depending - // on the parameter values. - std::unordered_set> graphPreservingConstraintSet; - - public: - /*! - * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for - * retrieval after the construction. - * - * @param dtmc The DTMC for which to create the constraints. - */ - ConstraintCollector(storm::models::sparse::Dtmc const& dtmc); - - /*! - * Returns the set of wellformed-ness constraints. - * - * @return The set of wellformed-ness constraints. - */ - std::unordered_set> const& getWellformedConstraints() const; - - /*! - * Returns the set of graph-preserving constraints. - * - * @return The set of graph-preserving constraints. - */ - std::unordered_set> const& getGraphPreservingConstraints() const; - - /*! - * Constructs the constraints for the given DTMC. - * - * @param dtmc The DTMC for which to create the constraints. - */ - void process(storm::models::sparse::Dtmc const& dtmc); - - /*! - * Constructs the constraints for the given DTMC by calling the process method. - * - * @param dtmc The DTMC for which to create the constraints. - */ - void operator()(storm::models::sparse::Dtmc const& dtmc); - - }; -#endif + }; } // namespace sparse diff --git a/src/storm/utility/storm.h b/src/storm/utility/storm.h index c2230c87c..0600c36d2 100644 --- a/src/storm/utility/storm.h +++ b/src/storm/utility/storm.h @@ -93,6 +93,9 @@ #include "storm/generator/PrismNextStateGenerator.h" #include "storm/generator/JaniNextStateGenerator.h" +#include "storm/analysis/GraphConditions.h" + + // Headers related to exception handling. #include "storm/exceptions/InvalidStateException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -580,19 +583,22 @@ namespace storm { return result; } - inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc::ConstraintCollector const& constraintCollector, std::string const& path) { + inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::analysis::ConstraintCollector const& constraintCollector, std::string const& path) { std::ofstream filestream; storm::utility::openFile(path, filestream); - // TODO: add checks. filestream << "!Parameters: "; std::set vars = result.gatherVariables(); std::copy(vars.begin(), vars.end(), std::ostream_iterator(filestream, "; ")); filestream << std::endl; filestream << "!Result: " << result << std::endl; filestream << "!Well-formed Constraints: " << std::endl; - std::copy(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::ostream_iterator>(filestream, "\n")); + std::vector stringConstraints; + std::transform(constraintCollector.getWellformedConstraints().begin(), constraintCollector.getWellformedConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); filestream << "!Graph-preserving Constraints: " << std::endl; - std::copy(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::ostream_iterator>(filestream, "\n")); + stringConstraints.clear(); + std::transform(constraintCollector.getGraphPreservingConstraints().begin(), constraintCollector.getGraphPreservingConstraints().end(), std::back_inserter(stringConstraints), [](carl::Formula const& c) -> std::string { return c.toString();}); + std::copy(stringConstraints.begin(), stringConstraints.end(), std::ostream_iterator(filestream, "\n")); storm::utility::closeFile(filestream); } From 165d168cd64cc9b60a088252177c090ff253e2a3 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 15 May 2017 22:29:53 +0200 Subject: [PATCH 15/22] fix for gcc, add state reward support for constraint collection --- src/storm/analysis/GraphConditions.cpp | 42 ++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 063c963b1..1872a4634 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -2,9 +2,11 @@ #include "GraphConditions.h" #include "storm/utility/constants.h" #include "storm/exceptions/NotImplementedException.h" +#include "storm/models/sparse/StandardRewardModel.h" namespace storm { namespace analysis { + template ConstraintCollector::ConstraintCollector(storm::models::sparse::Dtmc const& dtmc) { process(dtmc); @@ -20,6 +22,7 @@ namespace storm { return this->graphPreservingConstraintSet; } + template void ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) { @@ -50,6 +53,45 @@ namespace storm { } } + for(auto const& rewModelEntry : dtmc.getRewardModels()) { + if (rewModelEntry.second.hasStateRewards()) { + for(auto const& stateReward : rewModelEntry.second.getStateRewardVector()) { + if (!storm::utility::isConstant(stateReward)) { + if (stateReward.denominator().isConstant()) { + if (stateReward.denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace(stateReward.nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (stateReward.denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace(stateReward.nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(stateReward.denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + } + } + } + } + if (rewModelEntry.second.hasStateActionRewards()) { + for(auto const& saReward : rewModelEntry.second.getStateActionRewardVector()) { + if (!storm::utility::isConstant(saReward)) { + if (saReward.denominator().isConstant()) { + if (saReward.denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace(saReward.nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (saReward.denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace(saReward.nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(saReward.denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + } + } + } + } + + } } template From 5693144f32b1111de00ed63099f5574104bf1b7a Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 15 May 2017 23:07:35 +0200 Subject: [PATCH 16/22] refactored code to prevent duplication, added support for rational functions at edges when collecting constraints --- src/storm/analysis/GraphConditions.cpp | 60 +++++++++++++++----------- src/storm/analysis/GraphConditions.h | 1 + 2 files changed, 35 insertions(+), 26 deletions(-) diff --git a/src/storm/analysis/GraphConditions.cpp b/src/storm/analysis/GraphConditions.cpp index 1872a4634..0a6b55e57 100644 --- a/src/storm/analysis/GraphConditions.cpp +++ b/src/storm/analysis/GraphConditions.cpp @@ -7,6 +7,7 @@ namespace storm { namespace analysis { + template ConstraintCollector::ConstraintCollector(storm::models::sparse::Dtmc const& dtmc) { process(dtmc); @@ -22,6 +23,25 @@ namespace storm { return this->graphPreservingConstraintSet; } + template + void ConstraintCollector::wellformedRequiresNonNegativeEntries(std::vector const& vec) { + for(auto const& entry : vec) { + if (!storm::utility::isConstant(entry)) { + if (entry.denominator().isConstant()) { + if (entry.denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace(entry.nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (entry.denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace(entry.nominator().polynomial(), storm::CompareRelation::LEQ); + } else { + assert(false); // Should fail before. + } + } else { + wellformedConstraintSet.emplace(entry.denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + } + } + } + } template void ConstraintCollector::process(storm::models::sparse::Dtmc const& dtmc) { @@ -42,7 +62,7 @@ namespace storm { } } else { wellformedConstraintSet.emplace(transition.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at edges not yet supported."); + wellformedConstraintSet.emplace(carl::FormulaType::ITE, typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GREATER), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::GEQ), typename ConstraintType::val(transition.getValue().nominator().polynomial(), storm::CompareRelation::LEQ)); } graphPreservingConstraintSet.emplace(transition.getValue().nominator().polynomial(), storm::CompareRelation::NEQ); } @@ -55,37 +75,25 @@ namespace storm { } for(auto const& rewModelEntry : dtmc.getRewardModels()) { if (rewModelEntry.second.hasStateRewards()) { - for(auto const& stateReward : rewModelEntry.second.getStateRewardVector()) { - if (!storm::utility::isConstant(stateReward)) { - if (stateReward.denominator().isConstant()) { - if (stateReward.denominatorAsNumber() > 0) { - wellformedConstraintSet.emplace(stateReward.nominator().polynomial(), storm::CompareRelation::GEQ); - } else if (stateReward.denominatorAsNumber() < 0) { - wellformedConstraintSet.emplace(stateReward.nominator().polynomial(), storm::CompareRelation::LEQ); - } else { - assert(false); // Should fail before. - } - } else { - wellformedConstraintSet.emplace(stateReward.denominator().polynomial(), storm::CompareRelation::NEQ); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); - } - } - } + wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateRewardVector()); } if (rewModelEntry.second.hasStateActionRewards()) { - for(auto const& saReward : rewModelEntry.second.getStateActionRewardVector()) { - if (!storm::utility::isConstant(saReward)) { - if (saReward.denominator().isConstant()) { - if (saReward.denominatorAsNumber() > 0) { - wellformedConstraintSet.emplace(saReward.nominator().polynomial(), storm::CompareRelation::GEQ); - } else if (saReward.denominatorAsNumber() < 0) { - wellformedConstraintSet.emplace(saReward.nominator().polynomial(), storm::CompareRelation::LEQ); + wellformedRequiresNonNegativeEntries(rewModelEntry.second.getStateActionRewardVector()); + } + if (rewModelEntry.second.hasTransitionRewards()) { + for (auto const& entry : rewModelEntry.second.getTransitionRewardMatrix()) { + if(!entry.getValue().isConstant()) { + if (entry.getValue().denominator().isConstant()) { + if (entry.getValue().denominatorAsNumber() > 0) { + wellformedConstraintSet.emplace(entry.getValue().nominator().polynomial(), storm::CompareRelation::GEQ); + } else if (entry.getValue().denominatorAsNumber() < 0) { + wellformedConstraintSet.emplace(entry.getValue().nominator().polynomial(), storm::CompareRelation::LEQ); } else { assert(false); // Should fail before. } } else { - wellformedConstraintSet.emplace(saReward.denominator().polynomial(), storm::CompareRelation::NEQ); - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at state rewards not yet supported."); + wellformedConstraintSet.emplace(entry.getValue().denominator().polynomial(), storm::CompareRelation::NEQ); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Rational functions at transition rewards are not yet supported."); } } } diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h index 14bdd994f..4bcf1a00a 100644 --- a/src/storm/analysis/GraphConditions.h +++ b/src/storm/analysis/GraphConditions.h @@ -31,6 +31,7 @@ private: // on the parameter values. std::unordered_set::val> graphPreservingConstraintSet; + void wellformedRequiresNonNegativeEntries(std::vector const&); public: /*! * Constructs the a constraint collector for the given DTMC. The constraints are built and ready for From f72200bd2c8d3bea4b6820d90f92296e03aa4012 Mon Sep 17 00:00:00 2001 From: sjunges Date: Mon, 15 May 2017 23:24:29 +0200 Subject: [PATCH 17/22] - removed deprecated option USE_CARL (now a variable). - changed behaviour of POPCNT: we usually rely on march=native which uses popcnt if available, and now can force its usuage in other situations --- CMakeLists.txt | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 64c2c6ac7..024fc9689 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -27,12 +27,13 @@ option(STORM_USE_LTO "Sets whether link-time optimizations are enabled." ON) MARK_AS_ADVANCED(STORM_USE_LTO) option(STORM_PORTABLE "Sets whether a build needs to be portable." OFF) MARK_AS_ADVANCED(STORM_PORTABLE) -option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) -MARK_AS_ADVANCED(STORM_USE_POPCNT) +# Force POPCNT is helpful for portable code targetting platforms with SSE4.2 operation support. +option(STORM_FORCE_POPCNT "Sets whether the popcnt instruction is forced to be used (advanced)." OFF) +MARK_AS_ADVANCED(STORM_FORCE_POPCNT) option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF) option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF) option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF) -option(USE_CARL "Sets whether carl should be included." ON) +set(USE_CARL ON) option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF) MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL) option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF) @@ -198,7 +199,7 @@ endif() ## Compiler independent settings ## ############################################################# -if (STORM_USE_POPCNT) +if (STORM_FORCE_POPCNT) set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt") endif() From 8a7609fb83a8aeac6f421f3e6c90b7a0fd45b4fb Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 17 May 2017 09:51:24 +0200 Subject: [PATCH 18/22] fixed Rmin computation with exact sparse engine when very high rewards occur --- .../prctl/helper/SparseMdpPrctlHelper.cpp | 56 +++++++++++-------- src/storm/storage/SparseMatrix.cpp | 21 +++++++ src/storm/storage/SparseMatrix.h | 11 ++++ src/storm/utility/vector.h | 12 ++++ 4 files changed, 77 insertions(+), 23 deletions(-) diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 73fa080c0..b4d818ad2 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -378,25 +378,20 @@ namespace storm { if (!maybeStates.empty()) { // In this case we have to compute the reward values for the remaining states. - // We can eliminate the rows and columns from the original transition probability matrix for states - // whose reward values are already known. - storm::storage::SparseMatrix submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); - - // Prepare the right-hand side of the equation system. - std::vector b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); - - // Since we are cutting away target and infinity states, we need to account for this by giving - // choices the value infinity that have some successor contained in the infinity states. - uint_fast64_t currentRow = 0; - for (auto state : maybeStates) { - for (uint_fast64_t row = nondeterministicChoiceIndices[state]; row < nondeterministicChoiceIndices[state + 1]; ++row, ++currentRow) { - for (auto const& element : transitionMatrix.getRow(row)) { - if (infinityStates.get(element.getColumn())) { - b[currentRow] = storm::utility::infinity(); - break; - } - } - } + // Prepare matrix and vector for the equation system. + storm::storage::SparseMatrix submatrix; + std::vector b; + // Remove rows and columns from the original transition probability matrix for states whose reward values are already known. + // If there are infinity states, we additionaly have to remove choices of maybeState that lead to infinity + boost::optional selectedChoices; // if not given, all maybeState choices are selected + if (infinityStates.empty()) { + submatrix = transitionMatrix.getSubmatrix(true, maybeStates, maybeStates, false); + b = totalStateRewardVectorGetter(submatrix.getRowCount(), transitionMatrix, maybeStates); + } else { + selectedChoices = transitionMatrix.getRowFilter(maybeStates, ~infinityStates); + submatrix = transitionMatrix.getSubmatrix(false, *selectedChoices, maybeStates, false); + b = totalStateRewardVectorGetter(transitionMatrix.getRowCount(), transitionMatrix, storm::storage::BitVector(transitionMatrix.getRowGroupCount(), true)); + storm::utility::vector::filterVectorInPlace(b, *selectedChoices); } bool skipEcWithinMaybeStatesCheck = !goal.minimize() || (hint.isExplicitModelCheckerHint() && hint.asExplicitModelCheckerHint().getNoEndComponentsInMaybeStates()); @@ -408,10 +403,25 @@ namespace storm { if (produceScheduler) { storm::storage::Scheduler const& subscheduler = *resultForMaybeStates.scheduler; - uint_fast64_t currentSubState = 0; - for (auto maybeState : maybeStates) { - scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); - ++currentSubState; + if (selectedChoices) { + uint_fast64_t currentSubState = 0; + for (auto maybeState : maybeStates) { + uint_fast64_t subChoice = subscheduler.getChoice(currentSubState); + // find the rowindex that corresponds to the selected row of the submodel + uint_fast64_t firstRowIndex = transitionMatrix.getRowGroupIndices()[maybeState]; + uint_fast64_t selectedRowIndex = selectedChoices->getNextSetIndex(firstRowIndex); + for (uint_fast64_t choice = 0; choice < subChoice; ++choice) { + selectedRowIndex = selectedChoices->getNextSetIndex(selectedRowIndex + 1); + } + scheduler->setChoice(maybeState, selectedRowIndex - firstRowIndex); + ++currentSubState; + } + } else { + uint_fast64_t currentSubState = 0; + for (auto maybeState : maybeStates) { + scheduler->setChoice(maybeState, subscheduler.getChoice(currentSubState)); + ++currentSubState; + } } } } diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index d71fa7ba4..36319b394 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -565,6 +565,27 @@ namespace storm { return res; } + template + storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraint) const { + storm::storage::BitVector result(this->getRowCount(), false); + for (auto const& group : groupConstraint) { + uint_fast64_t const endOfGroup = this->getRowGroupIndices()[group + 1]; + for (uint_fast64_t row = this->getRowGroupIndices()[group]; row < endOfGroup; ++row) { + bool choiceSatisfiesColumnConstraint = true; + for (auto const& entry : this->getRow(row)) { + if (!columnConstraint.get(entry.getColumn())) { + choiceSatisfiesColumnConstraint = false; + break; + } + } + if (choiceSatisfiesColumnConstraint) { + result.set(row, true); + } + } + } + return result; + } + template void SparseMatrix::makeRowsAbsorbing(storm::storage::BitVector const& rows) { for (auto row : rows) { diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 686574518..8aab0d397 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -571,6 +571,17 @@ namespace storm { */ storm::storage::BitVector getRowIndicesOfRowGroups(storm::storage::BitVector const& groups) const; + /*! + * Returns the indices of all rows that + * * are in a selected group and + * * only have entries within the selected columns. + * + * @param groupConstraint the selected groups + * @param columnConstraints the selected columns + * @return a bit vector that is true at position i iff row i satisfies the constraints. + */ + storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint, storm::storage::BitVector const& columnConstraints) const; + /*! * This function makes the given rows absorbing. * diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 9482d35b2..c26c17774 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -859,6 +859,18 @@ namespace storm { return result; } + template + void filterVectorInPlace(std::vector& v, storm::storage::BitVector const& filter) { + STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector"); + auto vIt = v.begin(); + for(auto index : filter) { + *vIt = std::move(v[index]); + ++vIt; + } + v.resize(vIt - v.begin()); + STORM_LOG_ASSERT(v.size() == filter.getNumberOfSetBits(), "Result does not match."); + } + template bool hasNegativeEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return value < storm::utility::zero();}); From 4413afb5422dcd1df4c385045446273bd36c52da Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 May 2017 09:49:32 +0200 Subject: [PATCH 19/22] used new helper functions at some points in the code --- .../pcaa/SparseMaPcaaWeightVectorChecker.cpp | 2 +- .../SparseMdpParameterLiftingModelChecker.cpp | 16 ++++------------ src/storm/models/sparse/MarkovAutomaton.cpp | 6 +++--- src/storm/storage/SparseMatrix.cpp | 7 ++++--- src/storm/storage/SparseMatrix.h | 2 +- .../nativepolytopeconversion/QuickHull.cpp | 4 ++-- src/storm/transformer/GoalStateMerger.cpp | 11 ++++++----- .../SparseParametricModelSimplifier.cpp | 4 ++-- src/storm/utility/vector.h | 13 ++++++++++--- 9 files changed, 33 insertions(+), 32 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp index 45d99f003..d06b3ce40 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp @@ -102,7 +102,7 @@ namespace storm { storm::storage::BitVector probabilisticStates = ~this->model.getMarkovianStates(); result.states = createMS ? this->model.getMarkovianStates() : probabilisticStates; - result.choices = this->model.getTransitionMatrix().getRowIndicesOfRowGroups(result.states); + result.choices = this->model.getTransitionMatrix().getRowFilter(result.states); STORM_LOG_ASSERT(!createMS || result.states.getNumberOfSetBits() == result.choices.getNumberOfSetBits(), "row groups for Markovian states should consist of exactly one row"); //We need to add diagonal entries for selfloops on Markovian states. diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp index 066a5f1b7..d9e2610fe 100644 --- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp +++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp @@ -69,7 +69,7 @@ namespace storm { // Create the vector of one-step probabilities to go to target states. std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), psiStates); - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates), maybeStates); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); computePlayer1Matrix(); applyPreviousResultAsHint = false; @@ -104,7 +104,7 @@ namespace storm { // Create the vector of one-step probabilities to go to target states. std::vector b = this->parametricModel.getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), statesWithProbability01.second); - parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates), maybeStates); + parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates); computePlayer1Matrix(); // Check whether there is an EC consisting of maybestates @@ -146,16 +146,8 @@ namespace storm { std::vector b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix()); // We need to handle choices that lead to an infinity state. - // As a maybeState does not have reward infinity, such a choice will never be picked. Hence, we can unselect the corresponding rows - storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates); - for (uint_fast64_t row : selectedRows) { - for (auto const& element : this->parametricModel.getTransitionMatrix().getRow(row)) { - if (infinityStates.get(element.getColumn())) { - selectedRows.set(row, false); - break; - } - } - } + // As a maybeState does not have reward infinity, a choice leading to an infinity state will never be picked. Hence, we can unselect the corresponding rows + storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates); parameterLifter = std::make_unique>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates); computePlayer1Matrix(); diff --git a/src/storm/models/sparse/MarkovAutomaton.cpp b/src/storm/models/sparse/MarkovAutomaton.cpp index f0eb0fc39..88a77b43d 100644 --- a/src/storm/models/sparse/MarkovAutomaton.cpp +++ b/src/storm/models/sparse/MarkovAutomaton.cpp @@ -140,14 +140,14 @@ namespace storm { this->getTransitionMatrix() = this->getTransitionMatrix().restrictRows(keptChoices); for(auto& rewModel : this->getRewardModels()) { if(rewModel.second.hasStateActionRewards()) { - rewModel.second.getStateActionRewardVector() = storm::utility::vector::filterVector(rewModel.second.getStateActionRewardVector(), keptChoices); + storm::utility::vector::filterVectorInPlace(rewModel.second.getStateActionRewardVector(), keptChoices); } if(rewModel.second.hasTransitionRewards()) { rewModel.second.getTransitionRewardMatrix() = rewModel.second.getTransitionRewardMatrix().restrictRows(keptChoices); } } if(this->hasChoiceLabeling()) { - this->getOptionalChoiceLabeling() = storm::utility::vector::filterVector(this->getOptionalChoiceLabeling().get(), keptChoices); + storm::utility::vector::filterVectorInPlace(this->getOptionalChoiceLabeling().get(), keptChoices); } // Mark the automaton as closed. @@ -329,7 +329,7 @@ namespace storm { storm::models::sparse::StateLabeling stateLabeling = this->getStateLabeling().getSubLabeling(keepStates); boost::optional> optionalChoiceLabeling = this->getOptionalChoiceLabeling(); if (optionalChoiceLabeling) { - optionalChoiceLabeling = storm::utility::vector::filterVector(optionalChoiceLabeling.get(), keepStates); + storm::utility::vector::filterVectorInPlace(optionalChoiceLabeling.get(), keepStates); } //TODO update reward models according to kept states STORM_LOG_WARN_COND(this->getRewardModels().empty(), "Conversion of MA to CTMC does not preserve rewards."); diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 36319b394..d481f7063 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/src/storm/storage/SparseMatrix.cpp @@ -555,10 +555,11 @@ namespace storm { } template - storm::storage::BitVector SparseMatrix::getRowIndicesOfRowGroups(storm::storage::BitVector const& groups) const { + storm::storage::BitVector SparseMatrix::getRowFilter(storm::storage::BitVector const& groupConstraint) const { storm::storage::BitVector res(this->getRowCount(), false); - for(auto group : groups) { - for(uint_fast64_t row = this->getRowGroupIndices()[group]; row < this->getRowGroupIndices()[group+1]; ++row) { + for(auto group : groupConstraint) { + uint_fast64_t const endOfGroup = this->getRowGroupIndices()[group + 1]; + for(uint_fast64_t row = this->getRowGroupIndices()[group]; row < endOfGroup; ++row) { res.set(row, true); } } diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h index 8aab0d397..cf9211849 100644 --- a/src/storm/storage/SparseMatrix.h +++ b/src/storm/storage/SparseMatrix.h @@ -569,7 +569,7 @@ namespace storm { * @param groups the selected row groups * @return a bit vector that is true at position i iff the row group of row i is selected. */ - storm::storage::BitVector getRowIndicesOfRowGroups(storm::storage::BitVector const& groups) const; + storm::storage::BitVector getRowFilter(storm::storage::BitVector const& groupConstraint) const; /*! * Returns the indices of all rows that diff --git a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp index 2f6e524f9..edd19d833 100644 --- a/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp +++ b/src/storm/storage/geometry/nativepolytopeconversion/QuickHull.cpp @@ -173,7 +173,7 @@ namespace storm { } } } - points = storm::utility::vector::filterVector(points, keptPoints); + storm::utility::vector::filterVectorInPlace(points, keptPoints); if (generateRelevantVerticesAndVertexSets) { storm::storage::BitVector keptVertices(relevantVertices.size(), true); @@ -185,7 +185,7 @@ namespace storm { } } } - relevantVertices = storm::utility::vector::filterVector(relevantVertices, keptVertices); + storm::utility::vector::filterVectorInPlace(relevantVertices, keptVertices); STORM_LOG_WARN("Can not retrieve vertex sets for degenerated polytope (not implemented)"); vertexSets.clear(); diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp index f7ccc7f19..f9b81f3f6 100644 --- a/src/storm/transformer/GoalStateMerger.cpp +++ b/src/storm/transformer/GoalStateMerger.cpp @@ -46,11 +46,12 @@ namespace storm { // Get the reward models std::unordered_map rewardModels; for (auto rewardModelName : selectedRewardModels) { - auto origTotalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix()); - auto transitionsOfMaybeStates = originalModel.getTransitionMatrix().getRowIndicesOfRowGroups(maybeStates); - auto resTotalRewards = storm::utility::vector::filterVector(origTotalRewards, transitionsOfMaybeStates); - resTotalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero()); - rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, resTotalRewards))); + auto totalRewards = originalModel.getRewardModel(rewardModelName).getTotalRewardVector(originalModel.getTransitionMatrix()); + auto choicesOfMaybeStates = originalModel.getTransitionMatrix().getRowFilter(maybeStates); + storm::utility::vector::filterVectorInPlace(totalRewards, choicesOfMaybeStates); + // add zero reward for the sink and goal states (if they exists) + totalRewards.resize(transitionMatrix.getRowCount(), storm::utility::zero()); + rewardModels.insert(std::make_pair(rewardModelName, typename SparseModelType::RewardModelType(boost::none, totalRewards))); } // modify the given target and sink states diff --git a/src/storm/transformer/SparseParametricModelSimplifier.cpp b/src/storm/transformer/SparseParametricModelSimplifier.cpp index 54fba2338..2dd62ce6b 100644 --- a/src/storm/transformer/SparseParametricModelSimplifier.cpp +++ b/src/storm/transformer/SparseParametricModelSimplifier.cpp @@ -138,13 +138,13 @@ namespace storm { stateEliminator.eliminateState(state, true); } selectedStates.complement(); - auto keptRows = sparseMatrix.getRowIndicesOfRowGroups(selectedStates); + auto keptRows = sparseMatrix.getRowFilter(selectedStates); storm::storage::SparseMatrix newTransitionMatrix = flexibleMatrix.createSparseMatrix(keptRows, selectedStates); // obtain the reward model for the resulting system std::unordered_map rewardModels; if(rewardModelName) { - actionRewards = storm::utility::vector::filterVector(actionRewards, keptRows); + storm::utility::vector::filterVectorInPlace(actionRewards, keptRows); rewardModels.insert(std::make_pair(*rewardModelName, typename SparseModelType::RewardModelType(boost::none, std::move(actionRewards)))); } diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index c26c17774..6bf06a4f9 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -863,8 +863,15 @@ namespace storm { void filterVectorInPlace(std::vector& v, storm::storage::BitVector const& filter) { STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector"); auto vIt = v.begin(); - for(auto index : filter) { - *vIt = std::move(v[index]); + auto filterIt = filter.begin(); + // get the first position where the filter has a 0. + // Note that we do not have to modify the entries of v on all positions before + for (uint_fast64_t i = 0; i == *filterIt && filterIt != filter.end(); ++i) { + ++filterIt; + ++vIt; + } + for (; filterIt != filter.end(); ++filterIt) { + *vIt = std::move(v[*filterIt]); ++vIt; } v.resize(vIt - v.begin()); @@ -875,7 +882,7 @@ namespace storm { bool hasNegativeEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return value < storm::utility::zero();}); } - + template bool hasPositiveEntry(std::vector const& v){ return std::any_of(v.begin(), v.end(), [](T value){return value > storm::utility::zero();}); From 25074b50a9094e374d71dc941976fb4ee516ae29 Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 May 2017 10:54:38 +0200 Subject: [PATCH 20/22] Added function to get the next unset bit in a bitvector --- src/storm/storage/BitVector.cpp | 90 +++++++++++++++++++++--------- src/storm/storage/BitVector.h | 16 +++++- src/storm/utility/vector.h | 23 ++++---- src/test/storage/BitVectorTest.cpp | 15 +++++ 4 files changed, 104 insertions(+), 40 deletions(-) diff --git a/src/storm/storage/BitVector.cpp b/src/storm/storage/BitVector.cpp index a0004263a..532e923e3 100644 --- a/src/storm/storage/BitVector.cpp +++ b/src/storm/storage/BitVector.cpp @@ -22,7 +22,7 @@ namespace storm { BitVector::const_iterator::const_iterator(uint64_t const* dataPtr, uint_fast64_t startIndex, uint_fast64_t endIndex, bool setOnFirstBit) : dataPtr(dataPtr), endIndex(endIndex) { if (setOnFirstBit) { // Set the index of the first set bit in the vector. - currentIndex = getNextSetIndex(dataPtr, startIndex, endIndex); + currentIndex = getNextIndexWithValue(true, dataPtr, startIndex, endIndex); } else { currentIndex = startIndex; } @@ -43,13 +43,13 @@ namespace storm { } BitVector::const_iterator& BitVector::const_iterator::operator++() { - currentIndex = getNextSetIndex(dataPtr, ++currentIndex, endIndex); + currentIndex = getNextIndexWithValue(true, dataPtr, ++currentIndex, endIndex); return *this; } BitVector::const_iterator& BitVector::const_iterator::operator+=(size_t n) { for(size_t i = 0; i < n; ++i) { - currentIndex = getNextSetIndex(dataPtr, ++currentIndex, endIndex); + currentIndex = getNextIndexWithValue(true, dataPtr, ++currentIndex, endIndex); } return *this; } @@ -628,10 +628,17 @@ namespace storm { } uint_fast64_t BitVector::getNextSetIndex(uint_fast64_t startingIndex) const { - return getNextSetIndex(buckets, startingIndex, bitCount); + return getNextIndexWithValue(true, buckets, startingIndex, bitCount); } - uint_fast64_t BitVector::getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) { + uint_fast64_t BitVector::getNextUnsetIndex(uint_fast64_t startingIndex) const { +#ifdef ASSERT_BITVECTOR + STORM_LOG_ASSERT(getNextIndexWithValue(false, buckets, startingIndex, bitCount) == (~(*this)).getNextSetIndex(startingIndex), "The result is inconsistent with the next set index of the complement of this bitvector"); +#endif + return getNextIndexWithValue(false, buckets, startingIndex, bitCount); + } + + uint_fast64_t BitVector::getNextIndexWithValue(bool value, uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex) { uint_fast8_t currentBitInByte = startingIndex & mod64mask; uint64_t const* bucketIt = dataPtr + (startingIndex >> 6); startingIndex = (startingIndex >> 6 << 6); @@ -642,31 +649,62 @@ namespace storm { } else { mask = (1ull << (64 - currentBitInByte)) - 1ull; } - while (startingIndex < endIndex) { - // Compute the remaining bucket content. - uint64_t remainingInBucket = *bucketIt & mask; - - // Check if there is at least one bit in the remainder of the bucket that is set to true. - if (remainingInBucket != 0) { - // As long as the current bit is not set, move the current bit. - while ((remainingInBucket & (1ull << (63 - currentBitInByte))) == 0) { - ++currentBitInByte; + + // For efficiency reasons, we branch on the desired value at this point + if (value) { + while (startingIndex < endIndex) { + // Compute the remaining bucket content. + uint64_t remainingInBucket = *bucketIt & mask; + + // Check if there is at least one bit in the remainder of the bucket that is set to true. + if (remainingInBucket != 0) { + // As long as the current bit is not set, move the current bit. + while ((remainingInBucket & (1ull << (63 - currentBitInByte))) == 0) { + ++currentBitInByte; + } + + // Only return the index of the set bit if we are still in the valid range. + if (startingIndex + currentBitInByte < endIndex) { + return startingIndex + currentBitInByte; + } else { + return endIndex; + } } - - // Only return the index of the set bit if we are still in the valid range. - if (startingIndex + currentBitInByte < endIndex) { - return startingIndex + currentBitInByte; - } else { - return endIndex; + + // Advance to the next bucket. + startingIndex += 64; + ++bucketIt; + mask = -1ull; + currentBitInByte = 0; + } + } else { + while (startingIndex < endIndex) { + // Compute the remaining bucket content. + uint64_t remainingInBucket = *bucketIt & mask; + + // Check if there is at least one bit in the remainder of the bucket that is set to false. + if (remainingInBucket != (-1ull & mask)) { + // As long as the current bit is not false, move the current bit. + while ((remainingInBucket & (1ull << (63 - currentBitInByte))) != 0) { + ++currentBitInByte; + } + + // Only return the index of the set bit if we are still in the valid range. + if (startingIndex + currentBitInByte < endIndex) { + return startingIndex + currentBitInByte; + } else { + return endIndex; + } } + + // Advance to the next bucket. + startingIndex += 64; + ++bucketIt; + mask = -1ull; + currentBitInByte = 0; } - - // Advance to the next bucket. - startingIndex += 64; - ++bucketIt; - mask = -1ull; - currentBitInByte = 0; } + return endIndex; } diff --git a/src/storm/storage/BitVector.h b/src/storm/storage/BitVector.h index ecdd03536..dccfa0830 100644 --- a/src/storm/storage/BitVector.h +++ b/src/storm/storage/BitVector.h @@ -477,6 +477,17 @@ namespace storm { */ uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const; + /* + * Retrieves the index of the bit that is the next bit set to false in the bit vector. If there is none, + * this function returns the number of bits this vector holds in total. Put differently, if the return + * value is equal to a call to size(), then there is no unset bit after the specified position. + * + * @param startingIndex The index at which to start the search for the next bit that is not set. The + * bit at this index itself is included in the search range. + * @return The index of the next bit that is set after the given index. + */ + uint_fast64_t getNextUnsetIndex(uint_fast64_t startingIndex) const; + /* * Compare two intervals [start1, start1+length] and [start2, start2+length] and swap them if the second * one is larger than the first one. After the method the intervals are sorted in decreasing order. @@ -502,15 +513,16 @@ namespace storm { BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount); /*! - * Retrieves the index of the next bit that is set to true after (and including) the given starting index. + * Retrieves the index of the next bit that is set to the given value after (and including) the given starting index. * + * @param value the value of the bit whose index is to be found. * @param dataPtr A pointer to the first bucket of the data storage. * @param startingIndex The index where to start the search. * @param endIndex The index at which to stop the search. * @return The index of the bit that is set after the given starting index, but before the given end index * in the given bit vector or endIndex in case the end index was reached. */ - static uint_fast64_t getNextSetIndex(uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex); + static uint_fast64_t getNextIndexWithValue(bool value, uint64_t const* dataPtr, uint_fast64_t startingIndex, uint_fast64_t endIndex); /*! * Truncate the last bucket so that no bits are set starting from bitCount. diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h index 6bf06a4f9..76fc58a5c 100644 --- a/src/storm/utility/vector.h +++ b/src/storm/utility/vector.h @@ -862,19 +862,18 @@ namespace storm { template void filterVectorInPlace(std::vector& v, storm::storage::BitVector const& filter) { STORM_LOG_ASSERT(v.size() == filter.size(), "The filter size does not match the size of the input vector"); - auto vIt = v.begin(); - auto filterIt = filter.begin(); - // get the first position where the filter has a 0. - // Note that we do not have to modify the entries of v on all positions before - for (uint_fast64_t i = 0; i == *filterIt && filterIt != filter.end(); ++i) { - ++filterIt; - ++vIt; - } - for (; filterIt != filter.end(); ++filterIt) { - *vIt = std::move(v[*filterIt]); - ++vIt; + uint_fast64_t size = v.size(); + // we can start our work at the first index where the filter has value zero + uint_fast64_t firstUnsetIndex = filter.getNextUnsetIndex(0); + if (firstUnsetIndex < size) { + auto vIt = v.begin() + firstUnsetIndex; + for (uint_fast64_t index = filter.getNextSetIndex(firstUnsetIndex + 1); index != size; index = filter.getNextSetIndex(index + 1)) { + *vIt = std::move(v[index]); + ++vIt; + } + v.resize(vIt - v.begin()); + v.shrink_to_fit(); } - v.resize(vIt - v.begin()); STORM_LOG_ASSERT(v.size() == filter.getNumberOfSetBits(), "Result does not match."); } diff --git a/src/test/storage/BitVectorTest.cpp b/src/test/storage/BitVectorTest.cpp index 9d2fd60c5..0bb9847f6 100644 --- a/src/test/storage/BitVectorTest.cpp +++ b/src/test/storage/BitVectorTest.cpp @@ -482,6 +482,21 @@ TEST(BitVectorTest, NextSetIndex) { ASSERT_EQ(vector.size(), vector.getNextSetIndex(18)); } +TEST(BitVectorTest, NextUnsetIndex) { + storm::storage::BitVector vector(32); + + vector.set(14); + vector.set(17); + + vector.complement(); + + ASSERT_EQ(14ul, vector.getNextUnsetIndex(14)); + ASSERT_EQ(17ul, vector.getNextUnsetIndex(15)); + ASSERT_EQ(17ul, vector.getNextUnsetIndex(16)); + ASSERT_EQ(17ul, vector.getNextUnsetIndex(17)); + ASSERT_EQ(vector.size(), vector.getNextUnsetIndex(18)); +} + TEST(BitVectorTest, Iterator) { storm::storage::BitVector vector(32); From cb90600abb5ac77e93f31225c7e82c2d460430cf Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 18 May 2017 10:54:53 +0200 Subject: [PATCH 21/22] Silenced a warning --- src/storm/logic/VariableSubstitutionVisitor.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index 758147c28..96ede4769 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -50,11 +50,11 @@ namespace storm { return std::static_pointer_cast(std::make_shared(left, right, lowerBound, upperBound, f.getTimeBoundType())); } - boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const { + boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(storm::logic::TimeBound(f.isBoundStrict(), f.getBound().substitute(substitution)), f.getTimeBoundType())); } - boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const { + boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const { return std::static_pointer_cast(std::make_shared(f.getBound().substitute(substitution), f.getTimeBoundType())); } From c595fee4dc139c5cb58f54afba5cc507c8198aa5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 19 May 2017 13:04:16 +0200 Subject: [PATCH 22/22] removed some unnecessary transition insertions in parser --- .../DeterministicSparseTransitionParser.cpp | 75 +------------------ .../DeterministicSparseTransitionParser.h | 3 +- 2 files changed, 3 insertions(+), 75 deletions(-) diff --git a/src/storm/parser/DeterministicSparseTransitionParser.cpp b/src/storm/parser/DeterministicSparseTransitionParser.cpp index 9aacb7e4c..94a66b066 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.cpp +++ b/src/storm/parser/DeterministicSparseTransitionParser.cpp @@ -46,8 +46,7 @@ namespace storm { char const* buf = file.getData(); // Perform first pass, i.e. count entries that are not zero. - bool insertDiagonalEntriesIfMissing = !isRewardFile; - DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData(), insertDiagonalEntriesIfMissing); + DeterministicSparseTransitionParser::FirstPassResult firstPass = DeterministicSparseTransitionParser::firstPass(file.getData()); STORM_LOG_TRACE("First pass on " << filename << " shows " << firstPass.numberOfNonzeroEntries << " non-zeros."); @@ -85,7 +84,6 @@ namespace storm { double val; bool dontFixDeadlocks = storm::settings::getModule().isDontFixDeadlocksSet(); bool hadDeadlocks = false; - bool rowHadDiagonalEntry = false; // Read all transitions from file. Note that we assume that the // transitions are listed in canonical order, otherwise this will not @@ -131,16 +129,6 @@ namespace storm { // Test if we moved to a new row. // Handle all incomplete or skipped rows. if (lastRow != row) { - if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero()); - STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (1)"); - } else { - STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); - } - // No increment for lastRow. - rowHadDiagonalEntry = true; - } for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { hadDeadlocks = true; if (!dontFixDeadlocks) { @@ -152,36 +140,12 @@ namespace storm { } } lastRow = row; - rowHadDiagonalEntry = false; - } - - if (col == row) { - rowHadDiagonalEntry = true; - } - - if (col > row && !rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(row, row, storm::utility::zero()); - STORM_LOG_DEBUG("While parsing " << filename << ": state " << row << " has no transition to itself. Inserted a 0-transition. (2)"); - } else { - STORM_LOG_WARN("Warning while parsing " << filename << ": state " << row << " has no transition to itself."); - } - rowHadDiagonalEntry = true; } resultMatrix.addNextValue(row, col, val); buf = trimWhitespaces(buf); } - if (!rowHadDiagonalEntry) { - if (insertDiagonalEntriesIfMissing) { - resultMatrix.addNextValue(lastRow, lastRow, storm::utility::zero()); - STORM_LOG_DEBUG("While parsing " << filename << ": state " << lastRow << " has no transition to itself. Inserted a 0-transition. (3)"); - } else { - STORM_LOG_WARN("Warning while parsing " << filename << ": state " << lastRow << " has no transition to itself."); - } - } - // If we encountered deadlock and did not fix them, now is the time to throw the exception. if (dontFixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFormatException() << "Some of the states do not have outgoing transitions."; } @@ -199,7 +163,7 @@ namespace storm { } template - typename DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf, bool insertDiagonalEntriesIfMissing) { + typename DeterministicSparseTransitionParser::FirstPassResult DeterministicSparseTransitionParser::firstPass(char const* buf) { DeterministicSparseTransitionParser::FirstPassResult result; @@ -231,30 +195,6 @@ namespace storm { // The actual read value is not needed here. checked_strtod(buf, &buf); - // Compensate for missing diagonal entries if desired. - if (insertDiagonalEntriesIfMissing) { - if (lastRow != row) { - if (!rowHadDiagonalEntry) { - ++result.numberOfNonzeroEntries; - } - - // Compensate for missing rows. - for (uint_fast64_t skippedRow = lastRow + 1; skippedRow < row; ++skippedRow) { - ++result.numberOfNonzeroEntries; - } - rowHadDiagonalEntry = false; - } - - if (col == row) { - rowHadDiagonalEntry = true; - } - - if (col > row && !rowHadDiagonalEntry) { - rowHadDiagonalEntry = true; - ++result.numberOfNonzeroEntries; - } - } - // Check if a higher state id was found. if (row > result.highestStateIndex) result.highestStateIndex = row; if (col > result.highestStateIndex) result.highestStateIndex = col; @@ -273,17 +213,6 @@ namespace storm { buf = trimWhitespaces(buf); } - if (insertDiagonalEntriesIfMissing) { - if (!rowHadDiagonalEntry) { - ++result.numberOfNonzeroEntries; - } - - //Compensate for missing rows at the end of the file. - for (uint_fast64_t skippedRow = (uint_fast64_t) (lastRow + 1); skippedRow <= result.highestStateIndex; ++skippedRow) { - ++result.numberOfNonzeroEntries; - } - } - return result; } diff --git a/src/storm/parser/DeterministicSparseTransitionParser.h b/src/storm/parser/DeterministicSparseTransitionParser.h index 0515e120a..0d830d2f9 100644 --- a/src/storm/parser/DeterministicSparseTransitionParser.h +++ b/src/storm/parser/DeterministicSparseTransitionParser.h @@ -65,10 +65,9 @@ namespace storm { * transitions and the maximum node id. * * @param buffer The buffer that contains the input. - * @param insertDiagonalEntriesIfMissing A flag set iff entries on the primary diagonal of the matrix should be added in case they are missing in the parsed file. * @return A structure representing the result of the first pass. */ - static FirstPassResult firstPass(char const* buffer, bool insertDiagonalEntriesIfMissing = true); + static FirstPassResult firstPass(char const* buffer); /* * The main parsing routine.