Re: [tlaplus] Debugging and checking the edge cases

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 17.08.2018 05:23, s.triv...@xxxxxxxxx wrote:
>    When I am model checking the following program x_account is going negative how to resolve that problem and also how to check the edge cases and how to use invariants and properties in model checking.
>   Can you please figerout the problem in the following code.

Hi,

the Toolbox's trace explorer will help you figure out the problem
yourself.  Lecture #3 of the TLA+ video course introduces this Toolbox
feature [1].

Hope this help,
Markus

[1] https://lamport.azurewebsites.net/video/video3.html