sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

"fixed" the tests that failed because of unsound value iteration

tempestpy_adaptions
TimQu 7 years ago
parent
3571f0ddca
commit
f44ce8801c
4 changed files with 18 additions and 18 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 8
      src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  2. 4
      src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  3. 16
      src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  4. 8
      src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp

8
src/test/storm/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -285,8 +285,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
@ -365,8 +365,8 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.2857145335329694, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");

4
src/test/storm/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -123,7 +123,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.check(*formula); result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666666666666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -181,7 +181,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.2857129064503061, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");

16
src/test/storm/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
View File

@ -103,8 +103,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -200,8 +200,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice_Sylvan) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult7.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult7.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -280,8 +280,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>();
EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
@ -360,8 +360,8 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates())); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>(); storm::modelchecker::HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asHybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.2857085969694237, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMin(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5.getMax(), storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");

8
src/test/storm/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -76,7 +76,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333294987678528, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult7[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -98,7 +98,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
result = stateRewardModelChecker.check(*formula); result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.3333294987678528, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(7.333333333, quantitativeResult9[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -120,7 +120,7 @@ TEST(NativeMdpPrctlModelCheckerTest, Dice) {
result = stateAndTransitionRewardModelChecker.check(*formula); result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658997535706, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(14.6666675, quantitativeResult11[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
@ -178,7 +178,7 @@ TEST(NativeMdpPrctlModelCheckerTest, AsynchronousLeader) {
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>(); storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.2857092687973175, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
EXPECT_NEAR(4.285716, quantitativeResult5[0], storm::settings::getModule<storm::settings::modules::NativeEquationSolverSettings>().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]"); formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");

Write Preview
Loading…
Cancel
Save