TLA+ : Model works, but income of requests is too heavy, have to model the system to be less charged