RobustMdpPrctlModelCheckerTest.cpp

Go to the documentation of this file.

#include "storm-config.h"
#include "storm/adapters/RationalNumberForward.h"
#include "storm/exceptions/NotImplementedException.h"
#include "test/storm_gtest.h"
 
#include "storm-parsers/api/model_descriptions.h"
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/DirectEncodingParser.h"
#include "storm/adapters/IntervalAdapter.h"
#include "storm/api/builder.h"
#include "storm/api/properties.h"
#include "storm/api/verification.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/solver/OptimizationDirection.h"
#include "storm/transformer/AddUncertainty.h"
 
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> const& model) {
    return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult<double>>(model->getInitialStates());
}
 
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::sparse::Model<double>> const& model) {
    return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult<double>>(model->getInitialStates());
}
 
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(
    std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> const& model) {
    return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult<storm::RationalNumber>>(model->getInitialStates());
}
 
storm::ExtendedRationalNumber getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> const& model,
                                                                  std::unique_ptr<storm::modelchecker::CheckResult>& result) {
    auto filter = getInitialStateFilter(model);
    result->filter(*filter);
    return result->asQuantitativeCheckResult<storm::RationalNumber>().getMin();
}
 
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(
    std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> const& model) {
    return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult<storm::RationalNumber>>(model->getInitialStates());
}
 
double getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::sparse::Model<storm::Interval>> const& model,
                                           std::unique_ptr<storm::modelchecker::CheckResult>& result) {
    auto filter = getInitialStateFilter(model);
    result->filter(*filter);
    return result->asQuantitativeCheckResult<double>().getMin();
}
 
double getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::sparse::Model<double>> const& model,
                                           std::unique_ptr<storm::modelchecker::CheckResult>& result) {
    auto filter = getInitialStateFilter(model);
    result->filter(*filter);
    return result->asQuantitativeCheckResult<double>().getMin();
}
 
storm::ExtendedRationalNumber getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> const& model,
                                                                  std::unique_ptr<storm::modelchecker::CheckResult>& result) {
    auto filter = getInitialStateFilter(model);
    result->filter(*filter);
    return result->asQuantitativeCheckResult<storm::RationalNumber>().getMin();
}
 
void expectSolutionBoundsSound(std::unique_ptr<storm::modelchecker::CheckResult> const& result, double expected) {
    auto const& explicitResult = result->asExplicitQuantitativeCheckResult<double>();
    ASSERT_TRUE(explicitResult.hasLowerBounds() || explicitResult.hasUpperBounds()) << "No bound on the solution was reported.";
    if (explicitResult.hasLowerBounds()) {
        EXPECT_LE(explicitResult.getLowerBoundVector().front(), expected + 0.0001) << "The lower bound exceeds the expected value.";
    }
    if (explicitResult.hasUpperBounds()) {
        EXPECT_LE(expected, explicitResult.getUpperBoundVector().front() + 0.0001) << "The upper bound falls below the expected value.";
    }
}
 
void expectSolutionBoundsSound(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::RationalNumber const& expected) {
    auto const& explicitResult = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
    ASSERT_TRUE(explicitResult.hasLowerBounds() || explicitResult.hasUpperBounds()) << "No bound on the solution was reported.";
    if (explicitResult.hasLowerBounds()) {
        EXPECT_LE(explicitResult.getLowerBoundVector().front(), expected) << "The lower bound exceeds the expected value.";
    }
    if (explicitResult.hasUpperBounds()) {
        EXPECT_LE(expected, explicitResult.getUpperBoundVector().front()) << "The upper bound falls below the expected value.";
    }
}
 
void expectThrow(std::string const& path, std::string const& formulaString) {
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr = storm::parser::parseDirectEncodingModel<storm::Interval>(path);
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString));
 
    storm::Environment env;
    env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
 
    std::shared_ptr<storm::models::sparse::Mdp<storm::Interval>> mdp = modelPtr->as<storm::models::sparse::Mdp<storm::Interval>>();
    ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
    auto task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0]);
 
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
    STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::NotImplementedException);
}
 
void checkModel(std::string const& path, std::string const& formulaString, double maxmin, double maxmax, double minmax, double minmin, bool produceScheduler) {
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr = storm::parser::parseDirectEncodingModel<storm::Interval>(path);
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString));
    storm::Environment env;
    env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
    env.solver().setForceSoundness(true);
 
    std::shared_ptr<storm::models::sparse::Mdp<storm::Interval>> mdp = modelPtr->as<storm::models::sparse::Mdp<storm::Interval>>();
    ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
    auto taskMax = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0]);
    taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust);
    taskMax.setProduceSchedulers(produceScheduler);
 
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
    auto resultMax = checker.check(env, taskMax);
    EXPECT_NEAR(maxmin, getQuantitativeResultAtInitialState(mdp, resultMax), 0.0001);
    expectSolutionBoundsSound(resultMax, maxmin);
    taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative);
    auto resultMaxNonRobust = checker.check(env, taskMax);
    EXPECT_NEAR(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxNonRobust), 0.0001);
    expectSolutionBoundsSound(resultMaxNonRobust, maxmax);
 
    auto taskMin = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1]);
    taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust);
    taskMin.setProduceSchedulers(produceScheduler);
 
    auto resultMin = checker.check(env, taskMin);
    EXPECT_NEAR(minmax, getQuantitativeResultAtInitialState(mdp, resultMin), 0.0001);
    expectSolutionBoundsSound(resultMin, minmax);
    taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative);
    auto resultMinNonRobust = checker.check(env, taskMin);
    EXPECT_NEAR(minmin, getQuantitativeResultAtInitialState(mdp, resultMinNonRobust), 0.0001);
    expectSolutionBoundsSound(resultMinNonRobust, minmin);
}
 
void checkPrismModelForQuantitativeResult(std::string const& path, std::string const& formulaString, double minmin, double minmax, double maxmin, double maxmax,
                                          std::string constantsString) {
    storm::prism::Program program = storm::api::parseProgram(path);
    program = program.preprocess(constantsString);
 
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString));
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr = storm::api::buildSparseModel<storm::Interval>(program, formulas);
 
    storm::Environment env;
    env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
 
    std::shared_ptr<storm::models::sparse::Mdp<storm::Interval>> mdp = modelPtr->as<storm::models::sparse::Mdp<storm::Interval>>();
    ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
 
    auto taskMinMin = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0]);
    taskMinMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize);
 
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
    auto resultMinMin = checker.check(env, taskMinMin);
    EXPECT_NEAR(minmin, getQuantitativeResultAtInitialState(mdp, resultMinMin), 0.0001);
 
    auto taskMinMax = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[1]);
    taskMinMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize);
 
    auto resultMinMax = checker.check(env, taskMinMax);
    EXPECT_NEAR(minmax, getQuantitativeResultAtInitialState(mdp, resultMinMax), 0.0001);
 
    auto taskMaxMin = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[2]);
    taskMaxMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize);
 
    auto resultMaxMin = checker.check(env, taskMaxMin);
    EXPECT_NEAR(maxmin, getQuantitativeResultAtInitialState(mdp, resultMaxMin), 0.0001);
 
    auto taskMaxMax = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[3]);
    taskMaxMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize);
 
    auto resultMaxMax = checker.check(env, taskMaxMax);
    EXPECT_NEAR(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxMax), 0.0001);
}
 
void checkModelRational(std::string const& path, std::string const& formulaString, storm::RationalNumber maxmin, storm::RationalNumber maxmax,
                        storm::RationalNumber minmax, storm::RationalNumber minmin, bool produceScheduler) {
    std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> modelPtr = storm::parser::parseDirectEncodingModel<storm::RationalInterval>(path);
 
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString));
    storm::Environment env;
    env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
    env.solver().setForceSoundness(true);
 
    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalInterval>> mdp = modelPtr->as<storm::models::sparse::Mdp<storm::RationalInterval>>();
    ASSERT_EQ(storm::models::ModelType::Mdp, modelPtr->getType());
    auto taskMax = storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber>(*formulas[0]);
    taskMax.setProduceSchedulers(produceScheduler);
 
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalInterval>>(*mdp);
    taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust);
    auto resultMax = checker.check(env, taskMax);
    EXPECT_EQ(maxmin, getQuantitativeResultAtInitialState(mdp, resultMax));
    expectSolutionBoundsSound(resultMax, maxmin);
    taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative);
    auto resultMaxNonRobust = checker.check(env, taskMax);
    EXPECT_EQ(maxmax, getQuantitativeResultAtInitialState(mdp, resultMaxNonRobust));
    expectSolutionBoundsSound(resultMaxNonRobust, maxmax);
 
    auto taskMin = storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber>(*formulas[1]);
    taskMin.setProduceSchedulers(produceScheduler);
 
    taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Robust);
    auto resultMin = checker.check(env, taskMin);
    EXPECT_EQ(minmax, getQuantitativeResultAtInitialState(mdp, resultMin));
    expectSolutionBoundsSound(resultMin, minmax);
    taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative);
    auto resultMinNonRobust = checker.check(env, taskMin);
    EXPECT_EQ(minmin, getQuantitativeResultAtInitialState(mdp, resultMinNonRobust));
}
 
TEST(RobustMdpModelCheckerTest, RobotMinMaxTest) {
#ifndef STORM_HAVE_Z3
    GTEST_SKIP() << "Z3 not available.";
#endif
    // Maxima reachability rewards using PRISM format.
    checkPrismModelForQuantitativeResult(STORM_TEST_RESOURCES_DIR "/imdp/robot.prism",
                                         "Pmin=? [ F \"goal2\"];Pmin=? [ F \"goal2\"];Pmax=? [ F \"goal2\"];Pmax=? [ F \"goal2\"]", 0.4, 0.6, 1.0, 1.0,
                                         "delta=0.1");
}
 
void makeUncertainAndCheck(std::string const& path, std::string const& formulaString, double amountOfUncertainty) {
    storm::prism::Program program = storm::api::parseProgram(path);
    program = program.preprocess("");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
        storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program));
    std::shared_ptr<storm::models::sparse::Model<double>> modelPtr = storm::api::buildSparseModel<double>(program, formulas);
 
    auto mdp = modelPtr->as<storm::models::sparse::Mdp<double>>();
 
    ASSERT_TRUE(formulas[0]->isProbabilityOperatorFormula());
    // These tests cases where written with max in mind.
    ASSERT_TRUE(formulas[0]->asProbabilityOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize);
    auto task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0]);
    storm::Environment env;
 
    // First compute certain value
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>>(*mdp);
    auto exresult = checker.check(env, task);
    double certainValue = getQuantitativeResultAtInitialState(mdp, exresult);
 
    storm::Environment envIntervals;
    envIntervals.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
    auto transformer = storm::transformer::AddUncertainty<double>(modelPtr);
    auto imdp = transformer.transform(amountOfUncertainty)->as<storm::models::sparse::Mdp<storm::Interval>>();
    auto ichecker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*imdp);
    auto iresultMin = checker.check(env, task);
    double minValue = getQuantitativeResultAtInitialState(mdp, iresultMin);
    EXPECT_LE(minValue, certainValue);
    task.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative);
    auto iresultMax = checker.check(env, task);
    double maxValue = getQuantitativeResultAtInitialState(mdp, iresultMax);
    EXPECT_LE(certainValue, maxValue);
}
 
void makeUncertainAndCheckRational(std::string const& path, std::string const& formulaString, storm::RationalNumber amountOfUncertainty) {
    storm::prism::Program program = storm::api::parseProgram(path);
    program = program.preprocess("");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
        storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulaString, program));
    std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> modelPtr = storm::api::buildSparseModel<storm::RationalNumber>(program, formulas);
    auto mdp = modelPtr->as<storm::models::sparse::Mdp<storm::RationalNumber>>();
 
    ASSERT_TRUE(formulas[0]->isProbabilityOperatorFormula());
    ASSERT_TRUE(formulas[0]->asProbabilityOperatorFormula().getOptimalityType() == storm::solver::OptimizationDirection::Maximize);
 
    storm::Environment env;
    auto taskCertain = storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber>(*formulas[0]);
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>(*mdp);
    auto exresult = checker.check(env, taskCertain);
    auto const certainValue = getQuantitativeResultAtInitialState(modelPtr, exresult);
 
    storm::Environment envIntervals;
    envIntervals.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
    auto transformer = storm::transformer::AddUncertainty<storm::RationalNumber>(modelPtr);
    auto imdp = transformer.transform(amountOfUncertainty)->as<storm::models::sparse::Mdp<storm::RationalInterval>>();
    auto ichecker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalInterval>>(*imdp);
 
    auto taskMin = storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber>(*formulas[0]);
    taskMin.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Minimize);
    auto iresultMin = ichecker.check(envIntervals, taskMin);
    auto const minValue = getQuantitativeResultAtInitialState(imdp, iresultMin);
    EXPECT_LE(minValue, certainValue);
 
    auto taskMax = storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber>(*formulas[0]);
    taskMax.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Maximize);
    auto iresultMax = ichecker.check(envIntervals, taskMax);
    auto const maxValue = getQuantitativeResultAtInitialState(imdp, iresultMax);
    EXPECT_LE(certainValue, maxValue);
}
 
// TODO: Add next properties
 
TEST(RobustMDPModelCheckingTest, Tiny01maxmin) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-01.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 0.4, 0.5, 0.5, 0.4, false);
}
 
TEST(RobustMDPModelCheckingTest, Tiny03maxmin) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 0.4, 0.6, 0.5, 0.3, true);
}
 
TEST(RobustMDPModelCheckingTest, BoundedTiny03maxmin) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F<=1 \"target\"];Pmin=? [ F<=1 \"target\"]", 0.4, 0.6, 0.5, 0.3, true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F[1,1] \"target\"];Pmin=? [ F[1,1] \"target\"]", 0.4, 0.6, 0.5, 0.3, true);
}
 
TEST(RobustMDPModelCheckingTest, BoundedMaxmin) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F<=4 \"target\"];Pmin=? [ F<=4 \"target\"]", 0.6528, 0.81, 0.81, 0.6528, true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[0,4] \"target\"];Pmin=? [ F[0,4] \"target\"]", 0.6528, 0.81, 0.81, 0.6528, true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[4,4] \"target\"];Pmin=? [ F[4,4] \"target\"]", 0.1952, 0.324, 0.324, 0.1952,
               true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[4,5] \"target\"];Pmin=? [ F[4,5] \"target\"]", 0.3236, 0.50292, 0.50292, 0.3236,
               true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[4,6] \"target\"];Pmin=? [ F[4,6] \"target\"]", 0.37928, 0.57888, 0.57888, 0.37928,
               true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[2,2] \"target\"];Pmin=? [ F[2,2] \"target\"]", 0.32, 0.45, 0.45, 0.32, true);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F<=2 \"target\"];Pmin=? [ F<=2 \"target\"]", 0.32, 0.45, 0.45, 0.32, true);
}
 
TEST(RobustMDPModelCheckingTest, Tiny04maxmin) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-04.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 1, 1, 0.42857, 0.42, false);
}
 
TEST(RobustMDPModelCheckingTest, Tiny05maxmin) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-05.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", 0.3, 0.4, 0.4, 0.3, false);
}
 
TEST(RobustMDPModelCheckingTest, Tiny04MinRewards) {
    // The reward of a state is collected every time the state is visited. Only the cycle 0 -> 2 -> 0 can be repeated without reaching infinite reward, and
    // state 0 reaches the target with (fixed) probability 0.3. From state 1 (reached with probability 0.4) one has to move on to state 2 (reward 1).
    // This yields V0 = 1 + 0.4 * (1 + V2) + 0.3 * V2 with V2 = 1 + V0, i.e., V0 = 7. Rmax is infinite as the sink state 4 is reachable.
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-04.drn", "Rmin=? [ F \"target\" ];Rmin=? [ F \"target\" ]", 7, 7, 7, 7, false);
}
 
TEST(RobustMDPModelCheckingTest, RewardsTargetTransitionInterval) {
    // The self-loop probability p is in [0.2, 0.5], the probability of moving to the target is in [0.5, 0.8]. The expected reward 1 / (1 - p) is thus in
    // [1.25, 2]. This requires that the interval of the transition to the target state is respected when resolving the uncertainty.
    // Arguments: Rmax robust, Rmax cooperative, Rmin robust, Rmin cooperative.
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-09.drn", "Rmax=? [ F \"target\" ];Rmin=? [ F \"target\" ]", 1.25, 2, 2, 1.25, false);
}
 
TEST(RobustMDPModelCheckingTest, RewardsTargetStateBeforeMaybeStates) {
    // Same as above, but the target state has a smaller index than the other state. The values of target states must not be mixed up with the values of
    // the remaining states.
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-11.drn", "Rmax=? [ F \"target\" ];Rmin=? [ F \"target\" ]", 1.25, 2, 2, 1.25, false);
}
 
TEST(RobustMDPModelCheckingTest, ReachabilityTimes) {
    // Action 0 has self-loop probability p in [0.2, 0.5], i.e., expected time 1 / (1 - p) in [1.25, 2]. Action 1 has expected time 1 + 0.5 * 1 = 1.5.
    // Arguments: Tmax robust, Tmax cooperative, Tmin robust, Tmin cooperative.
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-10.drn", "Tmax=? [ F \"target\" ];Tmin=? [ F \"target\" ]", 1.5, 2, 1.5, 1.25, false);
}
 
TEST(RobustMDPModelCheckingTest, ReachabilityTimesSingleAction) {
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-09.drn", "Tmax=? [ F \"target\" ];Tmin=? [ F \"target\" ]", 1.25, 2, 2, 1.25, false);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-11.drn", "Tmax=? [ F \"target\" ];Tmin=? [ F \"target\" ]", 1.25, 2, 2, 1.25, false);
}
 
TEST(RobustMDPModelCheckingTest, GraphPreservationRequired) {
    // The self-loop interval [0, 1] allows to never reach the target, i.e., the graph of the model is not preserved.
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr =
        storm::parser::parseDirectEncodingModel<storm::Interval>(STORM_TEST_RESOURCES_DIR "/imdp/tiny-12.drn");
    auto mdp = modelPtr->as<storm::models::sparse::Mdp<storm::Interval>>();
    EXPECT_FALSE(mdp->getTransitionMatrix().isProbabilisticGraphPreserving());
    storm::Environment env;
    env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
    for (std::string const formulaString : {"Pmax=? [ F \"target\" ]", "Rmin=? [ F \"target\" ]", "Tmin=? [ F \"target\" ]"}) {
        std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
            storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString));
        auto task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0]);
        task.setUncertaintyResolutionMode(storm::UncertaintyResolutionMode::Cooperative);
        STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::InvalidSettingsException);
    }
}
 
TEST(RobustMDPModelCheckingTest, GraphPreservationAfterTightening) {
    // The self-loop interval [0, 0.5] is tightened to [0.5, 0.5] as the other transition has probability at most 0.5. The model is graph preserving.
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr =
        storm::parser::parseDirectEncodingModel<storm::Interval>(STORM_TEST_RESOURCES_DIR "/imdp/tiny-13.drn");
    EXPECT_FALSE(modelPtr->getTransitionMatrix().hasOnlyPositiveEntries());
    EXPECT_TRUE(modelPtr->getTransitionMatrix().isProbabilisticGraphPreserving());
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-13.drn", "Tmax=? [ F \"target\" ];Tmin=? [ F \"target\" ]", 2, 2, 2, 2, false);
}
 
TEST(RobustMDPModelCheckingTest, MinRewardsUniqueSolution) {
    // There is no end component with zero reward among the states with finite reward, i.e., the solution of the equation system is unique and no upper
    // reward bounds are required. Arguments: Rmin robust, Rmin cooperative, Rmin robust, Rmin cooperative.
    // Choosing action 0 in state 0 yields 2 + 1 / (1 - p) with self-loop probability p in [0.2, 0.5], which is cheaper than action 1 (cost 6).
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-08.drn", "Rmin=? [ F \"target\" ];Rmin=? [ F \"target\" ]", 4, 3.25, 4, 3.25, false);
}
 
TEST(RobustMDPModelCheckingTest, MinRewardsNonUniqueSolution) {
    // State 0 has a zero-reward self loop, i.e., there is an end component with zero reward. The solution is not unique and we cannot compute the required
    // upper reward bounds for interval models.
    expectThrow(STORM_TEST_RESOURCES_DIR "/imdp/tiny-07.drn", "Rmin=? [ F \"target\" ]");
}
 
TEST(RobustMDPModelCheckingTest, CumulativeRewards) {
    // Arguments: Rmax robust, Rmax cooperative, Rmin robust, Rmin cooperative
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn", "Rmax=? [ C<=0 ];Rmin=? [ C<=0 ]", 0, 0, 0, 0, false);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn", "Rmax=? [ C<=1 ];Rmin=? [ C<=1 ]", 7, 7, 1, 1, false);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn", "Rmax=? [ C<=2 ];Rmin=? [ C<=2 ]", 9, 9.5, 9, 7.5, false);
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn", "Rmax=? [ C<=3 ];Rmin=? [ C<=3 ]", 11, 11.5, 11, 9.5, false);
}
 
TEST(RobustMDPModelCheckingTest, CumulativeRewardsNoUncertaintyResolutionMode) {
    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> modelPtr =
        storm::parser::parseDirectEncodingModel<storm::Interval>(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn");
    std::vector<std::shared_ptr<storm::logic::Formula const>> formulas =
        storm::api::extractFormulasFromProperties(storm::api::parseProperties("Rmax=? [ C<=2 ]"));
    storm::Environment env;
    env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
    auto mdp = modelPtr->as<storm::models::sparse::Mdp<storm::Interval>>();
    auto task = storm::modelchecker::CheckTask<storm::logic::Formula, double>(*formulas[0]);
    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
    STORM_SILENT_EXPECT_THROW(checker.check(env, task), storm::exceptions::BaseException);
}
 
TEST(RobustMDPModelCheckingTest, CrowdsQuotientIMDP) {
    // Ensuring equivalent behavior when checking identical model as IDTMC and IMDP (cf. CrowdsQuotientIDTMC)
    checkModel(STORM_TEST_RESOURCES_DIR "/imdp/crowds-quotient-3-5.drn", "Pmax=? [ F \"observe0Greater1\"]; Pmin=? [ F \"observe0Greater1\"]", 0.1383409,
               0.1383409, 0.1383409, 0.1383409, false);
}
 
// ---- RationalInterval tests (exact arithmetic) ----
 
TEST(RobustRationalMDPModelCheckingTest, CumulativeRewards) {
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn", "Rmax=? [ C<=2 ];Rmin=? [ C<=2 ]", storm::RationalNumber(9), storm::RationalNumber("19/2"),
                       storm::RationalNumber(9), storm::RationalNumber("15/2"), false);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-06.drn", "Rmax=? [ C<=3 ];Rmin=? [ C<=3 ]", storm::RationalNumber(11),
                       storm::RationalNumber("23/2"), storm::RationalNumber(11), storm::RationalNumber("19/2"), false);
}
 
TEST(RobustRationalMDPModelCheckingTest, Tiny01maxmin) {
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-01.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber("2/5"),
                       storm::RationalNumber("1/2"), storm::RationalNumber("1/2"), storm::RationalNumber("2/5"), false);
}
 
TEST(RobustRationalMDPModelCheckingTest, Tiny03maxmin) {
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber("2/5"),
                       storm::RationalNumber("3/5"), storm::RationalNumber("1/2"), storm::RationalNumber("3/10"), true);
}
 
TEST(RobustRationalMDPModelCheckingTest, BoundedTiny03maxmin) {
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F<=1 \"target\"];Pmin=? [ F<=1 \"target\"]", storm::RationalNumber("2/5"),
                       storm::RationalNumber("3/5"), storm::RationalNumber("1/2"), storm::RationalNumber("3/10"), true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-03.drn", "Pmax=? [ F[1,1] \"target\"];Pmin=? [ F[1,1] \"target\"]", storm::RationalNumber("2/5"),
                       storm::RationalNumber("3/5"), storm::RationalNumber("1/2"), storm::RationalNumber("3/10"), true);
}
 
TEST(RobustRationalMDPModelCheckingTest, BoundedMaxmin) {
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F<=4 \"target\"];Pmin=? [ F<=4 \"target\"]",
                       storm::RationalNumber("408/625"), storm::RationalNumber("81/100"), storm::RationalNumber("81/100"), storm::RationalNumber("408/625"),
                       true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[0,4] \"target\"];Pmin=? [ F[0,4] \"target\"]",
                       storm::RationalNumber("408/625"), storm::RationalNumber("81/100"), storm::RationalNumber("81/100"), storm::RationalNumber("408/625"),
                       true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[4,4] \"target\"];Pmin=? [ F[4,4] \"target\"]",
                       storm::RationalNumber("122/625"), storm::RationalNumber("81/250"), storm::RationalNumber("81/250"), storm::RationalNumber("122/625"),
                       true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[4,5] \"target\"];Pmin=? [ F[4,5] \"target\"]",
                       storm::RationalNumber("809/2500"), storm::RationalNumber("12573/25000"), storm::RationalNumber("12573/25000"),
                       storm::RationalNumber("809/2500"), true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[4,6] \"target\"];Pmin=? [ F[4,6] \"target\"]",
                       storm::RationalNumber("4741/12500"), storm::RationalNumber("1809/3125"), storm::RationalNumber("1809/3125"),
                       storm::RationalNumber("4741/12500"), true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F[2,2] \"target\"];Pmin=? [ F[2,2] \"target\"]",
                       storm::RationalNumber("8/25"), storm::RationalNumber("9/20"), storm::RationalNumber("9/20"), storm::RationalNumber("8/25"), true);
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-bounded.drn", "Pmax=? [ F<=2 \"target\"];Pmin=? [ F<=2 \"target\"]", storm::RationalNumber("8/25"),
                       storm::RationalNumber("9/20"), storm::RationalNumber("9/20"), storm::RationalNumber("8/25"), true);
}
 
TEST(RobustRationalMDPModelCheckingTest, Tiny04maxmin) {
    // Fill in exact rational values once test output is known.
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-04.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber(1),
                       storm::RationalNumber(1), storm::RationalNumber("42857140807299/100000000000000"), storm::RationalNumber("21/50"), false);
}
 
TEST(RobustRationalMDPModelCheckingTest, Tiny05maxmin) {
    checkModelRational(STORM_TEST_RESOURCES_DIR "/imdp/tiny-05.drn", "Pmax=? [ F \"target\"];Pmin=? [ F \"target\"]", storm::RationalNumber("3/10"),
                       storm::RationalNumber("2/5"), storm::RationalNumber("2/5"), storm::RationalNumber("3/10"), false);
}
 
TEST(RobustMDPModelCheckingTest, AddUncertaintyCoin22max) {
#ifndef STORM_HAVE_Z3
    GTEST_SKIP() << "Z3 not available.";
#endif
    makeUncertainAndCheck(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", 0.1);
    makeUncertainAndCheck(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", 0.2);
}
 
TEST(RobustRationalMDPModelCheckingTest, AddUncertaintyCoin22max) {
#ifndef STORM_HAVE_Z3
    GTEST_SKIP() << "Z3 not available.";
#endif
    makeUncertainAndCheckRational(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", storm::RationalNumber("1/10"));
    makeUncertainAndCheckRational(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", "Pmax=? [F \"all_coins_equal_1\"]", storm::RationalNumber("1/5"));
}