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

Re: Stuttering state when fairness specified

Is the next version 1.4.9? I tried to download it from https://tla.msr-inria.inria.fr/tlatoolbox/ci/products/, same result.

This is a modification of the Alternating Bit Protocol, except the sender only has finite number of messages (PckCount) to send, and the channels (msgC, ackC) are reliable, they can not lose messages.

The liveness  condition is <>(pc["R"]="Done"); i.e. the Receiver eventually receives all messages and finishes

The model checker should not generate infinite number of states for this spec, all the state variables are bounded: All the integer variables are bounded by range 0..PckCount. PckCount is a constant, and I give it a value 10 to the model checker. I also tell the model checker to restrict the length of the two tuples (msgC and ackC) to 10. element of those two tuples can only be in 0..(PckCount-1).