| Hi Shuai, I had a quick look at your spec, and I am not surprised that TLC blows up on it. Yes, it does "brutal search" of the state space, enumerating the reachable states, creating successor states by trying to evaluate all actions on every state it has seen so far. What you have seen is the well-known problem of combinatorial explosion (i.e., exponential growth of the state space) as you add more processes. PlusCal labels define the atomic actions of your spec: the more you have, the more fine-grained your transitions are and the more states you'll generate. On the other hand, inserting fewer labels may mask problems due to concurrent execution of actions that access shared variables. Fortunately, exhaustive search tends to find errors in very small configurations because TLC explores states that are extremely unlikely to occur in actual executions. You should therefore ask yourself what are the smallest meaningful configurations that give you confidence in the correctness of the overall system. Also, can you tear apart your algorithm and verify pieces independently of the rest? (Your description seems to say that this is difficult.) Finally, it looks like you "only" verify the liveness property <>SrzAcyclic(srz). Liveness checking takes more time than invariant checking, and I'd try to think of invariant properties (describing relations among variables that you expect to hold) and have TLC check those as well. If exhaustive search is taking too long, you may consider doing random exploration (see Advanced Options -> TLC Options -> Simulation mode) which may find deeper invariant violations more quickly than standard breadth-first exploration. Regards, Stephan
|