[tlaplus] toy strong fairness PlusCal example

[jack malkovick <sillymouse333@xxxxxxxxx>]

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/0075d026-4233-4758-9e39-89136257f118n%40googlegroups.com.