Wrong result for p2p LTOL spec

[lou1306]

channels: c
message-structure: MSG : bool

agent Client
    local: counter : integer
    init: counter == 0
    receive-guard: (channel == *)

    repeat: ( 
            s: <TRUE> SUPPLY@two()[]
            +
            g: <TRUE> GET@one[]
            )
system = Client(one,TRUE) | Client(two,TRUE) | Client(three,TRUE)


SPEC G F <p2p == TRUE && sender == two> TRUE

Should be pass but returns fail with this counterexample:

WARNING: single-value variable 'one-automaton-state' has been stored as a constant
WARNING: single-value variable 'two-automaton-state' has been stored as a constant
WARNING: single-value variable 'three-automaton-state' has been stored as a constant
-- no proof or counterexample found with bound 0
-- no proof or counterexample found with bound 1
-- LTL specification  G ( F ( X (obs0 & TRUE = TRUE)))  is false
-- as demonstrated by the following execution sequence
Trace Description: IC3 smt counterexample 
Trace Type: Counterexample 
  -> State: 1.1 <-
    obs0 = FALSE
    one-name = one
    one-counter = 0
    two-name = two
    two-counter = 0
    three-name = three
    three-counter = 0
    progress = TRUE
    one-s-three-g-progress = TRUE
    one-s-two-g-progress = TRUE
    falsify-three = TRUE
    falsify-not-three = TRUE
    falsify-two = TRUE
    falsify-not-two = TRUE
    falsify-one = TRUE
    falsify-not-one = TRUE
    one-automaton-state = 0
    two-automaton-state = 0
    three-automaton-state = 0
    no-observations = TRUE
    transition = TRUE
    one-s-three-g = TRUE
    one-s-two-g = TRUE
    keep-all = TRUE
    keep-all-three = TRUE
    keep-all-two = TRUE
    keep-all-one = TRUE
 
-- Loop starts here
  -> State: 1.2 <-
  -> State: 1.3 <-
  -> State: 1.4 <-

[lou1306]

This was dumb. I was resolving sender to the supplier and not the getter.