From f0b174b75652bb9b58d25f1a382fea9c0e5fd24e Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Feb 2015 17:58:10 +0100 Subject: [PATCH] Fixed performance tests. Former-commit-id: f58e2eb92300c4aae1fdec8a013b84cd39daddba --- .../csl/SparseMarkovAutomatonCslModelChecker.cpp | 2 ++ .../prctl/SparseDtmcPrctlModelChecker.cpp | 1 + .../prctl/SparseMdpPrctlModelChecker.cpp | 1 + src/models/sparse/Ctmc.h | 2 -- src/models/sparse/DeterministicModel.h | 3 --- src/models/sparse/Dtmc.cpp | 1 + src/models/sparse/Dtmc.h | 15 --------------- src/models/sparse/MarkovAutomaton.h | 8 -------- src/models/sparse/Mdp.h | 12 +----------- src/models/sparse/Model.cpp | 1 + src/models/sparse/Model.h | 9 +-------- src/models/sparse/NondeterministicModel.h | 2 -- .../DeterministicModelBisimulationDecomposition.h | 1 + test/performance/graph/GraphTest.cpp | 12 ++++++------ .../GmmxxDtmcPrctModelCheckerTest.cpp | 8 ++++---- .../SparseMdpPrctlModelCheckerTest.cpp | 8 ++++---- .../MaximalEndComponentDecompositionTest.cpp | 6 +++--- ...tronglyConnectedComponentDecompositionTest.cpp | 12 ++++++------ 18 files changed, 32 insertions(+), 72 deletions(-) diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp index 22b891379..45558db78 100644 --- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp +++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp @@ -3,6 +3,8 @@ #include #include +#include "src/storage/StronglyConnectedComponentDecomposition.h" + #include "src/utility/constants.h" #include "src/utility/macros.h" #include "src/utility/vector.h" diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index df3724f7e..7dbc8c9b5 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -9,6 +9,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" namespace storm { diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index c94524b8a..5078cd8d8 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" namespace storm { diff --git a/src/models/sparse/Ctmc.h b/src/models/sparse/Ctmc.h index 1c0da3922..abfe0aba5 100644 --- a/src/models/sparse/Ctmc.h +++ b/src/models/sparse/Ctmc.h @@ -5,8 +5,6 @@ #include #include "src/models/sparse/DeterministicModel.h" -#include "src/models/sparse/StateLabeling.h" -#include "src/storage/SparseMatrix.h" #include "src/utility/OsDetection.h" namespace storm { diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h index a26998be0..940048dc6 100644 --- a/src/models/sparse/DeterministicModel.h +++ b/src/models/sparse/DeterministicModel.h @@ -1,9 +1,6 @@ #ifndef STORM_MODELS_SPARSE_DETERMINISTICMODEL_H_ #define STORM_MODELS_SPARSE_DETERMINISTICMODEL_H_ -#include -#include - #include "src/models/sparse/Model.h" #include "src/utility/OsDetection.h" diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp index 898bfc0cb..20ae981a2 100644 --- a/src/models/sparse/Dtmc.cpp +++ b/src/models/sparse/Dtmc.cpp @@ -1,6 +1,7 @@ #include "src/models/sparse/Dtmc.h" #include "src/adapters/CarlAdapter.h" +#include "src/exceptions/NotImplementedException.h" namespace storm { namespace models { diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h index 06211f1a8..2ff6dd884 100644 --- a/src/models/sparse/Dtmc.h +++ b/src/models/sparse/Dtmc.h @@ -1,23 +1,8 @@ #ifndef STORM_MODELS_SPARSE_DTMC_H_ #define STORM_MODELS_SPARSE_DTMC_H_ -#include -#include -#include -#include - #include "src/models/sparse/DeterministicModel.h" -#include "src/models/sparse/StateLabeling.h" -#include "src/storage/SparseMatrix.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/exceptions/NotImplementedException.h" -#include "src/settings/SettingsManager.h" #include "src/utility/OsDetection.h" -#include "src/utility/constants.h" -#include "src/utility/vector.h" -#include "src/utility/macros.h" -#include "src/utility/matrix.h" -#include "src/utility/constants.h" namespace storm { namespace models { diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h index 4b551f6e9..d051965cc 100644 --- a/src/models/sparse/MarkovAutomaton.h +++ b/src/models/sparse/MarkovAutomaton.h @@ -2,15 +2,7 @@ #define STORM_MODELS_SPARSE_MARKOVAUTOMATON_H_ #include "src/models/sparse/NondeterministicModel.h" -#include "src/models/sparse/StateLabeling.h" -#include "src/storage/SparseMatrix.h" -#include "src/storage/sparse/StateType.h" -#include "src/exceptions/InvalidArgumentException.h" -#include "src/settings/SettingsManager.h" #include "src/utility/OsDetection.h" -#include "src/utility/constants.h" -#include "src/utility/vector.h" -#include "src/utility/matrix.h" namespace storm { namespace models { diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h index f6ef7691f..4b62f7377 100644 --- a/src/models/sparse/Mdp.h +++ b/src/models/sparse/Mdp.h @@ -1,18 +1,8 @@ #ifndef STORM_MODELS_SPARSE_MDP_H_ #define STORM_MODELS_SPARSE_MDP_H_ -#include -#include -#include -#include -#include - -#include "src/models/sparse/StateLabeling.h" -#include "src/storage/SparseMatrix.h" -#include "src/settings/SettingsManager.h" #include "src/models/sparse/NondeterministicModel.h" -#include "src/utility/constants.h" -#include "src/utility/matrix.h" +#include "src/utility/OsDetection.h" namespace storm { namespace models { diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp index 1df5446bc..5dd29c3b6 100644 --- a/src/models/sparse/Model.cpp +++ b/src/models/sparse/Model.cpp @@ -1,5 +1,6 @@ #include "src/models/sparse/Model.h" +#include "src/utility/vector.h" #include "src/adapters/CarlAdapter.h" namespace storm { diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h index e2253b64b..3c8f56fd2 100644 --- a/src/models/sparse/Model.h +++ b/src/models/sparse/Model.h @@ -1,7 +1,6 @@ #ifndef STORM_MODELS_SPARSE_MODEL_H_ #define STORM_MODELS_SPARSE_MODEL_H_ -#include #include #include #include @@ -11,14 +10,8 @@ #include "src/storage/sparse/StateType.h" #include "src/storage/BitVector.h" #include "src/storage/SparseMatrix.h" -#include "src/storage/Scheduler.h" -#include "src/storage/StronglyConnectedComponentDecomposition.h" -#include "src/utility/constants.h" +#include "src/storage/Decomposition.h" #include "src/utility/OsDetection.h" -#include "src/utility/macros.h" -#include "src/utility/vector.h" - -#include "src/exceptions/InvalidOperationException.h" namespace storm { namespace models { diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h index a6ae98a50..87d77111b 100644 --- a/src/models/sparse/NondeterministicModel.h +++ b/src/models/sparse/NondeterministicModel.h @@ -1,8 +1,6 @@ #ifndef STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ #define STORM_MODELS_SPARSE_NONDETERMINISTICMODEL_H_ -#include - #include "src/models/sparse/Model.h" #include "src/utility/OsDetection.h" diff --git a/src/storage/DeterministicModelBisimulationDecomposition.h b/src/storage/DeterministicModelBisimulationDecomposition.h index 862f9148f..7dcc67614 100644 --- a/src/storage/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/DeterministicModelBisimulationDecomposition.h @@ -6,6 +6,7 @@ #include "src/storage/sparse/StateType.h" #include "src/storage/Decomposition.h" +#include "src/storage/StateBlock.h" #include "src/logic/Formulas.h" #include "src/models/sparse/Dtmc.h" #include "src/models/sparse/Ctmc.h" diff --git a/test/performance/graph/GraphTest.cpp b/test/performance/graph/GraphTest.cpp index 9969c4004..10f65ea20 100644 --- a/test/performance/graph/GraphTest.cpp +++ b/test/performance/graph/GraphTest.cpp @@ -4,13 +4,13 @@ #include "src/parser/AutoParser.h" #include "src/utility/graph.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" -#include "src/models/Mdp.h" -#include "src/models/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Dtmc.h" TEST(GraphTest, PerformProb01) { std::shared_ptr> 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> dtmc = abstractModel->as>(); + std::shared_ptr> dtmc = abstractModel->as>(); storm::storage::BitVector trueStates(dtmc->getNumberOfStates(), true); LOG4CPLUS_WARN(logger, "Computing prob01 (3 times) for crowds/crowds20_5..."); @@ -35,7 +35,7 @@ TEST(GraphTest, PerformProb01) { abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", ""); - std::shared_ptr> dtmc2 = abstractModel->as>(); + std::shared_ptr> dtmc2 = abstractModel->as>(); trueStates = storm::storage::BitVector(dtmc2->getNumberOfStates(), true); LOG4CPLUS_WARN(logger, "Computing prob01 for synchronous_leader/leader6_8..."); @@ -50,7 +50,7 @@ TEST(GraphTest, PerformProb01) { TEST(GraphTest, PerformProb01MinMax) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); storm::storage::BitVector trueStates(mdp->getNumberOfStates(), true); LOG4CPLUS_WARN(logger, "Computing prob01min for asynchronous_leader/leader7..."); @@ -70,7 +70,7 @@ TEST(GraphTest, PerformProb01MinMax) { mdp = nullptr; abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); - std::shared_ptr> mdp2 = abstractModel->as>(); + std::shared_ptr> mdp2 = abstractModel->as>(); trueStates = storm::storage::BitVector(mdp2->getNumberOfStates(), true); LOG4CPLUS_WARN(logger, "Computing prob01min for consensus/coin4_6..."); diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index e144254fc..ae366ae29 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -10,9 +10,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> 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", "", ""); - ASSERT_EQ(abstractModel->getType(), storm::models::DTMC); + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - std::shared_ptr> dtmc = abstractModel->as>(); + std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(2036647ull, dtmc->getNumberOfStates()); ASSERT_EQ(7362293ull, dtmc->getNumberOfTransitions()); @@ -48,9 +48,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(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(abstractModel->getType(), storm::models::DTMC); + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); - std::shared_ptr> dtmc = abstractModel->as>(); + std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(1312334ull, dtmc->getNumberOfStates()); ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions()); diff --git a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp index 65bbbc023..1ef78c021 100644 --- a/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp @@ -10,9 +10,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(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(abstractModel->getType(), storm::models::MDP); + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); ASSERT_EQ(2095783ull, mdp->getNumberOfStates()); ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions()); @@ -72,9 +72,9 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) { TEST(SparseMdpPrctlModelCheckerTest, Consensus) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.steps.state.rew", ""); - ASSERT_EQ(abstractModel->getType(), storm::models::MDP); + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); ASSERT_EQ(63616ull, mdp->getNumberOfStates()); ASSERT_EQ(213472ull, mdp->getNumberOfTransitions()); diff --git a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp index 675cc1384..2dc879341 100644 --- a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp +++ b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp @@ -2,11 +2,11 @@ #include "storm-config.h" #include "src/parser/AutoParser.h" #include "src/storage/MaximalEndComponentDecomposition.h" -#include "src/models/Mdp.h" +#include "src/models/sparse/Mdp.h" TEST(MaximalEndComponentDecomposition, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); @@ -17,7 +17,7 @@ TEST(MaximalEndComponentDecomposition, AsynchronousLeader) { TEST(MaximalEndComponentDecomposition, Consensus) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); storm::storage::MaximalEndComponentDecomposition mecDecomposition; ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp index 25a5cfcaa..1a368b807 100644 --- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -2,12 +2,12 @@ #include "storm-config.h" #include "src/parser/AutoParser.h" #include "src/storage/StronglyConnectedComponentDecomposition.h" -#include "src/models/Mdp.h" -#include "src/models/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Dtmc.h" TEST(StronglyConnectedComponentDecomposition, Crowds) { std::shared_ptr> 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> dtmc = abstractModel->as>(); + std::shared_ptr> dtmc = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -25,7 +25,7 @@ TEST(StronglyConnectedComponentDecomposition, Crowds) { TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_9.lab", "", ""); - std::shared_ptr> dtmc = abstractModel->as>(); + std::shared_ptr> dtmc = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -43,7 +43,7 @@ TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; @@ -61,7 +61,7 @@ TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { TEST(StronglyConnectedComponentDecomposition, Consensus) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); - std::shared_ptr> mdp = abstractModel->as>(); + std::shared_ptr> mdp = abstractModel->as>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition;