From aae472389e72e1c83c865b83bde7891d5af4458c Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 4 Apr 2019 17:03:25 +0200
Subject: [PATCH] Added test for scheduler

---
 tests/storage/test_scheduler.py | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 tests/storage/test_scheduler.py

diff --git a/tests/storage/test_scheduler.py b/tests/storage/test_scheduler.py
new file mode 100644
index 0000000..b1bbefe
--- /dev/null
+++ b/tests/storage/test_scheduler.py
@@ -0,0 +1,30 @@
+import stormpy
+import stormpy.logic
+from helpers.helper import get_example_path
+import pytest
+
+
+class TestScheduler:
+
+    def test_scheduler_mdp(self):
+        program = stormpy.parse_prism_program(get_example_path("mdp", "coin2-2.nm"))
+        formulas = stormpy.parse_properties_for_prism_program("Pmin=? [ F \"finished\" & \"all_coins_equal_1\"]", program)
+        model = stormpy.build_model(program, formulas)
+        assert model.nr_states == 272
+        assert model.nr_transitions == 492
+        assert len(model.initial_states) == 1
+        initial_state = model.initial_states[0]
+        assert initial_state == 0
+        result = stormpy.model_checking(model, formulas[0], extract_scheduler=True)
+        assert result.has_scheduler
+        scheduler = result.scheduler
+        assert scheduler.memoryless
+        assert scheduler.memory_size == 1
+        assert scheduler.deterministic
+        for state in model.states:
+            choice = scheduler.get_choice(state)
+            assert choice.defined
+            assert choice.deterministic
+            action = choice.get_deterministic_choice()
+            assert 0 <= action
+            assert action < len(state.actions)