Files
neon/safekeeper/spec
2024-11-18 14:06:13 +03:00
..
2024-11-18 14:06:13 +03:00
2024-11-18 14:06:13 +03:00
2024-11-18 14:06:13 +03:00
2024-11-18 14:06:13 +03:00
2024-11-18 14:06:13 +03:00

Directory structure:

  • Use modelcheck.sh to run TLC.
  • MC*.tla contains bits of TLA+ needed for TLC like constraining the state space, and models/ actual models.
  • Other .tla files are the actual specs.

Structure is partially borrowed from logless-reconfig, thanks to it.