F0 computation not terminating
6 views
Skip to first unread message
Paul Kobialka
Apr 8, 2024, 5:48:23 AMApr 8
to PRISM model checker
Dear Prism-games team,
when evaluating the expected minimal cost of only reaching a positive outcome, <<providerPlayer>>R{"gas_neg"}min=? [ F0 positive ], the computation does not terminate.
The ''last switching point" is set to 2147483647, and is not further updated within hours.
In my understanding, the game is a stopping game as it is almost surely guaranteed to reach a final state.
The model, query, and log are attached.
I'm using PRISM-games 3.2.1 on Linux64.
Thank you very much for your help.
Sincerely,
Paul
when evaluating the expected minimal cost of only reaching a positive outcome, <<providerPlayer>>R{"gas_neg"}min=? [ F0 positive ], the computation does not terminate.
The ''last switching point" is set to 2147483647, and is not further updated within hours.
In my understanding, the game is a stopping game as it is almost surely guaranteed to reach a final state.
The model, query, and log are attached.
I'm using PRISM-games 3.2.1 on Linux64.
Thank you very much for your help.
Sincerely,
Paul
Reply all
Reply to author
Forward
0 new messages