diff --git a/resources/examples/testfiles/rpatl/probabilisticFormula.rpatl b/resources/examples/testfiles/rpatl/probabilisticFormula.rpatl new file mode 100644 index 000000000..1b0eed235 --- /dev/null +++ b/resources/examples/testfiles/rpatl/probabilisticFormula.rpatl @@ -0,0 +1 @@ +<> Pmax=? [ F "goal" ] \ No newline at end of file diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield new file mode 100644 index 000000000..f14bbb1ba --- /dev/null +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmax.shield @@ -0,0 +1,5 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.700000): +model state: correction [: ()}: + 4 0: 2; 1: 2; 2: 2 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield new file mode 100644 index 000000000..26c138cc2 --- /dev/null +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetygamma07Pmin.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.700000): +model state: correction [: ()}: + 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 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield new file mode 100644 index 000000000..89cc541ed --- /dev/null +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmax.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.700000): +model state: correction [: ()}: + 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 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield new file mode 100644 index 000000000..5cbf8cc99 --- /dev/null +++ b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPostSafetylambda07Pmin.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.700000): +model state: correction [: ()}: + 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 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmax.shield new file mode 100644 index 000000000..3014f95c4 --- /dev/null +++ b/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) [: ()}: + 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) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetygamma08Pmin.shield new file mode 100644 index 000000000..6b32fa01a --- /dev/null +++ b/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) [: ()}: + 0 0.58: (0); 0.566: (1); 0.552: (2) + 3 0.755: (0); 0.706: (1); 0.657: (2) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmax.shield new file mode 100644 index 000000000..7d91ac6f8 --- /dev/null +++ b/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) [: ()}: + 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) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield b/resources/examples/testfiles/shields/mdp-shields/dieSelectionPreSafetylambda08Pmin.shield new file mode 100644 index 000000000..dcd83f02c --- /dev/null +++ b/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) [: ()}: +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield new file mode 100644 index 000000000..73f8c1342 --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PmaxF5.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.500000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield new file mode 100644 index 000000000..c5e6ddce1 --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma05PminF5.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.500000): +model state: correction [: ()}: + 4 0: 0 + 5 0: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield new file mode 100644 index 000000000..b8cf860c2 --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PmaxF3.shield @@ -0,0 +1,7 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.900000): +model state: correction [: ()}: + 0 0: 0; 1: 0 + 5 0: 0 + 9 0: 0; 1: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield new file mode 100644 index 000000000..dbdb1771a --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyGamma09PminF3.shield @@ -0,0 +1,6 @@ +___________________________________________________________________ +Post-Safety-Shield with absolute comparison (gamma = 0.900000): +model state: correction [: ()}: + 4 0: 0 + 5 0: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield new file mode 100644 index 000000000..6385fca02 --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PmaxF5.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.500000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield new file mode 100644 index 000000000..6385fca02 --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda05PminF5.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.500000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield new file mode 100644 index 000000000..c115a997a --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PmaxF3.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.900000): +model state: correction [: ()}: + 0 0: 0; 1: 0 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 0 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield new file mode 100644 index 000000000..24a913b11 --- /dev/null +++ b/resources/examples/testfiles/shields/smg-shields/rightDecisionPostSafetyLambda09PminF3.shield @@ -0,0 +1,8 @@ +___________________________________________________________________ +Post-Safety-Shield with relative comparison (lambda = 0.900000): +model state: correction [: ()}: + 0 0: 0; 1: 1 + 4 0: 0 + 5 0: 0 + 9 0: 0; 1: 1 +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PmaxF5.shield new file mode 100644 index 000000000..083d98dc2 --- /dev/null +++ b/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) [: ()}: + 0 0.9: (0); 1: (1) + 5 1: (0) + 9 1: (0); 0.9: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma05PminF5.shield new file mode 100644 index 000000000..854110128 --- /dev/null +++ b/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) [: ()}: + 4 0: (0) + 5 0: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PmaxF3.shield new file mode 100644 index 000000000..5cc5423f1 --- /dev/null +++ b/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) [: ()}: + 0 0.9: (0) + 5 1: (0) + 9 1: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyGamma09PminF3.shield new file mode 100644 index 000000000..5afcb6598 --- /dev/null +++ b/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) [: ()}: + 4 0: (0) + 5 0: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PmaxF5.shield new file mode 100644 index 000000000..f38157e63 --- /dev/null +++ b/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) [: ()}: + 0 0.9: (0); 1: (1) + 4 0: (0) + 5 1: (0) + 9 1: (0); 0.9: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda05PminF5.shield new file mode 100644 index 000000000..363275926 --- /dev/null +++ b/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) [: ()}: + 0 0: (1) + 4 0: (0) + 5 0: (0) + 9 0: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PmaxF3.shield new file mode 100644 index 000000000..0f9beb691 --- /dev/null +++ b/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) [: ()}: + 0 0.9: (0) + 4 0: (0) + 5 1: (0) + 9 1: (0) +___________________________________________________________________ diff --git a/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield b/resources/examples/testfiles/shields/smg-shields/rightDecisionPreSafetyLambda09PminF3.shield new file mode 100644 index 000000000..eb3d29cd3 --- /dev/null +++ b/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) [: ()}: + 0 0: (1) + 4 0: (0) + 5 0: (0) + 9 0: (1) +___________________________________________________________________ diff --git a/resources/examples/testfiles/smg/messageHack.nm b/resources/examples/testfiles/smg/messageHack.nm new file mode 100644 index 000000000..e67352bef --- /dev/null +++ b/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 diff --git a/resources/examples/testfiles/smg/rightDecision.nm b/resources/examples/testfiles/smg/rightDecision.nm new file mode 100644 index 000000000..a47222e10 --- /dev/null +++ b/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 diff --git a/resources/examples/testfiles/smg/robotCircle.nm b/resources/examples/testfiles/smg/robotCircle.nm new file mode 100644 index 000000000..92170a97a --- /dev/null +++ b/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 (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 (y1'=y1+1) & (move'=1); +endmodule + +module robot2 + x2 : [0..width] init width; + y2 : [0..height] init height; + + [e2] move=1 & x2 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 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 diff --git a/resources/examples/testfiles/smg/walker.nm b/resources/examples/testfiles/smg/walker.nm new file mode 100644 index 000000000..e50b3aa5b --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 13b56d8a9..ea96f31a2 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/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(rewardModelName, handler(qi::_1, qi::_2, qi::_3, qi::_4)); @@ -386,6 +404,11 @@ namespace storm { } } + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + } + + /* std::shared_ptr FormulaParserGrammar::createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const { if (timeBounds && !timeBounds.get().empty()) { std::vector> lowerBounds, upperBounds; @@ -401,6 +424,7 @@ namespace storm { return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); } } + */ std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { return std::shared_ptr(new storm::logic::NextFormula(subformula)); @@ -619,6 +643,29 @@ namespace storm { } } + std::pair FormulaParserGrammar::createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value) { + return std::make_pair(comparisonType, value); + } + + std::shared_ptr FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> 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(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(new storm::logic::ShieldExpression(type, name)); + } + } + + storm::jani::Property FormulaParserGrammar::createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr 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> const& playerIds) const { return storm::logic::PlayerCoalition(playerIds); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index fca3b3a1c..9f0953577 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -234,6 +234,12 @@ namespace storm { }; qi::rule, Skipper> constantDefinition; + // Shielding properties + qi::rule(), Skipper> shieldExpression; + qi::rule shieldingType; + qi::rule probability; + qi::rule, qi::locals, Skipper> shieldComparison; + // Start symbol qi::rule(), Skipper> start; @@ -242,6 +248,9 @@ namespace storm { storm::logic::PlayerCoalition createPlayerCoalition(std::vector> const& playerIds) const; std::shared_ptr createGameFormula(storm::logic::PlayerCoalition const& coalition, std::shared_ptr const& subformula) const; + std::pair createShieldComparisonStruct(storm::logic::ShieldComparison comparisonType, double value); + std::shared_ptr createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional> comparisonStruct); + bool areConstantDefinitionsAllowed() const; void addConstant(std::string const& name, ConstantDataType type, boost::optional const& expression); void addProperty(std::vector& properties, boost::optional const& name, std::shared_ptr const& formula); @@ -259,6 +268,7 @@ namespace storm { std::shared_ptr createBooleanLiteralFormula(bool literal) const; std::shared_ptr createAtomicLabelFormula(std::string const& label) const; std::shared_ptr createEventuallyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + //std::shared_ptr createGloballyFormula(boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& subformula) const; std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, boost::optional, std::shared_ptr>>> const& timeBounds, std::shared_ptr const& rightSubformula); @@ -285,6 +295,7 @@ namespace storm { std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional const& propertyName, std::shared_ptr const& formula); + storm::jani::Property createShieldingProperty(boost::optional const& propertyName, std::shared_ptr const& formula, std::shared_ptr const& shieldingExpression); bool isBooleanReturnType(std::shared_ptr const& formula, bool raiseErrorMessage = false); bool raiseAmbiguousNonAssociativeOperatorError(std::shared_ptr const& formula, std::string const& op); diff --git a/src/storm/generator/PrismNextStateGenerator.cpp b/src/storm/generator/PrismNextStateGenerator.cpp index a9c845d32..600615c64 100644 --- a/src/storm/generator/PrismNextStateGenerator.cpp +++ b/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()) { diff --git a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp index 0d88c456e..8e3da6930 100644 --- a/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp +++ b/src/storm/modelchecker/helper/finitehorizon/SparseNondeterministicStepBoundedHorizonHelper.cpp @@ -20,10 +20,11 @@ namespace storm { template void SparseNondeterministicStepBoundedHorizonHelper::getMaybeStatesRowGroupSizes(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& maybeStates, std::vector& maybeStatesRowGroupSizes, uint& choiceValuesCounter) { std::vector 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 rowGroupIndices = transitionMatrix.getRowGroupIndices(); std::vector maybeStatesRowGroupSizes; - uint choiceValuesCounter; + uint choiceValuesCounter = 0; getMaybeStatesRowGroupSizes(transitionMatrix, maybeStates, maybeStatesRowGroupSizes, choiceValuesCounter); choiceValues = std::vector(choiceValuesCounter, storm::utility::zero()); diff --git a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 19b1f627e..ee7c2d91d 100644 --- a/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/storm/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -221,7 +221,7 @@ namespace storm { STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler."); return *scheduler.get(); } - + template void print(std::ostream& out, ValueType const& value) { if (value == storm::utility::infinity()) { diff --git a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp b/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp index bf04dc000..3e8cd7569 100644 --- a/src/storm/modelchecker/rpatl/SparseSmgRpatlModelChecker.cpp +++ b/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::computeBoundedUntilProbabilities(env, storm::solver::SolveGoal(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), checkTask.isQualitativeSet(), statesOfCoalition, checkTask.isProduceSchedulersSet(), checkTask.getHint(), pathFormula.getNonStrictLowerBound(), pathFormula.getNonStrictUpperBound()); std::unique_ptr result(new ExplicitQuantitativeCheckResult(std::move(ret.values))); if(checkTask.isShieldingTask()) { - tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); + tempest::shields::createShield(std::make_shared>(this->getModel()), std::move(ret.choiceValues), checkTask.getShieldingExpression(), checkTask.getOptimizationDirection(), std::move(ret.relevantStates), ~statesOfCoalition); } return result; } diff --git a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp index 85a08ea96..bc18f35ff 100644 --- a/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/SparseSmgRpatlHelper.cpp @@ -1,4 +1,5 @@ #include +#include #include "SparseSmgRpatlHelper.h" #include "storm/environment/Environment.h" @@ -15,7 +16,6 @@ namespace storm { template SMGSparseModelCheckingHelperReturnType SparseSmgRpatlHelper::computeUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix 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>(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()); @@ -109,7 +110,9 @@ namespace storm { } // Create a multiplier for reduction. auto multiplier = storm::solver::MultiplierFactory().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 subResult = std::vector(transitionMatrix.getRowGroupCount(), storm::utility::zero()); @@ -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(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero()); b = std::vector(transitionMatrix.getConstrainedRowGroupSumVector(relevantStates, newPsiStates).size(), storm::utility::zero()); // 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()); } diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp index 4ddadc247..54efd3c7c 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp +++ b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.cpp @@ -25,13 +25,14 @@ namespace storm { } template - void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir) { + void GameViHelper::performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, std::vector& constrainedChoiceValues) { prepareSolversAndMultipliers(env); // Get precision for convergence check. ValueType precision = storm::utility::convertNumber(env.solver().game().getPrecision()); uint64_t maxIter = env.solver().game().getMaximalNumberOfIterations(); _b = b; - _x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + //_x1.assign(_transitionMatrix.getRowGroupCount(), storm::utility::zero()); + _x1 = x; _x2 = _x1; if (this->isProduceSchedulerSet()) { @@ -42,17 +43,25 @@ namespace storm { } uint64_t iter = 0; - std::vector result = x; + constrainedChoiceValues = std::vector(b.size(), storm::utility::zero()); + 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(xOld(), xNew(), xNew(), [&dir] (ValueType const& a, ValueType const& b) -> ValueType { - if(a > b) return a; - else return b; - }); } template bool GameViHelper::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(), "Did not expect a non-positive threshold."); auto x1It = xOld().begin(); @@ -113,43 +115,6 @@ namespace storm { return true; } - template - void GameViHelper::performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& 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 - void GameViHelper::performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* 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 void GameViHelper::setProduceScheduler(bool value) { _produceScheduler = value; @@ -166,8 +131,8 @@ namespace storm { } template - void GameViHelper::updateStatesOfCoaltion(storm::storage::BitVector newStatesOfCoaltion) { - _statesOfCoalition = newStatesOfCoaltion; + void GameViHelper::updateStatesOfCoalition(storm::storage::BitVector newStatesOfCoalition) { + _statesOfCoalition = newStatesOfCoalition; } template diff --git a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h b/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h index 393f8a79a..507eb60b7 100644 --- a/src/storm/modelchecker/rpatl/helper/internal/GameViHelper.h +++ b/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& x, std::vector b, storm::solver::OptimizationDirection const dir); - - /*! - * Perform value iteration until upper bound - */ - void performValueIterationUpperBound(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, uint64_t upperBound, std::vector& constrainedChoiceValues); + void performValueIteration(Environment const& env, std::vector& x, std::vector b, storm::solver::OptimizationDirection const dir, std::vector& 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 extractScheduler() const; @@ -68,11 +63,6 @@ namespace storm { */ void performIterationStep(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - /*! - * Performs one iteration step for value iteration with upper bound - */ - void performIterationStepUpperBound(Environment const& env, storm::solver::OptimizationDirection const dir, std::vector* choices = nullptr); - /*! * Checks whether the curently computed value achieves the desired precision */ diff --git a/src/storm/solver/Multiplier.cpp b/src/storm/solver/Multiplier.cpp index 2324b7833..e5df00b05 100644 --- a/src/storm/solver/Multiplier.cpp +++ b/src/storm/solver/Multiplier.cpp @@ -92,8 +92,13 @@ namespace storm { template void Multiplier::reduce(Environment const& env, OptimizationDirection const& dir, std::vector const& choiceValues, std::vector::index_type> rowGroupIndices, std::vector& 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); diff --git a/src/storm/storage/PostScheduler.cpp b/src/storm/storage/PostScheduler.cpp index 2e4392891..92a81b434 100644 --- a/src/storm/storage/PostScheduler.cpp +++ b/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; diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp index a7acff700..08bf13d65 100644 --- a/src/storm/storage/Scheduler.cpp +++ b/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 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' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<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' = "<memoryStructure->getSuccessorMemoryState(memoryState, entryIt - model->getTransitionMatrix().begin()) <<")"; - // out << "model state' = " << entryIt->getColumn() << ": (transition = " << entryIt - model->getTransitionMatrix().begin() << ") -> " << "(m' = "<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' = "<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) { diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp index 228fb4604..08161b04e 100644 --- a/src/storm/storage/SparseMatrix.cpp +++ b/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); diff --git a/src/test/storm/CMakeLists.txt b/src/test/storm/CMakeLists.txt index 4fc60ab16..9adda6440 100755 --- a/src/test/storm/CMakeLists.txt +++ b/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() \ No newline at end of file diff --git a/src/test/storm/logic/FragmentCheckerTest.cpp b/src/test/storm/logic/FragmentCheckerTest.cpp index c0f10a5ed..3583ac019 100644 --- a/src/test/storm/logic/FragmentCheckerTest.cpp +++ b/src/test/storm/logic/FragmentCheckerTest.cpp @@ -12,16 +12,16 @@ TEST(FragmentCheckerTest, Propositional) { storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("true | \"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("!true")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prop)); @@ -42,10 +42,10 @@ TEST(FragmentCheckerTest, Pctl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification pctl = storm::logic::pctl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, pctl)); @@ -63,19 +63,19 @@ TEST(FragmentCheckerTest, Prctl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification prctl = storm::logic::prctl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); @@ -84,25 +84,34 @@ 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(" Pmax=? [\"label1\" U [5,7] \"label2\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmax=? [G \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" Pmin=? [F <5 \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, prctl)); } TEST(FragmentCheckerTest, Csl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csl = storm::logic::csl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, csl)); @@ -114,25 +123,25 @@ TEST(FragmentCheckerTest, Csrl) { auto expManager = std::make_shared(); storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification csrl = storm::logic::csrl(); - + storm::parser::FormulaParser formulaParser(expManager); std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F P=? [F \"label\"]]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [F \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("R=? [C<=3]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F[0,1] \"label\"]")); EXPECT_TRUE(checker.conformsToSpecification(*formula, csrl)); } @@ -140,32 +149,66 @@ TEST(FragmentCheckerTest, Csrl) { TEST(FragmentCheckerTest, MultiObjective) { storm::logic::FragmentChecker checker; storm::logic::FragmentSpecification multiobjective = storm::logic::multiObjective(); - + storm::parser::FormulaParser formulaParser; std::shared_ptr formula; - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("\"label\"")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("P=? [F \"label\"]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [(F \"label1\") & G \"label2\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("Pmax=? [ F multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"label\" & R<=4[F \"label\"]])]")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\"], R<=4[F \"label\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C<=3 ], P<0.6 [F \"label\"], R<=4[F \"label\"])")); EXPECT_FALSE(checker.conformsToSpecification(*formula, multiobjective)); - + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("multi(R<0.3 [ C ], P<0.6 [F \"label\" & \"otherlabel\"], P<=4[\"label\" U<=42 \"otherlabel\"])")); EXPECT_TRUE(checker.conformsToSpecification(*formula, 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::logic::FragmentChecker checker; + storm::logic::FragmentSpecification rpatl = storm::logic::rpatl(); + + storm::parser::FormulaParser formulaParser(expManager); + std::shared_ptr formula; + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> 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("<> Rmax=? [ LRA ]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString("<> 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(" <<1,2,3,4,5>> Pmax=? [\"label1\" U [0,7] \"label2\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmax=? [G \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(" <> Pmin=? [G \"label\"]")); + EXPECT_TRUE(checker.conformsToSpecification(*formula, rpatl)); + } diff --git a/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp new file mode 100644 index 000000000..7fda8f70c --- /dev/null +++ b/src/test/storm/modelchecker/prctl/mdp/ShieldGenerationMdpPrctlModelCheckerTest.cpp @@ -0,0 +1,198 @@ +#include +#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(1e-8)); + return env; + } + }; + + template + 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::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair>, std::vector>> 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(program, result.second)->template as>(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(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 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> 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(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(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(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(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(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(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(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(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) +} diff --git a/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp new file mode 100644 index 000000000..b0f26f02b --- /dev/null +++ b/src/test/storm/modelchecker/rpatl/smg/ShieldGenerationSmgRpatlModelCheckerTest.cpp @@ -0,0 +1,280 @@ +#include +#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(1e-8)); + return env; + } + }; + + template + 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::vector>> buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair>, std::vector>> 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(program, result.second)->template as>(); + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(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 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> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[1] + ", PreSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[2] + ", PreSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[3] + ", PreSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[4] + ", PostSafety, lambda=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[5] + ", PostSafety, lambda=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[6] + ", PostSafety, gamma=0.9> <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <" + fileNames[7] + ", PostSafety, gamma=0.9> <> Pmin=? [ F <=3 \"target\" ]"; + + formulasString += "; <" + fileNames[8] + ", PreSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[9] + ", PreSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[10] + ", PreSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[11] + ", PreSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[12] + ", PostSafety, lambda=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[13] + ", PostSafety, lambda=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[14] + ", PostSafety, gamma=0.5> <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <" + fileNames[15] + ", PostSafety, gamma=0.5> <> Pmin=? [ F <=5 \"target\" ]"; + + 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 result; + storm::modelchecker::SparseSmgRpatlModelChecker> 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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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(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) +} diff --git a/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp b/src/test/storm/modelchecker/rpatl/smg/SmgRpatlModelCheckerTest.cpp new file mode 100644 index 000000000..d8e9217dc --- /dev/null +++ b/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 ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(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 ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(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 ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(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 ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().minMax().setMethod(storm::solver::MinMaxMethod::ValueIteration); + env.solver().minMax().setPrecision(storm::utility::convertNumber(1e-10)); + env.solver().minMax().setMultiplicationStyle(storm::solver::MultiplicationStyle::Regular); + env.solver().multiplier().setType(storm::solver::MultiplierType::Native); + return env; + } + }; + + template + class SmgRpatlModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Smg SparseModelType; + + SmgRpatlModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + + template + typename std::enable_if::value, std::pair, std::vector>>>::type + buildModelFormulas(std::string const& pathToPrismFile, std::string const& formulasAsString, std::string const& constantDefinitionString = "") const { + std::pair, std::vector>> 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(program, result.second)->template as(); + } + return result; + } + + std::vector> getTasks(std::vector> const& formulas) const { + std::vector> result; + for (auto const& f : formulas) { + result.emplace_back(*f); + } + return result; + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == SmgEngine::PrismSparse) { + return std::make_shared>(*model); + } else { + STORM_LOG_ERROR("TestType::engine must be PrismSparse!"); + return nullptr; + } + } + + ValueType getQuantitativeResultAtInitialState(std::shared_ptr> const& model, std::unique_ptr& result) { + auto filter = getInitialStateFilter(model); + result->filter(*filter); + return result->asQuantitativeCheckResult().getMin(); + } + + private: + storm::Environment _environment; + + std::unique_ptr getInitialStateFilter(std::shared_ptr> const& model) const { + if (isSparseModel()) { + return std::make_unique(model->template as()->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 = "<> Pmax=? [X \"s2\"]"; + formulasString += "; <> Pmin=? [X \"s2\"]"; + formulasString += "; <> Pmax=? [X !\"s1\"]"; + formulasString += "; <> Pmin=? [X !\"s1\"]"; + // UNTIL tests + formulasString += "; <> Pmax=? [ a=0 U a=1 ]"; + formulasString += "; <> Pmin=? [ a=0 U a=1 ]"; + formulasString += "; <> Pmax=? [ b=0 U b=1 ]"; + formulasString += "; <> Pmin=? [ b=0 U b=1 ]"; + // GLOBALLY tests + formulasString += "; <> Pmax=? [G !\"s3\"]"; + formulasString += "; <> Pmin=? [G !\"s3\"]"; + formulasString += "; <> Pmax=? [G a=0 ]"; + formulasString += "; <> Pmin=? [G a=0 ]"; + // EVENTUALLY tests + formulasString += "; <> Pmax=? [F \"s3\"]"; + formulasString += "; <> Pmin=? [F \"s3\"]"; + formulasString += "; <> Pmax=? [F [3,4] \"s4\"]"; + formulasString += "; <> 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 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 = "<> Pmax=? [ G !\"hacked\" ]"; + + // bounded F + formulasString += "; <> Pmin=? [ F \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [1,2] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [3,16] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [0,17] \"hacked\" ]"; + formulasString += "; <> Pmin=? [ F [17,31] \"hacked\" ]"; + formulasString += "; <> 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 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 = "<> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=5 \"target\" ]"; + formulasString += "; <> Pmax=? [ F <=3 \"target\" ]"; + formulasString += "; <> 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 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 = " <> Pmax=? [ G<1 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=1 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=5 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=6 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=7 !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G<=8 !\"crash\" ]"; + + formulasString += "; <> Pmax=? [ G[1,5] !\"crash\" ]"; + formulasString += "; <> Pmax=? [ G[5,6] !\"crash\" ]"; + formulasString += "; <> 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 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) +} diff --git a/src/test/storm/parser/GameFormulaParserTest.cpp b/src/test/storm/parser/GameFormulaParserTest.cpp new file mode 100644 index 000000000..bdb551e53 --- /dev/null +++ b/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 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 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 = "<> Pmax=? [\"a\" U \"b\"]"; + std::shared_ptr 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 manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("a"); + storm::parser::FormulaParser formulaParser(manager); + + std::string input = "<

> Pmax=? [X \"a\"]"; + std::shared_ptr 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 = "<> 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 = "<> 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 = "<

> Pmax=? [\"a\" U \"b\"]"; + std::shared_ptr 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 = "<

> 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 = "<> 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 = "<> Rmin<0.9 [F \"a\"]"; + std::shared_ptr 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 = "<> 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 = "<> P<0.9 [F \"a\" || F \"b\"]"; + std::shared_ptr 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 = "<> P<0.9 [F X \"a\"]"; + std::shared_ptr 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<=0.5 [ F \"a\" ] The next line contains the actual formula. \n<

> P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment."; + std::shared_ptr 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 manager(new storm::expressions::ExpressionManager()); + manager->declareBooleanVariable("x"); + manager->declareIntegerVariable("y"); + + storm::parser::FormulaParser formulaParser(manager); + std::string input = "<> P>0.5 [ a ]"; + std::shared_ptr formula(nullptr); + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<

> P=0.5 [F \"a\"]"; + STORM_SILENT_EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException); + + input = "<> 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); +} diff --git a/src/test/storm/parser/GameShieldingParserTest.cpp b/src/test/storm/parser/GameShieldingParserTest.cpp new file mode 100644 index 000000000..53ae456a7 --- /dev/null +++ b/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 + "> <> Pmax=? [F \"label\"]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr 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 + "> <> Pmin=? [X !\"label\"]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr 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 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> <> Pmax=? [G x>y]"; + + std::shared_ptr formula(nullptr); + ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input)); + EXPECT_TRUE(formula->isGameFormula()); + + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr 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()); +} \ No newline at end of file diff --git a/src/test/storm/parser/MdpShieldingParserTest.cpp b/src/test/storm/parser/MdpShieldingParserTest.cpp new file mode 100644 index 000000000..2baf68f30 --- /dev/null +++ b/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 formula(nullptr); + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr 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 formula(nullptr); + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr 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 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 formula(nullptr); + std::vector property; + ASSERT_NO_THROW(property = formulaParser.parseFromString(input)); + EXPECT_TRUE(property.at(0).isShieldingProperty()); + + std::shared_ptr 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()); +} \ No newline at end of file diff --git a/src/test/storm/parser/PrismParserTest.cpp b/src/test/storm/parser/PrismParserTest.cpp index b9ed393b4..b28f94f0d 100644 --- a/src/test/storm/parser/PrismParserTest.cpp +++ b/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) { @@ -23,16 +24,16 @@ TEST(PrismParser, SimpleTest) { b : bool; [a] true -> 1: (b'=true != false = b => false); endmodule)"; - + storm::prism::Program result; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); EXPECT_EQ(storm::prism::Program::ModelType::DTMC, result.getModelType()); EXPECT_FALSE(result.hasUnboundedVariables()); - + testInput = R"(mdp - + module main x : [1..5] init 1; [] x=1 -> 1:(x'=2); @@ -51,21 +52,21 @@ TEST(PrismParser, SimpleTest) { TEST(PrismParser, ComplexTest) { std::string testInput = R"(ma - + const int a; const int b = 10; const bool c; const bool d = true | false; const double e; const double f = 9; - + formula test = a >= 10 & (max(a,b) > floor(e)); formula test2 = a+b; formula test3 = (a + b > 10 ? floor(e) : h) + a; - + global g : bool init false; global h : [0 .. b]; - + module mod1 i : bool; j : bool init c; @@ -74,25 +75,25 @@ TEST(PrismParser, ComplexTest) { [a] test&false -> (i'=true)&(k'=1+1) + 1 : (k'=floor(e) + max(k, b) - 1 + k); [b] true -> (i'=i); endmodule - + module mod2 [] (k > 3) & false & (min(a, 0) < max(h, k)) -> 1-e: (g'=(1-a) * 2 + floor(f) > 2); endmodule - + module mod3 = mod1 [ i = i1, j = j1, k = k1 ] endmodule - + label "mal" = max(a, 10) > 0; - + rewards "testrewards" [a] true : a + 7; max(f, a) <= 8 : 2*b; endrewards - + rewards "testrewards2" [b] true : a + 7; max(f, a) <= 8 : 2*b; endrewards)"; - + storm::prism::Program result; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(storm::prism::Program::ModelType::MA, result.getModelType()); @@ -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) { @@ -109,7 +147,7 @@ TEST(PrismParser, UnboundedTest) { b : int; [a] true -> 1: (b'=b+1); endmodule)"; - + storm::prism::Program result; EXPECT_NO_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile")); EXPECT_EQ(1ul, result.getNumberOfModules()); @@ -186,119 +224,119 @@ TEST(PrismParser, IllegalInputTest) { const int a; const bool a = true; - + module mod1 c : [0 .. 8] init 1; - [] c < 3 -> 2: (c' = c+1); + [] c < 3 -> 2: (c' = c+1); endmodule )"; - + storm::prism::Program result; STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + const int a; - + module mod1 a : [0 .. 8] init 1; - [] a < 3 -> 1: (a' = a+1); + [] a < 3 -> 1: (a' = a+1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + const int a = 2; formula a = 41; - + module mod1 c : [0 .. 8] init 1; - [] c < 3 -> 1: (c' = c+1); + [] c < 3 -> 1: (c' = c+1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + const int a = 2; - + init c > 3 endinit - + module mod1 c : [0 .. 8] init 1; - [] c < 3 -> 1: (c' = c+1); + [] c < 3 -> 1: (c' = c+1); endmodule - + init c > 3 endinit )"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c < 3 -> 1: (c' = c+1); endmodule - + module mod2 [] c < 3 -> 1: (c' = c+1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c < 3 -> 1: (c' = c+1)&(c'=c-1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c < 3 -> 1: (c' = true || false); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c + 3 -> 1: (c' = 1); endmodule)"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); - + testInput = R"(dtmc - + module mod1 c : [0 .. 8] init 1; [] c + 3 -> 1: (c' = 1); endmodule - + label "test" = c + 1; - + )"; - + STORM_SILENT_EXPECT_THROW(result = storm::parser::PrismParser::parseFromString(testInput, "testfile"), storm::exceptions::WrongFormatException); }