Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Pass LP results for multi-objective achievability queries #244

Open
wants to merge 1 commit into
base: master
Choose a base branch
from

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