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

Re: [tlaplus] Where is the code for the state space traversal algorithm in TLC?

On 29 Sep 2022, at 11:16 pm, Gareth Smith <anythingwithawire@xxxxxxxxx> wrote:
> I haven't worked in TLA+ (yet) but designed a lot of state machine architectures for industrial controls and safety systems and the real art is system and sub-system decomposition, but getting this right is the key to avoiding state explosions.
> ...
> As I said, the system/subsystem decomposition is where the black art is and it seems surprisngly difficult to teach/artitculate a general methodology, it seems to something you learn like German, one day you are all at sea and then one day all of a sudden the word order just sort of clicks,
> Hope this is helpful.

Excellent insights Gareth. I wish you would write an article series on the design patterns you've used.

Clifford Heath.

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/763FFAF7-1538-44B4-9534-7FA8FA689915%40gmail.com.