1#include "storm-config.h"
17class EigenEnvironment {
26class EliminationEnvironment {
35template<
typename TestType>
36class ParametricDtmcPrctlModelCheckerTest :
public ::testing::Test {
38 ParametricDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
40 void SetUp()
override {
42 GTEST_SKIP() <<
"Z3 not available.";
49 storm::RationalFunctionCoefficient
parseNumber(std::string
const& input)
const {
50 return storm::utility::convertNumber<storm::RationalFunctionCoefficient>(input);
57typedef ::testing::Types<EigenEnvironment, EliminationEnvironment>
TestingTypes;
60TYPED_TEST(ParametricDtmcPrctlModelCheckerTest, Die) {
64 std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model =
69 auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
76 ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
77 ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
79 std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
81 ASSERT_EQ(variables.size(), 1ull);
82 instantiation.emplace(*variables.begin(), this->parseNumber(
"1/2"));
86 std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"one\"]");
88 std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
94 formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"two\"]");
96 result = checker.check(this->env(), *formula);
102 formula = formulaParser.parseSingleFormulaFromString(
"P=? [F \"three\"]");
104 result = checker.check(this->env(), *formula);
110 formula = formulaParser.parseSingleFormulaFromString(
"R=? [F \"done\"]");
112 result = checker.check(this->env(), *formula);
SolverEnvironment & solver()
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
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()
This class represents a discrete-time Markov chain.
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.
std::set< storm::RationalFunctionVariable > getProbabilityParameters(Model< storm::RationalFunction > const &model)
Get all probability parameters occurring on transitions.
NumberType parseNumber(std::string const &value)
Parse number from string.
CoefficientType< FunctionType >::type evaluate(FunctionType const &function, Valuation< FunctionType > const &valuation)
Evaluates the given function wrt.
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes