[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Re: Modelling a REST API server in TLA+ - suggestions/examples

First, you should produce the finite state machine according to the logical architecture of your system, which usually described by UML interaction and State diagrams.

Then try to define the state variables of each objects in the interaction course, which can be obtained by refinning the key attributes of the corresponding classes.

So far, you will get a vivid description in your mind about how the state machine of each object transited according to the interactions, 

now you can easily depicts this event driven discret system by TLA+.

You can get some exmaple from Specifying System  

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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/99d0cc9d-5e06-469e-a362-8e6d8ba1152c%40googlegroups.com.