Pass LP results for multi-objective achievability queries #244
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Right now, the results of a multi-objective achievability query can be returned as if it were a multi-objective numerical query when using the -lp flag. For this reason, the LP solver can state that the answer is true, even though the answer computed by the LP solver was false.
For example, on the MDP model.txt, we can evaluate the property:
multi(R{"hire"}>=4 [C], R{"money"}<=1000 [C])
which is unachievable. In this case the output contains the lineLP problem solution not found; result is 0.000000
stating that no solution could be found, but it also reportsResult: true
, which is incorrect. This happens because if there are no probabilistic reachability subgoals,relops[0]
does not exist. However, this invalid field is checked to determine whether the query is a numerical or achievability query and therefore can mistake an achievability query for a numerical query. With this fix, this field is not longer accessed if there are no probabilistic reachability subgoals, and thus the output containsLP problem solution not found so result is false
andResult: false
instead, which is the correct answer.