%%% Liveness++: each enabled input/output action will meet a
%%% corresponding output/input, and enable a corresponding
%%% synchronisation, within a finite number of reductions
%%%
%%% Copyright 2018 Alceste Scalas <alceste.scalas @ imperial.ac.uk>
%%% Released under the MIT License: https://opensource.org/licenses/MIT

nu Z.(forall s1: Session, r1,r2: Role .
  ((exists m1: Message, p1: Payload . <i(s1, r1, r2, m1, p1)>true) =>
    mu Y.(
      (exists m1: Message, p1: Payload . <t(s1, r1, r2, m1, p1)>true)
      ||
      (
        (exists s2: Session, r3,r4: Role, m2: Message, p2: Payload .
           <t(s2, r3, r4, m2, p2)>true)
        &&
        (forall s2: Session, r3,r4: Role, m2: Message, p2: Payload .
           [t(s2, r3, r4, m2, p2)]Y)
      )
    )
  )
  &&
  (forall m1: Message, p1: Payload .
    <o(s1, r1, r2, m1, p1)>true =>
      mu Y.(
        <t(s1, r1, r2, m1, p1)>true
        ||
        (
          (exists s2: Session, r3,r4: Role, m2: Message, p2: Payload .
             <t(s2, r3, r4, m2, p2)>true)
          &&
          (forall s2: Session, r3,r4: Role, m2: Message, p2: Payload .
             [t(s1, r3, r4, m2, p2)]Y)
        )
      )        
  )
  &&
  (forall m1: Message, p1: Payload . [t(s1, r1, r2, m1, p1)]Z)
)