Storm 1.11.1.1
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 "test/storm_gtest.h"
3
4#include "storm/exceptions/InvalidOperationException.h"
5#include "storm/storage/Scheduler.h"
6
7TEST(SchedulerTest, TotalDeterministicMemorylessScheduler) {
8 storm::storage::Scheduler<double> scheduler(4);
9
10 ASSERT_NO_THROW(scheduler.setChoice(1, 0));
11 ASSERT_NO_THROW(scheduler.setChoice(3, 1));
12 ASSERT_NO_THROW(scheduler.setChoice(5, 2));
13 ASSERT_NO_THROW(scheduler.setChoice(4, 3));
14
15 ASSERT_FALSE(scheduler.isPartialScheduler());
16 ASSERT_TRUE(scheduler.isMemorylessScheduler());
17 ASSERT_TRUE(scheduler.isDeterministicScheduler());
18
19 ASSERT_TRUE(scheduler.getChoice(0).isDefined());
20 ASSERT_EQ(1ul, scheduler.getChoice(0).getDeterministicChoice());
21
22 ASSERT_TRUE(scheduler.getChoice(1).isDefined());
23 ASSERT_EQ(3ul, scheduler.getChoice(1).getDeterministicChoice());
24
25 ASSERT_TRUE(scheduler.getChoice(2).isDefined());
26 ASSERT_EQ(5ul, scheduler.getChoice(2).getDeterministicChoice());
27
28 ASSERT_TRUE(scheduler.getChoice(3).isDefined());
29 ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice());
30}
31
32TEST(SchedulerTest, PartialDeterministicMemorylessScheduler) {
33 storm::storage::Scheduler<double> scheduler(4);
34
35 ASSERT_NO_THROW(scheduler.setChoice(1, 0));
36 ASSERT_NO_THROW(scheduler.setChoice(3, 0));
37 ASSERT_NO_THROW(scheduler.setChoice(5, 2));
38 ASSERT_NO_THROW(scheduler.setChoice(4, 3));
39 ASSERT_NO_THROW(scheduler.clearChoice(2));
40
41 ASSERT_TRUE(scheduler.isPartialScheduler());
42 ASSERT_TRUE(scheduler.isMemorylessScheduler());
43 ASSERT_TRUE(scheduler.isDeterministicScheduler());
44
45 ASSERT_TRUE(scheduler.getChoice(0).isDefined());
46 ASSERT_EQ(3ul, scheduler.getChoice(0).getDeterministicChoice());
47
48 ASSERT_TRUE(scheduler.getChoice(3).isDefined());
49 ASSERT_EQ(4ul, scheduler.getChoice(3).getDeterministicChoice());
50
51 ASSERT_FALSE(scheduler.getChoice(1).isDefined());
52 ASSERT_FALSE(scheduler.getChoice(2).isDefined());
53}
TEST
TEST(SchedulerTest, TotalDeterministicMemorylessScheduler)
Definition SchedulerTest.cpp:7
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