diff --git a/src/storage/TotalScheduler.cpp b/src/storage/TotalScheduler.cpp index bcbc22e61..ae609a4f4 100644 --- a/src/storage/TotalScheduler.cpp +++ b/src/storage/TotalScheduler.cpp @@ -1,4 +1,5 @@ #include "src/storage/TotalScheduler.h" +#include "src/exceptions/InvalidArgumentException.h" namespace storm { namespace storage { @@ -11,6 +12,9 @@ namespace storm { } void TotalScheduler::setChoice(uint_fast64_t state, uint_fast64_t choice) { + if (state > choices.size()) { + throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::setChoice: scheduler cannot not define a choice for state " << state << "."; + } choices[state] = choice; } @@ -19,6 +23,10 @@ namespace storm { } uint_fast64_t TotalScheduler::getChoice(uint_fast64_t state) const { + if (state >= choices.size()) { + throw storm::exceptions::InvalidArgumentException() << "Invalid call to TotalScheduler::getChoice: scheduler does not define a choice for state " << state << "."; + } + return choices[state]; } diff --git a/test/functional/storage/SchedulerTest.cpp b/test/functional/storage/SchedulerTest.cpp new file mode 100644 index 000000000..df51ab2a9 --- /dev/null +++ b/test/functional/storage/SchedulerTest.cpp @@ -0,0 +1,42 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/storage/PartialScheduler.h" +#include "src/storage/TotalScheduler.h" + +TEST(SchedulerTest, PartialScheduler) { + storm::storage::PartialScheduler scheduler; + + ASSERT_NO_THROW(scheduler.setChoice(0, 1)); + ASSERT_NO_THROW(scheduler.setChoice(0, 3)); + ASSERT_NO_THROW(scheduler.setChoice(3, 4)); + + ASSERT_TRUE(scheduler.isChoiceDefined(0)); + ASSERT_EQ(3, scheduler.getChoice(0)); + + ASSERT_TRUE(scheduler.isChoiceDefined(3)); + ASSERT_EQ(4, scheduler.getChoice(3)); + + ASSERT_FALSE(scheduler.isChoiceDefined(1)); + ASSERT_THROW(scheduler.getChoice(1), storm::exceptions::InvalidArgumentException); +} + +TEST(SchedulerTest, TotalScheduler) { + storm::storage::TotalScheduler scheduler(4); + + ASSERT_NO_THROW(scheduler.setChoice(0, 1)); + ASSERT_NO_THROW(scheduler.setChoice(0, 3)); + ASSERT_NO_THROW(scheduler.setChoice(3, 4)); + + ASSERT_TRUE(scheduler.isChoiceDefined(0)); + ASSERT_EQ(3, scheduler.getChoice(0)); + + ASSERT_TRUE(scheduler.isChoiceDefined(3)); + ASSERT_EQ(4, scheduler.getChoice(3)); + + ASSERT_TRUE(scheduler.isChoiceDefined(1)); + ASSERT_EQ(0, scheduler.getChoice(1)); + + ASSERT_THROW(scheduler.getChoice(4), storm::exceptions::InvalidArgumentException); + ASSERT_THROW(scheduler.setChoice(5, 2), storm::exceptions::InvalidArgumentException); +} \ No newline at end of file diff --git a/test/performance/storage/MaximalEndComponentDecompositionTest.cpp b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp new file mode 100644 index 000000000..a34a35091 --- /dev/null +++ b/test/performance/storage/MaximalEndComponentDecompositionTest.cpp @@ -0,0 +1,26 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/parser/AutoParser.h" +#include "src/storage/MaximalEndComponentDecomposition.h" + +TEST(MaximalEndComponentDecomposition, AsynchronousLeader) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); + std::shared_ptr> mdp = parser.getModel>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition; + ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); + + ASSERT_EQ(7, mecDecomposition.size()); + mdp = nullptr; +} + +TEST(MaximalEndComponentDecomposition, Consensus) { + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); + std::shared_ptr> mdp = parser.getModel>(); + + storm::storage::MaximalEndComponentDecomposition mecDecomposition; + ASSERT_NO_THROW(mecDecomposition = storm::storage::MaximalEndComponentDecomposition(*mdp)); + + ASSERT_EQ(384, mecDecomposition.size()); + mdp = nullptr; +} \ No newline at end of file diff --git a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp index 30bfd5734..b519c27be 100644 --- a/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp +++ b/test/performance/storage/StronglyConnectedComponentDecompositionTest.cpp @@ -8,41 +8,69 @@ TEST(StronglyConnectedComponentDecomposition, Crowds) { std::shared_ptr> dtmc = parser.getModel>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc)); - - ASSERT_EQ(sccDecomposition.size(), 1290297ull); + ASSERT_EQ(1290297ull, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true)); + ASSERT_EQ(1290297, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, true)); + ASSERT_EQ(425040, sccDecomposition.size()); + dtmc = nullptr; } TEST(StronglyConnectedComponentDecomposition, SynchronousLeader) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader6_8.lab", "", ""); + storm::parser::AutoParser parser(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 = parser.getModel>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc)); + ASSERT_EQ(2611835, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true)); + ASSERT_EQ(2611835, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*dtmc, true, true)); + ASSERT_EQ(1, sccDecomposition.size()); - ASSERT_EQ(sccDecomposition.size(), 1279673ull); dtmc = nullptr; } TEST(StronglyConnectedComponentDecomposition, AsynchronousLeader) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader6.lab", "", ""); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader7.lab", "", ""); std::shared_ptr> mdp = parser.getModel>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); - ASSERT_EQ(sccDecomposition.size(), 146844ull); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); + ASSERT_EQ(1461930, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); + ASSERT_EQ(127, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); + ASSERT_EQ(127, sccDecomposition.size()); + mdp = nullptr; } TEST(StronglyConnectedComponentDecomposition, Consensus) { - storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin4_6.lab", "", ""); + storm::parser::AutoParser parser(STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.tra", STORM_CPP_BASE_PATH "/examples/mdp/consensus/coin6_4.lab", "", ""); std::shared_ptr> mdp = parser.getModel>(); storm::storage::StronglyConnectedComponentDecomposition sccDecomposition; - ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); - ASSERT_EQ(sccDecomposition.size(), 2611ull); + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp)); + ASSERT_EQ(121251, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true)); + ASSERT_EQ(1049, sccDecomposition.size()); + + ASSERT_NO_THROW(sccDecomposition = storm::storage::StronglyConnectedComponentDecomposition(*mdp, true, true)); + ASSERT_EQ(384, sccDecomposition.size()); + mdp = nullptr; } \ No newline at end of file