Study Group 2021.03.19

Reading Notes

Configuring VS Code toolbox

• https://marketplace.visualstudio.com/items?itemName=BRBoer.vsc-conceal
• https://marketplace.visualstudio.com/items?itemName=alygin.vscode-tlaplus

I tried the ligatures and conceal with Alex's Configuration features. I felt the source was lying to me (a related opinion. It reminded me of confluenza's editor that transformed wiki text in real-time. It makes the cursor behave weird and I don't think its something I personally could get used to. Similarly, I don't like editors who render markdown in real-time either.

Overriding the Int in VsCode TLC

TLC has a limited understand of TLA+ syntax. Thus to use the TLC checker outside the toolbox you need to use extend the spec to provide extra definitions for TLC.

Reference: https://stackoverflow.com/questions/59101827/how-can-i-set-constants-in-tla-configuration-file-when-using-vs-code

Alex's CRDT

Original CRDT ≜ Conflict Free Replicated Datatype

Interesting link while researching CRDTs: https://www.infoq.com/articles/cap-twelve-years-later-how-the-rules-have-changed/

Discussion

Follow-up (Homework)