From a88b64bad35544194718fdf535afa3ecb36d5a0f Mon Sep 17 00:00:00 2001 From: hannah Date: Sun, 27 Jun 2021 15:14:41 +0200 Subject: [PATCH] DTMC HOA tests --- .../testfiles/hoa/automaton_Fandp0Xp1.hoa | 27 +++++++++++ .../testfiles/hoa/automaton_UXp0p1.hoa | 32 +++++++++++++ .../prctl/dtmc/DtmcPrctlModelCheckerTest.cpp | 48 +++++++++++++++++++ 3 files changed, 107 insertions(+) create mode 100644 resources/examples/testfiles/hoa/automaton_Fandp0Xp1.hoa create mode 100644 resources/examples/testfiles/hoa/automaton_UXp0p1.hoa diff --git a/resources/examples/testfiles/hoa/automaton_Fandp0Xp1.hoa b/resources/examples/testfiles/hoa/automaton_Fandp0Xp1.hoa new file mode 100644 index 000000000..1998df31e --- /dev/null +++ b/resources/examples/testfiles/hoa/automaton_Fandp0Xp1.hoa @@ -0,0 +1,27 @@ +HOA: v1 +States: 3 +properties: implicit-labels trans-labels no-univ-branch deterministic complete +tool: "ltl2dstar" "0.5.4" +name: "F & p0 X p1" +comment: "DBA2DRA[NBA=3]" +acc-name: Rabin 1 +Acceptance: 2 (Fin(0)&Inf(1)) +Start: 2 +AP: 2 "p0" "p1" +--BODY-- +State: 0 {1} +0 +0 +0 +0 +State: 1 {} +2 +1 +0 +0 +State: 2 {} +2 +1 +2 +1 +--END-- diff --git a/resources/examples/testfiles/hoa/automaton_UXp0p1.hoa b/resources/examples/testfiles/hoa/automaton_UXp0p1.hoa new file mode 100644 index 000000000..2927e0b91 --- /dev/null +++ b/resources/examples/testfiles/hoa/automaton_UXp0p1.hoa @@ -0,0 +1,32 @@ +HOA: v1 +States: 4 +properties: implicit-labels trans-labels no-univ-branch deterministic complete +tool: "ltl2dstar" "0.5.4" +name: "U X p0 p1" +comment: "DBA2DRA[NBA=3]" +acc-name: Rabin 1 +Acceptance: 2 (Fin(0)&Inf(1)) +Start: 1 +AP: 2 "p0" "p1" +--BODY-- +State: 0 {1} +0 +0 +0 +0 +State: 1 {} +2 +2 +0 +0 +State: 2 {} +3 +2 +3 +0 +State: 3 {} +3 +3 +3 +3 +--END-- diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index d45519900..419f744cc 100755 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -808,4 +808,52 @@ namespace { #endif } + TYPED_TEST(DtmcPrctlModelCheckerTest, HOAProbabilitiesDie) { + // "P=? [(X s>0) U (s=7 & d=2)]" + std::string formulasString = "P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (s=7 & d=2) }]"; + // "P=? [(X s>0) U (d=4 | d=2)]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s>0), \"p1\" -> (d=4 | d=2) }]"; + // "P=? [ (F s=4) & (X \"three\")]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4), \"p1\" -> \"three\" }]"; + // "P=? [ (F s=6) & (X \"done\")]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> \"done\" }]"; + // "P=? [ (F s=6) & (X !\"done\")]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=6), \"p1\" -> !\"done\" }]"; + // "P=? [ (F (s=4 | s=5)) & (X (\"three\" | \"five\"))]" + formulasString += "; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR "/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s=4 | s=5), \"p1\" -> s=7 & (d=3 | d=5) }]"; + + auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm", formulasString); + auto model = std::move(modelFormulas.first); + auto tasks = this->getTasks(modelFormulas.second); + EXPECT_EQ(13ul, model->getNumberOfStates()); + EXPECT_EQ(20ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc); + auto checker = this->createModelChecker(model); + std::unique_ptr result; + + // Not supported in all engines (Hybrid, PrismDd, JaniDd) + if (TypeParam::engine == DtmcEngine::PrismSparse || TypeParam::engine == DtmcEngine::JaniSparse || TypeParam::engine == DtmcEngine::JitSparse) { + result = checker->check(tasks[0]); + EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[1]); + EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[2]); + EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[3]); + EXPECT_NEAR(this->parseNumber("1/6"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[4]); + EXPECT_NEAR(this->parseNumber("1/8"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + + result = checker->check(tasks[5]); + EXPECT_NEAR(this->parseNumber("1/3"), this->getQuantitativeResultAtInitialState(model, result), this->precision()); + } else { + EXPECT_FALSE(checker->canHandle(tasks[0])); + } + + } + }