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

Added lab files for asynch_leader and corrected pctl file a bit. Included first (incorrect) tests for performance test suite.

tempestpy_adaptions
dehnert 12 years ago
parent
6ba1cf25c8
commit
5149a7a943
3 changed files with 336 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. 6
      examples/mdp/asynchronous_leader/leader.pctl
  2. 116
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  3. 217
      test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp

6
examples/mdp/asynchronous_leader/leader.pctl
View File

@ -1,8 +1,8 @@
Pmin=? [ F elected ]
const int K = 25;
Pmin=? [ F<=K elected ]
Pmax=? [ F<=K elected ]
// const int K = 25;
Pmin=? [ F<=25 elected ]
Pmax=? [ F<=25 elected ]
Rmin=? [ F elected ]
Rmax=? [ F elected ]

116
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -0,0 +1,116 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/utility/Settings.h"
#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
storm::settings::Settings* s = storm::settings::instance();
s->set("fix-deadlocks");
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
ASSERT_EQ(parser.getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 8607u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u);
storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("observe0Greater1");
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);
std::vector<double>* result = probFormula->check(mc);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.3328800375801578281), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("observeIGreater1");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.1522173670950556501), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("observeOnlyTrueSender");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.32153724292835045), s->get<double>("precision"));
delete probFormula;
delete result;
}
/*
TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
storm::settings::Settings* s = storm::settings::instance();
s->set("fix-deadlocks");
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.pick.trans.rew");
ASSERT_EQ(parser.getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 12400u);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u);
storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
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);
std::vector<double>* result = probFormula->check(mc);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::property::prctl::BoundedUntil<double>(new storm::property::prctl::Ap<double>("true"), apFormula, 20);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
result = probFormula->check(mc);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.9999965911265462636), s->get<double>("precision"));
delete probFormula;
delete result;
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);
result = rewardFormula->check(mc);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1.0448979591835938496), s->get<double>("precision"));
delete rewardFormula;
delete result;
}
*/

217
test/performance/modelchecker/GmmxxMdpPrctModelCheckerTest.cpp
View File

@ -0,0 +1,217 @@
#include "gtest/gtest.h"
#include "storm-config.h"
#include "src/utility/Settings.h"
#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
#include "src/parser/AutoParser.h"
TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
storm::settings::Settings* s = storm::settings::instance();
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.trans.rew");
ASSERT_EQ(parser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
storm::modelchecker::GmmxxMdpPrctlModelChecker<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);
std::vector<double>* result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
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);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
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, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
delete probFormula;
delete result;
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, false);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
delete probFormula;
delete result;
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);
ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision"));
delete rewardFormula;
delete result;
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);;
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
delete rewardFormula;
delete result;
}
TEST(GmmxxMdpPrctModelCheckerTest, Consensus) {
storm::settings::Settings* s = storm::settings::instance();
storm::parser::AutoParser<double> parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_6.steps.state.rew", "");
ASSERT_EQ(parser.getType(), storm::models::MDP);
std::shared_ptr<storm::models::Mdp<double>> mdp = parser.getModel<storm::models::Mdp<double>>();
storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
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_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Ap<double>* apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_0");
storm::property::prctl::And<double>* andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_1");
andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("agree");
storm::property::prctl::Not<double>* notFormula = new storm::property::prctl::Not<double>(apFormula2);
andFormula = new storm::property::prctl::And<double>(apFormula, notFormula);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 1), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 0.0625), s->get<double>("precision"));
delete probFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
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);
ASSERT_LT(std::abs((*result)[0] - 4.28568908480604982), s->get<double>("precision"));
delete rewardFormula;
delete result;
apFormula = new storm::property::prctl::Ap<double>("finished");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);;
ASSERT_NE(nullptr, result);
ASSERT_LT(std::abs((*result)[0] - 4.2856904354441400784), s->get<double>("precision"));
delete rewardFormula;
delete result;
}
Write Preview
Loading…
Cancel
Save