It's better for modeling sequential algorithms. Like if you want to define a system that does one thing, then does another thing, then some more things, then maybe branches or loops back around. It's hard to explicitly draw boundaries between when it's easier to use TLA+ vs. PlusCal but it has to do with the number of sequential actions taken in each loop of your system. This is a lesson that's best learned when trying to specify a sequential algorithm in TLA+; you basically end up writing the code PlusCal would generate, by hand.
On Friday, February 18, 2022 at 2:21:05 PM UTC-5 saleemk...@xxxxxxxxx wrote:
I tried learning PlusCal but found it cumbersome compared to TLA+.I can read TLA+ specifications and really enjoy it. Is there any advantage to learning pluscal?