Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
SchedulerTest.cpp
Go to the documentation of this file.
1#include "storm-config.h"
2#include "storm/exceptions/InvalidOperationException.h"
3#include "storm/storage/Scheduler.h"
4#include "test/storm_gtest.h"
5
6TEST(SchedulerTest, TotalDeterministicMemorylessScheduler) {
7 storm::storage::Scheduler<double> scheduler(4);
8
9 ASSERT_NO_THROW(scheduler.setChoice(1, 0));
10 ASSERT_NO_THROW(scheduler.setChoice(3, 1));
11 ASSERT_NO_THROW(scheduler.setChoice(5, 2));
12 ASSERT_NO_THROW(scheduler.setChoice(4, 3));
13
14 ASSERT_FALSE(scheduler.isPartialScheduler());
15 ASSERT_TRUE(scheduler.isMemorylessScheduler());
16 ASSERT_TRUE(scheduler.isDeterministicScheduler());
17
18 ASSERT_TRUE(scheduler.getChoice(0).isDefined());
19 ASSERT_EQ(1ul, scheduler.getChoice(0).getDeterministicChoice());
20
21 ASSERT_TRUE(scheduler.getChoice(1).isDefined());
22 ASSERT_EQ(3ul, scheduler.getChoice(1).getDeterministicChoice());
23
24 ASSERT_TRUE(scheduler.getChoice(2).isDefined());
25 ASSERT_EQ(5ul, scheduler.getChoice(2).getDeterministicChoice());
26
27 ASSERT_TRUE(scheduler.getChoice(3).isDefined());
28 ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice());
29}
30
31TEST(SchedulerTest, PartialDeterministicMemorylessScheduler) {
32 storm::storage::Scheduler<double> scheduler(4);
33
34 ASSERT_NO_THROW(scheduler.setChoice(1, 0));
35 ASSERT_NO_THROW(scheduler.setChoice(3, 0));
36 ASSERT_NO_THROW(scheduler.setChoice(5, 2));
37 ASSERT_NO_THROW(scheduler.setChoice(4, 3));
38 ASSERT_NO_THROW(scheduler.clearChoice(2));
39
40 ASSERT_TRUE(scheduler.isPartialScheduler());
41 ASSERT_TRUE(scheduler.isMemorylessScheduler());
42 ASSERT_TRUE(scheduler.isDeterministicScheduler());
43
44 ASSERT_TRUE(scheduler.getChoice(0).isDefined());
45 ASSERT_EQ(3ul, scheduler.getChoice(0).getDeterministicChoice());
46
47 ASSERT_TRUE(scheduler.getChoice(3).isDefined());
48 ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice());
49
50 ASSERT_FALSE(scheduler.getChoice(1).isDefined());
51 ASSERT_FALSE(scheduler.getChoice(2).isDefined());
52}
TEST
TEST(SchedulerTest, TotalDeterministicMemorylessScheduler)
Definition SchedulerTest.cpp:6
storm::storage::Scheduler
This class defines which action is chosen in a particular state of a non-deterministic model.
Definition Scheduler.h:18
storm::storage::Scheduler::isDeterministicScheduler
bool isDeterministicScheduler() const
Retrieves whether all defined choices are deterministic.
Definition Scheduler.cpp:150
storm::storage::Scheduler::isPartialScheduler
bool isPartialScheduler() const
Retrieves whether there is a reachable pair of model and memory state for which the choice is undefin...
Definition Scheduler.cpp:145
storm::storage::Scheduler::getChoice
SchedulerChoice< ValueType > const & getChoice(uint_fast64_t modelState, uint_fast64_t memoryState=0) const
Gets the choice defined by the scheduler for the given model and memory state.
Definition Scheduler.cpp:86
storm::storage::Scheduler::clearChoice
void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState=0)
Clears the choice defined by the scheduler for the given state.
Definition Scheduler.cpp:79
storm::storage::Scheduler::setChoice
void setChoice(SchedulerChoice< ValueType > const &choice, uint_fast64_t modelState, uint_fast64_t memoryState=0)
Sets the choice defined by the scheduler for the given state.
Definition Scheduler.cpp:37
storm::storage::Scheduler::isMemorylessScheduler
bool isMemorylessScheduler() const
Retrieves whether the scheduler considers a trivial memory structure (i.e., a memory structure with j...
Definition Scheduler.cpp:155
storm_gtest.h