Add optional fields to manifest.json recording total and unique states for each model

tlaplus / Examples

A collection of TLA⁺ specifications of varying complexities

Other

1.29k stars 200 forks source link

Add optional fields to manifest.json recording total and unique states for each model #120

Closed ahelwer closed 8 months ago

ahelwer commented 9 months ago

The check_small_models.py script will then validate that TLC execution produces the expected values. This will significantly improve the value of these models as TLC regression tests, since this number should not ever change unless the spec or model changes.