TLA+ encourages algorithmic thinking which is independent of any programing language or paradigm. So I would focus on:- what are the state variables of your algorithm. These get encoded in TLA+ via VARIABLES- what are the allowed transitions between states. These are the actions, i.e. v' = <new value>These concepts are all you need to model an algorithm.Re visualization: When you create a model for your spec, there is an option to export the discovered state space as a graphviz state diagram. I use this all the time to get an understanding of the state space of the algorithm. Of course, be careful, because some state spaces can be very large. In that case, the program will be unable to export the diagram, or if it can it will be unreadable.In this case, try and create a model which is bounded by some configurable CONSTANTS which you can create more or less of in your model.On Tuesday, December 1, 2020 at 11:43:12 PM UTC-5 imran...@xxxxxxxxx wrote:There used by a modeling language called LePUS3 (https://en.wikipedia.org/wiki/LePUS3) which was used to formally model object oriented design. It was popular in 2000s but seems to have disappeared about 10 years ago.With that I am exploring using TLA+ for formally modeling an object oriented design.The way I see it should be workable solution.Class/Object are represented as data structure , I think we call them record in TLA+.Define transition rules that will mutate this object.So far, I am still pondering how to model a class instantiation as in creation of an object from class. I guess if it is singleton pattern, it wouldn't matter.My goals:to start with -Use TLA+ as tool to understand complex object oriented designNext step-Try modeling checking some invariants.Would be nice- To visualize the model in some form of diagram.What I am looking for:Is TLA+ suitable for object oriented modeling/specification. Is there precedent for this application?