Design Validation using TLA+/TLC Model checker

[I Made Putrama]

Hello,

I'm trying to develop a specification for a distributed system. When I use some temporal properties in the specification and run the model checker, it runs successfully without any issues/errors. However, I have a question: how do I know/validate that the design I made has been proper or optimal? For example, my system design consists of uploading and downloading shared files. I simulated several scenarios with a different number of files, e.g., 10, 20, 50, and 100, the termination state was reached and the files were all successfully consumed by several downloaders. I see that the number of states being executed is proportional to the number of files being processed. But how to tell whether the design has been optimal? How do I measure that based on the TLC model checker's results?
In addition, if I want to compare several different approaches/designs for the same system and measure how good their performance is, can this be achieved by analyzing the results of the TLC model checker? If yes, what could be considered to determine whether one design has better performance than the others? Thank you for your attention and I really appreciate your opinion and suggestions.

Best regards,
Putrama

[Gareth Smith]

Yes I am interested to understand how issues of synchronicity and asynchronicity are managed in this context where some logic is running on a different processor and the relative sequence of execution is not guaranteed.

It seems best (only?) option is to run some kind of semaphore that signals "don't start before" to have relative known sequence of execution, if you think you need to care.

--
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/31b5948c-4694-4004-a376-7561ce6ba785n%40googlegroups.com.

[I Made Putrama]

Hello Gareth Smith,

Thanks for taking the time to answer my doubts. I really appreciate it. Actually, I'm completely new to formal specification languages, especially TLA+ and I'm not aware of any special properties or operators I can use to achieve the semaphore as mentioned. But so far, I'm using the 'await' and 'fairness' keywords (https://learntla.com/core/concurrency.html?highlight=await) to make a process run only when certain conditions are met and ensure it always makes some progress. I'm not sure if this is what achieves the same 'semaphore'.

My curiosity is mostly in the results of the TLC model checker and how to interpret them against the efficiency or effectiveness of my model. When I run my specs for validation, it ends successfully with statistical results. However, I don't quite understand how to interpret the results yet. Does that mean when I have two different approaches to modeling the system, the one that runs faster and explores less state will be considered the better design? Also, in statistics, there are several columns: Diameter, Status Found, Distinct States, Queue Size, etc. But I can only find a simple explanation here (https://learntla.com/reference/standard-library.html?highlight=diameter) and it is not so detailed, or am I missing a specific location / URL that talks about them?

Regards,

Putrama

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/Mhf3EEmMVmE/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CALDKJw0OGrkTKw1gP%3D63JVV_%2Bq%3DDMSJqw47FU37yhheJM5Sf1A%40mail.gmail.com.