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

renamed storm::Variable to storm::RationalFunctionVariable to avoid confusion with storm::expressions::Variable. fixed some Eigen tests 

Former-commit-id: 62c70330c2
main
dehnert 9 years ago
parent
f3fa90cc37
commit
a699272dc6
13 changed files with 83 additions and 72 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. 2
      src/adapters/CarlAdapter.h
  2. 2
      src/generator/PrismNextStateGenerator.cpp
  3. 5
      src/modelchecker/results/CheckResult.cpp
  4. 4
      src/models/sparse/Model.cpp
  5. 2
      src/models/sparse/Model.h
  6. 4
      src/storage/SparseMatrix.cpp
  7. 2
      src/storage/SparseMatrix.h
  8. 4
      src/utility/export.h
  9. 2
      src/utility/parametric.h
  10. 3
      src/utility/solver.cpp
  11. 4
      src/utility/storm.h
  12. 85
      test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
  13. 34
      test/functional/utility/ModelInstantiatorTest.cpp

2
src/adapters/CarlAdapter.h
View File

@ -57,7 +57,7 @@ namespace storm {
#else #else
typedef mpq_class RationalNumber; typedef mpq_class RationalNumber;
#endif #endif
typedef carl::Variable Variable;
typedef carl::Variable RationalFunctionVariable;
typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial; typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial;
typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial; typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
typedef carl::Relation CompareRelation; typedef carl::Relation CompareRelation;

2
src/generator/PrismNextStateGenerator.cpp
View File

@ -395,7 +395,7 @@ namespace storm {
if (rewardModel.get().hasStateActionRewards()) { if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) { for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) { if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
} }
} }
} }

5
src/modelchecker/results/CheckResult.cpp
View File

@ -145,9 +145,10 @@ namespace storm {
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult(); template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const; template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
#ifdef STORM_HAVE_CARL
template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asExplicitQuantitativeCheckResult() const;
template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult(); template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const; template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
#endif
} }
} }

4
src/models/sparse/Model.cpp
View File

@ -346,9 +346,7 @@ namespace storm {
return this->rewardModels; return this->rewardModels;
} }
std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
return storm::storage::getVariables(model.getTransitionMatrix()); return storm::storage::getVariables(model.getTransitionMatrix());
} }

2
src/models/sparse/Model.h
View File

@ -357,7 +357,7 @@ namespace storm {
boost::optional<std::vector<LabelSet>> choiceLabeling; boost::optional<std::vector<LabelSet>> choiceLabeling;
}; };
std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
} // namespace sparse } // namespace sparse
} // namespace models } // namespace models
} // namespace storm } // namespace storm

4
src/storage/SparseMatrix.cpp
View File

@ -1417,9 +1417,9 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
std::set<storm::RationalFunctionVariable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
{ {
std::set<storm::Variable> result;
std::set<storm::RationalFunctionVariable> result;
for(auto const& entry : matrix) { for(auto const& entry : matrix) {
entry.getValue().gatherVariables(result); entry.getValue().gatherVariables(result);
} }

2
src/storage/SparseMatrix.h
View File

@ -1004,7 +1004,7 @@ namespace storm {
}; };
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
std::set<storm::RationalFunctionVariable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
#endif #endif
} // namespace storage } // namespace storage

4
src/utility/export.h
View File

@ -24,8 +24,8 @@ void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::re
filestream.open(path); filestream.open(path);
// todo add checks. // todo add checks.
filestream << "!Parameters: "; filestream << "!Parameters: ";
std::set<storm::Variable> vars = mcresult.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
std::set<storm::RationalFunctionVariable> vars = mcresult.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, ", "));
filestream << std::endl; filestream << std::endl;
filestream << "!Result: " << mcresult << std::endl; filestream << "!Result: " << mcresult << std::endl;
filestream << "!Well-formed Constraints: " << std::endl; filestream << "!Well-formed Constraints: " << std::endl;

2
src/utility/parametric.h
View File

@ -28,7 +28,7 @@ namespace storm {
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
template<> template<>
struct VariableType<storm::RationalFunction> { typedef storm::Variable type; };
struct VariableType<storm::RationalFunction> { typedef storm::RationalFunctionVariable type; };
template<> template<>
struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; }; struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
#endif #endif

3
src/utility/solver.cpp
View File

@ -229,6 +229,9 @@ namespace storm {
template class GameSolverFactory<double>; template class GameSolverFactory<double>;
template class LinearEquationSolverFactory<storm::RationalNumber>; template class LinearEquationSolverFactory<storm::RationalNumber>;
template class EigenLinearEquationSolverFactory<storm::RationalNumber>;
template class LinearEquationSolverFactory<storm::RationalFunction>;
template class EigenLinearEquationSolverFactory<storm::RationalFunction>; template class EigenLinearEquationSolverFactory<storm::RationalFunction>;
} }
} }

4
src/utility/storm.h
View File

@ -344,8 +344,8 @@ namespace storm {
filestream.open(path); filestream.open(path);
// TODO: add checks. // TODO: add checks.
filestream << "!Parameters: "; filestream << "!Parameters: ";
std::set<storm::Variable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, "; "));
std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
filestream << std::endl; filestream << std::endl;
filestream << "!Result: " << result << std::endl; filestream << "!Result: " << result << std::endl;
filestream << "!Well-formed Constraints: " << std::endl; filestream << "!Well-formed Constraints: " << std::endl;

85
test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
View File

@ -61,55 +61,58 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) {
} }
TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) { TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
// FIXME: this should use rational numbers not functions.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program).build();
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build();
// A parser that we use for conveniently constructing the formulas. // A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser; storm::parser::FormulaParser formulaParser;
ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); 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>>();
std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalNumber>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]);
EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0]);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]"); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]);
EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0]);
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]"); formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]);
EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0]);
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]"); formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula); result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]);
EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0]);
} }
TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) { TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
// FIXME: this should use rational numbers not functions.
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm");
std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program).build();
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. // A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser formulaParser; storm::parser::FormulaParser formulaParser;
@ -121,6 +124,11 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
ASSERT_EQ(dtmc->getNumberOfStates(), 13ull); ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull); ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
std::map<storm::RationalFunctionVariable, storm::RationalNumber> instantiation;
std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*dtmc);
ASSERT_EQ(variables.size(), 1ull);
instantiation.emplace(*variables.begin(), storm::RationalNumber(1) / storm::RationalNumber(2));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>()); storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
@ -128,29 +136,28 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula); std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>(); storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
std::cout << quantitativeResult1 << std::endl;
// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]);
//
// formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
//
// result = checker.check(*formula);
// storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
//
// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]);
//
// formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
//
// result = checker.check(*formula);
// storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
//
// EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]);
//
// formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
//
// result = checker.check(*formula);
// storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
//
// EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]);
EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0].evaluate(instantiation));
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation));
} }
@ -378,7 +385,9 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) {
TEST(EigenDtmcPrctlModelCheckerTest, Conditional) { TEST(EigenDtmcPrctlModelCheckerTest, Conditional) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm"); storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
storm::generator::NextStateGeneratorOptions options;
options.setBuildAllLabels().setBuildAllRewardModels();
std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc); ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
ASSERT_EQ(4ul, model->getNumberOfStates()); ASSERT_EQ(4ul, model->getNumberOfStates());
ASSERT_EQ(5ul, model->getNumberOfTransitions()); ASSERT_EQ(5ul, model->getNumberOfTransitions());

34
test/functional/utility/ModelInstantiatorTest.cpp
View File

@ -36,10 +36,10 @@ TEST(ModelInstantiatorTest, BrpProb) {
EXPECT_FALSE(dtmc->hasRewardModel()); EXPECT_FALSE(dtmc->hasRewardModel());
{ {
std::map<storm::Variable, storm::RationalNumber> valuation;
storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE); ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE); ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.8))); valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.8)));
valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9))); valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
@ -69,10 +69,10 @@ TEST(ModelInstantiatorTest, BrpProb) {
} }
{ {
std::map<storm::Variable, storm::RationalNumber> valuation;
storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE); ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE); ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0))); valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0))); valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0)));
@ -102,10 +102,10 @@ TEST(ModelInstantiatorTest, BrpProb) {
} }
{ {
std::map<storm::Variable, storm::RationalNumber> valuation;
storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE); ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE); ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0))); valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9))); valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
@ -153,14 +153,14 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc); storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
{ {
std::map<storm::Variable, storm::RationalNumber> valuation;
storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
ASSERT_NE(pL, carl::Variable::NO_VARIABLE); ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE); ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
storm::Variable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg");
storm::RationalFunctionVariable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE); ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
storm::Variable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
storm::RationalFunctionVariable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
ASSERT_NE(pK, carl::Variable::NO_VARIABLE); ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.9))); valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.9)));
valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3))); valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3)));
@ -222,10 +222,10 @@ TEST(ModelInstantiatorTest, Consensus) {
storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp); storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
std::map<storm::Variable, storm::RationalNumber> valuation;
storm::Variable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
storm::RationalFunctionVariable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
ASSERT_NE(p1, carl::Variable::NO_VARIABLE); ASSERT_NE(p1, carl::Variable::NO_VARIABLE);
storm::Variable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
storm::RationalFunctionVariable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
ASSERT_NE(p2, carl::Variable::NO_VARIABLE); ASSERT_NE(p2, carl::Variable::NO_VARIABLE);
valuation.insert(std::make_pair(p1,carl::rationalize<storm::RationalNumber>(0.51))); valuation.insert(std::make_pair(p1,carl::rationalize<storm::RationalNumber>(0.51)));
valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49))); valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49)));

Write Preview
Loading…
Cancel
Save