From 56d1928b9b7834f73eb480a0ba18d354f123b39b Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Dec 2016 17:02:11 +0100 Subject: [PATCH] resolved some issues (ambiguity for call to carl::rationalize and several warnings because of signed/unsigned comparison) --- src/storm/utility/constants.cpp | 3 +- src/test/abstraction/PrismMenuGameTest.cpp | 144 ++++++------ .../GmmxxMdpPrctlModelCheckerTest.cpp | 34 +-- src/test/parser/FormulaParserTest.cpp | 4 +- src/test/solver/MathsatSmtSolverTest.cpp | 6 +- src/test/solver/Z3SmtSolverTest.cpp | 6 +- src/test/storage/JaniModelTest.cpp | 48 ++-- src/test/storage/PrismProgramTest.cpp | 48 ++-- src/test/utility/GraphTest.cpp | 218 +++++++++--------- 9 files changed, 256 insertions(+), 255 deletions(-) diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp index 991ce4b9d..42be42060 100644 --- a/src/storm/utility/constants.cpp +++ b/src/storm/utility/constants.cpp @@ -315,7 +315,8 @@ namespace storm { template<> RationalNumber convertNumber(uint_fast64_t const& number){ - return carl::rationalize(number); + STORM_LOG_ASSERT(static_cast(number) == number, "Rationalizing failed, because the number is too large."); + return carl::rationalize(static_cast(number)); } template<> diff --git a/src/test/abstraction/PrismMenuGameTest.cpp b/src/test/abstraction/PrismMenuGameTest.cpp index c8e6100c8..9fc283cdb 100644 --- a/src/test/abstraction/PrismMenuGameTest.cpp +++ b/src/test/abstraction/PrismMenuGameTest.cpp @@ -34,9 +34,9 @@ TEST(PrismMenuGame, DieAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(26, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(26ull, game.getNumberOfTransitions()); + EXPECT_EQ(4ull, game.getNumberOfStates()); + EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { @@ -55,9 +55,9 @@ TEST(PrismMenuGame, DieAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(26, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(26ull, game.getNumberOfTransitions()); + EXPECT_EQ(4ull, game.getNumberOfStates()); + EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount()); } #ifdef STORM_HAVE_CARL @@ -103,9 +103,9 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(24, game.getNumberOfTransitions()); - EXPECT_EQ(5, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(24ull, game.getNumberOfTransitions()); + EXPECT_EQ(5ull, game.getNumberOfStates()); + EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { @@ -126,9 +126,9 @@ TEST(PrismMenuGame, DieAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(24, game.getNumberOfTransitions()); - EXPECT_EQ(5, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(24ull, game.getNumberOfTransitions()); + EXPECT_EQ(5ull, game.getNumberOfStates()); + EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { @@ -162,9 +162,9 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(20, game.getNumberOfTransitions()); - EXPECT_EQ(13, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(20ull, game.getNumberOfTransitions()); + EXPECT_EQ(13ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { @@ -198,9 +198,9 @@ TEST(PrismMenuGame, DieFullAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(20, game.getNumberOfTransitions()); - EXPECT_EQ(13, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(20ull, game.getNumberOfTransitions()); + EXPECT_EQ(13ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { @@ -220,9 +220,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(31, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(31ull, game.getNumberOfTransitions()); + EXPECT_EQ(4ull, game.getNumberOfStates()); + EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { @@ -242,9 +242,9 @@ TEST(PrismMenuGame, CrowdsAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(31, game.getNumberOfTransitions()); - EXPECT_EQ(4, game.getNumberOfStates()); - EXPECT_EQ(2, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(31ull, game.getNumberOfTransitions()); + EXPECT_EQ(4ull, game.getNumberOfStates()); + EXPECT_EQ(2ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { @@ -266,9 +266,9 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(68, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(68ull, game.getNumberOfTransitions()); + EXPECT_EQ(8ull, game.getNumberOfStates()); + EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { @@ -290,9 +290,9 @@ TEST(PrismMenuGame, CrowdsAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(68, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(68ull, game.getNumberOfTransitions()); + EXPECT_EQ(8ull, game.getNumberOfStates()); + EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { @@ -366,9 +366,9 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(15113, game.getNumberOfTransitions()); - EXPECT_EQ(8607, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(15113ull, game.getNumberOfTransitions()); + EXPECT_EQ(8607ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { @@ -442,9 +442,9 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(15113, game.getNumberOfTransitions()); - EXPECT_EQ(8607, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(15113ull, game.getNumberOfTransitions()); + EXPECT_EQ(8607ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { @@ -466,9 +466,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(90, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(90ull, game.getNumberOfTransitions()); + EXPECT_EQ(8ull, game.getNumberOfStates()); + EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { @@ -490,9 +490,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(90, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(90ull, game.getNumberOfTransitions()); + EXPECT_EQ(8ull, game.getNumberOfStates()); + EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { @@ -516,9 +516,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(276, game.getNumberOfTransitions()); - EXPECT_EQ(16, game.getNumberOfStates()); - EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(276ull, game.getNumberOfTransitions()); + EXPECT_EQ(16ull, game.getNumberOfStates()); + EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { @@ -542,9 +542,9 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(276, game.getNumberOfTransitions()); - EXPECT_EQ(16, game.getNumberOfStates()); - EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(276ull, game.getNumberOfTransitions()); + EXPECT_EQ(16ull, game.getNumberOfStates()); + EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { @@ -597,9 +597,9 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(436, game.getNumberOfTransitions()); - EXPECT_EQ(169, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(436ull, game.getNumberOfTransitions()); + EXPECT_EQ(169ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { @@ -652,9 +652,9 @@ TEST(PrismMenuGame, TwoDiceFullAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(436, game.getNumberOfTransitions()); - EXPECT_EQ(169, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(436ull, game.getNumberOfTransitions()); + EXPECT_EQ(169ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { @@ -677,9 +677,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(915, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(915ull, game.getNumberOfTransitions()); + EXPECT_EQ(8ull, game.getNumberOfStates()); + EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { @@ -702,9 +702,9 @@ TEST(PrismMenuGame, WlanAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(915, game.getNumberOfTransitions()); - EXPECT_EQ(8, game.getNumberOfStates()); - EXPECT_EQ(4, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(915ull, game.getNumberOfTransitions()); + EXPECT_EQ(8ull, game.getNumberOfStates()); + EXPECT_EQ(4ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { @@ -729,9 +729,9 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(1824, game.getNumberOfTransitions()); - EXPECT_EQ(16, game.getNumberOfStates()); - EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(1824ull, game.getNumberOfTransitions()); + EXPECT_EQ(16ull, game.getNumberOfStates()); + EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { @@ -756,9 +756,9 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(1824, game.getNumberOfTransitions()); - EXPECT_EQ(16, game.getNumberOfStates()); - EXPECT_EQ(8, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(1824ull, game.getNumberOfTransitions()); + EXPECT_EQ(16ull, game.getNumberOfStates()); + EXPECT_EQ(8ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { @@ -879,9 +879,9 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Cudd) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(9503, game.getNumberOfTransitions()); - EXPECT_EQ(5523, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(9503ull, game.getNumberOfTransitions()); + EXPECT_EQ(5523ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { @@ -1002,9 +1002,9 @@ TEST(PrismMenuGame, WlanFullAbstractionTest_Sylvan) { storm::abstraction::MenuGame game = abstractor.abstract(); - EXPECT_EQ(9503, game.getNumberOfTransitions()); - EXPECT_EQ(5523, game.getNumberOfStates()); - EXPECT_EQ(0, game.getBottomStates().getNonZeroCount()); + EXPECT_EQ(9503ull, game.getNumberOfTransitions()); + EXPECT_EQ(5523ull, game.getNumberOfStates()); + EXPECT_EQ(0ull, game.getBottomStates().getNonZeroCount()); } #endif diff --git a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 2d70b05d0..9f253ff2f 100644 --- a/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -200,14 +200,14 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { storm::generator::NextStateGeneratorOptions options; options.setBuildAllLabels(); std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, options).build(); - EXPECT_EQ(4ul, model->getNumberOfStates()); - EXPECT_EQ(11ul, model->getNumberOfTransitions()); + EXPECT_EQ(4ull, model->getNumberOfStates()); + EXPECT_EQ(11ull, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); - EXPECT_EQ(7ul, mdp->getNumberOfChoices()); + EXPECT_EQ(7ull, mdp->getNumberOfChoices()); auto solverFactory = std::make_unique>(); solverFactory->getSettings().setSolutionMethod(storm::solver::StandardMinMaxLinearEquationSolverSettings::SolutionMethod::PolicyIteration); @@ -223,10 +223,10 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const& scheduler = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(0, scheduler.getChoice(0)); - EXPECT_EQ(1, scheduler.getChoice(1)); - EXPECT_EQ(0, scheduler.getChoice(2)); - EXPECT_EQ(0, scheduler.getChoice(3)); + EXPECT_EQ(0ull, scheduler.getChoice(0)); + EXPECT_EQ(1ull, scheduler.getChoice(1)); + EXPECT_EQ(0ull, scheduler.getChoice(2)); + EXPECT_EQ(0ull, scheduler.getChoice(3)); formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"target\"]"); @@ -237,10 +237,10 @@ TEST(GmmxxMdpPrctlModelCheckerTest, SchedulerGeneration) { ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); ASSERT_TRUE(result->asExplicitQuantitativeCheckResult().hasScheduler()); storm::storage::Scheduler const& scheduler2 = result->asExplicitQuantitativeCheckResult().getScheduler(); - EXPECT_EQ(1, scheduler2.getChoice(0)); - EXPECT_EQ(2, scheduler2.getChoice(1)); - EXPECT_EQ(0, scheduler2.getChoice(2)); - EXPECT_EQ(0, scheduler2.getChoice(3)); + EXPECT_EQ(1ull, scheduler2.getChoice(0)); + EXPECT_EQ(2ull, scheduler2.getChoice(1)); + EXPECT_EQ(0ull, scheduler2.getChoice(2)); + EXPECT_EQ(0ull, scheduler2.getChoice(3)); } TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) { @@ -250,14 +250,14 @@ TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) { storm::parser::FormulaParser formulaParser; std::shared_ptr> model = storm::builder::ExplicitModelBuilder(program, storm::generator::NextStateGeneratorOptions(true, true)).build(); - EXPECT_EQ(3ul, model->getNumberOfStates()); - EXPECT_EQ(4ul, model->getNumberOfTransitions()); + EXPECT_EQ(3ull, model->getNumberOfStates()); + EXPECT_EQ(4ull, model->getNumberOfTransitions()); ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp); std::shared_ptr> mdp = model->as>(); - EXPECT_EQ(4ul, mdp->getNumberOfChoices()); + EXPECT_EQ(4ull, mdp->getNumberOfChoices()); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp, std::make_unique>()); @@ -268,8 +268,8 @@ TEST(GmmxxMdpPrctlModelCheckerTest, TinyRewards) { std::unique_ptr result = checker.check(checkTask); ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); - EXPECT_NEAR(1,result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(1,result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0,result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[0], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(1, result->asExplicitQuantitativeCheckResult().getValueVector()[1], storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0, result->asExplicitQuantitativeCheckResult().getValueVector()[2], storm::settings::getModule().getPrecision()); } diff --git a/src/test/parser/FormulaParserTest.cpp b/src/test/parser/FormulaParserTest.cpp index 69c07a220..15ffc4055 100644 --- a/src/test/parser/FormulaParserTest.cpp +++ b/src/test/parser/FormulaParserTest.cpp @@ -156,10 +156,10 @@ TEST(FormulaParserTest, MultiObjectiveFormulaTest) { std::string input = "multi(P<0.9 [ F \"a\" ], R<42 [ F \"b\" ], Pmin=? [ F\"c\" ])"; std::vector> formulas; ASSERT_NO_THROW(formulas = formulaParser.parseFromString(input)); - ASSERT_EQ(1, formulas.size()); + ASSERT_EQ(1ull, formulas.size()); ASSERT_TRUE(formulas[0]->isMultiObjectiveFormula()); storm::logic::MultiObjectiveFormula mof = formulas[0]->asMultiObjectiveFormula(); - ASSERT_EQ(3, mof.getNumberOfSubformulas()); + ASSERT_EQ(3ull, mof.getNumberOfSubformulas()); ASSERT_TRUE(mof.getSubformula(0).isProbabilityOperatorFormula()); ASSERT_TRUE(mof.getSubformula(0).asProbabilityOperatorFormula().getSubformula().isEventuallyFormula()); diff --git a/src/test/solver/MathsatSmtSolverTest.cpp b/src/test/solver/MathsatSmtSolverTest.cpp index 586ebb496..ae5c9a765 100644 --- a/src/test/solver/MathsatSmtSolverTest.cpp +++ b/src/test/solver/MathsatSmtSolverTest.cpp @@ -179,10 +179,10 @@ TEST(MathsatSmtSolver, AllSat) { std::vector valuations = s.allSat({x,y}); ASSERT_TRUE(valuations.size() == 3); - for (int i = 0; i < valuations.size(); ++i) { + for (uint64_t i = 0; i < valuations.size(); ++i) { ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y)); - for (int j = i+1; j < valuations.size(); ++j) { + for (uint64_t j = i+1; j < valuations.size(); ++j) { ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) || (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y))); } } @@ -206,7 +206,7 @@ TEST(MathsatSmtSolver, UnsatAssumptions) { result = s.checkWithAssumptions({ f2 }); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); std::vector unsatCore = s.getUnsatAssumptions(); - ASSERT_EQ(unsatCore.size(), 1); + ASSERT_EQ(1ull, unsatCore.size()); ASSERT_TRUE(unsatCore[0].isVariable()); ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); } diff --git a/src/test/solver/Z3SmtSolverTest.cpp b/src/test/solver/Z3SmtSolverTest.cpp index b75da18a0..507356bc0 100644 --- a/src/test/solver/Z3SmtSolverTest.cpp +++ b/src/test/solver/Z3SmtSolverTest.cpp @@ -179,10 +179,10 @@ TEST(Z3SmtSolver, AllSat) { std::vector valuations = s.allSat({x,y}); ASSERT_TRUE(valuations.size() == 3); - for (int i = 0; i < valuations.size(); ++i) { + for (uint64_t i = 0; i < valuations.size(); ++i) { ASSERT_FALSE(valuations[i].getBooleanValue(x) && valuations[i].getBooleanValue(y)); - for (int j = i+1; j < valuations.size(); ++j) { + for (uint64_t j = i+1; j < valuations.size(); ++j) { ASSERT_TRUE((valuations[i].getBooleanValue(x) != valuations[j].getBooleanValue(x)) || (valuations[i].getBooleanValue(y) != valuations[j].getBooleanValue(y))); } } @@ -206,7 +206,7 @@ TEST(Z3SmtSolver, UnsatAssumptions) { result = s.checkWithAssumptions({ f2 }); ASSERT_TRUE(result == storm::solver::SmtSolver::CheckResult::Unsat); std::vector unsatCore = s.getUnsatAssumptions(); - ASSERT_EQ(unsatCore.size(), 1); + ASSERT_EQ(1ull, unsatCore.size()); ASSERT_TRUE(unsatCore[0].isVariable()); ASSERT_STREQ("f2", unsatCore[0].getIdentifier().c_str()); } diff --git a/src/test/storage/JaniModelTest.cpp b/src/test/storage/JaniModelTest.cpp index 613e491de..764bfe5bc 100644 --- a/src/test/storage/JaniModelTest.cpp +++ b/src/test/storage/JaniModelTest.cpp @@ -15,8 +15,8 @@ TEST(JaniModelTest, FlattenModules) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(74, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { @@ -27,8 +27,8 @@ TEST(JaniModelTest, FlattenModules_Wlan_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(179, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { @@ -39,8 +39,8 @@ TEST(JaniModelTest, FlattenModules_Csma_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(70, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { @@ -51,8 +51,8 @@ TEST(JaniModelTest, FlattenModules_Firewire_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(5024, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { @@ -63,8 +63,8 @@ TEST(JaniModelTest, FlattenModules_Coin_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(13, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { @@ -75,8 +75,8 @@ TEST(JaniModelTest, FlattenModules_Dice_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(16, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges()); } #endif @@ -89,8 +89,8 @@ TEST(JaniModelTest, FlattenModules_Leader_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(74, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(74ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Wlan_Z3) { @@ -101,8 +101,8 @@ TEST(JaniModelTest, FlattenModules_Wlan_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(179, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(179ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Csma_Z3) { @@ -113,8 +113,8 @@ TEST(JaniModelTest, FlattenModules_Csma_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(70, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(70ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Firewire_Z3) { @@ -125,8 +125,8 @@ TEST(JaniModelTest, FlattenModules_Firewire_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(5024, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(5024ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Coin_Z3) { @@ -137,8 +137,8 @@ TEST(JaniModelTest, FlattenModules_Coin_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(13, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(13ull, janiModel.getAutomaton(0).getNumberOfEdges()); } TEST(JaniModelTest, FlattenModules_Dice_Z3) { @@ -149,7 +149,7 @@ TEST(JaniModelTest, FlattenModules_Dice_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(janiModel = janiModel.flattenComposition(smtSolverFactory)); - EXPECT_EQ(1, janiModel.getNumberOfAutomata()); - EXPECT_EQ(16, janiModel.getAutomaton(0).getNumberOfEdges()); + EXPECT_EQ(1ull, janiModel.getNumberOfAutomata()); + EXPECT_EQ(16ull, janiModel.getAutomaton(0).getNumberOfEdges()); } #endif diff --git a/src/test/storage/PrismProgramTest.cpp b/src/test/storage/PrismProgramTest.cpp index ba4beb5bf..8525f03e2 100644 --- a/src/test/storage/PrismProgramTest.cpp +++ b/src/test/storage/PrismProgramTest.cpp @@ -14,8 +14,8 @@ TEST(PrismProgramTest, FlattenModules) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Wlan_Mathsat) { @@ -25,8 +25,8 @@ TEST(PrismProgramTest, FlattenModules_Wlan_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(179, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Csma_Mathsat) { @@ -36,8 +36,8 @@ TEST(PrismProgramTest, FlattenModules_Csma_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(70, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Firewire_Mathsat) { @@ -47,8 +47,8 @@ TEST(PrismProgramTest, FlattenModules_Firewire_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(5024, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Coin_Mathsat) { @@ -58,8 +58,8 @@ TEST(PrismProgramTest, FlattenModules_Coin_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Dice_Mathsat) { @@ -69,8 +69,8 @@ TEST(PrismProgramTest, FlattenModules_Dice_Mathsat) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands()); } #endif @@ -82,8 +82,8 @@ TEST(PrismProgramTest, FlattenModules_Leader_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(74, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(74ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Wlan_Z3) { @@ -93,8 +93,8 @@ TEST(PrismProgramTest, FlattenModules_Wlan_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(179, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(179ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Csma_Z3) { @@ -104,8 +104,8 @@ TEST(PrismProgramTest, FlattenModules_Csma_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(70, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(70ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Firewire_Z3) { @@ -115,8 +115,8 @@ TEST(PrismProgramTest, FlattenModules_Firewire_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(5024, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(5024ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Coin_Z3) { @@ -126,8 +126,8 @@ TEST(PrismProgramTest, FlattenModules_Coin_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(13, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(13ull, program.getModule(0).getNumberOfCommands()); } TEST(PrismProgramTest, FlattenModules_Dice_Z3) { @@ -137,8 +137,8 @@ TEST(PrismProgramTest, FlattenModules_Dice_Z3) { std::shared_ptr smtSolverFactory = std::make_shared(); ASSERT_NO_THROW(program = program.flattenModules(smtSolverFactory)); - EXPECT_EQ(1, program.getNumberOfModules()); - EXPECT_EQ(16, program.getModule(0).getNumberOfCommands()); + EXPECT_EQ(1ull, program.getNumberOfModules()); + EXPECT_EQ(16ull, program.getModule(0).getNumberOfCommands()); } #endif diff --git a/src/test/utility/GraphTest.cpp b/src/test/utility/GraphTest.cpp index 1cac1d5cc..7e7e170c0 100644 --- a/src/test/utility/GraphTest.cpp +++ b/src/test/utility/GraphTest.cpp @@ -29,16 +29,16 @@ TEST(GraphTest, SymbolicProb01_Cudd) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observe0Greater1"))); - EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(4409ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(1316ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observeIGreater1"))); - EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(1091ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(4802ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender"))); - EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(5829ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(1032ull, statesWithProbability01.second.getNonZeroCount()); } } @@ -54,16 +54,16 @@ TEST(GraphTest, SymbolicProb01_Sylvan) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observe0Greater1"))); - EXPECT_EQ(4409ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(1316ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(4409ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(1316ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observeIGreater1"))); - EXPECT_EQ(1091ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(4802ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(1091ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(4802ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), model->getReachableStates(), model->getStates("observeOnlyTrueSender"))); - EXPECT_EQ(5829ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(1032ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(5829ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(1032ull, statesWithProbability01.second.getNonZeroCount()); } } @@ -79,12 +79,12 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount()); } modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); @@ -98,20 +98,20 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(77ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(149ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(74ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(198ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(94ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(33ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(83ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(35ull, statesWithProbability01.second.getNonZeroCount()); } modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); @@ -125,12 +125,12 @@ TEST(GraphTest, SymbolicProb01MinMax_Cudd) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount()); } } @@ -146,12 +146,12 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(0ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(364ull, statesWithProbability01.second.getNonZeroCount()); } modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); @@ -165,20 +165,20 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(77ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(149ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(77ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(149ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(74ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(198ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(74ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(198ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(94ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(33ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(94ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(33ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(83ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(35ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(83ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(35ull, statesWithProbability01.second.getNonZeroCount()); } modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); @@ -192,12 +192,12 @@ TEST(GraphTest, SymbolicProb01MinMax_Sylvan) { std::pair, storm::dd::Bdd> statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), model->getReachableStates(), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNonZeroCount()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNonZeroCount()); + EXPECT_EQ(993ull, statesWithProbability01.first.getNonZeroCount()); + EXPECT_EQ(16ull, statesWithProbability01.second.getNonZeroCount()); } } @@ -234,25 +234,25 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { EXPECT_TRUE(result.hasPlayer2Strategy()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(3, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(3ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(4, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(4ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(4, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(4ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); @@ -263,7 +263,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { targetStates = game.getStates(initialPredicates[0], true); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); ASSERT_TRUE(result.hasPlayer1Strategy()); ASSERT_TRUE(result.hasPlayer2Strategy()); @@ -273,32 +273,32 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // Proceed by checking whether they select exactly one action in each state. storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(0, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(0ull, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(0, stateDistributionCount.getMax()); + EXPECT_EQ(0.0, stateDistributionCount.getMax()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(5, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(5, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(5, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(0, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(0ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(5, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(5ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); @@ -308,11 +308,11 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) { // Proceed by checking whether they select exactly one action in each state. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(5, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(5ull, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1, stateDistributionCount.getMax()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); } TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { @@ -368,7 +368,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { storm::dd::Bdd targetStates = game.getStates(initialPredicates[7], false) && game.getStates(initialPredicates[22], false) && game.getStates(initialPredicates[9], false) && game.getStates(initialPredicates[24], false); storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); ASSERT_TRUE(result.hasPlayer1Strategy()); ASSERT_TRUE(result.hasPlayer2Strategy()); @@ -378,31 +378,31 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { // Proceed by checking whether they select exactly one exaction in each state. storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(153, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(153ull, stateDistributionsUnderStrategies.getNonZeroCount()); storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1, stateDistributionCount.getMax()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(153, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(153ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(1, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(1ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); @@ -412,11 +412,11 @@ TEST(GraphTest, SymbolicProb01StochasticGameTwoDice) { // Proceed by checking whether they select exactly one action in each state. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(1, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(1ull, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1, stateDistributionCount.getMax()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); } TEST(GraphTest, SymbolicProb01StochasticGameWlan) { @@ -540,7 +540,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { storm::dd::Bdd targetStates = game.getStates(initialPredicates[2], false); storm::utility::graph::GameProb01Result result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize, true, true); - EXPECT_EQ(2831, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); @@ -550,32 +550,32 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { // Proceed by checking whether they select exactly one action in each state. storm::dd::Add stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables());; - EXPECT_EQ(2831, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(2831ull, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob0 states). storm::dd::Add stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1, stateDistributionCount.getMax()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(2692, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(2831, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2831ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Minimize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(2692, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2692ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(2064, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Minimize); - EXPECT_EQ(2884, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb0(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize); - EXPECT_EQ(2064, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2064ull, result.getPlayer1States().getNonZeroCount()); result = storm::utility::graph::performProb1(game, game.getQualitativeTransitionMatrix(), game.getReachableStates(), targetStates, storm::OptimizationDirection::Maximize, storm::OptimizationDirection::Maximize, true, true); - EXPECT_EQ(2884, result.getPlayer1States().getNonZeroCount()); + EXPECT_EQ(2884ull, result.getPlayer1States().getNonZeroCount()); EXPECT_TRUE(result.hasPlayer1Strategy()); EXPECT_TRUE(result.hasPlayer2Strategy()); @@ -585,11 +585,11 @@ TEST(GraphTest, SymbolicProb01StochasticGameWlan) { // Proceed by checking whether they select exactly one action in each state. stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd() * result.player2Strategy.get().template toAdd()).sumAbstract(game.getColumnVariables()); - EXPECT_EQ(2884, stateDistributionsUnderStrategies.getNonZeroCount()); + EXPECT_EQ(2884ull, stateDistributionsUnderStrategies.getNonZeroCount()); // Check that the number of distributions per state is one (or zero in the case where there are no prob1 states). stateDistributionCount = stateDistributionsUnderStrategies.sumAbstract(game.getNondeterminismVariables()); - EXPECT_EQ(1, stateDistributionCount.getMax()); + EXPECT_EQ(1.0, stateDistributionCount.getMax()); } #endif @@ -604,16 +604,16 @@ TEST(GraphTest, ExplicitProb01) { std::pair statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observe0Greater1"))); - EXPECT_EQ(4409ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(1316ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(4409ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(1316ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeIGreater1"))); - EXPECT_EQ(1091ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(4802ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(1091ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(4802ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("observeOnlyTrueSender"))); - EXPECT_EQ(5829ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(1032ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(5829ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(1032ull, statesWithProbability01.second.getNumberOfSetBits()); } TEST(GraphTest, ExplicitProb01MinMax) { @@ -626,12 +626,12 @@ TEST(GraphTest, ExplicitProb01MinMax) { std::pair statesWithProbability01; ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(0ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(364ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("elected"))); - EXPECT_EQ(0ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(364ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(0ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(364ull, statesWithProbability01.second.getNumberOfSetBits()); modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/coin2-2.nm"); program = modelDescription.preprocess().asPrismProgram(); @@ -640,20 +640,20 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(77ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(149ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(77ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(149ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_0"))); - EXPECT_EQ(74ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(198ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(74ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(198ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(94ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(33ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(94ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(33ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("all_coins_equal_1"))); - EXPECT_EQ(83ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(35ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(83ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(35ull, statesWithProbability01.second.getNumberOfSetBits()); modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/csma2-2.nm"); program = modelDescription.preprocess().asPrismProgram(); @@ -662,10 +662,10 @@ TEST(GraphTest, ExplicitProb01MinMax) { ASSERT_TRUE(model->getType() == storm::models::ModelType::Mdp); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Min(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(993ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16ull, statesWithProbability01.second.getNumberOfSetBits()); ASSERT_NO_THROW(statesWithProbability01 = storm::utility::graph::performProb01Max(*model->as>(), storm::storage::BitVector(model->getNumberOfStates(), true), model->getStates("collision_max_backoff"))); - EXPECT_EQ(993ul, statesWithProbability01.first.getNumberOfSetBits()); - EXPECT_EQ(16ul, statesWithProbability01.second.getNumberOfSetBits()); + EXPECT_EQ(993ull, statesWithProbability01.first.getNumberOfSetBits()); + EXPECT_EQ(16ull, statesWithProbability01.second.getNumberOfSetBits()); }