Modeling an object oriented design

[Imran Meah]

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 design

Next 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?  

[Alex Weisberger]

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.

[Imran Meah]

Alex, 

Thanks, I wasn't aware TLA+ has visualization functionality. I will check it out.

[recepient recepient]

Long time programmer here learning TLA+ ... I agree with Alex's assessment: TLA+ is not best used to model UML or static class diagrams. In fact unless I was working on cache coherence or a router algorithm fairly single threaded --- extremely combinatorial and difficult algos --- or distributed systems on the other extreme, I'd prefer to rely on Hoare logic, Frama-C, unit & integration testing. TLA+ is good for when (*) you have communication sequential  systems has you have no idea if your exactly-once-message-processing strategy works or, whoops, it hadn't occurred to one that was a real issue. See https://github.com/rodgarrison/tla_note1 "A Note on Formal Specification for Programmers." 

[Younes]

@Alex : I'm using the official TLA+ toolbox, and I cannot find how to export the state space, nor how to get a visualization. Could you help?

[Alex Weisberger]

In your Model Overview, you should see a link to "Additional TLC Options." Once there, you can expand the "Features" section, and there is a checkbox for "Visualize the state graph after completion of model checking" which you should check. I attached an image of that last part.

Note, TLC assumes you have a working graphviz installation that is accessible via the "dot" command. You will have to handle installing that and making sure it's accessible in your path (I'm most familiar with Unix environments). If you need to use a different command, you can go to Preferences -> TLA+ Preferences -> PDF Viewer and there is a field named "Specify dot command." This is the command that TLC will use to generate the state graph.

Best of luck.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/bceb43ca-007e-447e-8d07-743ed0c6546en%40googlegroups.com.

--

- Alex Weisberger, Senior Software Engineer: House Manage