Skip to content

Conversation

@Chickenpowerrr
Copy link

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 line LP problem solution not found; result is 0.000000 stating that no solution could be found, but it also reports Result: 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 contains LP problem solution not found so result is false and Result: false instead, which is the correct answer.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant