From bcf45f68df5d714ea08aaec1b58758288d345fa1 Mon Sep 17 00:00:00 2001 From: hannah Date: Thu, 8 Apr 2021 11:07:13 +0200 Subject: [PATCH] modelchecker test update --- .../prctl/dtmc/DtmcPrctlModelCheckerTest.cpp | 27 ++++++++++++++----- 1 file changed, 20 insertions(+), 7 deletions(-) diff --git a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp index dc3eb96ac..4367cee7d 100755 --- a/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/dtmc/DtmcPrctlModelCheckerTest.cpp @@ -722,10 +722,12 @@ namespace { setenv("LTL2DA", "ltl2da-ltl2tgba", true); //todo set PATH variable std::string formulasString = "P=? [(X s>0) U (s=7 & d=2)]"; - formulasString += "; P=? [ X (s=1) U (s=3) U (s=7)]"; // a U b U c is Treated as: (a U b ) U c - formulasString += "; P=? [ G s!=3 U (\"three\") ]"; - formulasString += "; P=? [ (F (X (s=6 & (XX s=5) ))) & (F G (d!=5))]"; - formulasString += "; P=? [ F ((s=6) & (X \"done\"))]"; + formulasString += "; P=? [ X (((s=1) U (s=3)) U (s=7))]"; + formulasString += "; P=? [ (F (X (s=6 & (XX s=5)))) & (F G (d!=5))]"; + formulasString += "; P=? [ F (s=3 U (\"three\"))]"; + formulasString += "; P=? [ F s=3 U (\"three\")]"; + formulasString += "; P=? [ F (s=6) & (X \"done\")]"; //todo without () + formulasString += "; P=? [ (F s=6) & (X \"done\")]"; storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/die.pm"); auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); @@ -744,20 +746,27 @@ namespace { EXPECT_NEAR(1/6, result->asQuantitativeCheckResult().getMin(), 1e-6); result = checker.check(tasks[2]); - EXPECT_NEAR(1/8, result->asQuantitativeCheckResult().getMin(), 1e-6); + EXPECT_NEAR(1/24, result->asQuantitativeCheckResult().getMin(), 1e-6); result = checker.check(tasks[3]); - EXPECT_NEAR(1/24, result->asQuantitativeCheckResult().getMin(), 1e-6); + EXPECT_NEAR(1/6, result->asQuantitativeCheckResult().getMin(), 1e-6); result = checker.check(tasks[4]); + EXPECT_NEAR(0, result->asQuantitativeCheckResult().getMin(), 1e-6); + + result = checker.check(tasks[5]); EXPECT_NEAR(1/2, result->asQuantitativeCheckResult().getMin(), 1e-6); + + result = checker.check(tasks[6]); + EXPECT_NEAR(0, result->asQuantitativeCheckResult().getMin(), 1e-6); } TEST(DtmcPrctlModelCheckerTest, LtlProbabilitiesSynchronousLeader) { setenv("LTL2DA", "ltl2da-ltl2tgba", true); std::string formulasString = "P=? [X (u1=true U \"elected\")]"; - formulasString += "; P=? [X v1=2 & (X v1=1)]"; // (X v1=2 & (XX v1=1) + formulasString += "; P=? [X v1=2 & (X v1=1)]"; // (X v1=2 & (XX v1=1)) formulasString += "; P=? [(X v1=2) & (X v1=1)]"; + //todo (X v1=2 & XX v1=1) storm::prism::Program program = storm::api::parseProgram(STORM_TEST_RESOURCES_DIR "/dtmc/leader-3-5.pm"); auto formulas = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasString, program)); @@ -777,6 +786,10 @@ namespace { result = checker.check(tasks[2]); EXPECT_NEAR(0, result->asQuantitativeCheckResult().getMin(), 1e-6); + + // (X v1=2 & XX v1=1) + //result = checker.check(tasks[3]); + //EXPECT_NEAR(1/25, result->asQuantitativeCheckResult().getMin(), 1e-6); } }