diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield index ac02291df..3014f95c4 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield @@ -1,8 +1,11 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.800000): model state: choice(s) [: ()}: + 0 0.8: (0) 1 0.9375: (0); 0.925: (1); 0.9125: (2) + 2 0.9625: (0); 0.97: (1); 0.9775: (2) 3 0.875: (0); 0.85: (1); 0.825: (2) 4 1: (0); 1: (1); 1: (2) - 5 1: (0); 0.82: (1) + 5 1: (0); 1: (1); 1: (2) + 6 0.925: (0); 0.91: (1); 0.895: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield index 2834984eb..6b32fa01a 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield @@ -1,7 +1,6 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.800000): model state: choice(s) [: ()}: - 0 0.33: (0); 0.366: (1); 0.402: (2) - 2 0.2025: (0); 0.243: (1); 0.2835: (2) + 0 0.58: (0); 0.566: (1); 0.552: (2) 3 0.755: (0); 0.706: (1); 0.657: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield index 8924f65da..7d91ac6f8 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield @@ -1,10 +1,11 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.800000): model state: choice(s) [: ()}: - 0 0.725: (0); 0.73: (1); 0.735: (2) + 0 0.8: (0); 0.79: (1); 0.78: (2) 1 0.9375: (0); 0.925: (1); 0.9125: (2) - 2 0.6: (1); 0.7: (2) + 2 0.9625: (0); 0.97: (1); 0.9775: (2) 3 0.875: (0); 0.85: (1); 0.825: (2) 4 1: (0); 1: (1); 1: (2) - 5 1: (0); 0.82: (1) + 5 1: (0); 1: (1); 1: (2) + 6 0.925: (0); 0.91: (1); 0.895: (2) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield index 5e126c2fc..dcd83f02c 100644 --- a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield @@ -1,6 +1,4 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.800000): model state: choice(s) [: ()}: - 2 0.2025: (0) - 5 0.49: (1); 0.405: (2) ___________________________________________________________________ diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp index a9e41a304..7fda8f70c 100644 --- a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -113,9 +113,9 @@ namespace { auto mdp = std::move(modelFormulas.first); auto tasks = this->getTasks(modelFormulas.second); EXPECT_EQ(13ul, mdp->getNumberOfStates()); - EXPECT_EQ(43ul, mdp->getNumberOfTransitions()); + EXPECT_EQ(48ul, mdp->getNumberOfTransitions()); ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp); - EXPECT_EQ(25ull, mdp->getNumberOfChoices()); + EXPECT_EQ(27ul, mdp->getNumberOfChoices()); storm::modelchecker::SparseMdpPrctlModelChecker> checker(*mdp);