Counter abstractions in model checking of distributed broadcast algorithms: some case studies