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

made symbolic MDP model checker tests work 

Former-commit-id: e2e0d07a55
main
dehnert 10 years ago
parent
7f75db2790
commit
7376eaf866
5 changed files with 185 additions and 3 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 1
      src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
  2. 1
      src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
  3. 3
      src/solver/SymbolicMinMaxLinearEquationSolver.cpp
  4. 1
      src/utility/solver.cpp
  5. 182
      test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp

1
src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.cpp
View File

@ -91,5 +91,6 @@ namespace storm {
}
template class SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double>;
template class SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double>;
}
}

1
src/modelchecker/prctl/helper/SymbolicMdpPrctlHelper.cpp
View File

@ -200,6 +200,7 @@ namespace storm {
}
template class SymbolicMdpPrctlHelper<storm::dd::DdType::CUDD, double>;
template class SymbolicMdpPrctlHelper<storm::dd::DdType::Sylvan, double>;
}
}
}

3
src/solver/SymbolicMinMaxLinearEquationSolver.cpp
View File

@ -61,7 +61,7 @@ namespace storm {
++iterations;
}
return xCopy;
}
@ -91,6 +91,7 @@ namespace storm {
}
template class SymbolicMinMaxLinearEquationSolver<storm::dd::DdType::CUDD, double>;
template class SymbolicMinMaxLinearEquationSolver<storm::dd::DdType::Sylvan, double>;
}
}

1
src/utility/solver.cpp
View File

@ -191,6 +191,7 @@ namespace storm {
template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
template class SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>;
template class SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>;
template class SymbolicGameSolverFactory<storm::dd::DdType::CUDD, double>;
template class SymbolicGameSolverFactory<storm::dd::DdType::Sylvan, double>;
template class LinearEquationSolverFactory<double>;

182
test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
View File

@ -17,7 +17,7 @@
#include "src/settings/modules/GeneralSettings.h"
TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
@ -114,7 +114,104 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
TEST(SymbolicMdpPrctlModelCheckerTest, Dice_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coinflips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
EXPECT_EQ(169ul, model->getNumberOfStates());
EXPECT_EQ(436ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult7 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult8 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.3333272933959961, quantitativeResult8.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Cudd) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
@ -192,3 +289,84 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2856890848060498, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
}
TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader_Sylvan) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#else
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::Options options;
#endif
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("rounds");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan>::translateProgram(program, options);
EXPECT_EQ(3172ul, model->getNumberOfStates());
EXPECT_EQ(7144ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Mdp);
std::shared_ptr<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>> mdp = model->as<storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan>>();
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::Sylvan, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::Sylvan, double>()));
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult5 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
// FIXME: this precision bound is not really good.
EXPECT_NEAR(4.2857, quantitativeResult5.getMin(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2857, quantitativeResult5.getMax(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision());
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>(model->getReachableStates(), model->getInitialStates()));
storm::modelchecker::SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>& quantitativeResult6 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>();
// FIXME: this precision bound is not really good.
EXPECT_NEAR(4.2857, quantitativeResult6.getMin(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2857, quantitativeResult6.getMax(), 100 * storm::settings::nativeEquationSolverSettings().getPrecision());
}
Write Preview
Loading…
Cancel
Save