Classify specifications by TLA+ / PlusCal

[nrinaudo]

As discussed on twitter.

[nrinaudo]

My first instinct is that all PlusCal specifications can be found through:

grep -lri -- "--\(fair\s\+\)\?algorithm" | grep -v toolbox | grep \.tla

• all PlusCall specifications must contain --algorithm or --fair algorithm
• I believe anything that's in the toolbox subdirectory is to be ignored?
• filter on tla files to avoid false-positives in README or such

Finding all TLA+ specifications is achieved by flipping the first test to exclude PlusCal files:

grep -lriv -- "--\(fair\s\+\)\?algorithm" | grep -v toolbox | grep \.tla 

I've confirmed that this worked by comparing the output of the first command with a manually crafted list of all PlusCal specifications (grepped on algorithm, opened all corresponding files to check whether they were PlusCal or TLA+).

The advantage of this approach over manually tagging the specifications (such as with comments) is that it needs no special maintenance - our commands do not need files to be tagged in any specific way.

The two flaws I can think of are:

• it's possible to craft a TLA+ file that'll fail these commands by including, for example, \* Don't look for --algorithm, this is raw tla.
• it's probably not reasonable to expect people to be able to craft github queries to reproduce the commands' behaviour.

If this is an acceptable solution, I'd be happy to submit a PR that includes the commands in the README.md, as well as list the categories somehow - in the large table, maybe with a new PlusCal column?

[lemmy]

The no maintenance of no tags is certainly appealing but does it work for other (non-technical) tags such as [beginner|intermediate|advanced]?

[nrinaudo]

Err... I'm not sure what you mean. The two grep commands I've listed work specifically and only for identifying PlusCal or TLA+ specifications. So if you're asking whether they'll pick other tags: no, they won't, they're not at all designed for that.

Looking at a couple of specifications, I'm not seeing the beginner|intermediate|advanced tag. Is this something that already exists, or something you'd like to add? If the later:

• I do not feel qualified to help with that, as I'm utterly incapable of deciding the "level" of a specification. Everything looks expert level to me :)
• I would suggest this is another, unrelated feature - whether a specification is PlusCal or TLA+ is a property of the file, what you're talking about is additional, handcrafted metadata.

[lemmy]

There is no additional metadata yet. I was just wondering if we can envision a tagging scheme that works for all metadata (let it be technical s.a. [tla|pcal|tlaps| or non-tech s.a. [beginner|intermediate|advanced]. It is not meant as a request to tag specifications.

[nrinaudo]

Sure, that'd work as well. It'd be more work to maintain, but it'd also be potentially more useful.

Additional work:

• specify acceptable metadata key (language, level, ...) and the values each can take
• go through all existing specifications to tag them
• make sure each new specification is tagged
• possibly have some sort of build step that fails a PR if a tla file is found without the proper tags, or with an invalid value for a known tag.

Benefit:

• more powerful searches
• potentially generate that massive README.md table automatically, ensuring it doesn't grow stale

You could still use the commands I listed above to help you with tagging tla or pcal, it might be slightly faster than doing it manually, I suppose.

This sounds like a lot of work to me, is this repository popular enough to warrant this amount of efforts?

[hwayne]

What if for now we put PlusCal and raw TLA+ in separate folders?

[lemmy]

I'm reluctant to change the directory layout because others might rely on the current layout. E.g. Apalache runs benchmarks based on the examples and likely has scripts setup for that.

[lemmy]

@konnov Does https://github.com/konnov/apalache depend on the directory structure of the TLA+ examples?

[konnov]

No, Apalache does not use the directory structure of tlaplus-examples. Perhaps, a few links somewhere in the docs might break, but that is not a big deal.

[jonesmartins]

Any new thoughts on this tagging system?