(DA) tests: HOAParsingTest

src/test/storm/CMakeLists.txt

@@ -10,7 +10,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test)
 include_directories(${GTEST_INCLUDE_DIR})
 
 # Set split and non-split test directories
-set(NON_SPLIT_TESTS abstraction adapter builder logic model parser permissiveschedulers simulator solver storage transformer utility)
+set(NON_SPLIT_TESTS abstraction adapter automata builder logic model parser permissiveschedulers solver storage transformer utility)
 set(MODELCHECKER_TEST_SPLITS abstraction csl exploration multiobjective reachability)
 set(MODELCHECKER_PRCTL_TEST_SPLITS dtmc mdp)
 

src/test/storm/automata/HOAParsingTest.cpp

@@ -0,0 +1,31 @@
+#include "gtest/gtest.h"
+#include "storm/automata/DeterministicAutomaton.h"
+
+#include <string>
+#include <sstream>
+
+TEST(DeterministicAutomaton, ParseAutomaton) {
+    std::string aUb =
+            "HOA: v1\n"
+            "States: 3\n"
+            "Start: 0\n"
+            "acc-name: Rabin 1\n"
+            "Acceptance: 2 (Fin(0) & Inf(1))\n"
+            "AP: 2 \"a\" \"b\""
+            "--BODY--\n"
+            "State: 0 \"a U b\" { 0 }\n"
+            "  2  /* !a  & !b */\n"
+            "  0  /*  a  & !b */\n"
+            "  1  /* !a  &  b */\n"
+            "  1  /*  a  &  b */\n"
+            "State: 1 { 1 }\n"
+            "  1 1 1 1       /* four transitions on one line */\n"
+            "State: 2 \"sink state\" { 0 }\n"
+            "  2 2 2 2\n"
+            "--END--\n";
+
+    std::istringstream in = std::istringstream(aUb);
+    storm::automata::DeterministicAutomaton::ptr da;
+    ASSERT_NO_THROW(da = storm::automata::DeterministicAutomaton::parse(in));
+    // da->printHOA(std::cout);
+}