Termination

Will the following PlusCal snippet ever finish?

EXTENDS TLC, Integers

(* --algorithm counter
variable x = 0;
begin
  while x < 10 do
    x := x + 1;
  end while;
end algorithm; *)

The most common temporal logic you’ll want to check is Termination, and TLC provides a handy button to test just that.

This will succeed if, for all behaviors, the spec ends. Let’s see what happens when we run this:

Well, that was certainly unexpected! This is called stuttering. The problem is that the system can choose not to run any step at all. This has never been a problem before because we were making sure things didn’t break if time passed, but now things break if time doesn’t pass.

How do we get around this? What we want is something called fairness: the property that if a given label is always enabled, we will eventually run it. We make this happen by specifying the process as a fair process.

EXTENDS TLC, Integers

(* --algorithm counter
variable x = 0;

fair process counter = "counter"
begin Count:
  while x < 10 do
    x := x + 1;
  end while;
end process;

end algorithm; *)

Confirm this works as expected.