Re: [tlaplus] Some distributed TLC errors not displayed in TLA+ Toolbox

[Jaak Ristioja <jaak.r...@xxxxxxxx>]

On 08.10.2015 13:41, Markus Alexander Kuppe wrote:
> 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
> 

Nice. Thanks! :)

Jaak