Interference

object intf = {
    action ping
    action pong
}

type side_t = {left,right}

object spec = {
    individual side : side_t
    init side = left

    before intf.ping {
    assert side = left;
    side := right
    }

    before intf.pong {
    assert side = right;
    side := left
    }
}

object left_player = {
    individual ball : bool
    init ball

    action hit = {
    if ball {
        call intf.ping;
        ball := false
    }
    }

    implement intf.pong {
    ball := true
    }

}

object right_player = {
    individual ball : bool
    init ~ball

    action hit = {
    if ball {
        call intf.pong;
        ball := false
    }
    }

    implement intf.ping {
    left_player.ball := true
    }

}


export left_player.hit
export right_player.hit

isolate iso_l = left_player with spec
isolate iso_r = right_player with spec