Browse Source

TYPED_TESTS for LTL modelchecker

tempestpy_adaptions
hannah 4 years ago
committed by Stefan Pranger
parent
commit
132c293105
  1. 2
      src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp

2
src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp

@ -740,7 +740,6 @@ namespace {
// LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse || TypeParam::engine == DtmcEngine::JitSparse) {
EXPECT_TRUE(checker->canHandle(tasks[0]));
result = checker->check(tasks[0]);
EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
@ -785,7 +784,6 @@ namespace {
// LTL not supported in all engines (Hybrid, PrismDd, JaniDd)
if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse || TypeParam::engine == DtmcEngine::JitSparse) {
EXPECT_TRUE(checker->canHandle(tasks[0]));
result = checker->check(tasks[0]);
EXPECT_NEAR(this->parseNumber("16/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());

Loading…
Cancel
Save