More termination detection algorithms about examples

[lemmy]

Huang's algorithm has been added (https://github.com/tlaplus/Examples/tree/master/specifications/Huang). Additionally, we could try and find a refinement mapping s.t. Huang refines AsyncTerminationDetection.tla.

[muenchnerkindl]

Safe == []TerminationDetected => []Terminated

The algorithm even has the stronger property [](TerminationDetected => []Terminated) Stephan

…

On 26 Jan 2022, at 17:42, Markus Alexander Kuppe ***@***.***> wrote: Huang's algorithm has been added (https://github.com/tlaplus/Examples/tree/master/specifications/Huang <https://github.com/tlaplus/Examples/tree/master/specifications/Huang>). Additionally, we could check if Huang refines AsyncTerminationDetection.tla <https://github.com/tlaplus/Examples/blob/master/specifications/ewd998/AsyncTerminationDetection.tla>. — Reply to this email directly, view it on GitHub <#45 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABZCW5P63VBKZJDC4NG6SITUYAQBDANCNFSM5KRWNLBA>. Triage notifications on the go with GitHub Mobile for iOS <https://apps.apple.com/app/apple-store/id1477376905?ct=notification-email&mt=8&pt=524675> or Android <https://play.google.com/store/apps/details?id=com.github.android&referrer=utm_campaign%3Dnotification-email%26utm_medium%3Demail%26utm_source%3Dgithub>. You are receiving this because you are subscribed to this thread.

[lemmy]

Thanks: 5ef47ac

[lemmy]

A first attempt showing refinement of AsyncTerminationDetecting by Huang. It is not a refinement because ATD doesn't allow pending decrement when an inactive Leader in Huang receives the last weight back.

Node ==
    0..Cardinality(Procs) - 1

M == 
    CHOOSE f \in [ Node -> Procs ]: IsInjective(f)

ATD ==
    INSTANCE AsyncTerminationDetection 
    WITH
        terminationDetected <- TerminationDetected,
        active <- [ n \in Node |-> active[M[n]] ],
        pending <- [n \in Node |-> Len(msgs[M[n]]) ],
        N <- Cardinality(Procs)

ATDSpec == 
    ATD!Spec

THEOREM Spec => ATDSpec

Action property line 63, col 20 to line 63, col 32 of module AsyncTerminationDetection is violated.
The behavior up to this point is:
1: <Initial predicate>
/\ active = {L}
/\ weights = (L :> "1")
/\ msgs = << >>
/\ Terminated = FALSE
/\ TerminationDetected = FALSE
2: <SendMsg line 48, col 5 to line 53, col 27 of module Huang>
/\ active = {L}
/\ weights = (L :> "1/2")
/\ msgs = (L :> <<"1/2">>)
/\ Terminated = FALSE
/\ TerminationDetected = FALSE
3: <IdleLdr line 72, col 5 to line 74, col 33 of module Huang>
/\ active = {}
/\ weights = (L :> "1/2")
/\ msgs = (L :> <<"1/2">>)
/\ Terminated = FALSE
/\ TerminationDetected = FALSE
4: <RcvLdr line 78, col 5 to line 81, col 27 of module Huang>
/\ active = {}
/\ weights = (L :> "1")
/\ msgs = << >>
/\ Terminated = TRUE
/\ TerminationDetected = TRUE

[muenchnerkindl]

The definition of Wakeup(i) in AsyncTerminationDetection could be changed to

/\ pending[i] > 0
/\ / UNCHANGED active
/ ~ active[i] /\ active' = [active EXCEPT ![i] = TRUE]
/\ pending' = [pending EXCEPT ![i] = @ - 1]
/\ UNCHANGED terminationDetected

allowing an inactive receiver to either become active or remain passive. (It should then probably be renamed to Receive.)

[muenchnerkindl]

Ah, GitHub formatting ... maybe this works better:

/\ pending[i] > 0
/\ \/ UNCHANGED active
   \/ ~ active[i] /\ active' = [active EXCEPT ![i] = TRUE]
/\ pending' = [pending EXCEPT ![i] = @ - 1]
/\ UNCHANGED terminationDetected