diff --git a/resources/examples/testfiles/smg/example_smg.nm b/resources/examples/testfiles/smg/example_smg.nm index 0050b1028..875070051 100644 --- a/resources/examples/testfiles/smg/example_smg.nm +++ b/resources/examples/testfiles/smg/example_smg.nm @@ -1,3 +1,7 @@ +// taken from Julia Eisentraut "Value iteration for simple stochastic games: Stopping criterion +// and learning algorithm" - Fig. 1 + + smg const double p = 2/3; diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp index cd37d9875..765d08135 100644 --- a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp @@ -361,9 +361,7 @@ namespace { std::unique_ptr result; auto transitionMatrix = model->getTransitionMatrix(); - auto formulas = std::move(modelFormulas.second); - storm::logic::GameFormula const& gameFormula = formulas[0]->asGameFormula(); storm::modelchecker::CheckTask checkTask(gameFormula); @@ -371,13 +369,12 @@ namespace { storm::storage::BitVector statesOfCoalition = model->computeStatesOfCoalition(gameFormula.getCoalition()); statesOfCoalition.complement(); - // TODO Fabian: get optimization direction storm::storage::BitVector psiStates = checker->check(this->env(), gameFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().asStateFormula())->asExplicitQualitativeCheckResult().getTruthValuesVector(); storm::storage::BitVector phiStates(model->getNumberOfStates(), true); storm::storage::SparseMatrix backwardTransitions = model->getBackwardTransitions(); - storm::OptimizationDirection optimizationDirection = storm::OptimizationDirection::Maximize; + storm::OptimizationDirection optimizationDirection = gameFormula.getSubformula().asOperatorFormula().getOptimalityType(); auto minimizerStates = optimizationDirection == storm::OptimizationDirection::Maximize ? statesOfCoalition : ~statesOfCoalition; storm::modelchecker::helper::internal::SoundGameViHelper viHelper(transitionMatrix, backwardTransitions, statesOfCoalition, psiStates, optimizationDirection); @@ -506,6 +503,8 @@ namespace { xL = _x1L; xU = _x1U; + // testing x vectors + // ===================================================== EXPECT_NEAR(this->parseNumber("0"), xL[0], this->precision()); EXPECT_NEAR(this->parseNumber("0.333333"), xL[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); @@ -515,6 +514,7 @@ namespace { EXPECT_NEAR(this->parseNumber("0.666666"), xU[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + // ===================================================== // perform second iteration step reducedMinimizerActions = {storm::storage::BitVector(transitionMatrix.getRowCount(), true)}; @@ -616,6 +616,8 @@ namespace { xL = _x2L; xU = _x2U; + // testing x vectors + // ===================================================== EXPECT_NEAR(this->parseNumber("0.333333"), xL[0], this->precision()); EXPECT_NEAR(this->parseNumber("0.444444"), xL[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xL[2], this->precision()); @@ -625,6 +627,7 @@ namespace { EXPECT_NEAR(this->parseNumber("0.555555"), xU[1], this->precision()); EXPECT_NEAR(this->parseNumber("1"), xU[2], this->precision()); EXPECT_NEAR(this->parseNumber("0"), xU[3], this->precision()); + // ===================================================== }