sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Removing old prctl locations

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
b55f828251
commit
7000dc6ff0
9 changed files with 0 additions and 3015 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 170
      src/test/storm/modelchecker/prctl/ConditionalDtmcPrctlModelCheckerTest.cpp
  2. 701
      src/test/storm/modelchecker/prctl/DtmcPrctlModelCheckerTest.cpp
  3. 158
      src/test/storm/modelchecker/prctl/ExplicitDtmcPrctlModelCheckerTest.cpp
  4. 199
      src/test/storm/modelchecker/prctl/ExplicitMdpPrctlModelCheckerTest.cpp
  5. 268
      src/test/storm/modelchecker/prctl/LraDtmcPrctlModelCheckerTest.cpp
  6. 468
      src/test/storm/modelchecker/prctl/LraMdpPrctlModelCheckerTest.cpp
  7. 607
      src/test/storm/modelchecker/prctl/MdpPrctlModelCheckerTest.cpp
  8. 302
      src/test/storm/modelchecker/prctl/QuantileQueryTest.cpp
  9. 142
      src/test/storm/modelchecker/prctl/SchedulerGenerationMdpPrctlModelCheckerTest.cpp

170
src/test/storm/modelchecker/prctl/ConditionalDtmcPrctlModelCheckerTest.cpp
View File

@ -1,170 +0,0 @@
#include "test/storm_gtest.h"
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/api/builder.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/environment/solver/GmmxxSolverEnvironment.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/environment/solver/NativeSolverEnvironment.h"
namespace {
class GmmxxDoubleGmresEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class EigenDoubleDGmresEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class EigenRationalLUEnvironment {
public:
typedef storm::RationalNumber ValueType;
static const bool isExact = true;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
return env;
}
};
class NativeSorEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.9));
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class NativePowerEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class NativeWalkerChaeEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
env.solver().native().setMaximalNumberOfIterations(50000);
return env;
}
};
template<typename TestType>
class ConditionalDtmcPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
private:
storm::Environment _environment;
};
typedef ::testing::Types<
GmmxxDoubleGmresEnvironment,
EigenDoubleDGmresEnvironment,
EigenRationalLUEnvironment,
NativeSorEnvironment,
NativePowerEnvironment,
NativeWalkerChaeEnvironment
> TestingTypes;
TYPED_TEST_SUITE(ConditionalDtmcPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
typedef typename TestFixture::ValueType ValueType;
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/test_conditional.pm");
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions());
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
// A parser that we use for conveniently constructing the formulas.
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"target\" || F \"condition\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"target\" || F \"condition\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult4[0], this->precision());
}
}

701
src/test/storm/modelchecker/prctl/DtmcPrctlModelCheckerTest.cpp
View File

@ -1,701 +0,0 @@
#include "test/storm_gtest.h"
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/api/builder.h"
#include "storm-conv/api/storm-conv.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/solver/EigenLinearEquationSolver.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/models/sparse/Dtmc.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/QualitativeCheckResult.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/environment/solver/NativeSolverEnvironment.h"
#include "storm/environment/solver/GmmxxSolverEnvironment.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
namespace {
enum class DtmcEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd};
class SparseGmmxxGmresIluEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class JaniSparseGmmxxGmresIluEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::JaniSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class JitSparseGmmxxGmresIluEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::JitSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseGmmxxGmresDiagEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Diagonal);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseGmmxxBicgstabIluEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Bicgstab);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseEigenDGmresEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseEigenDoubleLUEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
return env;
}
};
class SparseEigenRationalLUEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
return env;
}
};
class SparseRationalEliminationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
return env;
}
};
class SparseNativeJacobiEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseNativeWalkerChaeEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
env.solver().native().setMaximalNumberOfIterations(1000000);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-7));
return env;
}
};
class SparseNativeSorEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseNativePowerEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class SparseNativeSoundValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SoundValueIteration);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
};
class SparseNativeIntervalIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::IntervalIteration);
env.solver().native().setRelativeTerminationCriterion(false);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
};
class SparseNativeRationalSearchEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
return env;
}
};
class SparseTopologicalEigenLUEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // unused for sparse models
static const DtmcEngine engine = DtmcEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Dtmc<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Topological);
env.solver().topological().setUnderlyingEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
return env;
}
};
class HybridSylvanGmmxxGmresEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const DtmcEngine engine = DtmcEngine::Hybrid;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class HybridCuddNativeJacobiEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const DtmcEngine engine = DtmcEngine::Hybrid;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Jacobi);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class HybridCuddNativeSoundValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const DtmcEngine engine = DtmcEngine::Hybrid;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
};
class HybridSylvanNativeRationalSearchEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const DtmcEngine engine = DtmcEngine::Hybrid;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
return env;
}
};
class DdSylvanNativePowerEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const DtmcEngine engine = DtmcEngine::PrismDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class JaniDdSylvanNativePowerEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const DtmcEngine engine = DtmcEngine::JaniDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class DdCuddNativeJacobiEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const DtmcEngine engine = DtmcEngine::PrismDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::Power);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class DdSylvanRationalSearchEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const DtmcEngine engine = DtmcEngine::PrismDd;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::symbolic::Dtmc<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::RationalSearch);
return env;
}
};
template<typename TestType>
class DtmcPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
typedef typename storm::models::sparse::Dtmc<ValueType> SparseModelType;
typedef typename storm::models::symbolic::Dtmc<TestType::ddType, ValueType> SymbolicModelType;
DtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
bool isSymbolicModel() const { return std::is_same<typename TestType::ModelType, SymbolicModelType>::value; }
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
if (TestType::engine == DtmcEngine::PrismSparse) {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) {
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second, TestType::engine == DtmcEngine::JitSparse)->template as<MT>();
}
return result;
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
if (TestType::engine == DtmcEngine::Hybrid || TestType::engine == DtmcEngine::PrismDd) {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == DtmcEngine::JaniDd) {
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
}
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
if (TestType::engine == DtmcEngine::PrismSparse || TestType::engine == DtmcEngine::JaniSparse || TestType::engine == DtmcEngine::JitSparse) {
return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<SparseModelType>>(*model);
}
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
if (TestType::engine == DtmcEngine::Hybrid) {
return std::make_shared<storm::modelchecker::HybridDtmcPrctlModelChecker<SymbolicModelType>>(*model);
} else if (TestType::engine == DtmcEngine::PrismDd || TestType::engine == DtmcEngine::JaniDd) {
return std::make_shared<storm::modelchecker::SymbolicDtmcPrctlModelChecker<SymbolicModelType>>(*model);
}
}
bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
auto filter = getInitialStateFilter(model);
result->filter(*filter);
return result->asQualitativeCheckResult().forallTrue();
}
ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
auto filter = getInitialStateFilter(model);
result->filter(*filter);
return result->asQuantitativeCheckResult<ValueType>().getMin();
}
private:
storm::Environment _environment;
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
if (isSparseModel()) {
return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
} else {
return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
}
}
};
typedef ::testing::Types<
SparseGmmxxGmresIluEnvironment,
JaniSparseGmmxxGmresIluEnvironment,
JitSparseGmmxxGmresIluEnvironment,
SparseGmmxxGmresDiagEnvironment,
SparseGmmxxBicgstabIluEnvironment,
SparseEigenDGmresEnvironment,
SparseEigenDoubleLUEnvironment,
SparseEigenRationalLUEnvironment,
SparseRationalEliminationEnvironment,
SparseNativeJacobiEnvironment,
SparseNativeWalkerChaeEnvironment,
SparseNativeSorEnvironment,
SparseNativePowerEnvironment,
SparseNativeSoundValueIterationEnvironment,
SparseNativeIntervalIterationEnvironment,
SparseNativeRationalSearchEnvironment,
SparseTopologicalEigenLUEnvironment,
HybridSylvanGmmxxGmresEnvironment,
HybridCuddNativeJacobiEnvironment,
HybridCuddNativeSoundValueIterationEnvironment,
HybridSylvanNativeRationalSearchEnvironment,
DdSylvanNativePowerEnvironment,
JaniDdSylvanNativePowerEnvironment,
DdCuddNativeJacobiEnvironment,
DdSylvanRationalSearchEnvironment
> TestingTypes;
TYPED_TEST_SUITE(DtmcPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(DtmcPrctlModelCheckerTest, Die) {
std::string formulasString = "P=? [F \"one\"]";
formulasString += "; P=? [F \"two\"]";
formulasString += "; P=? [F \"three\"]";
formulasString += "; R=? [F \"done\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("11/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(DtmcPrctlModelCheckerTest, Crowds) {
std::string formulasString = "P=? [F observe0>1]";
formulasString += "; P=? [F \"observeIGreater1\"]";
formulasString += "; P=? [F observe1>1]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/crowds-4-3.pm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(726ul, model->getNumberOfStates());
EXPECT_EQ(1146ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("78686542099694893/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("40300855878315123/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("13433618626105041/1268858272000000000"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(DtmcPrctlModelCheckerTest, SynchronousLeader) {
std::string formulasString = "P=? [F \"elected\"]";
formulasString += "; P=? [F<=5 \"elected\"]";
formulasString += "; R=? [F \"elected\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(273ul, model->getNumberOfStates());
EXPECT_EQ(397ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("24/25"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("25/24"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TEST(DtmcPrctlModelCheckerTest, AllUntilProbabilities) {
std::string formulasString = "P=? [F \"one\"]";
formulasString += "; P=? [F \"two\"]";
formulasString += "; P=? [F \"three\"]";
storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm");
auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program));
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, double>> tasks;
for (auto const& f : formulas) {
tasks.emplace_back(*f);
}
auto model = storm::api::buildSparseModel<double>(program, formulas)->template as<storm::models::sparse::Dtmc<double>>();
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
storm::storage::SparseMatrix<double> matrix = model->getTransitionMatrix();
storm::storage::BitVector initialStates(13);
initialStates.set(0);
storm::storage::BitVector phiStates(13);
storm::storage::BitVector psiStates(13);
psiStates.set(7);
psiStates.set(8);
psiStates.set(9);
psiStates.set(10);
psiStates.set(11);
psiStates.set(12);
storm::Environment env;
storm::solver::SolveGoal<double> goal(*model, tasks[0]);
std::vector<double> result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates);
EXPECT_NEAR(1.0/6, result[7], 1e-6);
EXPECT_NEAR(1.0/6, result[8], 1e-6);
EXPECT_NEAR(1.0/6, result[9], 1e-6);
EXPECT_NEAR(1.0/6, result[10], 1e-6);
EXPECT_NEAR(1.0/6, result[11], 1e-6);
EXPECT_NEAR(1.0/6, result[12], 1e-6);
phiStates.set(6);
psiStates.set(1);
result = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeAllUntilProbabilities(env, std::move(goal), matrix, initialStates, phiStates, psiStates);
EXPECT_NEAR(1, result[0], 1e-6);
EXPECT_NEAR(0.5, result[1], 1e-6);
EXPECT_NEAR(0.5, result[2], 1e-6);
EXPECT_NEAR(0.25, result[5], 1e-6);
EXPECT_NEAR(0, result[7], 1e-6);
EXPECT_NEAR(0, result[8], 1e-6);
EXPECT_NEAR(0, result[9], 1e-6);
EXPECT_NEAR(0.125, result[10], 1e-6);
EXPECT_NEAR(0.125, result[11], 1e-6);
EXPECT_NEAR(0, result[12], 1e-6);
}
}

158
src/test/storm/modelchecker/prctl/ExplicitDtmcPrctlModelCheckerTest.cpp
View File

@ -1,158 +0,0 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/SettingMemento.h"
#include "storm-parsers/parser/AutoParser.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/builder/ExplicitModelBuilder.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/environment/solver/SolverEnvironment.h"
TEST(ExplicitDtmcPrctlModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew");
storm::Environment env;
double const precision = 1e-6;
// Increase precision a little to get more accurate results
env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
// A parser that we use for conveniently constructing the formulas.
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0 / 6.0, quantitativeResult1[0], precision);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0 / 6.0, quantitativeResult2[0], precision);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0 / 6.0, quantitativeResult3[0], precision);
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], precision);
}
TEST(ExplicitDtmcPrctlModelCheckerTest, Crowds) {
storm::Environment env;
double const precision = 1e-6;
// Increase precision a little to get more accurate results
env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/crowds5_5.tra", STORM_TEST_RESOURCES_DIR "/lab/crowds5_5.lab", "", "");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(15113ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], precision);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.1522194965, quantitativeResult2[0], precision);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], precision);
}
TEST(ExplicitDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::Environment env;
double const precision = 1e-6;
// Increase precision a little to get more accurate results
env.solver().setLinearEquationSolverPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4_8.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4_8.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4_8.pick.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(16495ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], precision);
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], precision);
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0448979591836789, quantitativeResult3[0], precision);
}

199
src/test/storm/modelchecker/prctl/ExplicitMdpPrctlModelCheckerTest.cpp
View File

@ -1,199 +0,0 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm-parsers/parser/AutoParser.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/builder/ExplicitModelBuilder.h"
TEST(ExplicitMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
storm::Environment env;
double const precision = 1e-6;
// Increase precision a little to get more accurate results
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/36.0, quantitativeResult1[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/36.0, quantitativeResult2[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.0/36.0, quantitativeResult3[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.0/36.0, quantitativeResult4[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(3.0/36.0, quantitativeResult5[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(3.0/36.0, quantitativeResult6[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(22.0/3.0, quantitativeResult7[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(22.0/3.0, quantitativeResult8[0], precision);
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", "");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> stateRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp);
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(22.0/3.0, quantitativeResult9[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(22.0/3.0, quantitativeResult10[0], precision);
abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.state.rew", STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<double>> stateAndTransitionRewardMdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(44.0/3.0, quantitativeResult11[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(44.0/3.0, quantitativeResult12[0], precision);
}
TEST(ExplicitMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::Environment env;
double const precision = 1e-6;
// Increase precision a little to get more accurate results
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/leader4.tra", STORM_TEST_RESOURCES_DIR "/lab/leader4.lab", "", STORM_TEST_RESOURCES_DIR "/rew/leader4.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType());
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = abstractModel->as<storm::models::sparse::Mdp<double>>();
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult2[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/16.0, quantitativeResult3[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/16.0, quantitativeResult4[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(30.0/7.0, quantitativeResult5[0], precision);
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(env, *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(30.0/7.0, quantitativeResult6[0], precision);
}

268
src/test/storm/modelchecker/prctl/LraDtmcPrctlModelCheckerTest.cpp
View File

@ -1,268 +0,0 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/settings/SettingMemento.h"
#include "storm/logic/Formulas.h"
#include "storm/solver/NativeLinearEquationSolver.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/settings/SettingsManager.h"
#include "storm/solver/NativeLinearEquationSolver.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/environment/solver/NativeSolverEnvironment.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
#include "storm/environment/solver/GmmxxSolverEnvironment.h"
#include "storm-parsers/parser/AutoParser.h"
#include "storm/builder/ExplicitModelBuilder.h"
namespace {
class GmmxxDoubleGmresEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx);
env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres);
env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu);
env.solver().gmmxx().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class EigenDoubleDGmresEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::DGmres);
env.solver().eigen().setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner::Ilu);
env.solver().eigen().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class EigenRationalLUEnvironment {
public:
typedef double ValueType;
static const bool isExact = true;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU);
return env;
}
};
class NativeSorEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::SOR);
env.solver().native().setSorOmega(storm::utility::convertNumber<storm::RationalNumber>(0.9));
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class NativeWalkerChaeEnvironment {
public:
typedef double ValueType;
static const bool isExact = false;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Native);
env.solver().native().setMethod(storm::solver::NativeLinearEquationSolverMethod::WalkerChae);
env.solver().native().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
env.solver().native().setMaximalNumberOfIterations(50000);
return env;
}
};
template<typename TestType>
class LraDtmcPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
LraDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
private:
storm::Environment _environment;
};
typedef ::testing::Types<
GmmxxDoubleGmresEnvironment,
EigenDoubleDGmresEnvironment,
EigenRationalLUEnvironment,
NativeSorEnvironment,
NativeWalkerChaeEnvironment
> TestingTypes;
TYPED_TEST_SUITE(LraDtmcPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRASingleBscc) {
typedef typename TestFixture::ValueType ValueType;
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(3, 3, 3);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(1, 2, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 2);
dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
}
}
TYPED_TEST(LraDtmcPrctlModelCheckerTest, LRA) {
typedef typename TestFixture::ValueType ValueType;
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(15, 15, 20, true);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(1, 4, this->parseNumber("0.7"));
matrixBuilder.addNextValue(1, 6, this->parseNumber("0.3"));
matrixBuilder.addNextValue(2, 0, this->parseNumber("1"));
matrixBuilder.addNextValue(3, 5, this->parseNumber("0.8"));
matrixBuilder.addNextValue(3, 9, this->parseNumber("0.2"));
matrixBuilder.addNextValue(4, 3, this->parseNumber("1"));
matrixBuilder.addNextValue(5, 3, this->parseNumber("1"));
matrixBuilder.addNextValue(6, 7, this->parseNumber("1"));
matrixBuilder.addNextValue(7, 8, this->parseNumber("1"));
matrixBuilder.addNextValue(8, 6, this->parseNumber("1"));
matrixBuilder.addNextValue(9, 10, this->parseNumber("1"));
matrixBuilder.addNextValue(10, 9, this->parseNumber("1"));
matrixBuilder.addNextValue(11, 9, this->parseNumber("1"));
matrixBuilder.addNextValue(12, 5, this->parseNumber("0.4"));
matrixBuilder.addNextValue(12, 8, this->parseNumber("0.3"));
matrixBuilder.addNextValue(12, 11, this->parseNumber("0.3"));
matrixBuilder.addNextValue(13, 7, this->parseNumber("0.7"));
matrixBuilder.addNextValue(13, 12, this->parseNumber("0.3"));
matrixBuilder.addNextValue(14, 12, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(15);
ap.addLabel("a");
ap.addLabelToState("a", 1);
ap.addLabelToState("a", 4);
ap.addLabelToState("a", 5);
ap.addLabelToState("a", 7);
ap.addLabelToState("a", 11);
ap.addLabelToState("a", 13);
ap.addLabelToState("a", 14);
dtmc.reset(new storm::models::sparse::Dtmc<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[3], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[6], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[9], this->precision());
EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[12], this->precision());
EXPECT_NEAR(this->parseNumber("79/300"), quantitativeResult1[13], this->precision());
EXPECT_NEAR(this->parseNumber("1/10"), quantitativeResult1[14], this->precision());
}
}
}

468
src/test/storm/modelchecker/prctl/LraMdpPrctlModelCheckerTest.cpp
View File

@ -1,468 +0,0 @@
#include "test/storm_gtest.h"
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/api/builder.h"
#include "storm-conv/api/storm-conv.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/settings/modules/NativeEquationSolverSettings.h"
#include "storm-parsers/parser/AutoParser.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
namespace {
class SparseValueTypeValueIterationEnvironment {
public:
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setLraMethod(storm::solver::LraMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class SparseValueTypeLinearProgrammingEnvironment {
public:
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class SparseRationalLinearProgrammingEnvironment {
public:
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setLraMethod(storm::solver::LraMethod::LinearProgramming);
return env;
}
};
template<typename TestType>
class LraMdpPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
LraMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<SparseModelType>();
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
private:
storm::Environment _environment;
};
typedef ::testing::Types<
SparseValueTypeValueIterationEnvironment,
SparseValueTypeLinearProgrammingEnvironment
#ifdef STORM_HAVE_Z3_OPTIMIZE
, SparseRationalLinearProgrammingEnvironment
#endif
> TestingTypes;
TYPED_TEST_SUITE(LraMdpPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA_SingleMec) {
typedef typename TestFixture::ValueType ValueType;
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 2);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(2, 2, 4);
matrixBuilder.addNextValue(0, 0, this->parseNumber("0.5"));
matrixBuilder.addNextValue(0, 1, this->parseNumber("0.5"));
matrixBuilder.addNextValue(1, 0, this->parseNumber("0.5"));
matrixBuilder.addNextValue(1, 1, this->parseNumber("0.5"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(2);
ap.addLabel("a");
ap.addLabelToState("a", 1);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[1], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult2[1], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
matrixBuilder.newRowGroup(3);
matrixBuilder.addNextValue(3, 0, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 2);
ap.addLabel("b");
ap.addLabelToState("b", 0);
ap.addLabel("c");
ap.addLabelToState("c", 0);
ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[1], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[1], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult3[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[0], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[1], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult4[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[0], this->precision());
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[1], this->precision());
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult5[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[0], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[1], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult6[2], this->precision());
}
}
TYPED_TEST(LraMdpPrctlModelCheckerTest, LRA) {
typedef typename TestFixture::ValueType ValueType;
storm::storage::SparseMatrixBuilder<ValueType> matrixBuilder;
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(4, 3, 4, true, true, 3);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 1, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
matrixBuilder.newRowGroup(3);
matrixBuilder.addNextValue(3, 2, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(3);
ap.addLabel("a");
ap.addLabelToState("a", 0);
ap.addLabel("b");
ap.addLabelToState("b", 1);
ap.addLabel("c");
ap.addLabelToState("c", 2);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult1[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[0], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult3[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult3[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[1], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult4[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[0], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[1], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult5[2], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult6[1], this->precision());
EXPECT_NEAR(this->parseNumber("1"), quantitativeResult6[2], this->precision());
}
{
matrixBuilder = storm::storage::SparseMatrixBuilder<ValueType>(22, 15, 28, true, true, 15);
matrixBuilder.newRowGroup(0);
matrixBuilder.addNextValue(0, 1, this->parseNumber("1"));
matrixBuilder.newRowGroup(1);
matrixBuilder.addNextValue(1, 0, this->parseNumber("1"));
matrixBuilder.addNextValue(2, 2, this->parseNumber("1"));
matrixBuilder.addNextValue(3, 4, this->parseNumber("0.7"));
matrixBuilder.addNextValue(3, 6, this->parseNumber("0.3"));
matrixBuilder.newRowGroup(4);
matrixBuilder.addNextValue(4, 0, this->parseNumber("1"));
matrixBuilder.newRowGroup(5);
matrixBuilder.addNextValue(5, 4, this->parseNumber("1"));
matrixBuilder.addNextValue(6, 5, this->parseNumber("0.8"));
matrixBuilder.addNextValue(6, 9, this->parseNumber("0.2"));
matrixBuilder.newRowGroup(7);
matrixBuilder.addNextValue(7, 3, this->parseNumber("1"));
matrixBuilder.addNextValue(8, 5, this->parseNumber("1"));
matrixBuilder.newRowGroup(9);
matrixBuilder.addNextValue(9, 3, this->parseNumber("1"));
matrixBuilder.newRowGroup(10);
matrixBuilder.addNextValue(10, 7, this->parseNumber("1"));
matrixBuilder.newRowGroup(11);
matrixBuilder.addNextValue(11, 6, this->parseNumber("1"));
matrixBuilder.addNextValue(12, 8, this->parseNumber("1"));
matrixBuilder.newRowGroup(13);
matrixBuilder.addNextValue(13, 6, this->parseNumber("1"));
matrixBuilder.newRowGroup(14);
matrixBuilder.addNextValue(14, 10, this->parseNumber("1"));
matrixBuilder.newRowGroup(15);
matrixBuilder.addNextValue(15, 9, this->parseNumber("1"));
matrixBuilder.addNextValue(16, 11, this->parseNumber("1"));
matrixBuilder.newRowGroup(17);
matrixBuilder.addNextValue(17, 9, this->parseNumber("1"));
matrixBuilder.newRowGroup(18);
matrixBuilder.addNextValue(18, 5, this->parseNumber("0.4"));
matrixBuilder.addNextValue(18, 8, this->parseNumber("0.3"));
matrixBuilder.addNextValue(18, 11, this->parseNumber("0.3"));
matrixBuilder.newRowGroup(19);
matrixBuilder.addNextValue(19, 7, this->parseNumber("0.7"));
matrixBuilder.addNextValue(19, 12, this->parseNumber("0.3"));
matrixBuilder.newRowGroup(20);
matrixBuilder.addNextValue(20, 12, this->parseNumber("0.1"));
matrixBuilder.addNextValue(20, 13, this->parseNumber("0.9"));
matrixBuilder.addNextValue(21, 12, this->parseNumber("1"));
storm::storage::SparseMatrix<ValueType> transitionMatrix = matrixBuilder.build();
storm::models::sparse::StateLabeling ap(15);
ap.addLabel("a");
ap.addLabelToState("a", 1);
ap.addLabelToState("a", 4);
ap.addLabelToState("a", 5);
ap.addLabelToState("a", 7);
ap.addLabelToState("a", 11);
ap.addLabelToState("a", 13);
ap.addLabelToState("a", 14);
mdp.reset(new storm::models::sparse::Mdp<ValueType>(transitionMatrix, ap));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("37 / 60"), quantitativeResult1[0], this->precision());
EXPECT_NEAR(this->parseNumber("2/3"), quantitativeResult1[3], this->precision());
EXPECT_NEAR(this->parseNumber("0.5"), quantitativeResult1[6], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult1[9], this->precision());
EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[12], this->precision());
EXPECT_NEAR(this->parseNumber("101 / 200"), quantitativeResult1[13], this->precision());
EXPECT_NEAR(this->parseNumber("31 / 60"), quantitativeResult1[14], this->precision());
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[0], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[3], this->precision());
EXPECT_NEAR(this->parseNumber("1/3"), quantitativeResult2[6], this->precision());
EXPECT_NEAR(this->parseNumber("0"), quantitativeResult2[9], this->precision());
EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[12], this->precision());
EXPECT_NEAR(this->parseNumber("79 / 300"), quantitativeResult2[13], this->precision());
EXPECT_NEAR(this->parseNumber("0.1"), quantitativeResult2[14], this->precision());
}
}
TYPED_TEST(LraMdpPrctlModelCheckerTest, cs_nfail) {
typedef typename TestFixture::ValueType ValueType;
std::string formulasString = "R{\"grants\"}max=? [ MP ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/cs_nfail3.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(184ul, model->getNumberOfStates());
EXPECT_EQ(541ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker.check(this->env(), tasks[0]);
storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>& quantitativeResult = result->asExplicitQuantitativeCheckResult<ValueType>();
EXPECT_NEAR(this->parseNumber("333/1000"), quantitativeResult[*mdp->getInitialStates().begin()], this->precision());
}
}

607
src/test/storm/modelchecker/prctl/MdpPrctlModelCheckerTest.cpp
View File

@ -1,607 +0,0 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm/api/builder.h"
#include "storm-conv/api/storm-conv.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/symbolic/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/QualitativeCheckResult.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/logic/Formulas.h"
#include "storm/storage/jani/Property.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace {
enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd};
class SparseDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class JaniSparseDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::JaniSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class JitSparseDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::JitSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class SparseDoubleIntervalIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::IntervalIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
env.solver().minMax().setRelativeTerminationCriterion(false);
return env;
}
};
class SparseDoubleSoundValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
env.solver().minMax().setRelativeTerminationCriterion(false);
return env;
}
};
class SparseDoubleTopologicalValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
env.solver().minMax().setRelativeTerminationCriterion(false);
return env;
}
};
class SparseDoubleTopologicalSoundValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::Topological);
env.solver().topological().setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod::SoundValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
env.solver().minMax().setRelativeTerminationCriterion(false);
return env;
}
};
class SparseRationalPolicyIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
return env;
}
};
class SparseRationalViToPiEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ViToPi);
return env;
}
};
class SparseRationalRationalSearchEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan; // Unused for sparse models
static const MdpEngine engine = MdpEngine::PrismSparse;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::sparse::Mdp<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
return env;
}
};
class HybridCuddDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const MdpEngine engine = MdpEngine::Hybrid;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class HybridSylvanDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const MdpEngine engine = MdpEngine::Hybrid;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class HybridCuddDoubleSoundValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const MdpEngine engine = MdpEngine::Hybrid;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::SoundValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
env.solver().minMax().setRelativeTerminationCriterion(false);
return env;
}
};
class HybridSylvanRationalPolicyIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const MdpEngine engine = MdpEngine::Hybrid;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
return env;
}
};
class DdCuddDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const MdpEngine engine = MdpEngine::PrismDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class JaniDdCuddDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const MdpEngine engine = MdpEngine::JaniDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class DdSylvanDoubleValueIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const MdpEngine engine = MdpEngine::PrismDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class DdCuddDoublePolicyIterationEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::CUDD;
static const MdpEngine engine = MdpEngine::PrismDd;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class DdSylvanRationalRationalSearchEnvironment {
public:
static const storm::dd::DdType ddType = storm::dd::DdType::Sylvan;
static const MdpEngine engine = MdpEngine::PrismDd;
static const bool isExact = true;
typedef storm::RationalNumber ValueType;
typedef storm::models::symbolic::Mdp<ddType, ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
return env;
}
};
template<typename TestType>
class MdpPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
typedef typename storm::models::sparse::Mdp<ValueType> SparseModelType;
typedef typename storm::models::symbolic::Mdp<TestType::ddType, ValueType> SymbolicModelType;
MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
bool isSymbolicModel() const { return std::is_same<typename TestType::ModelType, SymbolicModelType>::value; }
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
if (TestType::engine == MdpEngine::PrismSparse) {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) {
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second, TestType::engine == MdpEngine::JitSparse)->template as<MT>();
}
return result;
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
} else if (TestType::engine == MdpEngine::JaniDd) {
auto janiData = storm::api::convertPrismToJani(program, storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
janiData.first.substituteFunctions();
result.second = storm::api::extractFormulasFromProperties(janiData.second);
result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
}
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
if (TestType::engine == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse || TestType::engine == MdpEngine::JitSparse) {
return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model);
}
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
if (TestType::engine == MdpEngine::Hybrid) {
return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*model);
} else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) {
return std::make_shared<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*model);
}
}
bool getQualitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
auto filter = getInitialStateFilter(model);
result->filter(*filter);
return result->asQualitativeCheckResult().forallTrue();
}
ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
auto filter = getInitialStateFilter(model);
result->filter(*filter);
return result->asQuantitativeCheckResult<ValueType>().getMin();
}
private:
storm::Environment _environment;
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
if (isSparseModel()) {
return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
} else {
return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
}
}
};
typedef ::testing::Types<
SparseDoubleValueIterationEnvironment,
JaniSparseDoubleValueIterationEnvironment,
JitSparseDoubleValueIterationEnvironment,
SparseDoubleIntervalIterationEnvironment,
SparseDoubleSoundValueIterationEnvironment,
SparseDoubleTopologicalValueIterationEnvironment,
SparseDoubleTopologicalSoundValueIterationEnvironment,
SparseRationalPolicyIterationEnvironment,
SparseRationalViToPiEnvironment,
SparseRationalRationalSearchEnvironment,
HybridCuddDoubleValueIterationEnvironment,
HybridSylvanDoubleValueIterationEnvironment,
HybridCuddDoubleSoundValueIterationEnvironment,
HybridSylvanRationalPolicyIterationEnvironment,
DdCuddDoubleValueIterationEnvironment,
JaniDdCuddDoubleValueIterationEnvironment,
DdSylvanDoubleValueIterationEnvironment,
DdCuddDoublePolicyIterationEnvironment,
DdSylvanRationalRationalSearchEnvironment
> TestingTypes;
TYPED_TEST_SUITE(MdpPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(MdpPrctlModelCheckerTest, Dice) {
std::string formulasString = "Pmin=? [F \"two\"]";
formulasString += "; Pmax=? [F \"two\"]";
formulasString += "; Pmin=? [F \"three\"]";
formulasString += "; Pmax=? [F \"three\"]";
formulasString += "; Pmin=? [F \"four\"]";
formulasString += "; Pmax=? [F \"four\"]";
formulasString += "; Rmin=? [F \"done\"]";
formulasString += "; Rmax=? [F \"done\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("1/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("2/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("3/36"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[7]);
EXPECT_NEAR(this->parseNumber("22/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) {
std::string formulasString = "Pmin=? [F \"elected\"]";
formulasString += "; Pmax=? [F \"elected\"]";
formulasString += "; Pmin=? [F<=25 \"elected\"]";
formulasString += "; Pmax=? [F<=25 \"elected\"]";
formulasString += "; Rmin=? [F \"elected\"]";
formulasString += "; Rmax=? [F \"elected\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/leader4.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("1/16"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("30/7"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(MdpPrctlModelCheckerTest, consensus) {
std::string formulasString = "Pmax=? [F \"finished\"]";
formulasString += "; Pmax=? [F \"all_coins_equal_1\"]";
formulasString += "; P<0.8 [F \"all_coins_equal_1\"]";
formulasString += "; P<0.9 [F \"all_coins_equal_1\"]";
formulasString += "; Rmax=? [F \"all_coins_equal_1\"]";
formulasString += "; Rmin=? [F \"all_coins_equal_1\"]";
formulasString += "; Rmax=? [F \"finished\"]";
formulasString += "; Rmin=? [F \"finished\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(272ul, model->getNumberOfStates());
EXPECT_EQ(492ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("57/64"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_FALSE(this->getQualitativeResultAtInitialState(model, result));
result = checker->check(this->env(), tasks[3]);
EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
result = checker->check(this->env(), tasks[4]);
EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
result = checker->check(this->env(), tasks[5]);
EXPECT_TRUE(storm::utility::isInfinity(this->getQuantitativeResultAtInitialState(model, result)));
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("75"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[7]);
EXPECT_NEAR(this->parseNumber("48"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) {
std::string formulasString = "Rmin=? [F \"target\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/tiny_rewards.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(3ul, model->getNumberOfStates());
EXPECT_EQ(4ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// This example considers a zero-reward end component that does not reach the target
// For some methods this requires end-component elimination which is (currently) not supported in the Dd engine
if (TypeParam::engine == MdpEngine::PrismDd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) {
STORM_SILENT_EXPECT_THROW(checker->check(this->env(), tasks[0]), storm::exceptions::UncheckedRequirementException);
} else {
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
}
TYPED_TEST(MdpPrctlModelCheckerTest, Team) {
std::string formulasString = "R{\"w_1_total\"}max=? [ C ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/multiobj_team3.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(12475ul, model->getNumberOfStates());
EXPECT_EQ(15228ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// This example considers an expected total reward formula, which is not supported in all engines
if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse || TypeParam::engine == MdpEngine::JitSparse) {
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("114/49"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
} else {
EXPECT_FALSE(checker->canHandle(tasks[0]));
}
}
}

302
src/test/storm/modelchecker/prctl/QuantileQueryTest.cpp
View File

@ -1,302 +0,0 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm/api/builder.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm/parser/CSVParser.h"
#include "storm/models/sparse/Mdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/logic/Formulas.h"
#include "storm/storage/jani/Property.h"
namespace {
enum class MdpEngine {PrismSparse, JaniSparse, JitSparse, Hybrid, PrismDd, JaniDd};
class UnsoundEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
return env;
}
};
class SoundEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setForceSoundness(true);
return env;
}
};
class ExactEnvironment {
public:
typedef storm::RationalNumber ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
return env;
}
};
template<typename TestType>
class QuantileQueryTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
QuantileQueryTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const {
if (input.find("inf") != std::string::npos) {
return storm::utility::infinity<ValueType>();
}
return storm::utility::convertNumber<ValueType>(input);
}
template <typename MT>
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f, true); // only initial states are relevant
}
return result;
}
template <typename MT>
typename std::enable_if<std::is_same<MT, storm::models::sparse::Mdp<ValueType>>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<MT>>(*model);
}
template <typename MT>
typename std::enable_if<std::is_same<MT, storm::models::sparse::Dtmc<ValueType>>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
return std::make_shared<storm::modelchecker::SparseDtmcPrctlModelChecker<MT>>(*model);
}
std::pair<bool, std::string> compareResult(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result, std::vector<std::string> const& expected) {
bool equal = true;
std::string errorMessage = "";
auto filter = getInitialStateFilter(model);
result->filter(*filter);
std::vector<std::vector<ValueType>> resultPoints;
if (result->isExplicitParetoCurveCheckResult()) {
resultPoints = result->asExplicitParetoCurveCheckResult<ValueType>().getPoints();
} else {
if (!result->isExplicitQuantitativeCheckResult()) {
return { false, "The CheckResult has unexpected type."};
}
resultPoints = {{ result->asExplicitQuantitativeCheckResult<ValueType>().getMax() }};
}
std::vector<std::vector<ValueType>> expectedPoints;
for (auto const& pointAsString : expected) {
std::vector<ValueType> point;
for (auto const& entry : storm::parser::parseCommaSeperatedValues(pointAsString)) {
point.push_back(parseNumber(entry));
}
expectedPoints.push_back(std::move(point));
}
for (auto const& resPoint : resultPoints) {
bool contained = false;
for (auto const& expPoint : expectedPoints) {
if (resPoint == expPoint) {
contained = true;
break;
}
}
if (!contained) {
equal = false;
errorMessage += "The result " + storm::utility::vector::toString(resPoint) + " is not contained in the expected solution. ";
}
}
for (auto const& expPoint : expectedPoints) {
bool contained = false;
for (auto const& resPoint : resultPoints) {
if (resPoint == expPoint) {
contained = true;
break;
}
}
if (!contained) {
equal = false;
errorMessage += "The expected " + storm::utility::vector::toString(expPoint) + " is not contained in the obtained solution. ";
}
}
return {equal, errorMessage};
}
private:
storm::Environment _environment;
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model) const {
return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->getInitialStates());
}
};
typedef ::testing::Types<
UnsoundEnvironment,
SoundEnvironment,
ExactEnvironment
> TestingTypes;
TYPED_TEST_SUITE(QuantileQueryTest, TestingTypes);
TYPED_TEST(QuantileQueryTest, simple_Dtmc) {
typedef storm::models::sparse::Dtmc<typename TestFixture::ValueType> ModelType;
std::string formulasString = "quantile(max A, max B, P>0.95 [F{\"first\"}<=A,{\"second\"}<=B s=3]);\n";
auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/dtmc/quantiles_simple_dtmc.pm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(4ul, model->getNumberOfStates());
EXPECT_EQ(6ul, model->getNumberOfTransitions());
auto checker = this->template createModelChecker<ModelType>(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
std::vector<std::string> expectedResult;
std::pair<bool, std::string> compare;
uint64_t taskId = 0;
expectedResult.clear();
expectedResult.push_back("7, 18");
expectedResult.push_back("8, 16");
expectedResult.push_back("9, 14");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
}
TYPED_TEST(QuantileQueryTest, simple_Mdp) {
typedef storm::models::sparse::Mdp<typename TestFixture::ValueType> ModelType;
std::string formulasString = "quantile(B1, B2, Pmax>0.5 [F{\"first\"}>=B1,{\"second\"}>=B2 s=1]);\n";
formulasString += "quantile(B1, B2, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n";
formulasString += "quantile(B1, B2, Pmin>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2 s=1]);\n";
formulasString += "quantile(B1, Pmax>0.5 [F{\"second\"}>=B1 s=1]);\n";
formulasString += "quantile(B1, B2, B3, Pmax>0.5 [F{\"first\"}<=B1,{\"second\"}<=B2,{\"third\"}<=B3 s=1]);\n";
auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_simple_mdp.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(7ul, model->getNumberOfStates());
EXPECT_EQ(13ul, model->getNumberOfTransitions());
auto checker = this->template createModelChecker<ModelType>(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
std::vector<std::string> expectedResult;
std::pair<bool, std::string> compare;
uint64_t taskId = 0;
expectedResult.clear();
expectedResult.push_back(" 0, 6");
expectedResult.push_back(" 1, 5");
expectedResult.push_back(" 2, 4");
expectedResult.push_back(" 3, 3");
expectedResult.push_back("inf, 2");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
expectedResult.clear();
expectedResult.push_back(" 0, 2");
expectedResult.push_back(" 5, 1");
expectedResult.push_back(" 6, 0");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
expectedResult.clear();
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
expectedResult.clear();
expectedResult.push_back(" 6");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
expectedResult.clear();
expectedResult.push_back(" 0, 2, 1.4");
expectedResult.push_back(" 5, 1, 9.8");
expectedResult.push_back(" 6, 0, 9.8");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
}
TYPED_TEST(QuantileQueryTest, firewire) {
typedef storm::models::sparse::Mdp<typename TestFixture::ValueType> ModelType;
std::string formulasString = "quantile(min TIME, min ROUNDS, Pmax>0.95 [F{\"time\"}<=TIME,{\"rounds\"}<=ROUNDS \"done\"]);\n";
auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_firewire.nm", formulasString, "delay=36");
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(776ul, model->getNumberOfStates());
EXPECT_EQ(1411ul, model->getNumberOfTransitions());
auto checker = this->template createModelChecker<ModelType>(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
std::vector<std::string> expectedResult;
std::pair<bool, std::string> compare;
uint64_t taskId = 0;
expectedResult.clear();
expectedResult.push_back("123, 1");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
}
TYPED_TEST(QuantileQueryTest, resources) {
typedef storm::models::sparse::Mdp<typename TestFixture::ValueType> ModelType;
std::string formulasString = "quantile(max GOLD, max GEM, Pmax>0.95 [F{\"gold\"}>=GOLD,{\"gem\"}>=GEM,{\"steps\"}<=100 true]);\n";
auto modelFormulas = this->template buildModelFormulas<ModelType>(STORM_TEST_RESOURCES_DIR "/mdp/quantiles_resources.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(94ul, model->getNumberOfStates());
EXPECT_EQ(326ul, model->getNumberOfTransitions());
auto checker = this->template createModelChecker<ModelType>(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
std::vector<std::string> expectedResult;
std::pair<bool, std::string> compare;
uint64_t taskId = 0;
expectedResult.clear();
expectedResult.push_back("0, 10");
expectedResult.push_back("1, 9");
expectedResult.push_back("4, 8");
expectedResult.push_back("7, 7");
expectedResult.push_back("8, 4");
expectedResult.push_back("9, 2");
expectedResult.push_back("10, 0");
result = checker->check(this->env(), tasks[taskId++]);
compare = this->compareResult(model, result, expectedResult);
EXPECT_TRUE(compare.first) << compare.second;
}
}

142
src/test/storm/modelchecker/prctl/SchedulerGenerationMdpPrctlModelCheckerTest.cpp
View File

@ -1,142 +0,0 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/solver/StandardMinMaxLinearEquationSolver.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/modules/GeneralSettings.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm-parsers/parser/AutoParser.h"
#include "storm-parsers/parser/PrismParser.h"
#include "storm/builder/ExplicitModelBuilder.h"
namespace {
class DoubleViEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class DoubleSoundViEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().setForceSoundness(true);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-6));
return env;
}
};
class DoublePIEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
class RationalPIEnvironment {
public:
typedef storm::RationalNumber ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::PolicyIteration);
return env;
}
};
// class RationalRationalSearchEnvironment {
// public:
// typedef storm::RationalNumber ValueType;
// static storm::Environment createEnvironment() {
// storm::Environment env;
// env.solver().minMax().setMethod(storm::solver::MinMaxMethod::RationalSearch);
// return env;
// }
// };
template<typename TestType>
class SchedulerGenerationMdpPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
SchedulerGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
private:
storm::Environment _environment;
};
typedef ::testing::Types<
DoubleViEnvironment,
DoubleSoundViEnvironment,
DoublePIEnvironment,
RationalPIEnvironment
//RationalRationalSearchEnvironment
> TestingTypes;
TYPED_TEST_SUITE(SchedulerGenerationMdpPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(SchedulerGenerationMdpPrctlModelCheckerTest, reachability) {
typedef typename TestFixture::ValueType ValueType;
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/scheduler_generation.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels();
std::shared_ptr<storm::models::sparse::Model<ValueType>> model = storm::builder::ExplicitModelBuilder<ValueType>(program, options).build();
EXPECT_EQ(4ull, model->getNumberOfStates());
EXPECT_EQ(11ull, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::sparse::Mdp<ValueType>> mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
EXPECT_EQ(7ull, mdp->getNumberOfChoices());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"target\"]");
storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> checkTask(*formula);
checkTask.setProduceSchedulers(true);
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), checkTask);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const& scheduler = result->asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
EXPECT_EQ(0ull, scheduler.getChoice(0).getDeterministicChoice());
EXPECT_EQ(1ull, scheduler.getChoice(1).getDeterministicChoice());
EXPECT_EQ(0ull, scheduler.getChoice(2).getDeterministicChoice());
EXPECT_EQ(0ull, scheduler.getChoice(3).getDeterministicChoice());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]");
checkTask = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*formula);
checkTask.setProduceSchedulers(true);
result = checker.check(checkTask);
ASSERT_TRUE(result->isExplicitQuantitativeCheckResult());
ASSERT_TRUE(result->asExplicitQuantitativeCheckResult<ValueType>().hasScheduler());
storm::storage::Scheduler<ValueType> const& scheduler2 = result->asExplicitQuantitativeCheckResult<ValueType>().getScheduler();
EXPECT_EQ(1ull, scheduler2.getChoice(0).getDeterministicChoice());
EXPECT_EQ(2ull, scheduler2.getChoice(1).getDeterministicChoice());
EXPECT_EQ(0ull, scheduler2.getChoice(2).getDeterministicChoice());
EXPECT_EQ(0ull, scheduler2.getChoice(3).getDeterministicChoice());
}
}
Write Preview
Loading…
Cancel
Save