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

[Clifford Heath <clifford.heath@xxxxxxxxx>]

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.