3 ms·

I wish this wasn't so focused on PlusCal

• hwayne 4y ago
  In my teaching experience, more people find it easier to start with PlusCal. That said, I plan to also add a lot of topics and examples that are pure TLA+.
• ahelwer 4y ago
  They're both good to know - PlusCal for concurrent programs with more sequential if/then/else/while/for-type logic, and TLA+ for more event-driven systems that receive inputs and react with few sequential steps. Lamport has published lots of resources on TLA+ itself. I learned from Specifying Systems. I've also seen the video course and it's pretty good.