Comments (13)
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.
from examples.
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.
from examples.
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.
from examples.
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?
from examples.
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.
from examples.
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.
from examples.
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:
- Some specs (example: CarTalkPuzzle) follow the toolbox model scheme where cfgs are located in a
CarTalkPuzzle.toolbox/Model_N
subdirectory with a duplicatedCarTalkPuzzle.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? - 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 thespecifications
directory; thoughts? I would then want to pare these down over time by actually moving the linked spec into the repo, licensing allowing.
from examples.
- Rewrite the config files to reduce duplication will break the import for Toolbox users.
- If most of the external links are git repositories, we should considered git submodules.
from examples.
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.
from examples.
Assuming we have submodules, every clone will automatically create decentralized copies of those repos.
from examples.
Only if people pass the --recurse-submodules
command to git clone.
from examples.
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.
from examples.
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.
from examples.
Related Issues (20)
- Submodules vs. copying specs into the repo HOT 2
- `ctl[p]` is never equal `"req"` in specifications/SpecifyingSystems/Liveness properties HOT 6
- GitPod & Codespaces - make sure bitrot hasn't set in
- Add TLC models for all specs for which it's viable
- Add some Apalache models HOT 5
- Bakery-Boulangerie specs don't satisfy `DeadlockFree` or `StarvationFree` liveness properties HOT 1
- Can't come up with working model for cbc_max or spanning HOT 1
- Liveness and Safety properties fail in SpanTreeRandom.tla HOT 11
- Deactivate macOS CI runners? HOT 3
- Add optional fields to manifest.json recording total and unique states for each model
- Add proof checking time to manifest details
- EWD998 model checking failure when running TLC from outside tlaplus/examples repo HOT 5
- Parameterize version of TLA+ tools used during CI run HOT 2
- Question about the specification of reliable broadcast algorithm by Bracha & Toueg (1985) HOT 8
- CI workflow fails on ubuntu HOT 7
- Do not suppress TLC output HOT 3
- Possible TLC regression on specifications/ewd998/EWD998ChanID.cfg HOT 7
- ERROR in specifications/SpecifyingSystems/Composing/CompositeFIFO.tla: In evaluation, the identifier in is either undefined or not an operator. HOT 1
- Remove deadlock flag in manifest.json in favor of `CHECK_DEADLOCK` in config file HOT 4
- Install TLA+ unicode converter into gitpod and codespaces HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from examples.