diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index d99806231..ccf090674 100755 --- a/src/test/storm/CMakeLists.txt +++ b/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) diff --git a/src/test/storm/automata/HOAParsingTest.cpp b/src/test/storm/automata/HOAParsingTest.cpp new file mode 100644 index 000000000..1e733ee74 --- /dev/null +++ b/src/test/storm/automata/HOAParsingTest.cpp @@ -0,0 +1,31 @@ +#include "gtest/gtest.h" +#include "storm/automata/DeterministicAutomaton.h" + +#include +#include + +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); +}