search

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities
Other
1.29k stars 200 forks source link

GameOfLife spec minor improvement possible? #154

Closed ajrouvoet closed 2 weeks ago

ajrouvoet commented 2 weeks ago

As a complete TLA beginner I opened the GOL spec and I noticed that TypeOK and Init are identically defined but only the latter is used. Does this have a purpose or is this a slight oversight and would it make more sense to---for example---drop TypeOk?

https://github.com/tlaplus/Examples/blob/f532f0ac4e44b97edd939f73e1caf8b4071cf419/specifications/GameOfLife/GameOfLife.tla#L17

It is perhaps superficial, but given that these specs serve for education purposes it might be worth addressing.

ahelwer commented 2 weeks ago

TypeOK is the type invariant and is marked as invariant to check in GameOfLife.cfg. Type invariants are broad statements about what sets each variable can range across during the execution of the system.

lemmy commented 2 weeks ago

TypeOK is referenced by the .cfg and checked as an invariants.

https://github.com/tlaplus/Examples/blob/f532f0ac4e44b97edd939f73e1caf8b4071cf419/specifications/GameOfLife/GameOfLife.cfg#L2C1-L2C17

ajrouvoet commented 2 weeks ago

Ah, clear! Thanks for clarifying!