1#include "storm-config.h"
20class GmmxxDoubleGmresEnvironment {
23 static const bool isExact =
false;
34class EigenDoubleDGmresEnvironment {
37 static const bool isExact =
false;
49class EigenRationalLUEnvironment {
52 static const bool isExact =
true;
61class NativeSorEnvironment {
64 static const bool isExact =
false;
75class NativePowerEnvironment {
78 static const bool isExact =
false;
88class NativeWalkerChaeEnvironment {
91 static const bool isExact =
false;
102template<
typename TestType>
103class ConditionalDtmcPrctlModelCheckerTest :
public ::testing::Test {
105 typedef typename TestType::ValueType
ValueType;
106 ConditionalDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
108 void SetUp()
override {
110 GTEST_SKIP() <<
"Z3 not available.";
118 return storm::utility::convertNumber<ValueType>(input);
128typedef ::testing::Types<
130 GmmxxDoubleGmresEnvironment, EigenDoubleDGmresEnvironment,
132 EigenRationalLUEnvironment, NativeSorEnvironment, NativePowerEnvironment, NativeWalkerChaeEnvironment>
137TYPED_TEST(ConditionalDtmcPrctlModelCheckerTest, Conditional) {
138 typedef typename TestFixture::ValueType
ValueType;
146 ASSERT_EQ(4ul, model->getNumberOfStates());
147 ASSERT_EQ(5ul, model->getNumberOfTransitions());
149 std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
155 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
157 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"target\"]");
159 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
161 EXPECT_NEAR(this->
parseNumber(
"0.5"), quantitativeResult1[0], this->precision());
163 formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"target\" || F \"condition\"]");
165 result = checker.check(this->env(), *formula);
167 EXPECT_NEAR(storm::utility::one<ValueType>(), quantitativeResult2[0], this->precision());
169 formula = formulaParser.parseSingleFormulaFromString(
"R=? [F \"target\"]");
171 result = checker.check(this->env(), *formula);
173 EXPECT_EQ(storm::utility::infinity<ValueType>(), quantitativeResult3[0]);
175 formula = formulaParser.parseSingleFormulaFromString(
"R=? [F \"target\" || F \"condition\"]");
177 result = checker.check(this->env(), *formula);
179 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