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

Fixed performance tests. 

WARNING: I had to remove the SolverSelection in the call due to the new API - the performance tests might now all use the same Solver.

Former-commit-id: 7d5ed3191d
main
PBerger 9 years ago
parent
2c2049dc0b
commit
0f84cdcadb
5 changed files with 13 additions and 11 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. 5
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  2. 6
      test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  3. 5
      test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  4. 4
      test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  5. 4
      test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp

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

@ -10,6 +10,7 @@
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/parser/FormulaParser.h" #include "src/parser/FormulaParser.h"
#include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/StandardRewardModel.h"
#include "src/solver/GmmxxLinearEquationSolver.h"
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
@ -21,7 +22,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::GmmxxLinearEquationSolverFactory<double>()));
// 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;
@ -59,7 +60,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::GmmxxLinearEquationSolverFactory<double>()));
// 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;

6
test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -8,7 +8,7 @@
#include "src/utility/solver.h" #include "src/utility/solver.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/StandardRewardModel.h"
#include "src/solver/MinMaxLinearEquationSolver.h"
#include "src/parser/FormulaParser.h" #include "src/parser/FormulaParser.h"
TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
@ -24,7 +24,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -82,7 +82,7 @@ TEST(GmxxMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Gmmxx)));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");

5
test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -10,6 +10,7 @@
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/parser/FormulaParser.h" #include "src/parser/FormulaParser.h"
#include "src/models/sparse/StandardRewardModel.h" #include "src/models/sparse/StandardRewardModel.h"
#include "src/solver/NativeLinearEquationSolver.h"
TEST(NativeDtmcPrctlModelCheckerTest, Crowds) { TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", ""); std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds20_5.lab", "", "");
@ -21,7 +22,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::NativeLinearEquationSolverFactory<double>()));
// 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;
@ -59,7 +60,7 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::solver::LinearEquationSolverFactory<double>>(new storm::solver::NativeLinearEquationSolverFactory<double>()));
// 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;

4
test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -25,7 +25,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -83,7 +83,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Native)));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");

4
test/performance/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -20,7 +20,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLea
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull); ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
@ -67,7 +67,7 @@ TEST(DISABLED_TopologicalValueIterationMdpPrctlModelCheckerTest, Consensus) {
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull); ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull); ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::MinMaxLinearEquationSolverFactory<double>(storm::solver::EquationSolverTypeSelection::Topological)));
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::solver::GeneralMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]"); std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"finished\"]");

Write Preview
Loading…
Cancel
Save