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

added parametric model checking tests

main
TimQu 8 years ago
parent
c1b14fc250
commit
66d1c828c6
2 changed files with 182 additions and 0 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. 106
      src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp
  2. 76
      src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp

106
src/test/storm-pars/modelchecker/ParametricDtmcPrctlModelCheckerTest.cpp
View File

@ -0,0 +1,106 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "test/storm_gtest.h"
#include "storm/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
#include "storm/parser/AutoParser.h"
#include "storm/parser/PrismParser.h"
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm/api/builder.h"
#include "storm/environment/solver/SolverEnvironment.h"
namespace {
class EigenEnvironment {
public:
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen);
return env;
}
};
class EliminationEnvironment {
public:
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Elimination);
return env;
}
};
template<typename TestType>
class ParametricDtmcPrctlModelCheckerTest : public ::testing::Test {
public:
ParametricDtmcPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
storm::RationalFunctionCoefficient parseNumber(std::string const& input) const { return storm::utility::convertNumber<storm::RationalFunctionCoefficient>(input);}
private:
storm::Environment _environment;
};
typedef ::testing::Types<
EigenEnvironment,
EliminationEnvironment
> TestingTypes;
TYPED_TEST_CASE(ParametricDtmcPrctlModelCheckerTest, TestingTypes);
TYPED_TEST(ParametricDtmcPrctlModelCheckerTest, Die) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build();
// A parser that we use for conveniently constructing the formulas.
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::parser::FormulaParser formulaParser(expManager);
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*dtmc);
ASSERT_EQ(variables.size(), 1ull);
instantiation.emplace(*variables.begin(), this->parseNumber("1/2"));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult1[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult2[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(this->parseNumber("1/6"), quantitativeResult3[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(this->env(), *formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(this->parseNumber("11/3"), quantitativeResult4[0].evaluate(instantiation));
}
}

76
src/test/storm-pars/modelchecker/SymbolicParametricDtmcPrctlModelCheckerTest.cpp
View File

@ -0,0 +1,76 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "storm/parser/FormulaParser.h"
#include "storm/logic/Formulas.h"
#include "storm/utility/solver.h"
#include "storm/storage/SymbolicModelDescription.h"
#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
#include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
#include "storm/solver/SymbolicEliminationLinearEquationSolver.h"
#include "storm/parser/PrismParser.h"
#include "storm/builder/DdPrismModelBuilder.h"
#include "storm/models/symbolic/StandardRewardModel.h"
#include "storm/models/symbolic/Dtmc.h"
#include "storm/settings/SettingsManager.h"
#include "storm/environment/solver/SolverEnvironment.h"
TEST(SymbolicDtmcPrctlModelCheckerTest, Die_RationalFunction_Sylvan) {
storm::storage::SymbolicModelDescription modelDescription = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/pdtmc/parametric_die.pm");
storm::prism::Program program = modelDescription.preprocess().asPrismProgram();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
typename storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>::Options options;
options.buildAllRewardModels = false;
options.rewardModelsToBuild.insert("coin_flips");
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::Sylvan, storm::RationalFunction>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::Sylvan, storm::RationalFunction>().build(program, options);
EXPECT_EQ(13ul, model->getNumberOfStates());
EXPECT_EQ(20ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
std::map<storm::RationalFunctionVariable, storm::RationalFunctionCoefficient> instantiation;
std::set<storm::RationalFunctionVariable> variables = model->getParameters();
ASSERT_EQ(1ull, variables.size());
instantiation.emplace(*variables.begin(), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/2")));
std::shared_ptr<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> dtmc = model->as<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>>();
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, storm::RationalFunction>> checker(*dtmc, std::unique_ptr<storm::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>>(new storm::solver::SymbolicEliminationLinearEquationSolverFactory<storm::dd::DdType::Sylvan, storm::RationalFunction>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
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, storm::RationalFunction>& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult1.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
formula = formulaParser.parseSingleFormulaFromString("P=? [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, storm::RationalFunction>& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult2.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
formula = formulaParser.parseSingleFormulaFromString("P=? [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, storm::RationalFunction>& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult3.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("1/6")));
formula = formulaParser.parseSingleFormulaFromString("R=? [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, storm::RationalFunction>& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, storm::RationalFunction>();
EXPECT_EQ(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(quantitativeResult4.sum().evaluate(instantiation)), storm::utility::convertNumber<storm::RationalFunctionCoefficient>(std::string("11/3")));
}
Write Preview
Loading…
Cancel
Save