Verification under strategy

[Paul Kobialka]

Dear PRISM-team,
I generated a game with a binary outcome and costs.
My goal is to analyse the expected minimal cost of the strategy maximising the chances for a positive outcome.
When querying the expected minimal cost under this strategy is the result smaller than the established lower bound over all strategies.
The resulting cost of 7.5 seems to exclude the fixed player's cost.

Is this a bug or am I using the tool wrongly?

Attached is the model and the queries for a minimal example.
I am using PRISM-games 3.1 on Linux.

Thank you very much for your help.

Greetings,
Paul