Index examples in manifest.json

[lemmy]

Here's an example entry in the manifest.json:

{
  "specifications": [
    {
      "title": "Multi-Car Elevator System",
      "description": "A simple multi-car elevator system servicing a multi-floor building",
      "source": "https://groups.google.com/g/tlaplus/c/5Xd8kv288jE/m/IrliJIatBwAJ",
      "authors": ["Andrew Helwer"],
      "modules": [
        {
          "path": "specifications/MultiCarElevator/Elevator.tla",
          "communityDependencies": [],
          "tlaLanguageVersion": 2,
          "features": [],
          "models": [
            {
              "path": "specifications/MultiCarElevator/ElevatorLivenessSmall.cfg",
              "runtime": "00:00:10",
              "features": ["liveness"],
              "result": "success"
            },

So you have a specification (directory), with one or more modules (.tla files), where each module can have 0 or more models (.cfg files). Similar to the toolbox! I envision a number of interesting pieces of metadata associated with each of these entities that can be searched or filtered by a program consuming this repo:

• Spec title/description/source/authors: pretty self-explanatory
• Module communityDependencies: also self-explanatory
• module features: pluscal/proof/unicode
• model runtime: approximate runtime, we could encourage users to add at least one model that runs for less than ten seconds, for example - consumers of this repo could test-execute every model with a sub-10-second runtime
• model features: liveness/symmetry/state restriction
• result: success/liveness failure/safety failure/deadlock

I will write a CI script that runs to validate the following when a PR is open:

• The manifest.json file conforms to a json schema
• Every path in the manifest.json corresponds to a file in the repo
• Every .tla or .cfg file in the repo corresponds to an entry in the manifest
• Use tree-sitter queries to ensure the pluscal/proof feature tags are correct
• Use file search for .cfgs to ensure model feature tags are correct

I agree it would not be useful to have this information duplicated in a manifest and a README, which could get out of sync. I will look into whether it's possible to pull this info into an HTML file and have it displayed or something of that sort. It does look like this work would resolve that issue you linked.

Originally posted by @ahelwer in https://github.com/tlaplus/Examples/issues/55#issuecomment-1383242530

[lemmy]

My initial thought is that wall-clock time isn't terribly useful and quickly outdated anyway. Instead, we should encourage contributors to integrate new examples into our build automation, which can timeout, and, thus, fail the PR if a proof or model-checking with TLC or Apalache takes too long.

[ahelwer]

Could change runtime to be size with possible values small/medium/large. Small models must run in less than ten seconds on an ordinary computer built within the past ten years (so on the github CI hosts), medium models less than ten minutes, large models are unbounded. The small models can even be added to the CI to ensure that specs added here are capable of being model checked without errors.

[ahelwer]

Here's another idea: instead of having both a manifest.json and a summary table in the README, the README summary table can just list beginner-friendly specs. If people are looking for specs for other reasons they can just read the manifest.json (itself human-readable enough) or browse the repo itself.

[lemmy]

If technical obstacles prevent sourcing README.md from a manifest.json, we should accept the redundancy in the interest of beginner-friendly experience. @muenchnerkindl What do you think?

[muenchnerkindl]

I agree that having a manifest.json along the lines that you suggest would be useful (it would be good to include features related to Apalache such as type annotations, models for bounded model checking or for checking inductive invariants). At first glance it appears to me that it should be possible to generate a table such as the one in the current README.md from the information in the JSON file, but if not we should probably have both at the risk of inconsistencies.

[ahelwer]

I can also have the CI workflow auto-update the README.md table from the manifest.json, so only the manifest.json should be human-editable while the README is machine-generated. It's a bit messier but should be doable. I am partial to the idea of just having only a curated list of beginner specs in the README, though. I don't think a giant markdown table of all specs in the repo is super useful.

I agree it would also be useful to add apalache and snowcat related feature flags.

[ahelwer]

I've written a fair number of the validation scripts and am now engaged in the process of adding all the specs into the manifest.json. I have two design concerns:

1. Some specs (example: CarTalkPuzzle) follow the toolbox model scheme where cfgs are located in a CarTalkPuzzle.toolbox/Model_N subdirectory with a duplicated CarTalkPuzzle.tla spec. Should I rewrite the cfg files so they can live in the same directory as the main spec and avoid duplicating that spec?
2. Quite a few spec directories are just a README.md file that contains a link to somewhere else. I think we should move these to a separate external_links directory instead of the specifications directory; thoughts? I would then want to pare these down over time by actually moving the linked spec into the repo, licensing allowing.

[lemmy]

1. Rewrite the config files to reduce duplication will break the import for Toolbox users.
2. If most of the external links are git repositories, we should considered git submodules.

[ahelwer]

Finished first draft of the manifest work. I like submodules but we do need to consider that broken links are a possibility; if the repo is moved or deleted (pretty easy to have happen as years draw on) then the specs will disappear. This has already happened for a couple of the links to non-github-hosted specs.

[lemmy]

Assuming we have submodules, every clone will automatically create decentralized copies of those repos.

[ahelwer]

Only if people pass the --recurse-submodules command to git clone.

[lemmy]

Perhaps, Github UI already has the parameter in its clone string. Adding a note to our README.md to include --recurse-modules when cloning can spread the word, too. Secondly, we can quickly set up a cron job on our Inria machine to periodically clone this repo.

[lemmy]

I like submodules but we do need to consider that broken links are a possibility; if the repo is moved or deleted (pretty easy to have happen as years draw on) then the specs will disappear. This has already happened for a couple of the links to non-github-hosted specs.

Experimenting with submodules today: With submodules, our CI will detect broken links whereas lost specs go unnoticed with the current Readme.md files.