# Hillel Wayne - Practical TLA+ (Highlights) ## Metadata **Source**:: #from/zotero **Authors**:: [[Hillel Wayne]] **Full Title**:: Practical TLA+: Planning Driven Development **Category**:: #books #readwise/books **Zotero App Link**:: [Open in Zotero](zotero://select/library/items/KC4C5CZF) ## Highlights - If we put the two assignments in the same label, they’d happen simultaneously. ([page 8](zotero://open-pdf/library/items/7KTX2AJJ?page=25&annotation=WFFPCEI5)) ^9cbab708 - Checking an expression will also evaluate your spec. If you don’t want to run it, you can switch it to “No Behavior spec” under Model Overview > What is the behavior Spec? ([page 25](zotero://open-pdf/library/items/7KTX2AJJ?page=42&annotation=ZYTGP4XK)) ^199f6c23 - In order to use assertions, you need to add EXTENDS TLC. ([page 30](zotero://open-pdf/library/items/7KTX2AJJ?page=47&annotation=9W5SZNXA)) ^e0cf61cd - Finally, to generate a set of structures, we use a different syntax. Instead of writing [key |-> val], we write [key: set]. Then if x \in [key: set], x is a structure where the value of key is some element of set. ([page 35](zotero://open-pdf/library/items/7KTX2AJJ?page=52&annotation=S89JXYA9)) ^2bbc8e31 - If you want to define an operator using the variables of a PlusCal algorithm, you can place it in a define block ([page 44](zotero://open-pdf/library/items/7KTX2AJJ?page=61&annotation=SNRYTYKS)) ^38a3996f - The PlusCal translator is very simple and everything needs to be in the right order. Definitions must go above macro definitions and below variable definitions. ([page 44](zotero://open-pdf/library/items/7KTX2AJJ?page=61&annotation=ASVQ8SV9)) ^1f56e6e5 - You can define anonymous operators with LAMBDA. ([page 45](zotero://open-pdf/library/items/7KTX2AJJ?page=62&annotation=J8JP83QG)) ^c2dc7b6c -  ^5eb9c38e - To use @@ we need EXTENDS TLC. ([page 55](zotero://open-pdf/library/items/7KTX2AJJ?page=72&annotation=HDRV3373)) ^852ff88e - The set of functions [1..3 -> S], then, are all the sequences where the first value is some element in S ([page 56](zotero://open-pdf/library/items/7KTX2AJJ?page=73&annotation=T7TCVQUK)) ^97c21b91 - Just to be thorough, I ran both of them individually and confirmed that BestKnapsacksTwo was indeed faster for a capacity of 7. ([page 63](zotero://open-pdf/library/items/7KTX2AJJ?page=80&annotation=6MIGQGSJ)) ^d668e80a - You cannot have the set {TRUE, FALSE, "null"}, but you can have the set {TRUE, FALSE, NULL} if NULL is a model value. ([page 67](zotero://open-pdf/library/items/7KTX2AJJ?page=84&annotation=6XAPY46K)) ^fc9847c7 - If we’re assigning constants at the model level, we should have a way of making sure that you’ve got the right type of values. ([page 68](zotero://open-pdf/library/items/7KTX2AJJ?page=85&annotation=3AJ6GK6T)) ^e718450a - ASSUME may use constants and constant operators as part of the expression but may not use operators not defined as CONSTANT. ([page 68](zotero://open-pdf/library/items/7KTX2AJJ?page=85&annotation=5KW3AR9E)) ^7ca638cc - Simulation Mode will replace the methodical search with random traces. This is generally less effective but can sometimes be useful if you’ve validated the specification over a small state space and now want to stress test it with a very large state space. ([page 71](zotero://open-pdf/library/items/7KTX2AJJ?page=88&annotation=FUJ3M6RE)) ^d0dd09a3 - If you want to add detailed information in assertion, a fast way to do that is with a tuple or a struct ([page 73](zotero://open-pdf/library/items/7KTX2AJJ?page=90&annotation=YDJ2RGCB)) ^8e316ece - If you want something more polished, you can use the TLC helper ToString(_) ([page 73](zotero://open-pdf/library/items/7KTX2AJJ?page=90&annotation=XIYJ6PNP)) ^9c62ec67 - Like operators, you can prefix an instance with LOCAL to make it private to the module. ([page 75](zotero://open-pdf/library/items/7KTX2AJJ?page=92&annotation=A6LC7G7T)) ^766b6001 - PlusCal automatically defines a “Done” label at the end of every process. You cannot use “Done” as part of your own label, but you can jump to it with goto. ([page 79](zotero://open-pdf/library/items/7KTX2AJJ?page=96&annotation=S4LQ85SM)) ^e0c00424 - PlusCal has the || operator. You can combine two assignments with || and they will be evaluated simultaneously. ([page 80](zotero://open-pdf/library/items/7KTX2AJJ?page=97&annotation=W9LURBLV)) ^a303e273 - await Expression prevents a step from running until Expression is true. You can also use the keyword when. ([page 82](zotero://open-pdf/library/items/7KTX2AJJ?page=99&annotation=5LUD6JRV)) ^5d3214d1 - Macros cannot contain labels, so we cannot use them for this purpose. Our final piece of PlusCal syntax, procedures, addresses this use case ([page 85](zotero://open-pdf/library/items/7KTX2AJJ?page=102&annotation=ZST3PBSA)) ^b748bf04 - Procedures must be defined after macros and before processes. ([page 86](zotero://open-pdf/library/items/7KTX2AJJ?page=103&annotation=RD8PDIAA)) ^5460f28d - using symmetry sets is often a good first-pass optimization for your slower specs. ([page 92](zotero://open-pdf/library/items/7KTX2AJJ?page=109&annotation=GZ4LDE5Y)) ^1c12672a