--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/119e0b62-07c6-404b-89f9-a5f1f698ccb5%40googlegroups.com.
Hi Jam,
As of 1.6.0, you can access the diameter, level, etc during model checking via TLCGet. See https://github.com/tlaplus/tlaplus/blob/9dce6c7404552d70f728332c85aaa3af2aed719a/tlatools/src/tlc2/module/TLC.java#L168-L212. You can use this to constrain the model to help with debugging. I'd recommend using the -dump switch and then running the dump through a dedicated graph viewer.
H
Hi,You can set the profiling option equal to "on" in TLC's advanced options so that you can observe how many times each action in your spec is being taken.You may try making small edits in your spec and see how the model checking makes progress with each change. This is a lovely little cat and mouse game that you will have to solve.As another means of "debugging" your spec, you may define and set an invariant in your spec and let TLC check it. You then can violate this invariant deliberately at certain points in your spec that you suspect may be the source of error. This will cause TLC to print a useful sequence of states that may help you catch the error.During the process of model checking, if the queue of states keeps growing at a steady rate for a considerably long amount time, then there is a high probability that your spec has an error.Regards,AmirHossein
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.