From 3dab26463d931aca0b3eb335f76f2e2704e1a917 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 2 Dec 2013 17:48:14 +0100 Subject: [PATCH] Introduced precision for digitization-based techniques as a new parameter. Former-commit-id: e9c57f821b5176cef3952c812292e6c5e256dc93 --- .../csl/SparseMarkovAutomatonCslModelChecker.cpp | 8 ++++++++ .../csl/SparseMarkovAutomatonCslModelChecker.h | 4 +--- src/storm.cpp | 10 ++++++---- 3 files changed, 15 insertions(+), 7 deletions(-) create mode 100644 src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp new file mode 100644 index 000000000..82590e31e --- /dev/null +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -0,0 +1,8 @@ +#include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h" + +bool SparseMarkovAutomatonCslModelCheckerOptionsRegistered = storm::settings::Settings::registerNewModule([] (storm::settings::Settings* instance) -> bool { + + instance->addOption(storm::settings::OptionBuilder("GmmxxLinearEquationSolver", "digiprecision", "", "Precision used for iterative solving of linear equation systems").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("precision value", "Precision").setDefaultValueDouble(1e-4).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build()); + + return true; +}); \ No newline at end of file diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h index 378e8803a..80943c8e0 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h @@ -179,7 +179,7 @@ namespace storm { // (1) Compute the accuracy we need to achieve the required error bound. ValueType maxExitRate = this->getModel().getMaximalExitRate(); - ValueType delta = (2 * storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) / (upperBound * maxExitRate * maxExitRate); + ValueType delta = (2 * storm::settings::Settings::getInstance()->getOptionByLongName("digiprecision").getArgument(0).getValueAsDouble()) / (upperBound * maxExitRate * maxExitRate); // (2) Compute the number of steps we need to make for the interval. uint_fast64_t numberOfSteps = static_cast(std::ceil((upperBound - lowerBound) / delta)); @@ -203,10 +203,8 @@ namespace storm { // Create the starting value vectors for the next value iteration based on the results of the previous one. storm::utility::vector::setVectorValues(vAllProbabilistic, ~markovianStates % goalStates, storm::utility::constGetOne()); storm::utility::vector::setVectorValues(vAllProbabilistic, ~markovianStates % ~goalStates, vProbabilistic); - std::cout << vAllProbabilistic << std::endl; storm::utility::vector::setVectorValues(vAllMarkovian, markovianStates % goalStates, storm::utility::constGetOne()); storm::utility::vector::setVectorValues(vAllMarkovian, markovianStates % ~goalStates, vMarkovian); - std::cout << vAllMarkovian << std::endl; // Compute the number of steps to reach the target interval. numberOfSteps = static_cast(std::ceil(lowerBound / delta)); diff --git a/src/storm.cpp b/src/storm.cpp index 0babe7612..0ffd18d92 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -463,10 +463,12 @@ int main(const int argc, const char* argv[]) { std::shared_ptr> markovAutomaton = parser.getModel>(); markovAutomaton->close(); storm::modelchecker::csl::SparseMarkovAutomatonCslModelChecker mc(*markovAutomaton, std::shared_ptr>(new storm::solver::AbstractNondeterministicLinearEquationSolver())); - 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; +// std::cout << mc.checkExpectedTime(true, markovAutomaton->getLabeledStates("goal")) << std::endl; +// std::cout << mc.checkExpectedTime(false, markovAutomaton->getLabeledStates("goal")) << std::endl; +// std::cout << mc.checkLongRunAverage(true, markovAutomaton->getLabeledStates("goal")) << std::endl; +// std::cout << mc.checkLongRunAverage(false, 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; } case storm::models::Unknown: