Examples
Examples copied to clipboard
tlaplus
Classify specifications by TLA+ / PlusCal
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
--algorithmor--fair algorithm - I believe anything that's in the
toolboxsubdirectory 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?
The no maintenance of no tags is certainly appealing but does it work for other (non-technical) tags such as [beginner|intermediate|advanced]?
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.
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.
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?
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.
@konnov Does https://github.com/konnov/apalache depend on the directory structure of the TLA+ examples?
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.
