Browse Source

Markov automaton model checker now clearing basic requirements

tempestpy_adaptions
dehnert 7 years ago
parent
commit
b8120ed73a
  1. 4
      src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

4
src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@ -90,9 +90,11 @@ namespace storm {
// Check for requirements of the solver.
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::UntilProbabilities);
requirements.clearBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(aProbabilistic);
solver->setBounds(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
solver->setRequirementsChecked();
solver->setCachingEnabled(true);
@ -377,9 +379,11 @@ namespace storm {
// Check for requirements of the solver.
storm::solver::MinMaxLinearEquationSolverRequirements requirements = minMaxLinearEquationSolverFactory.getRequirements(storm::solver::EquationSystemType::StochasticShortestPath);
requirements.clearLowerBounds();
STORM_LOG_THROW(requirements.empty(), storm::exceptions::UncheckedRequirementException, "Cannot establish requirements for solver.");
std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = minMaxLinearEquationSolverFactory.create(sspMatrix);
solver->setLowerBound(storm::utility::zero<ValueType>());
solver->setRequirementsChecked();
solver->solveEquations(dir, x, b);

Loading…
Cancel
Save