Skip to content

Commit 8a420d6

Browse files
committed
param/exact: Fix Pmax/Pmin [ ! (F a) ] / [ !( a U b) ] computation
Switching between max and min when removing the negation was missing for MDPs. Test case: prism functionality/verify/mdps/ltl/simple_ltl.nm functionality/verify/mdps/ltl/simple_ltl.nm.props -exact -prop 3 from prism-tests.
1 parent 9bc5baa commit 8a420d6

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

prism/src/param/ParamModelChecker.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -903,6 +903,7 @@ private RegionValues checkProbPathFormulaSimple(ParamModel model, Expression exp
903903
if (expr instanceof ExpressionUnaryOp &&
904904
((ExpressionUnaryOp)expr).getOperator() == ExpressionUnaryOp.NOT) {
905905
negated = true;
906+
min = !min;
906907
expr = ((ExpressionUnaryOp)expr).getOperand();
907908
}
908909

0 commit comments

Comments
 (0)