toy strong fairness PlusCal example

[jack malkovick]

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

[Stephan Merz]

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

On 19 Mar 2025, at 15:52, jack malkovick <sillym...@gmail.com> wrote:

I have this simple SF PlusCal example

<trace1.png>

--
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+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/0075d026-4233-4758-9e39-89136257f118n%40googlegroups.com.

<trace1.png>

[jack malkovick]

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

[Hillel Wayne]

Here's one way you could do it purely through PlusCal:

(* --algorithm Test
variables jobActive = FALSE;

  jobActivating = FALSE;

fair process Job="Job"
begin

    Startup:
    while ~jobActive do
        jobActivating := ~jobActivating;
    end while;
end process;

fair+ process JobActivate="JA"
begin
    ActivateJob:
    await jobActivating;
    jobActive := TRUE;
end process;
end algorithm; *)

Here ActivateJob isn't always enabled, so is only guaranteed to run due to the strong fairness guarantee. Note this is only a sketch, I haven't run it to test that it doesn't have syntax errors or anything.

H

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/1BD4C44E-1A0B-4C9F-9616-0A6E7ED40DBE%40gmail.com.

[jack malkovick]

Very cool example! It worked without changes. Thank you!

[Stephan Merz]

Apologies, I meant to write

SF_vars(initial /\ pc’ = “active”)

The variable jobActive is only set to TRUE in the subsequent transition.

Stephan

On 19 Mar 2025, at 16:47, jack malkovick <sillym...@gmail.com> wrote:

Makes sense! 

To view this discussion visit https://groups.google.com/d/msgid/tlaplus/f412682b-652c-4105-ac72-9749c1eee8f2n%40googlegroups.com.

[jack malkovick]

Yup! Thank you! Works fine

Spec == 

Init 

/\ [][Next]_vars 

/\ SF_vars(initial /\ pc'["Job"] = "active")