[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Debugging and checking the edge cases
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.
the Toolbox's trace explorer will help you figure out the problem
yourself. Lecture #3 of the TLA+ video course introduces this Toolbox
Hope this help,