Browse Source

Merge pull request 'Introducing Unit Tests for SMG Extensions' (#46) from smg_unit_tests into main

Reviewed-on: https://git.pranger.xyz/TEMPEST/tempest-devel/pulls/46

```
...
100% tests passed, 0 tests failed out of 31

Total Test time (real) = 1144.27 sec

```
tempestpy_adaptions
Stefan Pranger 3 years ago
parent
commit
eb15fccfd2
  1. 1
      resources/examples/testfiles/rpatl/probabilisticFormula.rpatl
  2. 5
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield
  3. 8
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield
  4. 8
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield
  5. 8
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield
  6. 11
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield
  7. 6
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield
  8. 11
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield
  9. 4
      resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield
  10. 7
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield
  11. 6
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield
  12. 7
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield
  13. 6
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield
  14. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield
  15. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield
  16. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield
  17. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield
  18. 7
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield
  19. 6
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield
  20. 7
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield
  21. 6
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield
  22. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield
  23. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield
  24. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield
  25. 8
      resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield
  26. 52
      resources/examples/testfiles/smg/messageHack.nm
  27. 42
      resources/examples/testfiles/smg/rightDecision.nm
  28. 61
      resources/examples/testfiles/smg/robotCircle.nm
  29. 29
      resources/examples/testfiles/smg/walker.nm
  30. 127
      src/storm-parsers/parser/FormulaParserGrammar.cpp
  31. 11
      src/storm-parsers/parser/FormulaParserGrammar.h
  32. 13
      src/storm/generator/PrismNextStateGenerator.cpp
  33. 5
      src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp
  34. 4
      src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp
  35. 27
      src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp
  36. 67
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp
  37. 14
      src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h
  38. 9
      src/storm/solver/Multiplier.cpp
  39. 1
      src/storm/storage/PostScheduler.cpp
  40. 81
      src/storm/storage/Scheduler.cpp
  41. 7
      src/storm/storage/SparseMatrix.cpp
  42. 8
      src/test/storm/CMakeLists.txt
  43. 43
      src/test/storm/logic/FragmentCheckerTest.cpp
  44. 198
      src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp
  45. 280
      src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp
  46. 351
      src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp
  47. 204
      src/test/storm/parser/GameFormulaParserTest.cpp
  48. 81
      src/test/storm/parser/GameShieldingParserTest.cpp
  49. 72
      src/test/storm/parser/MdpShieldingParserTest.cpp
  50. 38
      src/test/storm/parser/PrismParserTest.cpp

1
resources/examples/testfiles/rpatl/probabilisticFormula.rpatl

@ -0,0 +1 @@
<<player>> Pmax=? [ F "goal" ]

5
resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield

@ -0,0 +1,5 @@
___________________________________________________________________
Post-Safety-Shield with absolute comparison (gamma = 0.700000):
model state: correction [<action>: (<corrected action>)}:
4 0: 2; 1: 2; 2: 2
___________________________________________________________________

8
resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with absolute comparison (gamma = 0.700000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 1; 2: 2
1 0: 0; 1: 1; 2: 2
3 0: 0; 1: 1; 2: 2
4 0: 0; 1: 1; 2: 2
___________________________________________________________________

8
resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with relative comparison (lambda = 0.700000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 1; 2: 2
1 0: 0; 1: 1; 2: 2
3 0: 0; 1: 1; 2: 2
4 0: 0; 1: 1; 2: 2
___________________________________________________________________

8
resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with relative comparison (lambda = 0.700000):
model state: correction [<action>: (<corrected action>)}:
0 0: 2; 1: 2; 2: 2
1 0: 0; 1: 0; 2: 0
3 0: 2; 1: 2; 2: 2
4 0: 2; 1: 2; 2: 2
___________________________________________________________________

11
resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield

@ -0,0 +1,11 @@
___________________________________________________________________
Pre-Safety-Shield with absolute comparison (gamma = 0.800000):
model state: choice(s) [<value>: (<action>)}:
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); 1: (1); 1: (2)
6 0.925: (0); 0.91: (1); 0.895: (2)
___________________________________________________________________

6
resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield

@ -0,0 +1,6 @@
___________________________________________________________________
Pre-Safety-Shield with absolute comparison (gamma = 0.800000):
model state: choice(s) [<value>: (<action>)}:
0 0.58: (0); 0.566: (1); 0.552: (2)
3 0.755: (0); 0.706: (1); 0.657: (2)
___________________________________________________________________

11
resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield

@ -0,0 +1,11 @@
___________________________________________________________________
Pre-Safety-Shield with relative comparison (lambda = 0.800000):
model state: choice(s) [<value>: (<action>)}:
0 0.8: (0); 0.79: (1); 0.78: (2)
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); 1: (1); 1: (2)
6 0.925: (0); 0.91: (1); 0.895: (2)
___________________________________________________________________

4
resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield

@ -0,0 +1,4 @@
___________________________________________________________________
Pre-Safety-Shield with relative comparison (lambda = 0.800000):
model state: choice(s) [<value>: (<action>)}:
___________________________________________________________________

7
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield

@ -0,0 +1,7 @@
___________________________________________________________________
Post-Safety-Shield with absolute comparison (gamma = 0.500000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 1
5 0: 0
9 0: 0; 1: 1
___________________________________________________________________

6
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield

@ -0,0 +1,6 @@
___________________________________________________________________
Post-Safety-Shield with absolute comparison (gamma = 0.500000):
model state: correction [<action>: (<corrected action>)}:
4 0: 0
5 0: 0
___________________________________________________________________

7
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield

@ -0,0 +1,7 @@
___________________________________________________________________
Post-Safety-Shield with absolute comparison (gamma = 0.900000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 0
5 0: 0
9 0: 0; 1: 0
___________________________________________________________________

6
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield

@ -0,0 +1,6 @@
___________________________________________________________________
Post-Safety-Shield with absolute comparison (gamma = 0.900000):
model state: correction [<action>: (<corrected action>)}:
4 0: 0
5 0: 0
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with relative comparison (lambda = 0.500000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 1
4 0: 0
5 0: 0
9 0: 0; 1: 1
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with relative comparison (lambda = 0.500000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 1
4 0: 0
5 0: 0
9 0: 0; 1: 1
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with relative comparison (lambda = 0.900000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 0
4 0: 0
5 0: 0
9 0: 0; 1: 0
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Post-Safety-Shield with relative comparison (lambda = 0.900000):
model state: correction [<action>: (<corrected action>)}:
0 0: 0; 1: 1
4 0: 0
5 0: 0
9 0: 0; 1: 1
___________________________________________________________________

7
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield

@ -0,0 +1,7 @@
___________________________________________________________________
Pre-Safety-Shield with absolute comparison (gamma = 0.500000):
model state: choice(s) [<value>: (<action>)}:
0 0.9: (0); 1: (1)
5 1: (0)
9 1: (0); 0.9: (1)
___________________________________________________________________

6
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield

@ -0,0 +1,6 @@
___________________________________________________________________
Pre-Safety-Shield with absolute comparison (gamma = 0.500000):
model state: choice(s) [<value>: (<action>)}:
4 0: (0)
5 0: (0)
___________________________________________________________________

7
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield

@ -0,0 +1,7 @@
___________________________________________________________________
Pre-Safety-Shield with absolute comparison (gamma = 0.900000):
model state: choice(s) [<value>: (<action>)}:
0 0.9: (0)
5 1: (0)
9 1: (0)
___________________________________________________________________

6
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield

@ -0,0 +1,6 @@
___________________________________________________________________
Pre-Safety-Shield with absolute comparison (gamma = 0.900000):
model state: choice(s) [<value>: (<action>)}:
4 0: (0)
5 0: (0)
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Pre-Safety-Shield with relative comparison (lambda = 0.500000):
model state: choice(s) [<value>: (<action>)}:
0 0.9: (0); 1: (1)
4 0: (0)
5 1: (0)
9 1: (0); 0.9: (1)
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Pre-Safety-Shield with relative comparison (lambda = 0.500000):
model state: choice(s) [<value>: (<action>)}:
0 0: (1)
4 0: (0)
5 0: (0)
9 0: (1)
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Pre-Safety-Shield with relative comparison (lambda = 0.900000):
model state: choice(s) [<value>: (<action>)}:
0 0.9: (0)
4 0: (0)
5 1: (0)
9 1: (0)
___________________________________________________________________

8
resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield

@ -0,0 +1,8 @@
___________________________________________________________________
Pre-Safety-Shield with relative comparison (lambda = 0.900000):
model state: choice(s) [<value>: (<action>)}:
0 0: (1)
4 0: (0)
5 0: (0)
9 0: (1)
___________________________________________________________________

52
resources/examples/testfiles/smg/messageHack.nm

@ -0,0 +1,52 @@
// PRISM Model of hacking a communication
// - Bob and Alice are chatting.
// - Eve wants to hack the messages from Bob.
// - The propability of successfull hacking is 0.05.
smg
player bob
[receiveB], [readWriteB], [sendB], [waitB]
endplayer
player alice
[receiveA], [readWriteA], [sendA], [waitA]
endplayer
player eve
[hackE], [waitE]
endplayer
// 0 bob, 1 eve, 2 alice
global move : [0..2] init 0;
//
global bobSent : [0..1] init 0;
global hacked : [0..1] init 0;
label "hacked" = hacked=1;
module communication
bobReceived : [0..1] init 0;
bobWroteMessage : [0..1] init 1;
aliceReceived : [0..1] init 0;
aliceWroteMessage : [0..1] init 0;
aliceSent : [0..1] init 0;
// bob's communication part
[receiveB] move=0 & aliceSent=1 -> (bobReceived'=1) & (aliceSent'=0) & (move'=1);
[readWriteB] move=0 & bobReceived=1 -> (bobWroteMessage'=1) & (bobReceived'=0) & (move'=1);
[sendB] move=0 & bobWroteMessage=1 -> (bobSent'=1) & (bobWroteMessage'=0) & (move'=1);
[waitB] move=0 & !(aliceSent=1 | bobReceived=1 | bobWroteMessage=1) -> (move'=1);
// alice's communication part
[receiveA] move=2 & bobSent=1 -> (aliceReceived'=1) & (bobSent'=0) & (move'=0);
[readWriteA] move=2 & aliceReceived=1 -> (aliceWroteMessage'=1) & (aliceReceived'=0) & (move'=0);
[sendA] move=2 & aliceWroteMessage=1 -> (aliceSent'=1) & (aliceWroteMessage'=0) & (move'=0);
[waitA] move=2 & !(bobSent=1 | aliceReceived=1 | aliceWroteMessage=1) -> (move'=0);
endmodule
module hacking
[hackE] move=1 & bobSent=1 -> 0.05: (hacked'=1) & (move'=2) + 0.95: (move'=2);
[waitE] move=1 & !(bobSent=1) -> (move'=2);
endmodule

42
resources/examples/testfiles/smg/rightDecision.nm

@ -0,0 +1,42 @@
// PRISM Model of a decision for a shortcut
// - A hiker has to make a decision of taking a shortcut.
// - On the shortcut a native can be asked for getting to the target waypoint.
// - The native can lead the hiker to the goal or can give a proposal for getting to 0.9 to the target.
smg
player hiker
[startShortcut], [startWay], [waypoint1], [waypoint2target], [waypoint2start], [target], [lost]
endplayer
player native
[wait], [shortcutBad], [shortcutGood]
endplayer
// 0 bob, 1 native,
global move : [0..1] init 0;
global shortcut : [0..1] init 0;
global target : [0..1] init 0;
global lost : [0..1] init 0;
label "target" = target=1;
module hikerModule
startpoint : [0..1] init 1;
waypoints : [0..2] init 0;
[startShortcut] move=0 & startpoint=1 -> (shortcut'=1) & (startpoint'=0) & (move'=1);
[startWay] move=0 & startpoint=1 -> (waypoints'=1) & (startpoint'=0) & (move'=1);
[waypoint1] move=0 & waypoints=1 -> (waypoints'=2) & (move'=1);
[waypoint2target] move=0 & waypoints=2 -> (waypoints'=0) & (target'=1) & (move'=1);
[waypoint2start] move=0 & waypoints=2 -> (waypoints'=0) & (startpoint'=1) & (move'=1);
[target] move=0 & target=1 -> (move'=1);
[lost] move=0 & lost=1 -> (move'=1);
endmodule
module nativeModule
[wait] move=1 & !(shortcut=1) -> (move'=0);
[shortcutBad] move=1 & shortcut=1 -> 0.9: (shortcut'=0) & (target'=1) & (move'=0) + 0.1: (shortcut'=0) & (lost'=1) & (move'=0);
[shortcutGood] move=1 & shortcut=1 -> (shortcut'=0) & (target'=1) & (move'=0);
endmodule

61
resources/examples/testfiles/smg/robotCircle.nm

@ -0,0 +1,61 @@
// PRISM Model of a simple robot game
// - A player - friendlyRobot - moves around and tries not to "crash" with another player - adversary Robot.
// - friendlyRobot can choose the direction of movement.
// - adversaryRobot should move in a circle counterclockwise on the grid, but has a probabilty to fail and move into the wrong direction.
// - The movement of adversaryRobot is defined as a pseudo random movement with probabilty = 1/4 into one of the 4 possible directions.
smg
player friendlyRobot
[e1], [w1], [n1], [s1]
endplayer
player adversaryRobot
[e2], [w2], [n2], [s2], [middle]
endplayer
// 3x3 grid
const int width = 2;
const int height = 2;
const int xmin = 0;
const int xmax = width;
const int ymin = 0;
const int ymax = height;
// probabilty to fail
const double failProb = 1/10;
const double notFailProb = 1-failProb;
// definition of randomProb, this has to be 0.25 since it is the prob of go into one direction from the middle for the adverseryRobot
const double randomProb = 1/4;
global move : [0..1] init 0;
//F__
//___
//__R
label "crash" = x1=x2 & y1=y2;
module robot1
x1 : [0..width] init 0;
y1 : [0..height] init 0;
[e1] move=0 & x1<xmax -> (x1'=x1+1) & (move'=1);
[w1] move=0 & x1>0 -> (x1'=x1-1) & (move'=1);
[n1] move=0 & y1>0 -> (y1'=y1-1) & (move'=1);
[s1] move=0 & y1<ymax -> (y1'=y1+1) & (move'=1);
endmodule
module robot2
x2 : [0..width] init width;
y2 : [0..height] init height;
[e2] move=1 & x2<xmax & y2=ymax -> notFailProb : (x2'=x2+1) & (move'=0) + failProb : (y2'=y2-1) & (move'=0);
[w2] move=1 & x2>0 & y2=0 -> notFailProb : (x2'=x2-1) & (move'=0) + failProb : (y2'=y2+1) & (move'=0);
[n2] move=1 & x2=xmax & y2>0 -> notFailProb : (y2'=y2-1) & (move'=0) + failProb : (x2'=x2-1) & (move'=0);
[s2] move=1 & x2=0 & y2<ymax -> notFailProb : (y2'=y2+1) & (move'=0) + failProb : (x2'=x2+1) & (move'=0);
[middle] move=1 & x2=1 & y2=1 -> randomProb : (x2'=x2+1) & (move'=0) + randomProb : (x2'=x2-1) & (move'=0) + randomProb : (y2'=y2-1) & (move'=0) + randomProb : (y2'=y2+1) & (move'=0);
endmodule

29
resources/examples/testfiles/smg/walker.nm

@ -0,0 +1,29 @@
smg
player walker
[a0], [a00], [a1], [a2], [a3]
endplayer
player blocker
[a40], [a41]
endplayer
label "s0" = c=0 & b=0 & a=0;
label "s1" = c=0 & b=0 & a=1;
label "s2" = c=0 & b=1 & a=0;
label "s3" = c=0 & b=1 & a=1;
label "s4" = c=1 & b=0 & a=0;
module transitions
a : [0..1] init 0;
b : [0..1] init 0;
c : [0..1] init 0;
[a0] a=0 & b=0 & c=0 -> 4/10 : (a'=1) + 6/10 : (b'=1);
[a00] a=0 & b=0 & c=0 -> true;
[a1] a=1 & b=0 & c=0 -> 3/10 : (a'=0) + 3/10 : (a'=0) & (b'=1) + 4/10 : (b'=1);
[a2] a=0 & b=1 & c=0 -> 2/10 : (a'=1) + 8/10 : (b'=0) & (c'=1);
[a3] a=1 & b=1 & c=0 -> true;
[a40] a=0 & b=0 & c=1 -> 3/10 : (c'=0) + 7/10 : (a'=1) & (b'=1) & (c'=0);
[a41] a=0 & b=0 & c=1 -> true;
endmodule

127
src/storm-parsers/parser/FormulaParserGrammar.cpp

@ -179,11 +179,29 @@ namespace storm {
constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)];
constantDefinition.name("constant definition");
// Shielding properties
shieldExpression = (qi::lit("<") > label > qi::lit(",") > shieldingType > -(qi::lit(",") > shieldComparison) > qi::lit(">"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)];
shieldExpression.name("shield expression");
shieldingType = (qi::lit("PreSafety")[qi::_val = storm::logic::ShieldingType::PreSafety] |
qi::lit("PostSafety")[qi::_val = storm::logic::ShieldingType::PostSafety] |
qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield");
shieldingType.name("shielding type");
probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ];
probability.name("double between 0 and 1");
shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] |
qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)];
shieldComparison.name("shield comparison type");
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > topLevelFormula > qi::lit(",") > formula(FormulaKind::State, storm::logic::FormulaContext::Undefined)> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] |
(-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
(-formulaName >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] |
(-formulaName >> shieldExpression >> topLevelFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)];
filterProperty.name("filter property");
#pragma clang diagnostic pop
@ -195,45 +213,45 @@ namespace storm {
start.name("start");
// Enable the following lines to print debug output for most the rules.
// debug(rewardModelName)
// debug(rewardMeasureType)
// debug(operatorFormula)
// debug(labelFormula)
// debug(expressionFormula)
// debug(booleanLiteralFormula)
// debug(atomicPropositionFormula)
// debug(basicPropositionalFormula)
// debug(negationPropositionalFormula)
// debug(andLevelPropositionalFormula)
// debug(orLevelPropositionalFormula)
// debug(propositionalFormula)
// debug(timeBoundReference)
// debug(timeBound)
// debug(timeBounds)
// debug(eventuallyFormula)
// debug(nextFormula)
// debug(globallyFormula)
// debug(hoaPathFormula)
// debug(multiBoundedPathFormula)
// debug(prefixOperatorPathFormula)
// debug(basicPathFormula)
// debug(untilLevelPathFormula)
// debug(pathFormula)
// debug(longRunAverageRewardFormula)
// debug(instantaneousRewardFormula)
// debug(cumulativeRewardFormula)
// debug(totalRewardFormula)
// debug(playerCoalition)
// debug(gameFormula)
// debug(multiOperatorFormula)
// debug(quantileBoundVariable)
// debug(quantileFormula)
// debug(formula)
// debug(topLevelFormula)
// debug(formulaName)
// debug(filterProperty)
// debug(constantDefinition )
// debug(start)
//debug(rewardModelName);
//debug(rewardMeasureType);
//debug(operatorFormula);
//debug(labelFormula);
//debug(expressionFormula);
//debug(booleanLiteralFormula);
//debug(atomicPropositionFormula);
//debug(basicPropositionalFormula);
//debug(negationPropositionalFormula);
//debug(andLevelPropositionalFormula);
//debug(orLevelPropositionalFormula);
//debug(propositionalFormula);
//debug(timeBoundReference);
//debug(timeBound);
//debug(timeBounds);
//debug(eventuallyFormula);
//debug(nextFormula);
//debug(globallyFormula);
//debug(hoaPathFormula);
//debug(multiBoundedPathFormula);
//debug(prefixOperatorPathFormula);
//debug(basicPathFormula);
//debug(untilLevelPathFormula);
//debug(pathFormula);
//debug(longRunAverageRewardFormula);
//debug(instantaneousRewardFormula);
//debug(cumulativeRewardFormula);
//debug(totalRewardFormula);
////debug(playerCoalition);
//debug(gameFormula);
//debug(multiOperatorFormula);
//debug(quantileBoundVariable);
//debug(quantileFormula);
//debug(formula);
//debug(topLevelFormula);
//debug(formulaName);
//debug(filterProperty);
////debug(constantDefinition);
//debug(start);
// Enable error reporting.
qi::on_error<qi::fail>(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@ -386,6 +404,11 @@ namespace storm {
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
}
/*
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
if (timeBounds && !timeBounds.get().empty()) {
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
@ -401,6 +424,7 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
}
}
*/
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));
@ -619,6 +643,29 @@ namespace storm {
}
}
std::pair<storm::logic::ShieldComparison, double> FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) {
return std::make_pair(comparisonType, value);
}
std::shared_ptr<storm::logic::ShieldExpression const> FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional<std::pair<storm::logic::ShieldComparison, double>> comparisonStruct) {
if(comparisonStruct.is_initialized()) {
STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored.");
return std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second));
} else {
STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)");
return std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(type, name));
}
}
storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldExpression) {
++propertyCount;
if (propertyName) {
return storm::jani::Property(propertyName.get(), formula, this->getUndefinedConstants(formula), shieldExpression);
} else {
return storm::jani::Property(std::to_string(propertyCount), formula, this->getUndefinedConstants(formula), shieldExpression);
}
}
storm::logic::PlayerCoalition FormulaParserGrammar::createPlayerCoalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const {
return storm::logic::PlayerCoalition(playerIds);
}

11
src/storm-parsers/parser/FormulaParserGrammar.h

@ -234,6 +234,12 @@ namespace storm {
};
qi::rule<Iterator, qi::unused_type(), qi::locals<ConstantDataType>, Skipper> constantDefinition;
// Shielding properties
qi::rule<Iterator, std::shared_ptr<storm::logic::ShieldExpression const>(), Skipper> shieldExpression;
qi::rule<Iterator, storm::logic::ShieldingType, Skipper> shieldingType;
qi::rule<Iterator, double, Skipper> probability;
qi::rule<Iterator, std::pair<storm::logic::ShieldComparison, double>, qi::locals<storm::logic::ShieldComparison>, Skipper> shieldComparison;
// Start symbol
qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start;
@ -242,6 +248,9 @@ namespace storm {
storm::logic::PlayerCoalition createPlayerCoalition(std::vector<boost::variant<std::string, storm::storage::PlayerIndex>> const& playerIds) const;
std::shared_ptr<storm::logic::Formula const> createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::pair<storm::logic::ShieldComparison, double> createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value);
std::shared_ptr<storm::logic::ShieldExpression const> createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional<std::pair<storm::logic::ShieldComparison, double>> comparisonStruct);
bool areConstantDefinitionsAllowed() const;
void addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression);
void addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula);
@ -259,6 +268,7 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createBooleanLiteralFormula(bool literal) const;
std::shared_ptr<storm::logic::Formula const> createAtomicLabelFormula(std::string const& label) const;
std::shared_ptr<storm::logic::Formula const> createEventuallyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
//std::shared_ptr<storm::logic::Formula const> createGloballyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const;
std::shared_ptr<storm::logic::Formula const> createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& rightSubformula);
@ -285,6 +295,7 @@ namespace storm {
std::set<storm::expressions::Variable> getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const;
storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);
storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
storm::jani::Property createShieldingProperty(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::ShieldExpression const> const& shieldingExpression);
bool isBooleanReturnType(std::shared_ptr<storm::logic::Formula const> const& formula, bool raiseErrorMessage = false);
bool raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& op);

13
src/storm/generator/PrismNextStateGenerator.cpp

@ -548,7 +548,6 @@ namespace storm {
// Iterate over all commands.
for (uint_fast64_t j = 0; j < module.getNumberOfCommands(); ++j) {
storm::prism::Command const& command = module.getCommand(j);
// Only consider commands that are not possibly synchronizing.
if (isCommandPotentiallySynchronizing(command)) continue;
@ -615,9 +614,15 @@ namespace storm {
}
if (program.getModelType() == storm::prism::Program::ModelType::SMG) {
storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i);
STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command.");
choice.setPlayerIndex(playerOfModule);
if(command.getActionName() != "") {
storm::storage::PlayerIndex const& playerOfAction = actionIndexToPlayerIndexMap.at(command.getActionIndex());
STORM_LOG_THROW(playerOfAction != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Command " << command.getActionName() << " is not owned by any player.");
choice.setPlayerIndex(playerOfAction);
} else {
storm::storage::PlayerIndex const& playerOfModule = moduleIndexToPlayerIndexMap.at(i);
STORM_LOG_THROW(playerOfModule != storm::storage::INVALID_PLAYER_INDEX, storm::exceptions::WrongFormatException, "Module " << module.getName() << " is not owned by any player but has at least one enabled, unlabeled command.");
choice.setPlayerIndex(playerOfModule);
}
}
if (this->options.isExplorationChecksSet()) {

5
src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp

@ -20,10 +20,11 @@ namespace storm {
template<typename ValueType>
void SparseNondeterministicStepBoundedHorizonHelper<ValueType>::getMaybeStatesRowGroupSizes(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& maybeStates, std::vector<uint64_t>& maybeStatesRowGroupSizes, uint& choiceValuesCounter) {
std::vector<uint64_t> rowGroupIndices = transitionMatrix.getRowGroupIndices();
choiceValuesCounter = 0;
for(uint counter = 0; counter < maybeStates.size(); counter++) {
if(maybeStates.get(counter)) {
maybeStatesRowGroupSizes.push_back(rowGroupIndices.at(counter));
choiceValuesCounter += transitionMatrix.getRowGroupSize(counter);
maybeStatesRowGroupSizes.push_back(choiceValuesCounter);
}
}
}
@ -87,7 +88,7 @@ namespace storm {
std::vector<uint64_t> rowGroupIndices = transitionMatrix.getRowGroupIndices();
std::vector<uint64_t> maybeStatesRowGroupSizes;
uint choiceValuesCounter;
uint choiceValuesCounter = 0;
getMaybeStatesRowGroupSizes(transitionMatrix, maybeStates, maybeStatesRowGroupSizes, choiceValuesCounter);
choiceValues = std::vector<ValueType>(choiceValuesCounter, storm::utility::zero<ValueType>());

4
src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp

@ -63,7 +63,7 @@ namespace storm {
storm::logic::Formula const& subFormula = gameFormula.getSubformula();
statesOfCoalition = this->getModel().computeStatesOfCoalition(gameFormula.getCoalition());
std::cout << "Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition." << std::endl;
STORM_LOG_INFO("Found " << statesOfCoalition.getNumberOfSetBits() << " states in coalition.");
statesOfCoalition.complement();
if (subFormula.isRewardOperatorFormula()) {
@ -216,7 +216,7 @@ namespace storm {
auto ret = storm::modelchecker::helper::SparseSmgRpatlHelper<ValueType>::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound<uint64_t>(), pathFormula.getNonStrictUpperBound<uint64_t>());
std::unique_ptr<CheckResult> result(new ExplicitQuantitativeCheckResult<ValueType>(std::move(ret.values)));
if(checkTask.isShieldingTask()) {
tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition);
tempest::shields::createShield<ValueType>(std::make_shared<storm::models::sparse::Smg<ValueType>>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition);
}
return result;
}

27
src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp

@ -1,4 +1,5 @@
#include <utility/graph.h>
#include <environment/solver/GameSolverEnvironment.h>
#include "SparseSmgRpatlHelper.h"
#include "storm/environment/Environment.h"
@ -15,7 +16,6 @@ namespace storm {
template<typename ValueType>
SMGSparseModelCheckingHelperReturnType<ValueType> SparseSmgRpatlHelper<ValueType>::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::storage::BitVector statesOfCoalition, bool produceScheduler, ModelCheckerHint const& hint) {
// TODO add Kwiatkowska original reference
auto solverEnv = env;
solverEnv.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration, false);
@ -40,7 +40,7 @@ namespace storm {
if (produceScheduler) {
viHelper.setProduceScheduler(true);
}
viHelper.performValueIteration(env, x, b, goal.direction());
viHelper.performValueIteration(env, x, b, goal.direction(), constrainedChoiceValues);
if(goal.isShieldingTask()) {
viHelper.getChoiceValues(env, x, constrainedChoiceValues);
}
@ -52,6 +52,7 @@ namespace storm {
scheduler = std::make_unique<storm::storage::Scheduler<ValueType>>(expandScheduler(viHelper.extractScheduler(), psiStates, ~phiStates));
}
}
// Fill up the result vector with the values of x for the relevant states, with 1s for psi states (0 is default)
storm::utility::vector::setVectorValues(result, relevantStates, x);
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
@ -109,7 +110,9 @@ namespace storm {
}
// Create a multiplier for reduction.
auto multiplier = storm::solver::MultiplierFactory<ValueType>().create(env, transitionMatrix);
multiplier->reduce(env, goal.direction(), b, transitionMatrix.getRowGroupIndices(), result, &statesOfCoalition);
auto rowGroupIndices = transitionMatrix.getRowGroupIndices();
rowGroupIndices.erase(rowGroupIndices.begin());
multiplier->reduce(env, goal.direction(), b, rowGroupIndices, result, &statesOfCoalition);
if (goal.isShieldingTask()) {
choiceValues = b;
}
@ -169,10 +172,12 @@ namespace storm {
}
// If the lowerBound = 0, value iteration is done until the upperBound.
if(lowerBound == 0) {
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound, constrainedChoiceValues);
solverEnv.solver().game().setMaximalNumberOfIterations(upperBound);
viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues);
} else {
// The lowerBound != 0, the first computation between the given bound steps is done.
viHelper.performValueIterationUpperBound(env, x, b, goal.direction(), upperBound - lowerBound, constrainedChoiceValues);
solverEnv.solver().game().setMaximalNumberOfIterations(upperBound - lowerBound);
viHelper.performValueIteration(solverEnv, x, b, goal.direction(), constrainedChoiceValues);
// Initialization of subResult, fill it with the result of the first computation and 1s for the psiStates in full range.
std::vector<ValueType> subResult = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
@ -189,14 +194,16 @@ namespace storm {
// Update the viHelper for the (full-size) submatrix and statesOfCoalition.
viHelper.updateTransitionMatrix(submatrix);
viHelper.updateStatesOfCoaltion(statesOfCoalition);
viHelper.updateStatesOfCoalition(statesOfCoalition);
// Reset constrainedChoiceValues and b to 0-vector in the correct dimension.
constrainedChoiceValues = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero<ValueType>());
b = std::vector<ValueType>(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero<ValueType>());
// The second computation is done between step 0 and the lowerBound
viHelper.performValueIterationUpperBound(env, subResult, b, goal.direction(), lowerBound, constrainedChoiceValues);
solverEnv.solver().game().setMaximalNumberOfIterations(lowerBound);
viHelper.performValueIteration(solverEnv, subResult, b, goal.direction(), constrainedChoiceValues);
x = subResult;
}
viHelper.fillChoiceValuesVector(constrainedChoiceValues, relevantStates, transitionMatrix.getRowGroupIndices());
@ -205,7 +212,11 @@ namespace storm {
}
storm::utility::vector::setVectorValues(result, relevantStates, x);
}
// In bounded-globally formulas we not only to reach a psiState on the path but also want to stay in a set of psiStates in the given step bounds.
// In bounded until and bounded eventually formula the psiStates have probability 1 to satisfy the formula,
// because once reaching a state where psi holds those formulas are satisfied.
// In bounded globally formulas we cannot set those states to 1 because it is possible to leave a set of safe states after reaching a psiState
// and in globally the formula has to hold in every time step (between the bounds).
// e.g. phiState -> phiState -> psiState -> unsafeState
if(!computeBoundedGlobally){
storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one<ValueType>());
}

67
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp

@ -25,13 +25,14 @@ namespace storm {
}
template <typename ValueType>
void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir) {
void GameViHelper<ValueType>::performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues) {
prepareSolversAndMultipliers(env);
// Get precision for convergence check.
ValueType precision = storm::utility::convertNumber<ValueType>(env.solver().game().getPrecision());
uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations();
_b = b;
_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
//_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
_x1 = x;
_x2 = _x1;
if (this->isProduceSchedulerSet()) {
@ -42,17 +43,25 @@ namespace storm {
}
uint64_t iter = 0;
std::vector<ValueType> result = x;
constrainedChoiceValues = std::vector<ValueType>(b.size(), storm::utility::zero<ValueType>());
while (iter < maxIter) {
++iter;
if(iter == maxIter - 1) {
_multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues);
auto rowGroupIndices = this->_transitionMatrix.getRowGroupIndices();
rowGroupIndices.erase(rowGroupIndices.begin());
_multiplier->reduce(env, dir, constrainedChoiceValues, rowGroupIndices, xNew());
break;
}
performIterationStep(env, dir);
if (checkConvergence(precision)) {
_multiplier->multiply(env, xNew(), &_b, constrainedChoiceValues);
break;
}
if (storm::utility::resources::isTerminate()) {
break;
}
++iter;
}
x = xNew();
@ -74,18 +83,11 @@ namespace storm {
} else {
_multiplier->multiplyAndReduce(env, dir, xOld(), &_b, xNew(), choices, &_statesOfCoalition);
}
// compare applyPointwise
storm::utility::vector::applyPointwise<ValueType, ValueType, ValueType>(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType {
if(a > b) return a;
else return b;
});
}
template <typename ValueType>
bool GameViHelper<ValueType>::checkConvergence(ValueType threshold) const {
STORM_LOG_ASSERT(_multiplier, "tried to check for convergence without doing an iteration first.");
// Now check whether the currently produced results are precise enough
STORM_LOG_ASSERT(threshold > storm::utility::zero<ValueType>(), "Did not expect a non-positive threshold.");
auto x1It = xOld().begin();
@ -113,43 +115,6 @@ namespace storm {
return true;
}
template <typename ValueType>
void GameViHelper<ValueType>::performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues) {
prepareSolversAndMultipliers(env);
_x = x;
_b = b;
if (this->isProduceSchedulerSet()) {
if (!this->_producedOptimalChoices.is_initialized()) {
this->_producedOptimalChoices.emplace();
}
this->_producedOptimalChoices->resize(this->_transitionMatrix.getRowGroupCount());
}
for (uint64_t iter = 0; iter < upperBound; iter++) {
if(iter == upperBound - 1) {
_multiplier->multiply(env, _x, &_b, constrainedChoiceValues);
}
performIterationStepUpperBound(env, dir);
}
x = _x;
}
template <typename ValueType>
void GameViHelper<ValueType>::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices) {
if (!_multiplier) {
prepareSolversAndMultipliers(env);
}
// multiplyandreducegaussseidel
// Ax = x'
if (choices == nullptr) {
_multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, nullptr, &_statesOfCoalition);
} else {
// Also keep track of the choices made.
_multiplier->multiplyAndReduce(env, dir, _x, &_b, _x, choices, &_statesOfCoalition);
}
}
template <typename ValueType>
void GameViHelper<ValueType>::setProduceScheduler(bool value) {
_produceScheduler = value;
@ -166,8 +131,8 @@ namespace storm {
}
template <typename ValueType>
void GameViHelper<ValueType>::updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion) {
_statesOfCoalition = newStatesOfCoaltion;
void GameViHelper<ValueType>::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) {
_statesOfCoalition = newStatesOfCoalition;
}
template <typename ValueType>

14
src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h

@ -26,12 +26,7 @@ namespace storm {
/*!
* Perform value iteration until convergence
*/
void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir);
/*!
* Perform value iteration until upper bound
*/
void performValueIterationUpperBound(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector<ValueType>& constrainedChoiceValues);
void performValueIteration(Environment const& env, std::vector<ValueType>& x, std::vector<ValueType> b, storm::solver::OptimizationDirection const dir, std::vector<ValueType>& constrainedChoiceValues);
/*!
* Sets whether an optimal scheduler shall be constructed during the computation
@ -51,7 +46,7 @@ namespace storm {
/*!
* Changes the statesOfCoalition to the given one.
*/
void updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion);
void updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition);
storm::storage::Scheduler<ValueType> extractScheduler() const;
@ -68,11 +63,6 @@ namespace storm {
*/
void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
/*!
* Performs one iteration step for value iteration with upper bound
*/
void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector<uint64_t>* choices = nullptr);
/*!
* Checks whether the curently computed value achieves the desired precision
*/

9
src/storm/solver/Multiplier.cpp

@ -92,8 +92,13 @@ namespace storm {
template<typename ValueType>
void Multiplier<ValueType>::reduce(Environment const& env, OptimizationDirection const& dir, std::vector<ValueType> const& choiceValues, std::vector<storm::storage::SparseMatrix<double>::index_type> rowGroupIndices, std::vector<ValueType>& result, storm::storage::BitVector const* dirOverride) const {
auto choice_it = choiceValues.begin();
for(uint state = 0; state < rowGroupIndices.size() - 1; state++) {
uint rowGroupSize = rowGroupIndices[state + 1] - rowGroupIndices[state];
for(uint state = 0; state < rowGroupIndices.size(); state++) {
uint rowGroupSize;
if(state == 0) {
rowGroupSize = rowGroupIndices[state];
} else {
rowGroupSize = rowGroupIndices[state] - rowGroupIndices[state-1];
}
if(dirOverride != nullptr) {
if((dir == storm::OptimizationDirection::Minimize && !dirOverride->get(state)) || (dir == storm::OptimizationDirection::Maximize && dirOverride->get(state))) {
result.at(state) = *std::min_element(choice_it, choice_it + rowGroupSize);

1
src/storm/storage/PostScheduler.cpp

@ -135,6 +135,7 @@ namespace storm {
// jump to label if we find one undefined choice.
skipStatesWithUndefinedChoices:;
}
out << "___________________________________________________________________" << std::endl;
}
template class PostScheduler<double>;

81
src/storm/storage/Scheduler.cpp

@ -182,6 +182,7 @@ namespace storm {
if (!isMemorylessScheduler()) {
out << " with " << getNumberOfMemoryStates() << " memory states";
}
out << ":" << std::endl;
STORM_LOG_WARN_COND(!(skipUniqueChoices && model == nullptr), "Can not skip unique choices if the model is not given.");
out << std::setw(widthOfStates) << "model state:" << " " << (isMemorylessScheduler() ? "" : " memory: ") << "choice(s)" << (isMemorylessScheduler() ? "" : " memory updates: ") << std::endl;
@ -203,6 +204,11 @@ namespace storm {
bool firstMemoryState = true;
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
// Ignore dontCare states
if(skipDontCareStates && isDontCare(state, memoryState)) {
continue;
}
// Indent if this is not the first memory state
if (firstMemoryState) {
firstMemoryState = false;
@ -216,26 +222,6 @@ namespace storm {
}
stateString << " ";
bool firstMemoryState = true;
for (uint_fast64_t memoryState = 0; memoryState < getNumberOfMemoryStates(); ++memoryState) {
// Ignore dontCare states
if(skipDontCareStates && isDontCare(state, memoryState)) {
continue;
}
// Indent if this is not the first memory state
if (firstMemoryState) {
firstMemoryState = false;
} else {
out << std::setw(widthOfStates) << "";
out << " ";
}
// Print the memory state info
if (!isMemorylessScheduler()) {
out << "m="<< memoryState << std::setw(8) << "";
}
// Print choice info
SchedulerChoice<ValueType> const& choice = schedulerChoices[memoryState][state];
if (choice.isDefined()) {
@ -275,51 +261,26 @@ namespace storm {
stateString << "undefined.";
}
// Print memory updates
if(!isMemorylessScheduler()) {
stateString << std::setw(widthOfStates) << "";
// The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state.
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
bool firstUpdate = true;
for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) {
if (firstUpdate) {
firstUpdate = false;
} else {
stateString << ", ";
}
stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
// out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
}
}
}
// Print memory updates
if(!isMemorylessScheduler()) {
out << std::setw(widthOfStates) << "";
// The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state.
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
bool firstUpdate = true;
for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) {
if (firstUpdate) {
firstUpdate = false;
} else {
out << ", ";
}
out << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
// out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
// Print memory updates
if(!isMemorylessScheduler()) {
stateString << std::setw(widthOfStates) << "";
// The memory updates do not depend on the actual choice, they only depend on the current model- and memory state as well as the successor model state.
for (auto const& choiceProbPair : choice.getChoiceAsDistribution()) {
uint64_t row = model->getTransitionMatrix().getRowGroupIndices()[state] + choiceProbPair.first;
bool firstUpdate = true;
for (auto entryIt = model->getTransitionMatrix().getRow(row).begin(); entryIt < model->getTransitionMatrix().getRow(row).end(); ++entryIt) {
if (firstUpdate) {
firstUpdate = false;
} else {
stateString << ", ";
}
stateString << "model state' = " << entryIt->getColumn() << ": -> " << "(m' = "<<this->memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")";
}
}
out << std::endl;
}
stateString << stateString.str();
stateString << std::endl;
out << stateString.str();
out << std::endl;
}
}
if (numOfSkippedStatesWithUniqueChoice > 0) {

7
src/storm/storage/SparseMatrix.cpp

@ -1848,11 +1848,11 @@ namespace storm {
// Finally write value to target vector.
*resultIt = currentValue;
if(dirOverridden) {
if (choices && dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue)) {
if (choices && (dirOverride->get(currentRowGroup) ? compare(oldSelectedChoiceValue, currentValue) : compare(currentValue, oldSelectedChoiceValue))) {
*choiceIt = selectedChoice;
}
} else {
if (choices && compare(currentValue, oldSelectedChoiceValue)) {
if (choices && (compare(currentValue, oldSelectedChoiceValue))) {
*choiceIt = selectedChoice;
}
}
@ -2129,8 +2129,7 @@ namespace storm {
} else {
target = &result;
}
this->multiplyAndReduceForward(dir, rowGroupIndices, vector, summand, *target, choices);
this->multiplyAndReduceForward(dir, rowGroupIndices, vector, summand, *target, choices, dirOverride);
if (target == &temporary) {
std::swap(temporary, result);

8
src/test/storm/CMakeLists.txt

@ -13,6 +13,7 @@ include_directories(${GTEST_INCLUDE_DIR})
set(NON_SPLIT_TESTS abstraction adapter automata builder logic model parser permissiveschedulers simulator solver storage transformer utility)
set(MODELCHECKER_TEST_SPLITS abstraction csl exploration multiobjective reachability)
set(MODELCHECKER_PRCTL_TEST_SPLITS dtmc mdp)
set(MODELCHECKER_RPATL_TEST_SPLITS smg)
function(configure_testsuite_target testsuite)
#message(CONFIGURING TESTSUITE '${testsuite}') #DEBUG
@ -43,3 +44,10 @@ foreach(prctl_split ${MODELCHECKER_PRCTL_TEST_SPLITS})
add_executable(test-modelchecker-prctl-${prctl_split} ${TEST_MODELCHECKER_PRCTL_${prctl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
configure_testsuite_target(modelchecker-prctl-${prctl_split})
endforeach()
# Modelchecker-Rpatl testsuite split
foreach(rpatl_split ${MODELCHECKER_RPATL_TEST_SPLITS})
file(GLOB_RECURSE TEST_MODELCHECKER_RPATL_${rpatl_split}_FILES ${STORM_TESTS_BASE_PATH}/modelchecker/rpatl/${rpatl_split}/*.h ${STORM_TESTS_BASE_PATH}/modelchecker/rpatl/${rpatl_split}/*.cpp)
add_executable(test-modelchecker-rpatl-${rpatl_split} ${TEST_MODELCHECKER_RPATL_${rpatl_split}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)
configure_testsuite_target(modelchecker-rpatl-${rpatl_split})
endforeach()

43
src/test/storm/logic/FragmentCheckerTest.cpp

@ -84,6 +84,15 @@ TEST(FragmentCheckerTest, Prctl) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PostSafety, gamma=0.678> Pmax=? [\"label1\" U [5,7] \"label2\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.9> Pmax=? [G \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> Pmin=? [F <5 \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl));
}
TEST(FragmentCheckerTest, Csl) {
@ -167,5 +176,39 @@ TEST(FragmentCheckerTest, MultiObjective) {
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(P=? [F P<0.5 [F \"label\"]], R<0.3 [ C ] )"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective));
}
TEST(FragmentCheckerTest, Rpatl) {
auto expManager = std::make_shared<storm::expressions::ExpressionManager>();
storm::logic::FragmentChecker checker;
storm::logic::FragmentSpecification rpatl = storm::logic::rpatl();
storm::parser::FormulaParser formulaParser(expManager);
std::shared_ptr<storm::logic::Formula const> formula;
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<p1>> P=? [F \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2>> Pmin=? [ \"label1\" U \"label2\" ]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<p1, p2>> Rmax=? [ LRA ]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<player1>> R=? [C<=3]"));
EXPECT_FALSE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<<1,2,3>> Pmin=? [F [2,5] \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PostSafety, gamma=0.749> <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shield, PreSafety, lambda=0.749> <<a,b,c>> Pmax=? [G \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<shieldFileName, Optimal> <<p1,p2>> Pmin=? [G \"label\"]"));
EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl));
}

198
src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp

@ -0,0 +1,198 @@
#include <io/file.h>
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/api/builder.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm/models/sparse/Smg.h"
#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/modelchecker/results/QualitativeCheckResult.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/logic/Formulas.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace {
class DoubleViEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
template<typename TestType>
class ShieldGenerationMdpPrctlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
ShieldGenerationMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
std::pair<std::shared_ptr<storm::models::sparse::Mdp<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<storm::models::sparse::Mdp<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<storm::models::sparse::Mdp<ValueType>>();
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
void convertShieldingFileToString(std::string filename, std::string &shieldingString) {
filename += shieldFiletype;
std::ifstream resultFile(filename);
std::stringstream resultBuffer;
resultBuffer << resultFile.rdbuf();
shieldingString = resultBuffer.str();
}
void getStringsToCompare(std::string filename, std::string &shieldingString, std::string &compareFileString) {
this->convertShieldingFileToString(filename, shieldingString);
std::string compareFileName = STORM_TEST_RESOURCES_DIR "/shields/mdp-shields/" + filename;
this->convertShieldingFileToString(compareFileName, compareFileString);
filename += shieldFiletype;
std::remove(filename.c_str());
}
private:
storm::Environment _environment;
std::string shieldFiletype = ".shield";
};
typedef ::testing::Types<
DoubleViEnvironment
> TestingTypes;
TYPED_TEST_SUITE(ShieldGenerationMdpPrctlModelCheckerTest, TestingTypes,);
TYPED_TEST(ShieldGenerationMdpPrctlModelCheckerTest, DieSelection) {
typedef typename TestFixture::ValueType ValueType;
// definition of shield file names
std::vector<std::string> fileNames;
fileNames.push_back("dieSelectionPreSafetylambda08Pmax");
fileNames.push_back("dieSelectionPreSafetygamma08Pmax");
fileNames.push_back("dieSelectionPreSafetylambda08Pmin");
fileNames.push_back("dieSelectionPreSafetygamma08Pmin");
fileNames.push_back("dieSelectionPostSafetylambda07Pmax");
fileNames.push_back("dieSelectionPostSafetygamma07Pmax");
fileNames.push_back("dieSelectionPostSafetylambda07Pmin");
fileNames.push_back("dieSelectionPostSafetygamma07Pmin");
// testing create shielding expressions
std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.8> Pmax=? [ F <5 \"done\" ]";
formulasString += "; <" + fileNames[1] + ", PreSafety, gamma=0.8> Pmax=? [ F <5 \"done\" ]";
formulasString += "; <" + fileNames[2] + ", PreSafety, lambda=0.8> Pmin=? [ F <5 \"done\" ]";
formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.8> Pmin=? [ F <5 \"done\" ]";
formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.7> Pmax=? [ F <6 \"two\" ]";
formulasString += "; <" + fileNames[5] + ", PostSafety, gamma=0.7> Pmax=? [ F <6 \"two\" ]";
formulasString += "; <" + fileNames[6] + ", PostSafety, lambda=0.7> Pmin=? [ F <6 \"two\" ]";
formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.7> Pmin=? [ F <6 \"two\" ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/mdp/die_selection.nm", formulasString);
auto mdp = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(13ul, mdp->getNumberOfStates());
EXPECT_EQ(48ul, mdp->getNumberOfTransitions());
ASSERT_EQ(mdp->getType(), storm::models::ModelType::Mdp);
EXPECT_EQ(27ul, mdp->getNumberOfChoices());
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> checker(*mdp);
// definitions
storm::logic::ShieldingType typePreSafety = storm::logic::ShieldingType::PreSafety;
storm::logic::ShieldingType typePostSafety = storm::logic::ShieldingType::PostSafety;
storm::logic::ShieldComparison comparisonRelative = storm::logic::ShieldComparison::Relative;
storm::logic::ShieldComparison comparisonAbsolute = storm::logic::ShieldComparison::Absolute;
double value08 = 0.8;
double value07 = 0.7;
std::string filename, shieldingString, compareFileString;
// shielding results
filename = fileNames[0];
auto preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08));
tasks[0].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[0].isShieldingTask());
auto result = checker.check(this->env(), tasks[0]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[1];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08));
tasks[1].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[1].isShieldingTask());
result = checker.check(this->env(), tasks[1]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[2];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value08));
tasks[2].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[2].isShieldingTask());
result = checker.check(this->env(), tasks[2]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[3];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value08));
tasks[3].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[3].isShieldingTask());
result = checker.check(this->env(), tasks[3]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[4];
auto postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07));
tasks[4].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[4].isShieldingTask());
result = checker.check(this->env(), tasks[4]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[5];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07));
tasks[5].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[5].isShieldingTask());
result = checker.check(this->env(), tasks[5]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[6];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value07));
tasks[6].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[6].isShieldingTask());
result = checker.check(this->env(), tasks[6]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[7];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value07));
tasks[7].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[7].isShieldingTask());
result = checker.check(this->env(), tasks[7]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
}
// TODO: create more test cases (files)
}

280
src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp

@ -0,0 +1,280 @@
#include <io/file.h>
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/api/builder.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm/models/sparse/Smg.h"
#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/modelchecker/results/QualitativeCheckResult.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/logic/Formulas.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace {
class DoubleViEnvironment {
public:
typedef double ValueType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-8));
return env;
}
};
template<typename TestType>
class ShieldGenerationSmgRpatlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
ShieldGenerationSmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
std::pair<std::shared_ptr<storm::models::sparse::Smg<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<storm::models::sparse::Smg<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<storm::models::sparse::Smg<ValueType>>();
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
void convertShieldingFileToString(std::string filename, std::string &shieldingString) {
filename += shieldFiletype;
std::ifstream resultFile(filename);
std::stringstream resultBuffer;
resultBuffer << resultFile.rdbuf();
shieldingString = resultBuffer.str();
}
void getStringsToCompare(std::string filename, std::string &shieldingString, std::string &compareFileString) {
this->convertShieldingFileToString(filename, shieldingString);
std::string compareFileName = STORM_TEST_RESOURCES_DIR "/shields/smg-shields/" + filename;
this->convertShieldingFileToString(compareFileName, compareFileString);
filename += shieldFiletype;
std::remove(filename.c_str());
}
private:
storm::Environment _environment;
std::string shieldFiletype = ".shield";
};
typedef ::testing::Types<
DoubleViEnvironment
> TestingTypes;
TYPED_TEST_SUITE(ShieldGenerationSmgRpatlModelCheckerTest, TestingTypes,);
TYPED_TEST(ShieldGenerationSmgRpatlModelCheckerTest, RightDecision) {
typedef typename TestFixture::ValueType ValueType;
// definition of shield file names
std::vector<std::string> fileNames;
fileNames.push_back("rightDecisionPreSafetyLambda09PmaxF3");
fileNames.push_back("rightDecisionPreSafetyLambda09PminF3");
fileNames.push_back("rightDecisionPreSafetyGamma09PmaxF3");
fileNames.push_back("rightDecisionPreSafetyGamma09PminF3");
fileNames.push_back("rightDecisionPostSafetyLambda09PmaxF3");
fileNames.push_back("rightDecisionPostSafetyLambda09PminF3");
fileNames.push_back("rightDecisionPostSafetyGamma09PmaxF3");
fileNames.push_back("rightDecisionPostSafetyGamma09PminF3");
fileNames.push_back("rightDecisionPreSafetyLambda05PmaxF5");
fileNames.push_back("rightDecisionPreSafetyLambda05PminF5");
fileNames.push_back("rightDecisionPreSafetyGamma05PmaxF5");
fileNames.push_back("rightDecisionPreSafetyGamma05PminF5");
fileNames.push_back("rightDecisionPostSafetyLambda05PmaxF5");
fileNames.push_back("rightDecisionPostSafetyLambda05PminF5");
fileNames.push_back("rightDecisionPostSafetyGamma05PmaxF5");
fileNames.push_back("rightDecisionPostSafetyGamma05PminF5");
// testing create shielding expressions
std::string formulasString = "<" + fileNames[0] + ", PreSafety, lambda=0.9> <<hiker>> Pmax=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <<hiker>> Pmin=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[2] + ", PreSafety, gamma=0.9> <<hiker>> Pmax=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <<hiker>> Pmin=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.9> <<hiker>> Pmax=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <<hiker>> Pmin=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[6] + ", PostSafety, gamma=0.9> <<hiker>> Pmax=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <<hiker>> Pmin=? [ F <=3 \"target\" ]";
formulasString += "; <" + fileNames[8] + ", PreSafety, lambda=0.5> <<hiker>> Pmax=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <<hiker>> Pmin=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[10] + ", PreSafety, gamma=0.5> <<hiker>> Pmax=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <<hiker>> Pmin=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[12] + ", PostSafety, lambda=0.5> <<hiker>> Pmax=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <<hiker>> Pmin=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[14] + ", PostSafety, gamma=0.5> <<hiker>> Pmax=? [ F <=5 \"target\" ]";
formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <<hiker>> Pmin=? [ F <=5 \"target\" ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString);
auto smg = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(11ul, smg->getNumberOfStates());
EXPECT_EQ(15ul, smg->getNumberOfTransitions());
ASSERT_EQ(smg->getType(), storm::models::ModelType::Smg);
EXPECT_EQ(14ull, smg->getNumberOfChoices());
//std::unique_ptr<storm::modelchecker::CheckResult> result;
storm::modelchecker::SparseSmgRpatlModelChecker<storm::models::sparse::Smg<ValueType>> checker(*smg);
// definitions
storm::logic::ShieldingType typePreSafety = storm::logic::ShieldingType::PreSafety;
storm::logic::ShieldingType typePostSafety = storm::logic::ShieldingType::PostSafety;
storm::logic::ShieldComparison comparisonRelative = storm::logic::ShieldComparison::Relative;
storm::logic::ShieldComparison comparisonAbsolute = storm::logic::ShieldComparison::Absolute;
double value09 = 0.9;
double value05 = 0.5;
std::string filename, shieldingString, compareFileString;
// shielding results
filename = fileNames[0];
auto preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09));
tasks[0].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[0].isShieldingTask());
auto result = checker.check(this->env(), tasks[0]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[1];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value09));
tasks[1].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[1].isShieldingTask());
result = checker.check(this->env(), tasks[1]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[2];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09));
tasks[2].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[2].isShieldingTask());
result = checker.check(this->env(), tasks[2]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[3];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value09));
tasks[3].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[3].isShieldingTask());
result = checker.check(this->env(), tasks[3]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[4];
auto postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09));
tasks[4].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[4].isShieldingTask());
result = checker.check(this->env(), tasks[4]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[5];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value09));
tasks[5].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[5].isShieldingTask());
result = checker.check(this->env(), tasks[5]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[6];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09));
tasks[6].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[6].isShieldingTask());
result = checker.check(this->env(), tasks[6]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[7];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value09));
tasks[7].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[7].isShieldingTask());
result = checker.check(this->env(), tasks[7]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[8];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05));
tasks[8].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[8].isShieldingTask());
result = checker.check(this->env(), tasks[8]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[9];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonRelative, value05));
tasks[9].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[9].isShieldingTask());
result = checker.check(this->env(), tasks[9]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[10];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05));
tasks[10].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[10].isShieldingTask());
result = checker.check(this->env(), tasks[10]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[11];
preSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePreSafety, filename, comparisonAbsolute, value05));
tasks[11].setShieldingExpression(preSafetyShieldingExpression);
EXPECT_TRUE(tasks[11].isShieldingTask());
result = checker.check(this->env(), tasks[11]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[12];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05));
tasks[12].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[12].isShieldingTask());
result = checker.check(this->env(), tasks[12]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[13];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonRelative, value05));
tasks[13].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[13].isShieldingTask());
result = checker.check(this->env(), tasks[13]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[14];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05));
tasks[14].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[14].isShieldingTask());
result = checker.check(this->env(), tasks[14]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
filename = fileNames[15];
postSafetyShieldingExpression = std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(typePostSafety, filename, comparisonAbsolute, value05));
tasks[15].setShieldingExpression(postSafetyShieldingExpression);
EXPECT_TRUE(tasks[15].isShieldingTask());
result = checker.check(this->env(), tasks[15]);
this->getStringsToCompare(filename, shieldingString, compareFileString);
EXPECT_EQ(shieldingString, compareFileString);
}
// TODO: create more test cases (files)
}

351
src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp

@ -0,0 +1,351 @@
#include "test/storm_gtest.h"
#include "storm-config.h"
#include "storm/api/builder.h"
#include "storm-parsers/api/model_descriptions.h"
#include "storm/api/properties.h"
#include "storm-parsers/api/properties.h"
#include "storm/models/sparse/Smg.h"
#include "storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.h"
#include "storm/modelchecker/results/QuantitativeCheckResult.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
#include "storm/modelchecker/results/QualitativeCheckResult.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/TopologicalSolverEnvironment.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/settings/modules/CoreSettings.h"
#include "storm/logic/Formulas.h"
#include "storm/exceptions/UncheckedRequirementException.h"
namespace {
enum class SmgEngine {PrismSparse};
class SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment {
public:
static const SmgEngine engine = SmgEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Smg<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel);
env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx);
return env;
}
};
class SparseDoubleValueIterationGmmxxRegularMultEnvironment {
public:
static const SmgEngine engine = SmgEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Smg<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular);
env.solver().multiplier().setType(storm::solver::MultiplierType::Gmmxx);
return env;
}
};
class SparseDoubleValueIterationNativeGaussSeidelMultEnvironment {
public:
static const SmgEngine engine = SmgEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Smg<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::GaussSeidel);
env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
return env;
}
};
class SparseDoubleValueIterationNativeRegularMultEnvironment {
public:
static const SmgEngine engine = SmgEngine::PrismSparse;
static const bool isExact = false;
typedef double ValueType;
typedef storm::models::sparse::Smg<ValueType> ModelType;
static storm::Environment createEnvironment() {
storm::Environment env;
env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration);
env.solver().minMax().setPrecision(storm::utility::convertNumber<storm::RationalNumber>(1e-10));
env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular);
env.solver().multiplier().setType(storm::solver::MultiplierType::Native);
return env;
}
};
template<typename TestType>
class SmgRpatlModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
typedef typename storm::models::sparse::Smg<ValueType> SparseModelType;
SmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const {
std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
storm::prism::Program program = storm::api::parseProgram(pathToPrismFile);
program = storm::utility::prism::preprocess(program, constantDefinitionString);
if (TestType::engine == SmgEngine::PrismSparse) {
result.second = storm::api::extractFormulasFromProperties(storm::api::parsePropertiesForPrismProgram(formulasAsString, program));
result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
}
return result;
}
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) const {
std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
for (auto const& f : formulas) {
result.emplace_back(*f);
}
return result;
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
if (TestType::engine == SmgEngine::PrismSparse) {
return std::make_shared<storm::modelchecker::SparseSmgRpatlModelChecker<SparseModelType>>(*model);
} else {
STORM_LOG_ERROR("TestType::engine must be PrismSparse!");
return nullptr;
}
}
ValueType getQuantitativeResultAtInitialState(std::shared_ptr<storm::models::Model<ValueType>> const& model, std::unique_ptr<storm::modelchecker::CheckResult>& result) {
auto filter = getInitialStateFilter(model);
result->filter(*filter);
return result->asQuantitativeCheckResult<ValueType>().getMin();
}
private:
storm::Environment _environment;
std::unique_ptr<storm::modelchecker::QualitativeCheckResult> getInitialStateFilter(std::shared_ptr<storm::models::Model<ValueType>> const& model) const {
if (isSparseModel()) {
return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
} else {
STORM_LOG_ERROR("Smg Rpatl Model must be a Sparse Model!");
return nullptr;
}
}
};
typedef ::testing::Types<
SparseDoubleValueIterationGmmxxGaussSeidelMultEnvironment,
SparseDoubleValueIterationGmmxxRegularMultEnvironment,
SparseDoubleValueIterationNativeGaussSeidelMultEnvironment,
SparseDoubleValueIterationNativeRegularMultEnvironment
> TestingTypes;
TYPED_TEST_SUITE(SmgRpatlModelCheckerTest, TestingTypes,);
TYPED_TEST(SmgRpatlModelCheckerTest, Walker) {
// NEXT tests
std::string formulasString = "<<walker>> Pmax=? [X \"s2\"]";
formulasString += "; <<walker>> Pmin=? [X \"s2\"]";
formulasString += "; <<walker>> Pmax=? [X !\"s1\"]";
formulasString += "; <<walker>> Pmin=? [X !\"s1\"]";
// UNTIL tests
formulasString += "; <<walker>> Pmax=? [ a=0 U a=1 ]";
formulasString += "; <<walker>> Pmin=? [ a=0 U a=1 ]";
formulasString += "; <<walker>> Pmax=? [ b=0 U b=1 ]";
formulasString += "; <<walker>> Pmin=? [ b=0 U b=1 ]";
// GLOBALLY tests
formulasString += "; <<walker>> Pmax=? [G !\"s3\"]";
formulasString += "; <<walker>> Pmin=? [G !\"s3\"]";
formulasString += "; <<walker>> Pmax=? [G a=0 ]";
formulasString += "; <<walker>> Pmin=? [G a=0 ]";
// EVENTUALLY tests
formulasString += "; <<walker>> Pmax=? [F \"s3\"]";
formulasString += "; <<walker>> Pmin=? [F \"s3\"]";
formulasString += "; <<walker>> Pmax=? [F [3,4] \"s4\"]";
formulasString += "; <<walker>> Pmax=? [F [3,5] \"s4\"]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/walker.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(5ul, model->getNumberOfStates());
EXPECT_EQ(12ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Smg);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// NEXT results
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("0.6"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// UNTIL results
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("0.52"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("0.9999996417"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[7]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// GLOBALLY tests
result = checker->check(this->env(), tasks[8]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[9]);
EXPECT_NEAR(this->parseNumber("0.65454565"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[10]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[11]);
EXPECT_NEAR(this->parseNumber("0.48"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// EVENTUALLY tests
result = checker->check(this->env(), tasks[12]);
EXPECT_NEAR(this->parseNumber("0.34545435"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[13]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[14]);
EXPECT_NEAR(this->parseNumber("0.576"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[15]);
EXPECT_NEAR(this->parseNumber("0.6336"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(SmgRpatlModelCheckerTest, MessageHack) {
// This test is for borders of bounded U with conversations from G and F
// G
std::string formulasString = "<<bob, alice>> Pmax=? [ G !\"hacked\" ]";
// bounded F
formulasString += "; <<bob, alice>> Pmin=? [ F \"hacked\" ]";
formulasString += "; <<bob, alice>> Pmin=? [ F [1,2] \"hacked\" ]";
formulasString += "; <<bob, alice>> Pmin=? [ F [3,16] \"hacked\" ]";
formulasString += "; <<bob, alice>> Pmin=? [ F [0,17] \"hacked\" ]";
formulasString += "; <<bob, alice>> Pmin=? [ F [17,31] \"hacked\" ]";
formulasString += "; <<bob, alice>> Pmin=? [ F [17,32] \"hacked\" ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/messageHack.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(30ul, model->getNumberOfStates());
EXPECT_EQ(31ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Smg);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// G results
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1.99379598e-05"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// bounded F results
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("0.999980062"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("0.05"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("0.0975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("0.142625"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
TYPED_TEST(SmgRpatlModelCheckerTest, RightDecision) {
// This test is for making decisions
// testing probabilities for decisions
std::string formulasString = "<<hiker>> Pmax=? [ F <=3 \"target\" ]";
formulasString += "; <<hiker>> Pmax=? [ F <=5 \"target\" ]";
formulasString += "; <<hiker, native>> Pmax=? [ F <=3 \"target\" ]";
formulasString += "; <<hiker>> Pmin=? [ F \"target\" ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/rightDecision.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(11ul, model->getNumberOfStates());
EXPECT_EQ(15ul, model->getNumberOfTransitions());
ASSERT_EQ(model->getType(), storm::models::ModelType::Smg);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// probability results
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("0.9"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("0"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
/*
TYPED_TEST(SmgRpatlModelCheckerTest, RobotCircle) {
// This test is for testing bounded globally with upper bound and in an interval (with upper and lower bound)
std::string formulasString = " <<friendlyRobot>> Pmax=? [ G<1 !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G<=1 !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G<=5 !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G<=6 !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G<=7 !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G<=8 !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G[1,5] !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G[5,6] !\"crash\" ]";
formulasString += "; <<friendlyRobot>> Pmax=? [ G[7,8] !\"crash\" ]";
auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR "/smg/robotCircle.nm", formulasString);
auto model = std::move(modelFormulas.first);
auto tasks = this->getTasks(modelFormulas.second);
EXPECT_EQ(81ul, model->getNumberOfStates());
EXPECT_EQ(196ul, model->getNumberOfTransitions());
EXPECT_EQ(148ul, model->getNumberOfChoices());
ASSERT_EQ(model->getType(), storm::models::ModelType::Smg);
auto checker = this->createModelChecker(model);
std::unique_ptr<storm::modelchecker::CheckResult> result;
// results for bounded globally with upper bound
result = checker->check(this->env(), tasks[0]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[1]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[2]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[3]);
EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[4]);
EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[5]);
EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
// results for bounded globally with upper and lower bound
result = checker->check(this->env(), tasks[6]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[7]);
EXPECT_NEAR(this->parseNumber("0.975"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
result = checker->check(this->env(), tasks[8]);
EXPECT_NEAR(this->parseNumber("1"), this->getQuantitativeResultAtInitialState(model, result), this->precision());
}
*/
// TODO: create more test cases (files)
}

204
src/test/storm/parser/GameFormulaParserTest.cpp

@ -0,0 +1,204 @@
#include "test/storm_gtest.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/storage/expressions/ExpressionManager.h"
TEST(GameFormulaParserTest, OnePlayerCoalitionTest) {
storm::parser::FormulaParser formulaParser;
std::string player = "p1";
std::string input = "<<" + player + ">>" + " Pmax=? [F \"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
auto const& playerCoalition = formula->asGameFormula().getCoalition();
std::ostringstream stream;
stream << playerCoalition;
std::string playerCoalitionString = stream.str();
EXPECT_EQ(player, playerCoalitionString);
}
TEST(GameFormulaParserTest, PlayersCoalitionTest) {
storm::parser::FormulaParser formulaParser;
std::string player = "p1, p2, p3, p4, p5";
std::string input = "<<" + player + ">>" + " Pmin=? [X \"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
auto const& playerCoalition = formula->asGameFormula().getCoalition();
EXPECT_EQ(5ul, playerCoalition.getPlayers().size());
std::ostringstream stream;
stream << playerCoalition;
std::string playerCoalitionString = stream.str();
std::string playerWithoutWhiteSpace = "p1,p2,p3,p4,p5";
EXPECT_EQ(playerWithoutWhiteSpace, playerCoalitionString);
}
TEST(GameFormulaParserTest, ProbabilityOperatorTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "<<player>> Pmax=? [\"a\" U \"b\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_FALSE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().hasBound());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().hasOptimalityType());
}
TEST(GameFormulaParserTest, NextOperatorTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("a");
storm::parser::FormulaParser formulaParser(manager);
std::string input = "<<p>> Pmax=? [X \"a\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula());
input = "<<p1, p2, p3>> Pmin=? [X !x ]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula());
input = "<<player1, player2, 3,4,5>> Pmax=? [ X a>5 ]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula());
}
TEST(GameFormulaParserTest, UntilOperatorTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "<<p>> Pmax=? [\"a\" U \"b\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isUntilFormula());
EXPECT_FALSE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula());
input = "<<p>> Pmax=? [ \"a\" U <= 4 \"b\" ]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getTimeBoundReference().isTimeBound());
EXPECT_FALSE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasLowerBound());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasUpperBound());
EXPECT_EQ(4, formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt());
input = "<<p1, p2>> Pmin=? [ \"a\" & \"b\" U [5,9] \"c\" ] ";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getTimeBoundReference().isTimeBound());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasLowerBound());
EXPECT_EQ(5, formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getLowerBound().evaluateAsInt());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().hasUpperBound());
EXPECT_EQ(9, formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula().getUpperBound().evaluateAsInt());
}
TEST(GameFormulaParserTest, RewardOperatorTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "<<p1, p2>> Rmin<0.9 [F \"a\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType());
EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
input = "<<p1, p2>> R=? [I=10]";
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isRewardOperatorFormula());
EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasBound());
EXPECT_FALSE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().hasOptimalityType());
EXPECT_TRUE(formula->asGameFormula().getSubformula().asRewardOperatorFormula().getSubformula().isInstantaneousRewardFormula());
EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
}
TEST(GameFormulaParserTest, ConditionalProbabilityTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "<<p1, p2>> P<0.9 [F \"a\" || F \"b\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asGameFormula().getSubformula().asProbabilityOperatorFormula();
EXPECT_TRUE(probFormula.getSubformula().isConditionalProbabilityFormula());
EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
}
TEST(GameFormulaParserTest, NestedPathFormulaTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "<<p1, p2, p3>> P<0.9 [F X \"a\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asEventuallyFormula().getSubformula().isNextFormula());
EXPECT_FALSE(formula->asGameFormula().getSubformula().isInFragment(storm::logic::rpatl()));
}
TEST(GameFormulaParserTest, CommentTest) {
storm::parser::FormulaParser formulaParser;
std::string input = "// This is a comment. And this is a commented out formula: <<p>> P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n<<p>> P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment.";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
EXPECT_TRUE(formula->asGameFormula().getSubformula().isProbabilityOperatorFormula());
ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().isNextFormula());
ASSERT_TRUE(formula->asGameFormula().getSubformula().asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
}
TEST(GameFormulaParserTest, WrongFormatTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser formulaParser(manager);
std::string input = "<<p1,p2>> P>0.5 [ a ]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "<<p>> P=0.5 [F \"a\"]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "<<p1, p2>> P>0.5 [F !(x = 0)]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "<< p1, p2 >> P>0.5 [F !y]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "<< 1,2,3 >> P>0.5 [F y!=0)]";
STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
}

81
src/test/storm/parser/GameShieldingParserTest.cpp

@ -0,0 +1,81 @@
#include "test/storm_gtest.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/storage/expressions/ExpressionManager.h"
TEST(GameShieldingParserTest, PreSafetyShieldTest) {
storm::parser::FormulaParser formulaParser;
std::string filename = "preSafetyShieldFileName";
std::string value = "0.9";
std::string input = "<" + filename + ", PreSafety, lambda=" + value + "> <<p1,p2>> Pmax=? [F \"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_TRUE(shieldExpression->isPreSafetyShield());
EXPECT_FALSE(shieldExpression->isPostSafetyShield());
EXPECT_FALSE(shieldExpression->isOptimalShield());
EXPECT_TRUE(shieldExpression->isRelative());
EXPECT_EQ(std::stod(value), shieldExpression->getValue());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
TEST(GameShieldingParserTest, PostSafetyShieldTest) {
storm::parser::FormulaParser formulaParser;
std::string filename = "postSafetyShieldFileName";
std::string value = "0.7569";
std::string input = "<" + filename + ", PostSafety, gamma=" + value + "> <<p1,p2,p3>> Pmin=? [X !\"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_FALSE(shieldExpression->isPreSafetyShield());
EXPECT_TRUE(shieldExpression->isPostSafetyShield());
EXPECT_FALSE(shieldExpression->isOptimalShield());
EXPECT_FALSE(shieldExpression->isRelative());
EXPECT_EQ(std::stod(value), shieldExpression->getValue());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
TEST(GameShieldingParserTest, OptimalShieldTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareIntegerVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser formulaParser(manager);
std::string filename = "optimalShieldFileName";
std::string input = "<" + filename + ", Optimal> <<p1,p2,p3>> Pmax=? [G x>y]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isGameFormula());
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_FALSE(shieldExpression->isPreSafetyShield());
EXPECT_FALSE(shieldExpression->isPostSafetyShield());
EXPECT_TRUE(shieldExpression->isOptimalShield());
EXPECT_FALSE(shieldExpression->isRelative());
EXPECT_EQ(filename, shieldExpression->getFilename());
}

72
src/test/storm/parser/MdpShieldingParserTest.cpp

@ -0,0 +1,72 @@
#include "test/storm_gtest.h"
#include "storm-parsers/parser/FormulaParser.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/storage/expressions/ExpressionManager.h"
TEST(MdpShieldingParserTest, PreSafetyShieldTest) {
storm::parser::FormulaParser formulaParser;
std::string filename = "preSafetyShieldFileName";
std::string value = "0.6667";
std::string input = "<" + filename + ", PreSafety, gamma=" + value + "> Pmax=? [F \"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_TRUE(shieldExpression->isPreSafetyShield());
EXPECT_FALSE(shieldExpression->isPostSafetyShield());
EXPECT_FALSE(shieldExpression->isOptimalShield());
EXPECT_FALSE(shieldExpression->isRelative());
EXPECT_EQ(std::stod(value), shieldExpression->getValue());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
TEST(MdpShieldingParserTest, PostSafetyShieldTest) {
storm::parser::FormulaParser formulaParser;
std::string filename = "postSafetyShieldFileName";
std::string value = "0.95";
std::string input = "<" + filename + ", PostSafety, lambda=" + value + "> Pmin=? [X !\"label\"]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_FALSE(shieldExpression->isPreSafetyShield());
EXPECT_TRUE(shieldExpression->isPostSafetyShield());
EXPECT_FALSE(shieldExpression->isOptimalShield());
EXPECT_TRUE(shieldExpression->isRelative());
EXPECT_EQ(std::stod(value), shieldExpression->getValue());
EXPECT_EQ(filename, shieldExpression->getFilename());
}
TEST(MdpShieldingParserTest, OptimalShieldTest) {
std::shared_ptr<storm::expressions::ExpressionManager> manager(new storm::expressions::ExpressionManager());
manager->declareBooleanVariable("a");
manager->declareIntegerVariable("x");
storm::parser::FormulaParser formulaParser(manager);
std::string filename = "optimalShieldFileName";
std::string input = "<" + filename + ", Optimal> Pmax=? [G (a|x>3)]";
std::shared_ptr<storm::logic::Formula const> formula(nullptr);
std::vector<storm::jani::Property> property;
ASSERT_NO_THROW(property = formulaParser.parseFromString(input));
EXPECT_TRUE(property.at(0).isShieldingProperty());
std::shared_ptr<storm::logic::ShieldExpression const> shieldExpression(nullptr);
ASSERT_NO_THROW(shieldExpression = property.at(0).getShieldingExpression());
EXPECT_FALSE(shieldExpression->isPreSafetyShield());
EXPECT_FALSE(shieldExpression->isPostSafetyShield());
EXPECT_TRUE(shieldExpression->isOptimalShield());
EXPECT_FALSE(shieldExpression->isRelative());
EXPECT_EQ(filename, shieldExpression->getFilename());
}

38
src/test/storm/parser/PrismParserTest.cpp

@ -14,6 +14,7 @@ TEST(PrismParser, StandardModelTest) {
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/dtmc/leader3_5.pm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/two_dice.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/wlan0_collide.nm"));
EXPECT_NO_THROW(result = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/smg/walker.nm"));
}
TEST(PrismParser, SimpleTest) {
@ -100,6 +101,43 @@ TEST(PrismParser, ComplexTest) {
EXPECT_EQ(2ul, result.getNumberOfRewardModels());
EXPECT_EQ(1ul, result.getNumberOfLabels());
EXPECT_FALSE(result.hasUnboundedVariables());
testInput =
R"(smg
player walker
[a0], [a00], [a1], [a2], [a3]
endplayer
player blocker
[a40], [a41]
endplayer
label "s0" = c=0 & b=0 & a=0;
label "s1" = c=0 & b=0 & a=1;
label "s2" = c=0 & b=1 & a=0;
label "s3" = c=0 & b=1 & a=1;
label "s4" = c=1 & b=0 & a=0;
module transitions
a : [0..1] init 0;
b : [0..1] init 0;
c : [0..1] init 0;
[a0] a=0 & b=0 & c=0 -> 4/10 : (a'=1) + 6/10 : (b'=1);
[a00] a=0 & b=0 & c=0 -> true;
[a1] a=1 & b=0 & c=0 -> 3/10 : (a'=0) + 3/10 : (a'=0) & (b'=1) + 4/10 : (b'=1);
[a2] a=0 & b=1 & c=0 -> 2/10 : (a'=1) + 8/10 : (b'=0) & (c'=1);
[a3] a=1 & b=1 & c=0 -> true;
[a40] a=0 & b=0 & c=1 -> 3/10 : (c'=0) + 7/10 : (a'=1) & (b'=1) & (c'=0);
[a41] a=0 & b=0 & c=1 -> true;
endmodule)";
EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"));
EXPECT_EQ(storm::prism::Program::ModelType::SMG, result.getModelType());
EXPECT_EQ(1ul, result.getNumberOfModules());
EXPECT_EQ(2ul, result.getNumberOfPlayers());
EXPECT_EQ(5ul, result.getNumberOfLabels());
}
TEST(PrismParser, UnboundedTest) {

Loading…
Cancel
Save