Read me

The main to do

• TLA+の勉強
  • Specifying Systems(DONE)
  • Auxiliary Variables in TLA+
• GoogleGroupで読んだことの蓄積

Auxiliary Variables in TLA+

"Specifying Systems"では自分がわかっていなかった、Higher-SpecとLower-Specとの間のimplmentationについて学ぶことができるので、それをやる。

This paper explains rules for adding history,prophecy, and stuttering variables to TLA+ specications, ensuring that the augmented specication is equivalent to the original one.

The Others to do

~配信で使う資料の共有~ => 配信しなくても勉強が続いた。

Tips

To inspect the modules

How to inspect the standard modules like Integers, Sequences and so on.

ctrl+click (command+click?) a module name that appears on the EXTENDS statement at the top of your spec

To check the eploring spec's model

• Use cloud services
• To make the size of constants smaller