Sorry for what? It was my first time using such a tool. I found it useful for understanding the system. I've improved my understanding of TLA+ since then and it has been valuable.