1#include "storm-config.h"
19class GmmxxDoubleGmresEnvironment {
22 static const bool isExact =
false;
33class EigenDoubleDGmresEnvironment {
36 static const bool isExact =
false;
47class EigenRationalLUEnvironment {
50 static const bool isExact =
true;
59class NativeSorEnvironment {
62 static const bool isExact =
false;
73class NativePowerEnvironment {
76 static const bool isExact =
false;
86class NativeWalkerChaeEnvironment {
89 static const bool isExact =
false;
100template<
typename TestType>
101class ConditionalDtmcPrctlModelCheckerTest :
public ::testing::Test {
103 typedef typename TestType::ValueType
ValueType;
104 ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
106 void SetUp()
override {
108 GTEST_SKIP() <<
"Z3 not available.";
116 return storm::utility::convertNumber<ValueType>(input);
126typedef ::testing::Types<GmmxxDoubleGmresEnvironment, EigenDoubleDGmresEnvironment, EigenRationalLUEnvironment, NativeSorEnvironment, NativePowerEnvironment,
127 NativeWalkerChaeEnvironment>
132TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
133 typedef typename TestFixture::ValueType
ValueType;
141 ASSERT_EQ(4ul, model->getNumberOfStates());
142 ASSERT_EQ(5ul, model->getNumberOfTransitions());
144 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
150 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
152 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"target\"]");
154 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
156 EXPECT_NEAR(this->
parseNumber(
"0.5"), quantitativeResult1[0], this->precision());
158 formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"target\" || F \"condition\"]");
160 result = checker.check(this->env(), *formula);
162 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
164 formula = formulaParser.parseSingleFormulaFromString(
"R=? [F \"target\"]");
166 result = checker.check(this->env(), *formula);
168 EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
170 formula = formulaParser.parseSingleFormulaFromString(
"R=? [F \"target\" || F \"condition\"]");
172 result = checker.check(this->env(), *formula);
174 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult4[0], this->precision());
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
SolverEnvironment & solver()
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
void setSorOmega(storm::RationalNumber const &value)
void setMaximalNumberOfIterations(uint64_t value)
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
EigenSolverEnvironment & eigen()
NativeSolverEnvironment & native()
GmmxxSolverEnvironment & gmmxx()
BuilderOptions & setBuildAllLabels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
BuilderOptions & setBuildAllRewardModels(bool newValue=true)
Should all reward models be built? If not set, only required reward models are build.
std::shared_ptr< storm::models::sparse::Model< ValueType, RewardModelType > > build()
Convert the program given at construction time to an abstract model.
ExplicitQuantitativeCheckResult< ValueType > & asExplicitQuantitativeCheckResult()
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes