Makes sense!
I've updated my PlusCal generated spec with
Spec == /\ Init /\ [][Next]_vars
/\ SF_vars(initial /\ jobActive')
but it fails in the same way
On Wednesday, March 19, 2025 at 5:40:59 PM UTC+2 Stephan Merz wrote:
The problem here is that a first atomic step corresponding to the “either” statement chooses between moving to the inactive or active label. Your strong fairness annotation for active has no effect beyond the weak fairness assumed at the top level because there is only one possible continuation. What you want is imposing strong fairness on the branch taken by the “either” statement. This cannot be expressed in PlusCal but you can achieve what you want by adding the fairness hypothesis
SF_vars(initial /\ jobActive’)
to the specification at the TLA+ level.
Stephan
I have this simple SF PlusCal example
(* --algorithm Test
variables jobActive = FALSE;
fair process Job="Job"
begin
initial:
while ~jobActive do
either
inactive:
jobActive := FALSE;
or
active:+
jobActive := TRUE;
end either;
end while;
end process;
end algorithm; *)
My expectation was that the spec will have this property
<>[][jobActive = TRUE]_vars
however it does not, the error trace is
--
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion visit
https://groups.google.com/d/msgid/tlaplus/f412682b-652c-4105-ac72-9749c1eee8f2n%40googlegroups.com.