2.1 Behaviors 「コンピュータシステムにおいて、状態の変化は非連続のステップで起こると仮定できるので、システムの実行をstatesのシーケンスと表すことができる。ここで、stateとはvalueをvariableにアサインすること。システムをpossible behaviorsの集…

1.1 Propositional Logic /\ (and) => (implies、日本語だとなんだっけ？ならば、とか？) \/ (or) (is equivalent to) ~ (not) このへんはまだTLA+関係ないので余裕。 1.2 Sets 集合ね。。大学一年の時、集合と位相の授業で人生初の赤点をとった苦い記憶が蘇…

このブログはアメブロよりもさらに読者が少ないので、ひっそりと一人輪読（というかただの読書）のまとめをかいていくことにする。英語のままだと何回読んでも頭に入ってこない。TLA+の本 http://research.microsoft.com/en-us/um/people/lamport/tla/book.h…

こんな簡単な例でも、読んだだけでは「ふーん、そう」という感じで、いまいちわかってない。問題は、この本をずっと読み進めていっても、いつまでたっても実際の使い方にたどり着かないことだ。（PlusCALのマニュアルはその点、少しだけ親切。それをもとにPl…