From 50cf8d8e7f3399d5575e9b303deef45a0c59d00a Mon Sep 17 00:00:00 2001 From: Stefan Pranger Date: Wed, 3 Nov 2021 13:40:55 +0100 Subject: [PATCH] updated smg shield tests --- .../rightDecisionPostSafetyGamma05PminF5.shield | 3 +-- .../rightDecisionPostSafetyGamma09PminF3.shield | 6 ++++-- .../rightDecisionPostSafetyLambda05PminF5.shield | 9 +++++---- .../rightDecisionPostSafetyLambda09PminF3.shield | 9 +++++---- .../rightDecisionPreSafetyGamma05PminF5.shield | 3 +-- .../rightDecisionPreSafetyGamma09PminF3.shield | 6 ++++-- .../rightDecisionPreSafetyLambda05PminF5.shield | 9 +++++---- .../rightDecisionPreSafetyLambda09PminF3.shield | 9 +++++---- .../ShieldGenerationSmgRpatlModelCheckerTest.cpp | 16 ++++++++-------- 9 files changed, 38 insertions(+), 32 deletions(-) diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield index c5e6ddce1..7e07d7004 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield @@ -1,6 +1,5 @@ ___________________________________________________________________ Post-Safety-Shield with absolute comparison (gamma = 0.500000): model state: correction [: ()}: - 4 0: 0 - 5 0: 0 + 7 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield index dbdb1771a..f5c8bef12 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield @@ -1,6 +1,8 @@ ___________________________________________________________________ Post-Safety-Shield with absolute comparison (gamma = 0.900000): model state: correction [: ()}: - 4 0: 0 - 5 0: 0 + 1 0: 0; 1: 0 + 2 0: 0 + 7 0: 0 + 10 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield index 6385fca02..4cfcbf587 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Post-Safety-Shield with relative comparison (lambda = 0.500000): model state: correction [: ()}: - 0 0: 0; 1: 1 - 4 0: 0 - 5 0: 0 - 9 0: 0; 1: 1 + 1 0: 0; 1: 1 + 2 0: 0 + 7 0: 0 + 8 0: 0 + 10 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield index 24a913b11..2431c28d3 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Post-Safety-Shield with relative comparison (lambda = 0.900000): model state: correction [: ()}: - 0 0: 0; 1: 1 - 4 0: 0 - 5 0: 0 - 9 0: 0; 1: 1 + 1 0: 0; 1: 1 + 2 0: 0 + 7 0: 0 + 8 0: 0 + 10 0: 0 ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield index 854110128..54eba5a4f 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield @@ -1,6 +1,5 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.500000): model state: choice(s) [: ()}: - 4 0: (0) - 5 0: (0) + 7 0: (0) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield index 5afcb6598..b2ef15a42 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield @@ -1,6 +1,8 @@ ___________________________________________________________________ Pre-Safety-Shield with absolute comparison (gamma = 0.900000): model state: choice(s) [: ()}: - 4 0: (0) - 5 0: (0) + 1 0.9: (0) + 2 0: (0) + 7 0: (0) + 10 0.9: (0) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield index 363275926..b841e7bbe 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.500000): model state: choice(s) [: ()}: - 0 0: (1) - 4 0: (0) - 5 0: (0) - 9 0: (1) + 1 0.9: (0); 1: (1) + 2 1: (0) + 7 0: (0) + 8 1: (0) + 10 0.9: (0) ___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield index eb3d29cd3..56a2a010c 100644 --- a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield @@ -1,8 +1,9 @@ ___________________________________________________________________ Pre-Safety-Shield with relative comparison (lambda = 0.900000): model state: choice(s) [: ()}: - 0 0: (1) - 4 0: (0) - 5 0: (0) - 9 0: (1) + 1 0.9: (0); 1: (1) + 2 0: (0) + 7 0: (0) + 8 1: (0) + 10 0.9: (0) ___________________________________________________________________ diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp index b0f26f02b..096766c29 100644 --- a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -108,22 +108,22 @@ namespace { // testing create shielding expressions std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[2] + ", PreSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[6] + ", PostSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; - formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; formulasString += "; <" + fileNames[8] + ", PreSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; formulasString += "; <" + fileNames[10] + ", PreSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; formulasString += "; <" + fileNames[12] + ", PostSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; formulasString += "; <" + fileNames[14] + ", PostSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; - formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString); auto smg = std::move(modelFormulas.first);