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

Fixes and test refactoring for TopologicalValueIterationMdpPrctlModelChecker 

- Explicit instantiation of matrix and scc decomposition for float
- Started to adapt TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to new formulas


Former-commit-id: 4685ae4939
main
David_Korzeniewski 11 years ago
parent
ee4c961cc9
commit
3748905bcf
3 changed files with 188 additions and 171 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. 21
      src/storage/SparseMatrix.cpp
  2. 3
      src/storage/StronglyConnectedComponentDecomposition.cpp
  3. 335
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

21
src/storage/SparseMatrix.cpp
View File

@ -958,12 +958,21 @@ namespace storm {
} }
// Explicitly instantiate the entry, builder and the matrix. // Explicitly instantiate the entry, builder and the matrix.
template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, double> const& entry);
template class SparseMatrixBuilder<double>;
template class SparseMatrix<double>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
//double
template class MatrixEntry<typename SparseMatrix<double>::index_type, double>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, double> const& entry);
template class SparseMatrixBuilder<double>;
template class SparseMatrix<double>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
//float
template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, float> const& entry);
template class SparseMatrixBuilder<float>;
template class SparseMatrix<float>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<float> const& matrix);
//int
template class MatrixEntry<typename SparseMatrix<int>::index_type, int>;
template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint_fast64_t, int> const& entry);
template class SparseMatrixBuilder<int>; template class SparseMatrixBuilder<int>;
template class SparseMatrix<int>; template class SparseMatrix<int>;
template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix); template std::ostream& operator<<(std::ostream& out, SparseMatrix<int> const& matrix);

3
src/storage/StronglyConnectedComponentDecomposition.cpp
View File

@ -209,6 +209,7 @@ namespace storm {
} }
// Explicitly instantiate the SCC decomposition. // Explicitly instantiate the SCC decomposition.
template class StronglyConnectedComponentDecomposition<double>;
template class StronglyConnectedComponentDecomposition<double>;
template class StronglyConnectedComponentDecomposition<float>;
} // namespace storage } // namespace storage
} // namespace storm } // namespace storm

335
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -1,16 +1,20 @@
#include "gtest/gtest.h" #include "gtest/gtest.h"
#include "storm-config.h" #include "storm-config.h"
#include "src/logic/Formulas.h"
#include "src/solver/NativeNondeterministicLinearEquationSolver.h" #include "src/solver/NativeNondeterministicLinearEquationSolver.h"
#include "src/settings/Settings.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h" #include "src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h"
#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
#include "src/settings/SettingsManager.h"
#include "src/settings/SettingMemento.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "storm-config.h" #include "storm-config.h"
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) { TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
//storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 169ull); ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
@ -18,223 +22,226 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp); storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);
auto apFormula = std::make_shared<storm::logic::AtomicLabelFormula>("two");
//storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(apFormula);
//storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*eventuallyFormula);
//std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 0.0277777612209320068),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
//ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//apFormula = new storm::property::prctl::Ap<double>("two");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
//
//result = mc.checkNoBoundOperator(*probFormula);
//
//ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//
//delete probFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("three");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
//
//result = mc.checkNoBoundOperator(*probFormula);
//
//ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//
//delete probFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("three");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
//
//result = mc.checkNoBoundOperator(*probFormula);
//
//ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//
//delete probFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("four");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
//
//result = mc.checkNoBoundOperator(*probFormula);
//
//ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//
//delete probFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("four");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
//
//result = mc.checkNoBoundOperator(*probFormula);
//
//ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//
//delete probFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("done");
//storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
//
//result = mc.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);;
//delete rewardFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("done");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
//
//result = mc.checkNoBoundOperator(*rewardFormula);;
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as<storm::models::Mdp<double>>();
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
//delete rewardFormula;
//std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", "")->as<storm::models::Mdp<double>>();
//
//storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
//apFormula = new storm::property::prctl::Ap<double>("done");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
//
//result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.33332904), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
//delete rewardFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("done");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
//
//result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 7.33333151), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::Mdp<double>>();
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
//delete rewardFormula;
//std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::Mdp<double>>();
//
//storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
//
//apFormula = new storm::property::prctl::Ap<double>("done");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
//
//result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 14.6666581), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 14.6666581), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
//delete rewardFormula;
//
//apFormula = new storm::property::prctl::Ap<double>("done");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
//
//result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 14.666663), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 14.666663), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
//delete rewardFormula;
} }
TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
//storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as<storm::models::Mdp<double>>(); std::shared_ptr<storm::models::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
//ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
//ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
//storm::modelchecker::prctl::TopologicalValueIterationMdpPrctlModelChecker<double> mc(*mdp);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
//storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
//storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
//std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
//delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
//apFormula = new storm::property::prctl::Ap<double>("elected");
//eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
//result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
//delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
//apFormula = new storm::property::prctl::Ap<double>("elected");
//storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
//result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
//delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
//apFormula = new storm::property::prctl::Ap<double>("elected");
//boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
//probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
//result = mc.checkNoBoundOperator(*probFormula);
ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
//delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
//apFormula = new storm::property::prctl::Ap<double>("elected");
//storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);
//result = mc.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 4.285701547), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 4.285701547), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
//delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
//apFormula = new storm::property::prctl::Ap<double>("elected");
//reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
//rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);
//result = mc.checkNoBoundOperator(*rewardFormula);
#ifdef STORM_HAVE_CUDAFORSTORM #ifdef STORM_HAVE_CUDAFORSTORM
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#else #else
ASSERT_LT(std::abs(result[0] - 4.285703591), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
//ASSERT_LT(std::abs(result[0] - 4.285703591), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
#endif #endif
delete rewardFormula;
//delete rewardFormula;
} }
Write Preview
Loading…
Cancel
Save