Browse Source

SteadyState: Issue a warning in sound mode because it is not supported.

main
Tim Quatmann 4 years ago
parent
commit
5245d77bfc
  1. 1
      src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp

1
src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp

@ -235,6 +235,7 @@ namespace storm {
subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType(), subEnv.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault());
}
subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion());
STORM_LOG_WARN_COND(!subEnv.solver().isForceSoundness(), "Sound computations are not properly implemented for this computation. You might get incorrect results.");
// Get a mapping from global state indices to local ones as well as a bitvector containing states within the BSCC.
std::unordered_map<uint64_t, uint64_t> toLocalIndexMap;

Loading…
Cancel
Save