On 01.10.2015 14:12, Jaak Ristioja wrote:
>> "Errors detected: No errors" sounds as if the Toolbox parser/error
>> > detection is broken. What number does it show for unexplored states
>> > ("Queue size") then?
>
> It was something above 600000. I guess next time I should check that its
> zero. The problem is that from the perspective of a TLA+ Toolbox user
> the "No errors" message makes it is too easy to incorrectly conclude
> that the model-checking completed successfully when in fact it was
> incomplete. I feel this warrants a better notification than a non-zero
> value in a cell in the statistics table.
Hi Jaak,
the next Toolbox will better warn about an incomplete state space
exploration (see the attached screenshot).
Thanks
Markus
Attachment:
SpaceExplorationIncomplete.png
Description: PNG image
