1#include "storm-config.h"
31enum class MdpEngine { PrismSparse, JaniSparse,
Hybrid, PrismDd, JaniDd };
33class SparseDoubleValueIterationViOpGaussSeidelMultEnvironment {
36 static const MdpEngine engine = MdpEngine::PrismSparse;
37 static const bool isExact =
false;
50class SparseDoubleValueIterationViOpRegularMultEnvironment {
53 static const MdpEngine engine = MdpEngine::PrismSparse;
54 static const bool isExact =
false;
67class SparseDoubleValueIterationNativeGaussSeidelMultEnvironment {
70 static const MdpEngine engine = MdpEngine::PrismSparse;
71 static const bool isExact =
false;
84class SparseDoubleValueIterationNativeRegularMultEnvironment {
87 static const MdpEngine engine = MdpEngine::PrismSparse;
88 static const bool isExact =
false;
101class JaniSparseDoubleValueIterationEnvironment {
104 static const MdpEngine engine = MdpEngine::JaniSparse;
105 static const bool isExact =
false;
116class SparseDoubleIntervalIterationEnvironment {
119 static const MdpEngine engine = MdpEngine::PrismSparse;
120 static const bool isExact =
false;
133class SparseDoubleSoundValueIterationEnvironment {
136 static const MdpEngine engine = MdpEngine::PrismSparse;
137 static const bool isExact =
false;
150class SparseDoubleOptimisticValueIterationEnvironment {
153 static const MdpEngine engine = MdpEngine::PrismSparse;
154 static const bool isExact =
false;
167class SparseDoubleGuessingValueIterationEnvironment {
170 static const MdpEngine engine = MdpEngine::PrismSparse;
171 static const bool isExact =
false;
184class SparseDoubleTopologicalValueIterationEnvironment {
187 static const MdpEngine engine = MdpEngine::PrismSparse;
188 static const bool isExact =
false;
201class SparseDoubleTopologicalSoundValueIterationEnvironment {
204 static const MdpEngine engine = MdpEngine::PrismSparse;
205 static const bool isExact =
false;
219class SparseDoubleTopologicalGuessingValueIterationEnvironment {
222 static const MdpEngine engine = MdpEngine::PrismSparse;
223 static const bool isExact =
false;
237class SparseDoubleLPEnvironment {
240 static const MdpEngine engine = MdpEngine::PrismSparse;
241 static const bool isExact =
false;
252class SparseDoubleViToLPEnvironment {
255 static const MdpEngine engine = MdpEngine::PrismSparse;
256 static const bool isExact =
false;
267class SparseRationalPolicyIterationEnvironment {
270 static const MdpEngine engine = MdpEngine::PrismSparse;
271 static const bool isExact =
true;
281class SparseRationalViToPiEnvironment {
284 static const MdpEngine engine = MdpEngine::PrismSparse;
285 static const bool isExact =
true;
295class SparseRationalRationalSearchEnvironment {
298 static const MdpEngine engine = MdpEngine::PrismSparse;
299 static const bool isExact =
true;
308class HybridCuddDoubleValueIterationEnvironment {
311 static const MdpEngine engine = MdpEngine::Hybrid;
312 static const bool isExact =
false;
322class HybridSylvanDoubleValueIterationEnvironment {
325 static const MdpEngine engine = MdpEngine::Hybrid;
326 static const bool isExact =
false;
336class HybridCuddDoubleSoundValueIterationEnvironment {
339 static const MdpEngine engine = MdpEngine::Hybrid;
340 static const bool isExact =
false;
352class HybridCuddDoubleOptimisticValueIterationEnvironment {
355 static const MdpEngine engine = MdpEngine::Hybrid;
356 static const bool isExact =
false;
368class HybridCuddDoubleGuessingValueIterationEnvironment {
371 static const MdpEngine engine = MdpEngine::Hybrid;
372 static const bool isExact =
false;
384class HybridSylvanRationalPolicyIterationEnvironment {
387 static const MdpEngine engine = MdpEngine::Hybrid;
388 static const bool isExact =
true;
397class DdCuddDoubleValueIterationEnvironment {
400 static const MdpEngine engine = MdpEngine::PrismDd;
401 static const bool isExact =
false;
411class JaniDdCuddDoubleValueIterationEnvironment {
414 static const MdpEngine engine = MdpEngine::JaniDd;
415 static const bool isExact =
false;
425class DdSylvanDoubleValueIterationEnvironment {
428 static const MdpEngine engine = MdpEngine::PrismDd;
429 static const bool isExact =
false;
439class DdCuddDoublePolicyIterationEnvironment {
442 static const MdpEngine engine = MdpEngine::PrismDd;
443 static const bool isExact =
false;
453class DdSylvanRationalRationalSearchEnvironment {
456 static const MdpEngine engine = MdpEngine::PrismDd;
457 static const bool isExact =
true;
467template<
typename TestType>
468class MdpPrctlModelCheckerTest :
public ::testing::Test {
470 typedef typename TestType::ValueType
ValueType;
474 MdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
476 void SetUp()
override {
478 GTEST_SKIP() <<
"Z3 not available.";
486 return storm::utility::convertNumber<ValueType>(input);
491 bool isSparseModel()
const {
492 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
494 bool isSymbolicModel()
const {
495 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
498 template<
typename MT =
typename TestType::ModelType>
499 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
500 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
501 buildModelFormulas(std::string
const& pathToPrismFile, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
502 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
505 if (TestType::engine == MdpEngine::PrismSparse) {
507 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
508 }
else if (TestType::engine == MdpEngine::JaniSparse) {
510 janiData.first.substituteFunctions();
512 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
517 template<
typename MT =
typename TestType::ModelType>
518 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
519 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
520 buildModelFormulas(std::string
const& pathToPrismFile, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
521 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
524 if (TestType::engine == MdpEngine::Hybrid || TestType::engine == MdpEngine::PrismDd) {
526 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
527 }
else if (TestType::engine == MdpEngine::JaniDd) {
529 janiData.first.substituteFunctions();
531 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
536 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
537 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas)
const {
538 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
539 for (
auto const& f : formulas) {
540 result.emplace_back(*f);
545 template<
typename MT =
typename TestType::ModelType>
546 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
547 std::shared_ptr<MT>
const& model)
const {
548 if (TestType::engine == MdpEngine::PrismSparse || TestType::engine == MdpEngine::JaniSparse) {
549 return std::make_shared<storm::modelchecker::SparseMdpPrctlModelChecker<SparseModelType>>(*model);
553 template<
typename MT =
typename TestType::ModelType>
554 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
555 createModelChecker(std::shared_ptr<MT>
const& model)
const {
556 if (TestType::engine == MdpEngine::Hybrid) {
557 return std::make_shared<storm::modelchecker::HybridMdpPrctlModelChecker<SymbolicModelType>>(*model);
558 }
else if (TestType::engine == MdpEngine::PrismDd || TestType::engine == MdpEngine::JaniDd) {
559 return std::make_shared<storm::modelchecker::SymbolicMdpPrctlModelChecker<SymbolicModelType>>(*model);
563 template<
typename MT =
typename TestType::ModelType>
564 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
void>::type execute(std::shared_ptr<MT>
const& model,
565 std::function<
void()>
const& f)
const {
569 template<
typename MT =
typename TestType::ModelType>
570 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
void>::type execute(std::shared_ptr<MT>
const& model,
571 std::function<
void()>
const& f)
const {
572 model->getManager().execute(f);
576 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
578 result->filter(*filter);
579 return result->asQualitativeCheckResult().forallTrue();
583 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
585 result->filter(*filter);
586 return result->asQuantitativeCheckResult<
ValueType>().getMin();
593 if (isSparseModel()) {
594 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
596 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
597 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
602typedef ::testing::Types<SparseDoubleValueIterationViOpGaussSeidelMultEnvironment, SparseDoubleValueIterationViOpRegularMultEnvironment,
603 SparseDoubleValueIterationNativeGaussSeidelMultEnvironment, SparseDoubleValueIterationNativeRegularMultEnvironment,
604 JaniSparseDoubleValueIterationEnvironment, SparseDoubleIntervalIterationEnvironment, SparseDoubleSoundValueIterationEnvironment,
605 SparseDoubleOptimisticValueIterationEnvironment, SparseDoubleGuessingValueIterationEnvironment,
606 SparseDoubleTopologicalValueIterationEnvironment, SparseDoubleTopologicalSoundValueIterationEnvironment,
607 SparseDoubleTopologicalGuessingValueIterationEnvironment, SparseDoubleLPEnvironment, SparseDoubleViToLPEnvironment,
608 SparseRationalPolicyIterationEnvironment, SparseRationalViToPiEnvironment, SparseRationalRationalSearchEnvironment,
609 HybridCuddDoubleValueIterationEnvironment, HybridSylvanDoubleValueIterationEnvironment, HybridCuddDoubleSoundValueIterationEnvironment,
610 HybridCuddDoubleOptimisticValueIterationEnvironment, HybridCuddDoubleGuessingValueIterationEnvironment,
611 HybridSylvanRationalPolicyIterationEnvironment, DdCuddDoubleValueIterationEnvironment, JaniDdCuddDoubleValueIterationEnvironment,
612 DdSylvanDoubleValueIterationEnvironment, DdCuddDoublePolicyIterationEnvironment, DdSylvanRationalRationalSearchEnvironment>
618 std::string formulasString =
"Pmin=? [F \"two\"]";
619 formulasString +=
"; Pmax=? [F \"two\"]";
620 formulasString +=
"; Pmin=? [F \"three\"]";
621 formulasString +=
"; Pmax=? [F \"three\"]";
622 formulasString +=
"; Pmin=? [F \"four\"]";
623 formulasString +=
"; Pmax=? [F \"four\"]";
624 formulasString +=
"; Rmin=? [F \"done\"]";
625 formulasString +=
"; Rmax=? [F \"done\"]";
627 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/two_dice.nm", formulasString);
628 auto model = std::move(modelFormulas.first);
629 auto tasks = this->getTasks(modelFormulas.second);
630 this->execute(model, [&]() {
631 EXPECT_EQ(169ul, model->getNumberOfStates());
632 EXPECT_EQ(436ul, model->getNumberOfTransitions());
635 auto checker = this->createModelChecker(model);
636 std::unique_ptr<storm::modelchecker::CheckResult> result;
638 result = checker->check(this->env(), tasks[0]);
641 result = checker->check(this->env(), tasks[1]);
644 result = checker->check(this->env(), tasks[2]);
647 result = checker->check(this->env(), tasks[3]);
650 result = checker->check(this->env(), tasks[4]);
653 result = checker->check(this->env(), tasks[5]);
656 result = checker->check(this->env(), tasks[6]);
659 result = checker->check(this->env(), tasks[7]);
664TYPED_TEST(MdpPrctlModelCheckerTest, AsynchronousLeader) {
665 std::string formulasString =
"Pmin=? [F \"elected\"]";
666 formulasString +=
"; Pmax=? [F \"elected\"]";
667 formulasString +=
"; Pmin=? [F<=25 \"elected\"]";
668 formulasString +=
"; Pmax=? [F<=25 \"elected\"]";
669 formulasString +=
"; Rmin=? [F \"elected\"]";
670 formulasString +=
"; Rmax=? [F \"elected\"]";
672 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/leader4.nm", formulasString);
673 auto model = std::move(modelFormulas.first);
674 auto tasks = this->getTasks(modelFormulas.second);
675 this->execute(model, [&]() {
676 EXPECT_EQ(3172ul, model->getNumberOfStates());
677 EXPECT_EQ(7144ul, model->getNumberOfTransitions());
679 auto checker = this->createModelChecker(model);
680 std::unique_ptr<storm::modelchecker::CheckResult> result;
682 result = checker->check(this->env(), tasks[0]);
685 result = checker->check(this->env(), tasks[1]);
688 result = checker->check(this->env(), tasks[2]);
691 result = checker->check(this->env(), tasks[3]);
694 result = checker->check(this->env(), tasks[4]);
697 result = checker->check(this->env(), tasks[5]);
702TYPED_TEST(MdpPrctlModelCheckerTest, consensus) {
703 std::string formulasString =
"Pmax=? [F \"finished\"]";
704 formulasString +=
"; Pmax=? [F \"all_coins_equal_1\"]";
705 formulasString +=
"; P<0.8 [F \"all_coins_equal_1\"]";
706 formulasString +=
"; P<0.9 [F \"all_coins_equal_1\"]";
707 formulasString +=
"; Rmax=? [F \"all_coins_equal_1\"]";
708 formulasString +=
"; Rmin=? [F \"all_coins_equal_1\"]";
709 formulasString +=
"; Rmax=? [F \"finished\"]";
710 formulasString +=
"; Rmin=? [F \"finished\"]";
712 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/coin2-2.nm", formulasString);
713 auto model = std::move(modelFormulas.first);
714 auto tasks = this->getTasks(modelFormulas.second);
715 this->execute(model, [&]() {
716 EXPECT_EQ(272ul, model->getNumberOfStates());
717 EXPECT_EQ(492ul, model->getNumberOfTransitions());
719 auto checker = this->createModelChecker(model);
720 std::unique_ptr<storm::modelchecker::CheckResult> result;
722 result = checker->check(this->env(), tasks[0]);
725 result = checker->check(this->env(), tasks[1]);
728 result = checker->check(this->env(), tasks[2]);
729 EXPECT_FALSE(this->getQualitativeResultAtInitialState(model, result));
731 result = checker->check(this->env(), tasks[3]);
732 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
734 result = checker->check(this->env(), tasks[4]);
737 result = checker->check(this->env(), tasks[5]);
740 result = checker->check(this->env(), tasks[6]);
743 result = checker->check(this->env(), tasks[7]);
748TYPED_TEST(MdpPrctlModelCheckerTest, TinyRewards) {
749 std::string formulasString =
"Rmin=? [F \"target\"]";
750 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/tiny_rewards.nm", formulasString);
751 auto model = std::move(modelFormulas.first);
752 auto tasks = this->getTasks(modelFormulas.second);
753 this->execute(model, [&]() {
754 EXPECT_EQ(3ul, model->getNumberOfStates());
755 EXPECT_EQ(4ul, model->getNumberOfTransitions());
757 auto checker = this->createModelChecker(model);
758 std::unique_ptr<storm::modelchecker::CheckResult> result;
763 if (TypeParam::engine == MdpEngine::PrismDd && this->env().solver().minMax().getMethod() == storm::solver::MinMaxMethod::RationalSearch) {
766 result = checker->check(this->env(), tasks[0]);
773 std::string formulasString =
"R{\"w_1_total\"}max=? [ C ]";
774 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/multiobj_team3.nm", formulasString);
775 auto model = std::move(modelFormulas.first);
776 auto tasks = this->getTasks(modelFormulas.second);
777 this->execute(model, [&]() {
778 EXPECT_EQ(12475ul, model->getNumberOfStates());
779 EXPECT_EQ(15228ul, model->getNumberOfTransitions());
781 auto checker = this->createModelChecker(model);
782 std::unique_ptr<storm::modelchecker::CheckResult> result;
786 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
787 result = checker->check(this->env(), tasks[0]);
790 EXPECT_FALSE(checker->canHandle(tasks[0]));
795TYPED_TEST(MdpPrctlModelCheckerTest, LtlProbabilitiesCoin) {
796#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
797 std::string formulasString =
"Pmin=? [!(GF \"all_coins_equal_1\")]";
798 formulasString +=
"; Pmax=? [F \"all_coins_equal_1\" U \"finished\"]";
799 formulasString +=
"; P>0.4 [!(GF \"all_coins_equal_1\")]";
800 formulasString +=
"; P<0.6 [F \"all_coins_equal_1\" U \"finished\"]";
802 formulasString +=
"; Pmax=?[ (GF \"all_coins_equal_1\") & ((GF \"all_coins_equal_0\") | (FG \"finished\"))]";
804 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/coin2-2.nm", formulasString);
805 auto model = std::move(modelFormulas.first);
806 auto tasks = this->getTasks(modelFormulas.second);
807 this->execute(model, [&]() {
808 EXPECT_EQ(272ul, model->getNumberOfStates());
809 EXPECT_EQ(492ul, model->getNumberOfTransitions());
811 auto checker = this->createModelChecker(model);
812 std::unique_ptr<storm::modelchecker::CheckResult> result;
815 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
816 result = checker->check(this->env(), tasks[0]);
819 result = checker->check(this->env(), tasks[1]);
822 result = checker->check(this->env(), tasks[2]);
823 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
825 result = checker->check(this->env(), tasks[3]);
826 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
828 result = checker->check(this->env(), tasks[4]);
832 EXPECT_FALSE(checker->canHandle(tasks[0]));
840TYPED_TEST(MdpPrctlModelCheckerTest, LtlDice) {
841#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
842 std::string formulasString =
"Pmax=? [ X (((s1=1) U (s1=3)) U (s1=7))]";
843 formulasString +=
"; Pmax=? [ (F (X (s1=6 & (XX s1=5)))) & (F G (d1!=5))]";
844 formulasString +=
"; Pmax=? [ F s1=3 U (\"three\")]";
845 formulasString +=
"; Pmin=? [! F (s2=6) & X \"done\"]";
847 formulasString +=
"; Pmax=? [ ( (G F !(\"two\")) | F G (\"three\") ) & ( (G F !(\"five\") ) | F G (\"seven\") )]";
849 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/two_dice.nm", formulasString);
850 auto model = std::move(modelFormulas.first);
851 auto tasks = this->getTasks(modelFormulas.second);
852 this->execute(model, [&]() {
853 EXPECT_EQ(169ul, model->getNumberOfStates());
854 EXPECT_EQ(436ul, model->getNumberOfTransitions());
856 auto checker = this->createModelChecker(model);
857 std::unique_ptr<storm::modelchecker::CheckResult> result;
860 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
861 result = checker->check(this->env(), tasks[0]);
864 result = checker->check(this->env(), tasks[1]);
867 result = checker->check(this->env(), tasks[2]);
870 result = checker->check(this->env(), tasks[3]);
873 result = checker->check(this->env(), tasks[4]);
877 EXPECT_FALSE(checker->canHandle(tasks[0]));
885TYPED_TEST(MdpPrctlModelCheckerTest, LtlCoinFlips) {
886#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
887 std::string formulasString =
"Pmax=? [ G (true U (heads | \"done\")) ]";
888 formulasString +=
"; Pmin=? [ G (true U (heads | \"done\")) ]";
889 formulasString +=
"; Pmax=? [ G (true U<=10 (heads | \"done\")) ]";
890 formulasString +=
"; Pmin=? [ G (true U<=10 (heads | \"done\")) ]";
891 formulasString +=
"; Pmax=? [ X G (true U<=0 (heads | \"done\")) ]";
892 formulasString +=
"; Pmax=? [ true U[10,12] heads ]";
893 formulasString +=
"; Pmax=? [ X (true U[0,0] heads) ]";
894 formulasString +=
"; Pmax=? [ G (!(P>=1 [\"done\"]) U<=10 (heads | P>=1 [ \"done\"])) ]";
895 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/coin_flips.nm", formulasString);
896 auto model = std::move(modelFormulas.first);
897 auto tasks = this->getTasks(modelFormulas.second);
898 this->execute(model, [&]() {
899 EXPECT_EQ(61ul, model->getNumberOfStates());
900 EXPECT_EQ(177ul, model->getNumberOfTransitions());
902 auto checker = this->createModelChecker(model);
903 std::unique_ptr<storm::modelchecker::CheckResult> result;
906 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
907 result = checker->check(this->env(), tasks[0]);
910 result = checker->check(this->env(), tasks[1]);
913 result = checker->check(this->env(), tasks[2]);
916 result = checker->check(this->env(), tasks[3]);
919 result = checker->check(this->env(), tasks[4]);
922 result = checker->check(this->env(), tasks[5]);
925 result = checker->check(this->env(), tasks[6]);
928 result = checker->check(this->env(), tasks[7]);
932 EXPECT_FALSE(checker->canHandle(tasks[0]));
940TYPED_TEST(MdpPrctlModelCheckerTest, HOADice) {
942 std::string formulasString =
"; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR
"/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"three\", \"p1\" -> s2=1 }]";
944 formulasString +=
"; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR
"/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s2=6), \"p1\" -> \"done\" }]";
946 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/mdp/two_dice.nm", formulasString);
947 auto model = std::move(modelFormulas.first);
948 auto tasks = this->getTasks(modelFormulas.second);
949 this->execute(model, [&]() {
950 EXPECT_EQ(169ul, model->getNumberOfStates());
951 EXPECT_EQ(436ul, model->getNumberOfTransitions());
953 auto checker = this->createModelChecker(model);
954 std::unique_ptr<storm::modelchecker::CheckResult> result;
957 if (TypeParam::engine == MdpEngine::PrismSparse || TypeParam::engine == MdpEngine::JaniSparse) {
958 result = checker->check(tasks[0]);
961 result = checker->check(tasks[1]);
964 EXPECT_FALSE(checker->canHandle(tasks[0]));
std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model)
double getQuantitativeResultAtInitialState(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
SolverEnvironment & solver()
void setMultiplicationStyle(storm::solver::MultiplicationStyle value)
void setPrecision(storm::RationalNumber value)
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
void setRelativeTerminationCriterion(bool value)
void setType(storm::solver::MultiplierType value, bool isSetFromDefault=false)
TopologicalSolverEnvironment & topological()
MinMaxSolverEnvironment & minMax()
void setForceSoundness(bool value)
MultiplierEnvironment & multiplier()
void setUnderlyingMinMaxMethod(storm::solver::MinMaxMethod value)
This class represents a (discrete-time) Markov decision process.
This class represents a discrete-time Markov decision process.
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > convertPrismToJani(storm::prism::Program const &program, storm::converter::PrismToJaniConverterOptions options)
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
storm::storage::BitVector filter(std::vector< T > const &values, std::function< bool(T const &value)> const &function)
Retrieves a bit vector containing all the indices for which the value at this position makes the give...
bool isInfinity(ValueType const &a)
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes
#define STORM_SILENT_EXPECT_THROW(statement, expected_exception)