Browse Source

Started refactoring Markov automaton model checker.

Former-commit-id: c4278de4f0
tempestpy_adaptions
dehnert 11 years ago
parent
commit
0a89d65f93
  1. 6
      src/counterexamples/MILPMinimalLabelSetGenerator.h
  2. 6
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  3. 228
      src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
  4. 85
      src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
  5. 6
      src/solver/AbstractNondeterministicLinearEquationSolver.h
  6. 8
      src/solver/GmmxxNondeterministicLinearEquationSolver.h
  7. 21
      src/storm.cpp
  8. 25
      src/utility/solver.cpp
  9. 11
      src/utility/solver.h
  10. 600
      src/utility/vector.h
  11. 8
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  12. 8
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  13. 4
      test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
  14. 4
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

6
src/counterexamples/MILPMinimalLabelSetGenerator.h

@ -961,7 +961,7 @@ namespace storm {
// (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
double maximalReachabilityProbability = 0;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
@ -977,7 +977,7 @@ namespace storm {
ChoiceInformation choiceInformation = determineRelevantAndProblematicChoices(labeledMdp, stateInformation, psiStates);
// (4) Encode resulting system as MILP problem.
std::unique_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample");
std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("MinimalCommandSetCounterexample");
// (4.1) Create variables.
VariableInformation variableInformation = createVariables(*solver, labeledMdp, stateInformation, choiceInformation);
@ -1025,7 +1025,7 @@ namespace storm {
storm::property::prctl::AbstractPathFormula<double> const& pathFormula = probBoundFormula->getPathFormula();
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
try {
storm::property::prctl::Until<double> const& untilFormula = dynamic_cast<storm::property::prctl::Until<double> const&>(pathFormula);

6
src/counterexamples/SMTMinimalCommandSetGenerator.h

@ -1635,7 +1635,7 @@ namespace storm {
// (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set.
double maximalReachabilityProbability = 0;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
for (auto state : labeledMdp.getInitialStates()) {
maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]);
@ -1701,7 +1701,7 @@ namespace storm {
modelCheckingClock = std::chrono::high_resolution_clock::now();
commandSet.insert(relevancyInformation.knownLabels);
storm::models::Mdp<T> subMdp = labeledMdp.restrictChoiceLabels(commandSet);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(subMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(subMdp);
LOG4CPLUS_DEBUG(logger, "Invoking model checker.");
std::vector<T> result = modelchecker.checkUntil(false, phiStates, psiStates, false).first;
LOG4CPLUS_DEBUG(logger, "Computed model checking results.");
@ -1786,7 +1786,7 @@ namespace storm {
storm::property::prctl::AbstractPathFormula<double> const& pathFormula = probBoundFormula->getPathFormula();
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<T>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
try {
storm::property::prctl::Until<double> const& untilFormula = dynamic_cast<storm::property::prctl::Until<double> const&>(pathFormula);

228
src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h

@ -2,7 +2,6 @@
#define STORM_MODELCHECKER_CSL_SPARSEMARKOVAUTOMATONCSLMODELCHECKER_H_
#include <stack>
#include <iomanip>
#include "src/modelchecker/csl/AbstractModelChecker.h"
#include "src/models/MarkovAutomaton.h"
@ -22,7 +21,7 @@ namespace storm {
class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker<ValueType> {
public:
explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton<ValueType> const& model) : AbstractModelChecker<ValueType>(model), minimumOperatorStack() {
explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton<ValueType> const& model, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>()) : AbstractModelChecker<ValueType>(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) {
// Intentionally left empty.
}
@ -78,10 +77,10 @@ namespace storm {
// * a matrix aProbabilisticToMarkovian with all (non-discretized) transitions from probabilistic non-goal states to all Markovian non-goal states.
typename storm::storage::SparseMatrix<ValueType> aMarkovian = transitionMatrix.getSubmatrix(markovianNonGoalStates, nondeterministicChoiceIndices, true);
typename storm::storage::SparseMatrix<ValueType> aMarkovianToProbabilistic = transitionMatrix.getSubmatrix(markovianNonGoalStates, probabilisticNonGoalStates, nondeterministicChoiceIndices);
std::vector<uint_fast64_t> markovianNondeterministicChoiceIndices = computeNondeterministicChoiceIndicesForConstraint(nondeterministicChoiceIndices, markovianNonGoalStates);
std::vector<uint_fast64_t> markovianNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, markovianNonGoalStates);
typename storm::storage::SparseMatrix<ValueType> aProbabilistic = transitionMatrix.getSubmatrix(probabilisticNonGoalStates, nondeterministicChoiceIndices);
typename storm::storage::SparseMatrix<ValueType> aProbabilisticToMarkovian = transitionMatrix.getSubmatrix(probabilisticNonGoalStates, markovianNonGoalStates, nondeterministicChoiceIndices);
std::vector<uint_fast64_t> probabilisticNondeterministicChoiceIndices = computeNondeterministicChoiceIndicesForConstraint(nondeterministicChoiceIndices, probabilisticNonGoalStates);
std::vector<uint_fast64_t> probabilisticNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(nondeterministicChoiceIndices, probabilisticNonGoalStates);
// The matrices with transitions from Markovian states need to be digitized.
// Digitize aMarkovian. Based on whether the transition is a self-loop or not, we apply the two digitization rules.
@ -128,7 +127,7 @@ namespace storm {
}
}
std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
// Perform the actual value iteration
// * loop until the step bound has been reached
@ -234,9 +233,20 @@ namespace storm {
}
std::vector<ValueType> checkLongRunAverage(bool min, storm::storage::BitVector const& goalStates) const {
// Check whether the automaton is closed.
if (!this->getModel().isClosed()) {
throw storm::exceptions::InvalidArgumentException() << "Unable to compute long-run average on non-closed Markov automaton.";
}
// If there are no goal states, we avoid the computation and directly return zero.
if (goalStates.empty()) {
return std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::constGetZero<ValueType>());
}
// Likewise, if all bits are set, we can avoid the computation and set.
if ((~goalStates).empty()) {
return std::vector<ValueType>(this->getModel().getNumberOfStates(), storm::utility::constGetOne<ValueType>());
}
// Start by decomposing the Markov automaton into its MECs.
storm::storage::MaximalEndComponentDecomposition<double> mecDecomposition(this->getModel());
@ -245,7 +255,7 @@ namespace storm {
typename storm::storage::SparseMatrix<ValueType> const& transitionMatrix = this->getModel().getTransitionMatrix();
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
// Now compute the long-run average for all end components in isolation.
// Now start with compute the long-run average for all end components in isolation.
std::vector<ValueType> lraValuesForEndComponents;
// While doing so, we already gather some information for the following steps.
@ -255,67 +265,16 @@ namespace storm {
for (uint_fast64_t currentMecIndex = 0; currentMecIndex < mecDecomposition.size(); ++currentMecIndex) {
storm::storage::MaximalEndComponent const& mec = mecDecomposition[currentMecIndex];
std::unique_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("LRA for MEC " + std::to_string(currentMecIndex));
solver->setModelSense(min ? storm::solver::LpSolver::MAXIMIZE : storm::solver::LpSolver::MINIMIZE);
// First, we need to create the variables for the problem.
std::map<uint_fast64_t, uint_fast64_t> stateToVariableIndexMap;
for (auto const& stateChoicesPair : mec) {
stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0);
}
uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1);
// Now we encode the problem as constraints.
std::vector<uint_fast64_t> variables;
std::vector<double> coefficients;
// Gather information for later use.
for (auto const& stateChoicesPair : mec) {
uint_fast64_t state = stateChoicesPair.first;
// Gather information for later use.
statesInMecs.set(state);
stateToMecIndexMap[state] = currentMecIndex;
// Now, based on the type of the state, create a suitable constraint.
if (this->getModel().isMarkovianState(state)) {
variables.clear();
coefficients.clear();
variables.push_back(stateToVariableIndexMap.at(state));
coefficients.push_back(1);
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]);
for (auto element : row) {
variables.push_back(stateToVariableIndexMap.at(element.column()));
coefficients.push_back(-element.value());
}
variables.push_back(lraValueVariableIndex);
coefficients.push_back(storm::utility::constGetOne<ValueType>() / this->getModel().getExitRate(state));
solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constGetOne<ValueType>() / this->getModel().getExitRate(state) : storm::utility::constGetZero<ValueType>());
} else {
// For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action
// and the sum ranges over all states s'.
for (auto choice : stateChoicesPair.second) {
variables.clear();
coefficients.clear();
variables.push_back(stateToVariableIndexMap.at(state));
coefficients.push_back(1);
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice);
for (auto element : row) {
variables.push_back(stateToVariableIndexMap.at(element.column()));
coefficients.push_back(-element.value());
}
solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constGetZero<ValueType>());
}
}
}
solver->optimize();
lraValuesForEndComponents.push_back(solver->getContinuousValue(lraValueVariableIndex));
// Compute the LRA value for the current MEC.
lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(min, transitionMatrix, nondeterministicChoiceIndices, this->getModel().getMarkovianStates(), this->getModel().getExitRates(), goalStates, mec));
}
// For fast transition rewriting, we build some auxiliary data structures.
@ -429,7 +388,7 @@ namespace storm {
// Finalize the matrix and solve the corresponding system of equations.
sspMatrix.finalize();
std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
nondeterministiclinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b, sspNondeterministicChoiceIndices);
// Prepare result vector.
@ -451,10 +410,102 @@ namespace storm {
}
std::vector<ValueType> checkExpectedTime(bool min, storm::storage::BitVector const& goalStates) const {
// Reduce the problem of computing the expected time to computing expected rewards where the rewards
// for all probabilistic states are zero and the reward values of Markovian states is 1.
std::vector<ValueType> rewardValues(this->getModel().getNumberOfStates(), storm::utility::constGetZero<ValueType>());
storm::utility::vector::setVectorValues(rewardValues, this->getModel().getMarkovianStates(), storm::utility::constGetOne<ValueType>());
return this->computeExpectedRewards(min, goalStates, rewardValues);
}
protected:
/*!
* Computes the long-run average value for the given maximal end component of a Markov automaton.
*
* @param min Sets whether the long-run average is to be minimized or maximized.
* @param transitionMatrix The transition matrix of the underlying Markov automaton.
* @param nondeterministicChoiceIndices A vector indicating at which row the choice of a given state begins.
* @param markovianStates A bit vector storing all markovian states.
* @param exitRates 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.
*/
static ValueType computeLraForMaximalEndComponent(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec) {
std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("LRA for MEC");
solver->setModelSense(min ? storm::solver::LpSolver::MAXIMIZE : storm::solver::LpSolver::MINIMIZE);
// First, we need to create the variables for the problem.
std::map<uint_fast64_t, uint_fast64_t> stateToVariableIndexMap;
for (auto const& stateChoicesPair : mec) {
stateToVariableIndexMap[stateChoicesPair.first] = solver->createContinuousVariable("x" + std::to_string(stateChoicesPair.first), storm::solver::LpSolver::UNBOUNDED, 0, 0, 0);
}
uint_fast64_t lraValueVariableIndex = solver->createContinuousVariable("k", storm::solver::LpSolver::UNBOUNDED, 0, 0, 1);
// Now we encode the problem as constraints.
std::vector<uint_fast64_t> variables;
std::vector<double> coefficients;
for (auto const& stateChoicesPair : mec) {
uint_fast64_t state = stateChoicesPair.first;
// Now, based on the type of the state, create a suitable constraint.
if (markovianStates.get(state)) {
variables.clear();
coefficients.clear();
variables.push_back(stateToVariableIndexMap.at(state));
coefficients.push_back(1);
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(nondeterministicChoiceIndices[state]);
for (auto element : row) {
variables.push_back(stateToVariableIndexMap.at(element.column()));
coefficients.push_back(-element.value());
}
variables.push_back(lraValueVariableIndex);
coefficients.push_back(storm::utility::constGetOne<ValueType>() / exitRates[state]);
solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, goalStates.get(state) ? storm::utility::constGetOne<ValueType>() / exitRates[state] : storm::utility::constGetZero<ValueType>());
} else {
// For probabilistic states, we want to add the constraint x_s <= sum P(s, a, s') * x_s' where a is the current action
// and the sum ranges over all states s'.
for (auto choice : stateChoicesPair.second) {
variables.clear();
coefficients.clear();
variables.push_back(stateToVariableIndexMap.at(state));
coefficients.push_back(1);
typename storm::storage::SparseMatrix<ValueType>::Rows row = transitionMatrix.getRow(choice);
for (auto element : row) {
variables.push_back(stateToVariableIndexMap.at(element.column()));
coefficients.push_back(-element.value());
}
solver->addConstraint("state" + std::to_string(state), variables, coefficients, min ? storm::solver::LpSolver::LESS_EQUAL : storm::solver::LpSolver::GREATER_EQUAL, storm::utility::constGetZero<ValueType>());
}
}
}
solver->optimize();
return solver->getContinuousValue(lraValueVariableIndex);
}
/*!
* Computes the expected reward that is gained from each state before entering any of the goal states.
*
* @param min Indicates whether minimal or maximal rewards are to be computed.
* @param goalStates The goal states that define until which point rewards are gained.
* @param stateRewards A vector that defines the reward gained in each state. For probabilistic states, this is an instantaneous reward
* that is fully gained and for Markovian states the actually gained reward is dependent on the expected time to stay in the
* state, i.e. it is gouverned by the exit rate of the state.
* @return A vector that contains the expected reward for each state of the model.
*/
std::vector<ValueType> computeExpectedRewards(bool min, storm::storage::BitVector const& goalStates, std::vector<ValueType> const& stateRewards) const {
// Check whether the automaton is closed.
if (!this->getModel().isClosed()) {
throw storm::exceptions::InvalidArgumentException() << "Unable to compute expected time on non-closed Markov automaton.";
}
// First, we need to check which states have infinite expected time (by definition).
storm::storage::BitVector infinityStates;
if (min) {
@ -501,77 +552,50 @@ namespace storm {
infinityStates = storm::storage::BitVector(this->getModel().getNumberOfStates());
}
}
// Now we identify the states for which values need to be computed.
storm::storage::BitVector maybeStates = ~(goalStates | infinityStates);
// Then, we can eliminate the rows and columns for all states whose values are already known to be 0.
std::vector<ValueType> x(maybeStates.getNumberOfSetBits());
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = computeNondeterministicChoiceIndicesForConstraint(this->getModel().getNondeterministicChoiceIndices(), maybeStates);
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates);
storm::storage::SparseMatrix<ValueType> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
// Now prepare the mean sojourn times for all states so they can be used as the right-hand side of the equation system.
std::vector<ValueType> meanSojournTimes(this->getModel().getExitRates());
// Now prepare the expected reward values for all states so they can be used as the right-hand side of the equation system.
std::vector<ValueType> rewardValues(stateRewards);
for (auto state : this->getModel().getMarkovianStates()) {
meanSojournTimes[state] = storm::utility::constGetOne<ValueType>() / meanSojournTimes[state];
rewardValues[state] = rewardValues[state] / this->getModel().getExitRates()[state];
}
// Finally, prepare the actual right-hand side.
std::vector<ValueType> b(submatrix.getRowCount());
storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), meanSojournTimes);
storm::utility::vector::selectVectorValuesRepeatedly(b, maybeStates, this->getModel().getNondeterministicChoiceIndices(), rewardValues);
// Solve the corresponding system of equations.
std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministiclinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>();
nondeterministiclinearEquationSolver->solveEquationSystem(min, submatrix, x, b, subNondeterministicChoiceIndices);
// Create resulting vector.
std::vector<ValueType> result(this->getModel().getNumberOfStates());
// Set values of resulting vector according to previous result and return the result.
storm::utility::vector::setVectorValues<ValueType>(result, maybeStates, x);
storm::utility::vector::setVectorValues(result, goalStates, storm::utility::constGetZero<ValueType>());
storm::utility::vector::setVectorValues(result, infinityStates, storm::utility::constGetInfinity<ValueType>());
return result;
}
protected:
/*!
* A stack used for storing whether we are currently computing min or max probabilities or rewards, respectively.
* The topmost element is true if and only if we are currently computing minimum probabilities or rewards.
*/
mutable std::stack<bool> minimumOperatorStack;
private:
/*!
* Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given
* by the parameter constraint.
*
* @param constraint A bit vector specifying which states are kept.
* @returns A vector of the nondeterministic choice indices of the subsystem induced by the given constraint.
* A solver that is used for solving systems of linear equations that are the result of nondeterministic choices.
*/
static std::vector<uint_fast64_t> computeNondeterministicChoiceIndicesForConstraint(std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::BitVector const& constraint) {
// Reserve the known amount of slots for the resulting vector.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1);
uint_fast64_t currentRowCount = 0;
uint_fast64_t currentIndexCount = 1;
// Set the first element as this will clearly begin at offset 0.
subNondeterministicChoiceIndices[0] = 0;
// Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over
// to the resulting vector.
for (auto index : constraint) {
subNondeterministicChoiceIndices[currentIndexCount] = currentRowCount + nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index];
currentRowCount += nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index];
++currentIndexCount;
}
// Put a sentinel element at the end.
subNondeterministicChoiceIndices[constraint.getNumberOfSetBits()] = currentRowCount;
return subNondeterministicChoiceIndices;
}
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver;
};
}
}

85
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h

@ -18,6 +18,7 @@
#include "src/models/Mdp.h"
#include "src/utility/vector.h"
#include "src/utility/graph.h"
#include "src/utility/solver.h"
#include "src/settings/Settings.h"
#include "src/storage/TotalScheduler.h"
@ -37,7 +38,7 @@ namespace storm {
*
* @param model The MDP to be checked.
*/
explicit SparseMdpPrctlModelChecker(storm::models::Mdp<Type> const& model, storm::solver::AbstractNondeterministicLinearEquationSolver<Type>* linearEquationSolver) : AbstractModelChecker<Type>(model), minimumOperatorStack(), linearEquationSolver(linearEquationSolver) {
explicit SparseMdpPrctlModelChecker(storm::models::Mdp<Type> const& model, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<Type>()) : AbstractModelChecker<Type>(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) {
// Intentionally left empty.
}
@ -46,7 +47,7 @@ namespace storm {
* constructed model checker will have the model of the given model checker as its associated model.
*/
explicit SparseMdpPrctlModelChecker(storm::modelchecker::prctl::SparseMdpPrctlModelChecker<Type> const& modelchecker)
: AbstractModelChecker<Type>(modelchecker), minimumOperatorStack(), linearEquationSolver(new storm::solver::AbstractNondeterministicLinearEquationSolver<Type>()) {
: AbstractModelChecker<Type>(modelchecker), minimumOperatorStack(), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<Type>()) {
// Intentionally left empty.
}
@ -115,7 +116,7 @@ namespace storm {
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(statesWithProbabilityGreater0, this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(statesWithProbabilityGreater0);
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), statesWithProbabilityGreater0);
// Compute the new set of target states in the reduced system.
storm::storage::BitVector rightStatesInReducedSystem = statesWithProbabilityGreater0 % psiStates;
@ -127,11 +128,7 @@ namespace storm {
std::vector<Type> subresult(statesWithProbabilityGreater0.getNumberOfSetBits());
storm::utility::vector::setVectorValues(subresult, rightStatesInReducedSystem, storm::utility::constGetOne<Type>());
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, subNondeterministicChoiceIndices, nullptr, stepBound);
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), submatrix, subresult, subNondeterministicChoiceIndices, nullptr, stepBound);
// Set the values of the resulting vector accordingly.
storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
@ -172,11 +169,7 @@ namespace storm {
std::vector<Type> result(this->getModel().getNumberOfStates());
storm::utility::vector::setVectorValues(result, nextStates, storm::utility::constGetOne<Type>());
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices());
return result;
}
@ -325,7 +318,7 @@ namespace storm {
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates);
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
@ -335,11 +328,7 @@ namespace storm {
std::vector<Type> x(maybeStates.getNumberOfSetBits());
// Solve the corresponding system of equations.
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices);
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
@ -376,11 +365,7 @@ namespace storm {
// Initialize result to state rewards of the model.
std::vector<Type> result(this->getModel().getStateRewardVector());
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), nullptr, formula.getBound());
return result;
}
@ -422,11 +407,7 @@ namespace storm {
result.resize(this->getModel().getNumberOfStates());
}
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
this->nondeterministicLinearEquationSolver->performMatrixVectorMultiplication(this->minimumOperatorStack.top(), this->getModel().getTransitionMatrix(), result, this->getModel().getNondeterministicChoiceIndices(), &totalRewardVector, formula.getBound());
return result;
}
@ -500,7 +481,7 @@ namespace storm {
storm::storage::SparseMatrix<Type> submatrix = this->getModel().getTransitionMatrix().getSubmatrix(maybeStates, this->getModel().getNondeterministicChoiceIndices());
// Get the "new" nondeterministic choice indices for the submatrix.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = this->computeNondeterministicChoiceIndicesForConstraint(maybeStates);
std::vector<uint_fast64_t> subNondeterministicChoiceIndices = storm::utility::vector::getConstrainedOffsetVector(this->getModel().getNondeterministicChoiceIndices(), maybeStates);
// Prepare the right-hand side of the equation system. For entry i this corresponds to
// the accumulated probability of going from state i to some 'yes' state.
@ -534,11 +515,7 @@ namespace storm {
std::vector<Type> x(maybeStates.getNumberOfSetBits());
// Solve the corresponding system of equations.
if (linearEquationSolver != nullptr) {
this->linearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices);
} else {
throw storm::exceptions::InvalidStateException() << "No valid linear equation solver available.";
}
this->nondeterministicLinearEquationSolver->solveEquationSystem(minimize, submatrix, x, b, subNondeterministicChoiceIndices);
// Set values of resulting vector according to result.
storm::utility::vector::setVectorValues<Type>(result, maybeStates, x);
@ -601,45 +578,11 @@ namespace storm {
*/
mutable std::stack<bool> minimumOperatorStack;
private:
/*!
* Computes the nondeterministic choice indices vector resulting from reducing the full system to the states given
* by the parameter constraint.
*
* @param constraint A bit vector specifying which states are kept.
* @returns A vector of the nondeterministic choice indices of the subsystem induced by the given constraint.
* A solver that is used for solving systems of linear equations that are the result of nondeterministic choices.
*/
std::vector<uint_fast64_t> computeNondeterministicChoiceIndicesForConstraint(storm::storage::BitVector const& constraint) const {
// First, get a reference to the full nondeterministic choice indices.
std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = this->getModel().getNondeterministicChoiceIndices();
// Reserve the known amount of slots for the resulting vector.
std::vector<uint_fast64_t> subNondeterministicChoiceIndices(constraint.getNumberOfSetBits() + 1);
uint_fast64_t currentRowCount = 0;
uint_fast64_t currentIndexCount = 1;
// Set the first element as this will clearly begin at offset 0.
subNondeterministicChoiceIndices[0] = 0;
// Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over
// to the resulting vector.
for (auto index : constraint) {
subNondeterministicChoiceIndices[currentIndexCount] = currentRowCount + nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index];
currentRowCount += nondeterministicChoiceIndices[index + 1] - nondeterministicChoiceIndices[index];
++currentIndexCount;
}
// Put a sentinel element at the end.
subNondeterministicChoiceIndices[constraint.getNumberOfSetBits()] = currentRowCount;
return subNondeterministicChoiceIndices;
}
// An object that is used for solving linear equations and performing matrix-vector multiplication.
std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<Type>> linearEquationSolver;
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<Type>> nondeterministicLinearEquationSolver;
};
} // namespace prctl
} // namespace modelchecker
} // namespace storm

6
src/solver/AbstractNondeterministicLinearEquationSolver.h

@ -86,8 +86,10 @@ namespace storm {
// auto startTime = std::chrono::high_resolution_clock::now();
// std::chrono::nanoseconds totalTime(0);
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<Type>(A.getRowCount());
multiplyResultMemoryProvided = false;
}
std::vector<Type>* currentX = &x;
bool xMemoryProvided = true;
@ -134,6 +136,10 @@ namespace storm {
} else if (!xMemoryProvided) {
delete newX;
}
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
// // Check if the solver converged and issue a warning otherwise.
// if (converged) {

8
src/solver/GmmxxNondeterministicLinearEquationSolver.h

@ -52,8 +52,10 @@ namespace storm {
gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(A);
// Set up the environment for the power method.
bool multiplyResultMemoryProvided = true;
if (multiplyResult == nullptr) {
multiplyResult = new std::vector<Type>(A.getRowCount());
multiplyResultMemoryProvided = false;
}
std::vector<Type>* currentX = &x;
@ -101,7 +103,11 @@ namespace storm {
delete newX;
}
delete gmmxxMatrix;
if (!multiplyResultMemoryProvided) {
delete multiplyResult;
}
// Check if the solver converged and issue a warning otherwise.
if (converged) {
LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iterations << " iterations.");

21
src/storm.cpp

@ -231,18 +231,7 @@ storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecke
*/
storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double>& mdp) {
// Create the appropriate model checker.
storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::string const chosenMatrixLibrary = s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString();
if (chosenMatrixLibrary == "gmm++") {
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
} else if (chosenMatrixLibrary == "native") {
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
}
// The control flow should never reach this point, as there is a default setting for matrixlib.
std::string message = "No matrix library suitable for MDP model checking has been set.";
throw storm::exceptions::InvalidSettingsException() << message;
return nullptr;
return new storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double>(mdp);
}
/*!
@ -473,10 +462,10 @@ int main(const int argc, const char* argv[]) {
LOG4CPLUS_INFO(logger, "Model is a Markov automaton.");
std::shared_ptr<storm::models::MarkovAutomaton<double>> markovAutomaton = parser.getModel<storm::models::MarkovAutomaton<double>>();
markovAutomaton->close();
storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(*markovAutomaton);
// std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
// std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
// std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl;
storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker<double> mc(*markovAutomaton, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl;
std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 0, 1) << std::endl;
std::cout << mc.checkTimeBoundedEventually(true, markovAutomaton->getLabeledStates("goal"), 1, 2) << std::endl;
break;
}

25
src/utility/solver.cpp

@ -0,0 +1,25 @@
#include "src/utility/solver.h"
namespace storm {
namespace utility {
namespace solver {
std::shared_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name) {
return std::shared_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
}
template<typename ValueType>
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver() {
std::string const& matrixLibrary = storm::settings::Settings::getInstance()->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString();
if (matrixLibrary == "gmm++") {
return std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<ValueType>());
} else if (matrixLibrary == "native") {
return std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>());
}
throw storm::exceptions::InvalidSettingsException() << "No suitable nondeterministic linear equation solver selected.";
}
template std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>> getNondeterministicLinearEquationSolver();
}
}
}

11
src/utility/solver.h

@ -5,19 +5,16 @@
#include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
#include "src/solver/GurobiLpSolver.h"
#include "src/exceptions/InvalidSettingsException.h"
namespace storm {
namespace utility {
namespace solver {
std::unique_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name) {
return std::unique_ptr<storm::solver::LpSolver>(new storm::solver::GurobiLpSolver(name));
}
std::shared_ptr<storm::solver::LpSolver> getLpSolver(std::string const& name);
template<typename ValueType>
std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver() {
return std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>());
// return std::unique_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<ValueType>());
}
std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<ValueType>> getNondeterministicLinearEquationSolver();
}
}
}

600
src/utility/vector.h

@ -1,10 +1,3 @@
/*
* vector.h
*
* Created on: 06.12.2012
* Author: Christian Dehnert
*/
#ifndef STORM_UTILITY_VECTOR_H_
#define STORM_UTILITY_VECTOR_H_
@ -14,295 +7,318 @@
#include <algorithm>
#include <functional>
#include "log4cplus/logger.h"
#include "log4cplus/loggingmacros.h"
extern log4cplus::Logger logger;
namespace storm {
namespace utility {
namespace vector {
/*!
* Sets the provided values at the provided positions in the given vector.
*
* @param vector The vector in which the values are to be set.
* @param positions The positions at which the values are to be set.
* @param values The values that are to be set.
*/
template<class T>
void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
vector[position] = values[oldPosition++];
}
}
/*!
* Sets the provided value at the provided positions in the given vector.
*
* @param vector The vector in which the value is to be set.
* @param positions The positions at which the value is to be set.
* @param value The value that is to be set.
*/
template<class T>
void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, T value) {
for (auto position : positions) {
vector[position] = value;
}
}
/*!
* Sets the provided value at the provided positions in the given vector.
*
* @param vector The vector in which the value is to be set.
* @param positions The positions at which the value is to be set.
* @param value The value that is to be set.
*/
template<class T>
void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>& eigenVector, storm::storage::BitVector const& positions, T value) {
for (auto position : positions) {
eigenVector(position, 0) = value;
}
}
/*!
* Selects the elements from a vector at the specified positions and writes them consecutively into another vector.
* @param vector The vector into which the selected elements are to be written.
* @param positions The positions at which to select the elements from the values vector.
* @param values The vector from which to select the elements.
*/
template<class T>
void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
vector[oldPosition++] = values[position];
}
}
/*!
* Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector.
*
* @param vector The vector into which the selected elements are to be written.
* @param positions The positions of the groups of elements that are to be selected.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector.
* @param values The vector from which to select groups of elements.
*/
template<class T>
void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) {
vector[oldPosition++] = values[i];
}
}
}
/*!
* Selects one element out of each row group and writes it to the target vector.
*
* @param vector The target vector to which the values are written.
* @param rowGroupToRowIndexMapping A mapping from row group indices to an offset that specifies which of the values to
* take from the row group.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector.
* @param values The vector from which to select the values.
*/
template<class T>
void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (uint_fast64_t i = 0; i < vector.size(); ++i) {
vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
}
}
/*!
* Selects values from a vector at the specified positions and writes them into another vector as often as given by
* the size of the corresponding group of elements.
*
* @param vector The vector into which the selected elements are written.
* @param positions The positions at which to select the values.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. This
* implicitly defines the number of times any element is written to the output vector.
*/
template<class T>
void selectVectorValuesRepeatedly(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) {
vector[oldPosition++] = values[position];
}
}
}
/*!
* Subtracts the given vector from the constant one-vector and writes the result to the input vector.
*
* @param vector The vector that is to be subtracted from the constant one-vector.
*/
template<class T>
void subtractFromConstantOneVector(std::vector<T>& vector) {
for (auto& element : vector) {
element = storm::utility::constGetOne<T>() - element;
}
}
/*!
* Adds the two given vectors and writes the result into the first operand.
*
* @param target The first summand and target vector.
* @param summand The second summand.
*/
template<class T>
void addVectorsInPlace(std::vector<T>& target, std::vector<T> const& summand) {
if (target.size() != summand.size()) {
LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible.");
throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible.";
}
std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus<T>());
}
/*!
* Reduces the given source vector by selecting an element according to the given filter out of each row group.
*
* @param source The source vector which is to be reduced.
* @param target The target vector into which a single element from each row group is written.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector.
* @param filter A function that compares two elements v1 and v2 according to some filter criterion. This function must
* return true iff v1 is supposed to be taken instead of v2.
* @param choices If non-null, this vector is used to store the choices made during the selection.
*/
template<class T>
void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::function<bool (T const&, T const&)> filter, std::vector<uint_fast64_t>* choices = nullptr) {
uint_fast64_t currentSourceRow = 0;
uint_fast64_t currentTargetRow = -1;
uint_fast64_t currentLocalRow = 0;
for (auto it = source.cbegin(), ite = source.cend(); it != ite; ++it, ++currentSourceRow, ++currentLocalRow) {
// Check whether we have considered all source rows for the current target row.
if (rowGrouping[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) {
currentLocalRow = 0;
++currentTargetRow;
target[currentTargetRow] = source[currentSourceRow];
if (choices != nullptr) {
(*choices)[currentTargetRow] = 0;
namespace utility {
namespace vector {
/*!
* Sets the provided values at the provided positions in the given vector.
*
* @param vector The vector in which the values are to be set.
* @param positions The positions at which the values are to be set.
* @param values The values that are to be set.
*/
template<class T>
void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
vector[position] = values[oldPosition++];
}
}
continue;
}
// We have to upate the value, so only overwrite the current value if the value passes the filter.
if (filter(*it, target[currentTargetRow])) {
target[currentTargetRow] = *it;
if (choices != nullptr) {
(*choices)[currentTargetRow] = currentLocalRow;
/*!
* Sets the provided value at the provided positions in the given vector.
*
* @param vector The vector in which the value is to be set.
* @param positions The positions at which the value is to be set.
* @param value The value that is to be set.
*/
template<class T>
void setVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, T value) {
for (auto position : positions) {
vector[position] = value;
}
}
}
}
}
/*!
* Reduces the given source vector by selecting the smallest element out of each row group.
*
* @param source The source vector which is to be reduced.
* @param target The target vector into which a single element from each row group is written.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector.
* @param choices If non-null, this vector is used to store the choices made during the selection.
*/
template<class T>
void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T>(source, target, rowGrouping, std::less<T>(), choices);
}
/*!
* Reduces the given source vector by selecting the largest element out of each row group.
*
* @param source The source vector which is to be reduced.
* @param target The target vector into which a single element from each row group is written.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector.
* @param choices If non-null, this vector is used to store the choices made during the selection.
*/
template<class T>
void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T>(source, target, rowGrouping, std::greater<T>(), choices);
}
/*!
* Compares the given elements and determines whether they are equal modulo the given precision. The provided flag
* additionaly specifies whether the error is computed in relative or absolute terms.
*
* @param val1 The first value to compare.
* @param val2 The second value to compare.
* @param precision The precision up to which the elements are compared.
* @param relativeError If set, the error is computed relative to the second value.
* @return True iff the elements are considered equal.
*/
template<class T>
bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) {
if (relativeError) {
if (std::abs(val1 - val2)/val2 > precision) return false;
} else {
if (std::abs(val1 - val2) > precision) return false;
}
return true;
}
/*!
* Compares the two vectors and determines whether they are equal modulo the provided precision. Depending on whether the
* flag is set, the difference between the vectors is computed relative to the value or in absolute terms.
*
* @param vectorLeft The first vector of the comparison.
* @param vectorRight The second vector of the comparison.
* @param precision The precision up to which the vectors are to be checked for equality.
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/
template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T precision, bool relativeError) {
if (vectorLeft.size() != vectorRight.size()) {
LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible.");
throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible.";
}
for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) {
if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) {
return false;
}
}
return true;
}
/*!
* Compares the two vectors at the specified positions and determines whether they are equal modulo the provided
* precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value
* or in absolute terms.
*
* @param vectorLeft The first vector of the comparison.
* @param vectorRight The second vector of the comparison.
* @param precision The precision up to which the vectors are to be checked for equality.
* @param positions A vector representing a set of positions at which the vectors are compared.
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/
template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T precision, bool relativeError) {
if (vectorLeft.size() != vectorRight.size()) {
LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible.");
throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible.";
}
for (uint_fast64_t position : positions) {
if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
return false;
}
}
return true;
}
} // namespace vector
} // namespace utility
/*!
* Sets the provided value at the provided positions in the given vector.
*
* @param vector The vector in which the value is to be set.
* @param positions The positions at which the value is to be set.
* @param value The value that is to be set.
*/
template<class T>
void setVectorValues(Eigen::Matrix<T, -1, 1, 0, -1, 1>& eigenVector, storm::storage::BitVector const& positions, T value) {
for (auto position : positions) {
eigenVector(position, 0) = value;
}
}
/*!
* Selects the elements from a vector at the specified positions and writes them consecutively into another vector.
* @param vector The vector into which the selected elements are to be written.
* @param positions The positions at which to select the elements from the values vector.
* @param values The vector from which to select the elements.
*/
template<class T>
void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
vector[oldPosition++] = values[position];
}
}
/*!
* Selects groups of elements from a vector at the specified positions and writes them consecutively into another vector.
*
* @param vector The vector into which the selected elements are to be written.
* @param positions The positions of the groups of elements that are to be selected.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector.
* @param values The vector from which to select groups of elements.
*/
template<class T>
void selectVectorValues(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) {
vector[oldPosition++] = values[i];
}
}
}
/*!
* Selects one element out of each row group and writes it to the target vector.
*
* @param vector The target vector to which the values are written.
* @param rowGroupToRowIndexMapping A mapping from row group indices to an offset that specifies which of the values to
* take from the row group.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector.
* @param values The vector from which to select the values.
*/
template<class T>
void selectVectorValues(std::vector<T>& vector, std::vector<uint_fast64_t> const& rowGroupToRowIndexMapping, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (uint_fast64_t i = 0; i < vector.size(); ++i) {
vector[i] = values[rowGrouping[i] + rowGroupToRowIndexMapping[i]];
}
}
/*!
* Selects values from a vector at the specified positions and writes them into another vector as often as given by
* the size of the corresponding group of elements.
*
* @param vector The vector into which the selected elements are written.
* @param positions The positions at which to select the values.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector. This
* implicitly defines the number of times any element is written to the output vector.
*/
template<class T>
void selectVectorValuesRepeatedly(std::vector<T>& vector, storm::storage::BitVector const& positions, std::vector<uint_fast64_t> const& rowGrouping, std::vector<T> const& values) {
uint_fast64_t oldPosition = 0;
for (auto position : positions) {
for (uint_fast64_t i = rowGrouping[position]; i < rowGrouping[position + 1]; ++i) {
vector[oldPosition++] = values[position];
}
}
}
/*!
* Subtracts the given vector from the constant one-vector and writes the result to the input vector.
*
* @param vector The vector that is to be subtracted from the constant one-vector.
*/
template<class T>
void subtractFromConstantOneVector(std::vector<T>& vector) {
for (auto& element : vector) {
element = storm::utility::constGetOne<T>() - element;
}
}
/*!
* Adds the two given vectors and writes the result into the first operand.
*
* @param target The first summand and target vector.
* @param summand The second summand.
*/
template<class T>
void addVectorsInPlace(std::vector<T>& target, std::vector<T> const& summand) {
if (target.size() != summand.size()) {
LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes operation impossible.");
throw storm::exceptions::InvalidArgumentException() << "Length of vectors do not match, which makes operation impossible.";
}
std::transform(target.begin(), target.end(), summand.begin(), target.begin(), std::plus<T>());
}
/*!
* Reduces the given source vector by selecting an element according to the given filter out of each row group.
*
* @param source The source vector which is to be reduced.
* @param target The target vector into which a single element from each row group is written.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the values vector.
* @param filter A function that compares two elements v1 and v2 according to some filter criterion. This function must
* return true iff v1 is supposed to be taken instead of v2.
* @param choices If non-null, this vector is used to store the choices made during the selection.
*/
template<class T>
void reduceVector(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::function<bool (T const&, T const&)> filter, std::vector<uint_fast64_t>* choices = nullptr) {
uint_fast64_t currentSourceRow = 0;
uint_fast64_t currentTargetRow = -1;
uint_fast64_t currentLocalRow = 0;
for (auto it = source.cbegin(), ite = source.cend(); it != ite; ++it, ++currentSourceRow, ++currentLocalRow) {
// Check whether we have considered all source rows for the current target row.
if (rowGrouping[currentTargetRow + 1] <= currentSourceRow || currentSourceRow == 0) {
currentLocalRow = 0;
++currentTargetRow;
target[currentTargetRow] = source[currentSourceRow];
if (choices != nullptr) {
(*choices)[currentTargetRow] = 0;
}
continue;
}
// We have to upate the value, so only overwrite the current value if the value passes the filter.
if (filter(*it, target[currentTargetRow])) {
target[currentTargetRow] = *it;
if (choices != nullptr) {
(*choices)[currentTargetRow] = currentLocalRow;
}
}
}
}
/*!
* Reduces the given source vector by selecting the smallest element out of each row group.
*
* @param source The source vector which is to be reduced.
* @param target The target vector into which a single element from each row group is written.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector.
* @param choices If non-null, this vector is used to store the choices made during the selection.
*/
template<class T>
void reduceVectorMin(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T>(source, target, rowGrouping, std::less<T>(), choices);
}
/*!
* Reduces the given source vector by selecting the largest element out of each row group.
*
* @param source The source vector which is to be reduced.
* @param target The target vector into which a single element from each row group is written.
* @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector.
* @param choices If non-null, this vector is used to store the choices made during the selection.
*/
template<class T>
void reduceVectorMax(std::vector<T> const& source, std::vector<T>& target, std::vector<uint_fast64_t> const& rowGrouping, std::vector<uint_fast64_t>* choices = nullptr) {
reduceVector<T>(source, target, rowGrouping, std::greater<T>(), choices);
}
/*!
* Compares the given elements and determines whether they are equal modulo the given precision. The provided flag
* additionaly specifies whether the error is computed in relative or absolute terms.
*
* @param val1 The first value to compare.
* @param val2 The second value to compare.
* @param precision The precision up to which the elements are compared.
* @param relativeError If set, the error is computed relative to the second value.
* @return True iff the elements are considered equal.
*/
template<class T>
bool equalModuloPrecision(T const& val1, T const& val2, T precision, bool relativeError = true) {
if (relativeError) {
if (std::abs(val1 - val2)/val2 > precision) return false;
} else {
if (std::abs(val1 - val2) > precision) return false;
}
return true;
}
/*!
* Compares the two vectors and determines whether they are equal modulo the provided precision. Depending on whether the
* flag is set, the difference between the vectors is computed relative to the value or in absolute terms.
*
* @param vectorLeft The first vector of the comparison.
* @param vectorRight The second vector of the comparison.
* @param precision The precision up to which the vectors are to be checked for equality.
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/
template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, T precision, bool relativeError) {
if (vectorLeft.size() != vectorRight.size()) {
LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible.");
throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible.";
}
for (uint_fast64_t i = 0; i < vectorLeft.size(); ++i) {
if (!equalModuloPrecision(vectorLeft[i], vectorRight[i], precision, relativeError)) {
return false;
}
}
return true;
}
/*!
* Compares the two vectors at the specified positions and determines whether they are equal modulo the provided
* precision. Depending on whether the flag is set, the difference between the vectors is computed relative to the value
* or in absolute terms.
*
* @param vectorLeft The first vector of the comparison.
* @param vectorRight The second vector of the comparison.
* @param precision The precision up to which the vectors are to be checked for equality.
* @param positions A vector representing a set of positions at which the vectors are compared.
* @param relativeError If set, the difference between the vectors is computed relative to the value or in absolute terms.
*/
template<class T>
bool equalModuloPrecision(std::vector<T> const& vectorLeft, std::vector<T> const& vectorRight, std::vector<uint_fast64_t> const& positions, T precision, bool relativeError) {
if (vectorLeft.size() != vectorRight.size()) {
LOG4CPLUS_ERROR(logger, "Lengths of vectors do not match, which makes comparison impossible.");
throw storm::exceptions::InvalidArgumentException() << "Lengths of vectors do not match, which makes comparison impossible.";
}
for (uint_fast64_t position : positions) {
if (!equalModuloPrecision(vectorLeft[position], vectorRight[position], precision, relativeError)) {
return false;
}
}
return true;
}
/*!
* Takes the given offset vector and applies the given contraint. That is, it produces another offset vector that contains
* the relative offsets of the entries given by the constraint.
*
* @param offsetVector The offset vector to constrain.
* @param constraint The constraint to apply to the offset vector.
* @return An offset vector that contains all selected relative offsets.
*/
template<class T>
std::vector<T> getConstrainedOffsetVector(std::vector<T> const& offsetVector, storm::storage::BitVector const& constraint) {
// Reserve the known amount of slots for the resulting vector.
std::vector<uint_fast64_t> subVector(constraint.getNumberOfSetBits() + 1);
uint_fast64_t currentRowCount = 0;
uint_fast64_t currentIndexCount = 1;
// Set the first element as this will clearly begin at offset 0.
subVector[0] = 0;
// Loop over all states that need to be kept and copy the relative indices of the nondeterministic choices over
// to the resulting vector.
for (auto index : constraint) {
subVector[currentIndexCount] = currentRowCount + offsetVector[index + 1] - offsetVector[index];
currentRowCount += offsetVector[index + 1] - offsetVector[index];
++currentIndexCount;
}
// Put a sentinel element at the end.
subVector[constraint.getNumberOfSetBits()] = currentRowCount;
return subVector;
}
} // namespace vector
} // namespace utility
} // namespace storm
#endif /* STORM_UTILITY_VECTOR_H_ */

8
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp

@ -17,7 +17,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@ -105,7 +105,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@ -133,7 +133,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@ -167,7 +167,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);

8
test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@ -16,7 +16,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@ -104,7 +104,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@ -132,7 +132,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@ -166,7 +166,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);

4
test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

@ -17,7 +17,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@ -104,7 +104,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::GmmxxNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);

4
test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

@ -17,7 +17,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@ -106,7 +106,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, new storm::solver::AbstractNondeterministicLinearEquationSolver<double>());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::AbstractNondeterministicLinearEquationSolver<double>>(new storm::solver::AbstractNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);

Loading…
Cancel
Save