diff --git a/CMakeLists.txt b/CMakeLists.txt index 3e17a4a08..7162aa250 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -23,7 +23,7 @@ include(imported) ############################################################# option(STORM_DEVELOPER "Sets whether the development mode is used." OFF) option(STORM_ALLWARNINGS "Compile with even more warnings" OFF) -option(STORM_PORTABLE_RELEASE "Sets whether a release build needs to be portable to another machine. This is only effective for release builds in non-development mode." OFF) +option(STORM_PORTABLE_RELEASE "Sets whether a release build needs to be portable to another machine." OFF) MARK_AS_ADVANCED(STORM_PORTABLE_RELEASE) option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON) MARK_AS_ADVANCED(STORM_USE_POPCNT) diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 29b3d7364..57b50fd5c 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -351,7 +351,7 @@ ExternalProject_Add( DOWNLOAD_COMMAND "" PREFIX "sylvan" SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan - CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -Dcarl_LIBRARIES=${carl_LIBRARIES} + CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DUSE_CARL=ON -Dcarl_INCLUDE_DIR=${carl_INCLUDE_DIR} -DSYLVAN_PORTABLE=${STORM_PORTABLE_RELEASE} -Dcarl_LIBRARIES=${carl_LIBRARIES} BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan BUILD_IN_SOURCE 0 INSTALL_COMMAND "" diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake index a23bb46f6..1c03de839 100644 --- a/resources/3rdparty/include_cudd.cmake +++ b/resources/3rdparty/include_cudd.cmake @@ -16,6 +16,11 @@ endif() set(CUDD_LIB_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib) +set(STORM_CUDD_FLAGS "CFLAGS=-O3 -w -DPIC -DHAVE_IEEE_754 -fno-common -ffast-math -fno-finite-math-only") +if (NOT STORM_PORTABLE_RELEASE) + set(STORM_CUDD_FLAGS "${STORM_CUDD_FLAGS} -march=native") +endif() + ExternalProject_Add( cudd3 DOWNLOAD_COMMAND "" @@ -23,7 +28,7 @@ ExternalProject_Add( PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 PATCH_COMMAND ${AUTORECONF} CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure --enable-shared --enable-obj --with-pic=yes --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${CUDD_LIB_DIR} CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} - BUILD_COMMAND make "CFLAGS=-O3 -w" + BUILD_COMMAND make ${STORM_CUDD_FLAGS} INSTALL_COMMAND make install BUILD_IN_SOURCE 0 LOG_CONFIGURE ON diff --git a/resources/3rdparty/sylvan/CMakeLists.txt b/resources/3rdparty/sylvan/CMakeLists.txt index 3cbc9f098..8de1feb14 100644 --- a/resources/3rdparty/sylvan/CMakeLists.txt +++ b/resources/3rdparty/sylvan/CMakeLists.txt @@ -2,9 +2,16 @@ cmake_minimum_required(VERSION 2.6) project(sylvan C CXX) enable_testing() +option(SYLVAN_PORTABLE "If set, the created library will be portable." OFF) + set(CMAKE_C_FLAGS "-O3 -Wextra -Wall -fno-strict-aliasing -std=gnu11 -fPIC") set(CMAKE_CXX_FLAGS "-O3 -Wextra -Wall -fno-strict-aliasing -Wno-deprecated-register -std=gnu++11 -fPIC") +if (NOT SYLVAN_PORTABLE) + set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -march=native") + set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -march=native") +endif() + option(USE_CARL "Sets whether carl should be included." ON) option(WITH_COVERAGE "Add generation of test coverage" OFF) if(WITH_COVERAGE) diff --git a/src/storm/builder/DdPrismModelBuilder.cpp b/src/storm/builder/DdPrismModelBuilder.cpp index 3a5b6e23e..e2afeeae6 100644 --- a/src/storm/builder/DdPrismModelBuilder.cpp +++ b/src/storm/builder/DdPrismModelBuilder.cpp @@ -618,14 +618,14 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) { STORM_LOG_TRACE("Translating guard " << command.getGuardExpression()); - storm::dd::Add guard = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()) * generationInfo.moduleToRangeMap[module.getName()]; + storm::dd::Bdd guard = generationInfo.rowExpressionAdapter->translateBooleanExpression(command.getGuardExpression()) && generationInfo.moduleToRangeMap[module.getName()].notZero(); STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); if (!guard.isZero()) { // Create the DDs representing the individual updates. std::vector updateResults; for (storm::prism::Update const& update : command.getUpdates()) { - updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guard, update)); + updateResults.push_back(createUpdateDecisionDiagram(generationInfo, module, guard.template toAdd(), update)); STORM_LOG_WARN_COND(!updateResults.back().updateDd.isZero(), "Update '" << update << "' does not have any effect."); } @@ -661,7 +661,7 @@ namespace storm { commandDd += updateResultsIt->updateDd * probabilityDd; } - return ActionDecisionDiagram(guard, guard * commandDd, globalVariablesInSomeUpdate); + return ActionDecisionDiagram(guard, guard.template toAdd() * commandDd, globalVariablesInSomeUpdate); } else { return ActionDecisionDiagram(*generationInfo.manager); } @@ -749,9 +749,9 @@ namespace storm { template typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMarkovChain(GenerationInformation& generationInfo, std::vector& commandDds) { - storm::dd::Add allGuards = generationInfo.manager->template getAddZero(); + storm::dd::Bdd allGuards = generationInfo.manager->getBddZero(); storm::dd::Add allCommands = generationInfo.manager->template getAddZero(); - storm::dd::Add temporary; + storm::dd::Bdd temporary; // Make all command DDs assign to the same global variables. std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, commandDds); @@ -759,12 +759,12 @@ namespace storm { // Then combine the commands to the full action DD and multiply missing identities along the way. for (auto& commandDd : commandDds) { // Check for overlapping guards. - temporary = commandDd.guardDd * allGuards; + temporary = commandDd.guardDd && allGuards; // Issue a warning if there are overlapping guards in a non-CTMC model. STORM_LOG_WARN_COND(temporary.isZero() || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC, "Guard of a command overlaps with previous guards."); - allGuards += commandDd.guardDd; + allGuards |= commandDd.guardDd; allCommands += commandDd.transitionsDd; } @@ -801,8 +801,8 @@ namespace storm { // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. storm::dd::Add sumOfGuards = generationInfo.manager->template getAddZero(); for (auto const& commandDd : commandDds) { - sumOfGuards += commandDd.guardDd; - allGuards |= commandDd.guardDd.toBdd(); + sumOfGuards += commandDd.guardDd.template toAdd(); + allGuards |= commandDd.guardDd; } uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); @@ -816,7 +816,7 @@ namespace storm { for (auto const& commandDd : commandDds) { allCommands += commandDd.transitionsDd; } - return ActionDecisionDiagram(sumOfGuards, allCommands, assignedGlobalVariables); + return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables); } else { // Calculate number of required variables to encode the nondeterminism. uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); @@ -843,7 +843,7 @@ namespace storm { for (std::size_t j = 0; j < commandDds.size(); ++j) { // Check if command guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices // choices such that one outgoing choice is given by the j-th command. - storm::dd::Bdd guardChoicesIntersection = commandDds[j].guardDd.toBdd() && equalsNumberOfChoicesDd; + storm::dd::Bdd guardChoicesIntersection = commandDds[j].guardDd && equalsNumberOfChoicesDd; // If there is no such state, continue with the next command. if (guardChoicesIntersection.isZero()) { @@ -883,7 +883,7 @@ namespace storm { sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd(); } - return ActionDecisionDiagram(allGuards.template toAdd(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); + return ActionDecisionDiagram(allGuards, allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables); } } @@ -891,7 +891,7 @@ namespace storm { typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { std::set assignedGlobalVariables; std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(assignedGlobalVariables, assignedGlobalVariables.begin())); - return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, assignedGlobalVariables, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); + return ActionDecisionDiagram(action1.guardDd && action2.guardDd, action1.transitionsDd * action2.transitionsDd, assignedGlobalVariables, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); } template @@ -914,7 +914,7 @@ namespace storm { std::set assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, action1, action2); if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) { - return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1.transitionsDd + action2.transitionsDd, assignedGlobalVariables, 0); + return ActionDecisionDiagram(action1.guardDd || action2.guardDd, action1.transitionsDd + action2.transitionsDd, assignedGlobalVariables, 0); } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { if (action1.transitionsDd.isZero()) { return ActionDecisionDiagram(action2.guardDd, action2.transitionsDd, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables); @@ -943,7 +943,7 @@ namespace storm { // Add a new variable that resolves the nondeterminism between the two choices. storm::dd::Add combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2.transitionsDd, action1.transitionsDd); - return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1); + return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); } @@ -1149,12 +1149,11 @@ namespace storm { synchronization = getSynchronizationDecisionDiagram(generationInfo, stateActionReward.getActionIndex()); } ActionDecisionDiagram const& actionDd = stateActionReward.isLabeled() ? globalModule.synchronizingActionToDecisionDiagramMap.at(stateActionReward.getActionIndex()) : globalModule.independentAction; - states *= actionDd.guardDd * reachableStatesAdd; + states *= actionDd.guardDd.template toAdd() * reachableStatesAdd; storm::dd::Add stateActionRewardDd = synchronization * states * rewards; - // If we are building the state-action rewards for an MDP, we need to make sure that the encoding - // of the nondeterminism is present in the reward vector, so we ne need to multiply it with the - // legal state-actions. + // If we are building the state-action rewards for an MDP, we need to make sure that the reward is + // only given on legal nondeterminism encodings, which is why we multiply with the state-action DD. if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { if (!stateActionDd) { stateActionDd = transitionMatrix.notZero().existsAbstract(generationInfo.columnMetaVariables).template toAdd(); @@ -1178,6 +1177,7 @@ namespace storm { if (!stateActionDd) { stateActionDd = transitionMatrix.sumAbstract(generationInfo.columnMetaVariables); } + stateActionRewards.get() /= stateActionDd.get(); } } diff --git a/src/storm/builder/DdPrismModelBuilder.h b/src/storm/builder/DdPrismModelBuilder.h index 7abbe08b0..f3b7adc31 100644 --- a/src/storm/builder/DdPrismModelBuilder.h +++ b/src/storm/builder/DdPrismModelBuilder.h @@ -122,11 +122,11 @@ namespace storm { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::DdManager const& manager, std::set const& assignedGlobalVariables = std::set(), uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.template getAddZero()), transitionsDd(manager.template getAddZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables), assignedGlobalVariables(assignedGlobalVariables) { + ActionDecisionDiagram(storm::dd::DdManager const& manager, std::set const& assignedGlobalVariables = std::set(), uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getBddZero()), transitionsDd(manager.template getAddZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables), assignedGlobalVariables(assignedGlobalVariables) { // Intentionally left empty. } - ActionDecisionDiagram(storm::dd::Add guardDd, storm::dd::Add transitionsDd, std::set const& assignedGlobalVariables = std::set(), uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables), assignedGlobalVariables(assignedGlobalVariables) { + ActionDecisionDiagram(storm::dd::Bdd guardDd, storm::dd::Add transitionsDd, std::set const& assignedGlobalVariables = std::set(), uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables), assignedGlobalVariables(assignedGlobalVariables) { // Intentionally left empty. } @@ -134,7 +134,7 @@ namespace storm { ActionDecisionDiagram& operator=(ActionDecisionDiagram const& other) = default; // The guard of the action. - storm::dd::Add guardDd; + storm::dd::Bdd guardDd; // The actual transitions (source and target states). storm::dd::Add transitionsDd; diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index 6b4c4c7d4..b3061db61 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/src/storm/generator/PrismNextStateGenerator.cpp @@ -256,13 +256,13 @@ namespace storm { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { for (auto const& choice : allChoices) { if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) { - stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate; + stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass(); } } } } - globalChoice.addReward(stateActionRewardValue); + globalChoice.addReward(stateActionRewardValue / totalExitRate); } // Move the newly fused choice in place. diff --git a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index 0f6fb9a4b..592ecc460 100644 --- a/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -269,7 +269,7 @@ namespace storm { // Then compute the state reward vector to use in the computation. storm::dd::Add totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, model.getColumnVariables(), exitRateVector, false); std::vector explicitTotalRewardVector = totalRewardVector.toVector(odd); - + // Finally, compute the transient probabilities. std::vector result = storm::modelchecker::helper::SparseCtmcCslHelper::computeTransientProbabilities(explicitUniformizedMatrix, nullptr, timeBound, uniformizationRate, explicitTotalRewardVector, linearEquationSolverFactory); return std::unique_ptr(new HybridQuantitativeCheckResult(model.getReachableStates(), model.getManager().getBddZero(), model.getManager().template getAddZero(), model.getReachableStates(), std::move(odd), std::move(result))); diff --git a/src/storm/parser/FormulaParser.cpp b/src/storm/parser/FormulaParser.cpp index 43bbb670b..6bb1687dc 100644 --- a/src/storm/parser/FormulaParser.cpp +++ b/src/storm/parser/FormulaParser.cpp @@ -31,11 +31,11 @@ namespace storm { // Intentionally left empty. } - FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { + FormulaParser::FormulaParser(storm::prism::Program const& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(program.getManager().getSharedPointer())) { this->addFormulasAsIdentifiers(program); } - FormulaParser::FormulaParser(storm::prism::Program& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { + FormulaParser::FormulaParser(storm::prism::Program& program) : manager(program.getManager().getSharedPointer()), grammar(new FormulaParserGrammar(program.getManager().getSharedPointer())) { this->addFormulasAsIdentifiers(program); } diff --git a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 451d2ad49..e9819a2c7 100644 --- a/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -166,8 +166,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.3328777473921436, quantitativeResult1.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.3328777473921436, quantitativeResult1.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]"); @@ -175,8 +175,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.15221847380560186, quantitativeResult2.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.15221847380560186, quantitativeResult2.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]"); @@ -184,8 +184,8 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(0.3215392962289586, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.32153516079959443, quantitativeResult3.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(0.32153516079959443, quantitativeResult3.getMax(), storm::settings::getModule().getPrecision()); } TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds_Sylvan) { diff --git a/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index 34fc37c2d..872a8dbdf 100644 --- a/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/src/test/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -103,8 +103,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -112,8 +112,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); } TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { @@ -201,8 +201,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule().getPrecision()); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); @@ -210,8 +210,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(7.3333294987678528, quantitativeResult8.getMax(), storm::settings::getModule().getPrecision()); } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { @@ -290,8 +290,8 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) { result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult(); - EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); - EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMin(), storm::settings::getModule().getPrecision()); + EXPECT_NEAR(4.2856904354441401, quantitativeResult6.getMax(), storm::settings::getModule().getPrecision()); } TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {