[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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).


Attachment: SpaceExplorationIncomplete.png
Description: PNG image