|
|
@ -22,10 +22,18 @@ namespace storm { |
|
|
|
template<typename ValueType> |
|
|
|
class SparseMarkovAutomatonCslModelChecker : public AbstractModelChecker<ValueType> { |
|
|
|
public: |
|
|
|
explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver = storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>()) : AbstractModelChecker<ValueType>(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { |
|
|
|
explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton<ValueType> const& model, std::shared_ptr<storm::solver::NondeterministicLinearEquationSolver<ValueType>> nondeterministicLinearEquationSolver) : AbstractModelChecker<ValueType>(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(nondeterministicLinearEquationSolver) { |
|
|
|
// Intentionally left empty. |
|
|
|
} |
|
|
|
|
|
|
|
/* |
|
|
|
This Second constructor is NEEDED and a workaround for a common Bug in C++ with nested templates |
|
|
|
See: http://stackoverflow.com/questions/14401308/visual-c-cannot-deduce-given-template-arguments-for-function-used-as-defaul |
|
|
|
*/ |
|
|
|
explicit SparseMarkovAutomatonCslModelChecker(storm::models::MarkovAutomaton<ValueType> const& model) : AbstractModelChecker<ValueType>(model), minimumOperatorStack(), nondeterministicLinearEquationSolver(storm::utility::solver::getNondeterministicLinearEquationSolver<ValueType>()) { |
|
|
|
// Intentionally left empty. |
|
|
|
} |
|
|
|
|
|
|
|
/*! |
|
|
|
* Returns a constant reference to the MDP associated with this model checker. |
|
|
|
* @returns A constant reference to the MDP associated with this model checker. |
|
|
|