diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp index 9fec51ff5..6af642da4 100644 --- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp +++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp @@ -647,7 +647,7 @@ namespace storm { STORM_LOG_INFO("Splitting based on region split estimates"); ConstantType diff = this->lastValue - (this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs()); for (auto &entry : regionSplitEstimates) { - if ((!this->isUseMonotonicitySet() || !monRes.isMonotone(entry.first)) && entry.second > diff) { + if ((!this->isUseMonotonicitySet() || !monRes.isMonotone(entry.first)) && storm::utility::convertNumber(entry.second) > diff) { sortedOnValues.insert({-(entry.second * storm::utility::convertNumber(region.getDifference(entry.first)) * storm::utility::convertNumber(region.getDifference(entry.first))), entry.first}); } } diff --git a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp index d3b82647d..1389a59da 100644 --- a/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp +++ b/src/storm-pomdp/generator/NondeterministicBeliefTracker.cpp @@ -139,7 +139,7 @@ namespace storm { if (lhs.belief.size() != rhs.belief.size()) { return false; } - storm::utility::ConstantsComparator cmp(0.00001, true); + storm::utility::ConstantsComparator cmp(storm::utility::convertNumber(0.00001), true); auto lhsIt = lhs.belief.begin(); auto rhsIt = rhs.belief.begin(); while(lhsIt != lhs.belief.end()) { diff --git a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index 212896447..461435816 100644 --- a/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -438,7 +438,7 @@ namespace storm { if (solver->hasUpperBound(storm::solver::AbstractEquationSolver::BoundType::Local)) { auto resultIt = x.begin(); for (auto const& entry : solver->getUpperBounds()) { - STORM_LOG_ASSERT(*resultIt <= entry + env.solver().minMax().getPrecision(), "Expecting result value for state " << std::distance(x.begin(), resultIt) << " to be <= " << entry << ", but got " << *resultIt << "."); + STORM_LOG_ASSERT(*resultIt <= entry + storm::utility::convertNumber(env.solver().minMax().getPrecision()), "Expecting result value for state " << std::distance(x.begin(), resultIt) << " to be <= " << entry << ", but got " << *resultIt << "."); ++resultIt; } } diff --git a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp index 63f4fd2d5..19b427f6a 100755 --- a/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/SchedulerGenerationMdpPrctlModelCheckerTest.cpp @@ -72,14 +72,14 @@ namespace { // return env; // } // }; - + template class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test { public: typedef typename TestType::ValueType ValueType; SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {} storm::Environment const& env() const { return _environment; } - + std::pair>, std::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { std::pair>, std::vector>> result; storm::prism::Program program = storm::api::parseProgram(pathToPrismFile); @@ -88,7 +88,7 @@ namespace { result.first = storm::api::buildSparseModel(program, result.second)->template as>(); return result; } - + std::vector> getTasks(std::vector> const& formulas) const { std::vector> result; for (auto const& f : formulas) { @@ -97,13 +97,13 @@ namespace { } return result; } - + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} - + private: storm::Environment _environment; }; - + typedef ::testing::Types< DoubleViEnvironment, DoubleSoundViEnvironment, @@ -111,10 +111,10 @@ namespace { RationalPIEnvironment //RationalRationalSearchEnvironment > TestingTypes; - + TYPED_TEST_SUITE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes,); - + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) { typedef typename TestFixture::ValueType ValueType; @@ -126,9 +126,9 @@ namespace { EXPECT_EQ(11ull, mdp->getNumberOfTransitions()); ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); EXPECT_EQ(7ull, mdp->getNumberOfChoices()); - + storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - + auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); @@ -137,7 +137,7 @@ namespace { EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice()); EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice()); EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice()); - + result = checker.check(tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); @@ -147,12 +147,12 @@ namespace { EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice()); EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice()); } - + TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, lra) { typedef typename TestFixture::ValueType ValueType; std::string formulasString = "R{\"grants\"}max=? [ MP ]; R{\"grants\"}min=? [ MP ];"; - + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString); auto mdp = std::move(modelFormulas.first); auto tasks = this->getTasks(modelFormulas.second); @@ -161,14 +161,14 @@ namespace { EXPECT_EQ(439ul, mdp->getNumberOfChoices()); ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp); - + if (!std::is_same::value) { GTEST_SKIP() << "Lra scheduler extraction not supported for LP based method"; } { auto result = checker.check(this->env(), tasks[0]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("333/1000"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + EXPECT_NEAR(this->parseNumber("333/1000"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::utility::convertNumber(this->env().solver().lra().getPrecision())); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); EXPECT_TRUE(scheduler.isDeterministicScheduler()); @@ -182,12 +182,12 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[0]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("333/1000"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + EXPECT_NEAR(this->parseNumber("333/1000"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::utility::convertNumber(this->env().solver().lra().getPrecision())); } { auto result = checker.check(this->env(), tasks[1]); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + EXPECT_NEAR(this->parseNumber("0"), result->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::utility::convertNumber(this->env().solver().lra().getPrecision())); ASSERT_TRUE(result->template asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const& scheduler = result->template asExplicitQuantitativeCheckResult().getScheduler(); EXPECT_TRUE(scheduler.isDeterministicScheduler()); @@ -200,7 +200,7 @@ namespace { storm::modelchecker::SparseMdpPrctlModelChecker> inducedChecker(*inducedMdp); auto inducedResult = inducedChecker.check(this->env(), tasks[1]); ASSERT_TRUE(inducedResult->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], this->env().solver().lra().getPrecision()); + EXPECT_NEAR(this->parseNumber("0"), inducedResult->template asExplicitQuantitativeCheckResult()[*mdp->getInitialStates().begin()], storm::utility::convertNumber(this->env().solver().lra().getPrecision())); } } @@ -414,4 +414,4 @@ namespace { } -} \ No newline at end of file +}