Added JSON manifest with CI validation #61

ahelwer · 2023-01-26T02:15:56Z

All specs, modules, and models are now recorded in a top-level manifest.json file along with metadata
All fields of the manifest.json that can be validated are validated, including:
- Whether the spec includes pluscal or proofs
- Whether the spec imports any community modules
All specs are now checked for parse errors with SANY
All models marked as size small are run with TLC
All non-small models are smoke-tested
Added .ciignore file to except directories from CI
Added directions to README.md

Closes #57
Closes #8

lemmy · 2023-01-26T15:39:27Z

Could you please add comments to the python scripts for others to know what they do?

ahelwer · 2023-01-26T21:06:23Z

@lemmy all specs are now automatically parsed by SANY. There were two with problems:

ewd998, which runs into a naming collision between the TLAPS and community modules. Specifically Functions.tla; it tries to use operators in the Community version of Functions.tla, while also importing various modules from the TLAPS standard library (which itself includes a Functions.tla that doesn't have those operators).

SumSequence.tla, which uses some definitions from the TLAPS SequenceTheorems module that seemingly no longer exist.

I hardcoded those as exceptions in the python script, so it continues to parse all the existing specs and will parse any newly-submitted specs until those are fixed.

There were two other specs that required small changes to successfully parse, including one from Specifying Systems - although strangely this same error is not present in the book, just the spec downloads. I emailed Leslie about it.

lemmy · 2023-01-26T22:10:34Z

I can't find the issue, but the name clash with TLAPS is known. IIRC Functions.tla is going to be removed from TLAPS in its 1.5 release, and SequenceTheorems are added. @muenchnerkindl Am I remembering things correctly?

tlaplus/CommunityModules#60

muenchnerkindl · 2023-01-27T09:10:18Z

I confirm that the name clash between the TLAPS standard theorem library and some of the Community Modules (in particular Functions) is known and should be fixed in the long overdue release of TLAPS. As for SequenceTheorems, they were split into two modules such that SequenceTheorems only contains lemmas about operators defined in the standard Sequences module of TLA+ and SequencesExtTheorems contains lemmas about additional operators, defined in SequencesExt. I made the corresponding change to module SumSequence and also fixed some of the proofs in that module (some that should never have passed and some bit rot).

ahelwer · 2023-01-27T13:10:36Z

Hmmm, maybe it would be a good idea for me to run TLAPS against all the modules with proofs, too. Although perhaps some modules contain proofs written for documentary reasons that are not detailed enough to be formally verified.

muenchnerkindl · 2023-01-27T13:13:16Z

Don't worry, I'll probably be able to fix proofs faster if they are broken.

lemmy · 2023-01-27T21:14:53Z

I saw something like -workers str(cpu_count) in one of the python scripts. It can be replaced with -workers auto.

lemmy · 2023-01-27T21:33:32Z

https://github.com/tlaplus/tlaplus/blob/master/general/performance/measure.tla shows how to check different models/specs without any extra dependency such as python. (CommunityModules' json module could be used to read the manifest). This approach could subsume run.sh and check_small_models.py.

ahelwer · 2023-01-31T18:38:21Z

@lemmy this work is now at a point where it would be good to merge. Given the number of commits it seems like a good idea to squash it before merging.
@muenchnerkindl these changes don't include running TLAPS on all the proof modules; I will do this in a future batch of changes, these were getting a bit cumbersome and already delivered a lot of value so it seemed good to get them in the main branch.

lemmy · 2023-01-31T19:06:02Z

This repo mainly serves as a "comprehensive example library demonstrating how to specify an algorithm in TLA⁺". Thus, having correct metadata is a "should," not a "must". This PR raises the bar for contributions by mandating contributors to write JSON and locally install python tooling. Will the automation allow contributors to contribute just a single spec file, or will this cause problems immediately or for subsequent contributors? If yes, I suggest adding a .ciignore concept for automation to ignore those specs.

I'm not qualified to review the python code, but I assume the scripts do what they should.

lemmy · 2023-01-31T19:08:48Z

.github/scripts/check_manifest_features.py

+)
+
+# All the standard modules available when using TLC
+tlc_modules = {


The module lists below are not static. What will happen if the lists become outdated?

Then you change it, this is a best-effort method of getting the community dependencies. The only alternative is self-reporting.

My question is how we can help whoever will diagnose this problem in the future. Something like a comment that says "if you see error XYZ in the CI output, add Frob to the list of modules below".

There won't be any sort of error, all that will happen is the communityModules list will be incorrect in the json. This field is for the benefit of humans who might be interested in community module usage and isn't consumed by any tools.

lemmy · 2023-01-31T19:11:05Z

.github/scripts/check_small_models.py

@@ -0,0 +1,66 @@
+"""
+Check all models marked as size "small" in the manifest with TLC. Small
+models should finish executing in less than ten seconds on the GitHub CI


How reliable (flaky tests) is this assumption given unpredictable load on shared CI infrastructure?

Pretty reliable. It finishes executing in about 2.5 minutes.

ahelwer · 2023-01-31T19:15:25Z

@lemmy take it or leave it, I'll maintain a fork otherwise.

lemmy · 2023-01-31T19:28:10Z

@lemmy take it or leave it, I'll maintain a fork otherwise.

Fortunately, I'm not the only one who can review PRs in this repo. I will unassign myself.

ahelwer · 2023-02-01T14:20:18Z

@lemmy all right I slept on it and it would be acceptable to add a .ciignore file even though it opens the door to bitrot. At least there would be a ratchet effect where specs can be taken off .ciignore over time (work which multiple people including me are incentivized to do) and it would be a better contribution experience for researchers who are not as confident navigating scripts and json. I will make these changes if you can affirm there will be no additional feature changes necessary to merge once they are complete, notwithstanding small nitpicking stuff of course.

lemmy · 2023-02-06T19:01:15Z

I'm still concerned that constraining the length of tests based on wall-clock time could make for brittle tests. Other than that, I would like some of the python scripts to eventually become obsolete once the relevant functionality is available in the tools. At any rate, I'm but one of the reviewers of this repo.

ahelwer · 2023-02-06T20:49:47Z

@lemmy the small model tests are given a timeout of 60 seconds each, but I restricted the "small" models to ones that complete in not much more than 10 seconds on the github CI machines (most complete in about 1 second) so there is plenty of margin for error. I can't make any promises about future work converting the python scripts to TLA⁺ modules. Is the other reviewer @muenchnerkindl?

lemmy · 2023-02-07T16:38:56Z

It occurred to me that I don't understand why the README has to ask the user to install and run python locally. Won't the CI validation automatically run when they push to their own fork of this repo?

lemmy · 2023-02-07T16:41:31Z

Minor: I just resolved a merge conflict in .gitignore. The .devcontainer.json has been installing tlaps, apalache, ... into tools/. I suggest to install the CommunityModules, ... into the same tools folder for consistency.

ahelwer · 2023-02-07T16:48:31Z

@lemmy the CI will validate that the JSON is correct. Users will need to add details about their specs to the JSON. They can do this manually but running the python script will get them most of the way there by filling out whatever it can and setting plausible default values. We could possibly run the python JSON generation script in the CI itself and commit the changes to the branch for the user to then pull and modify, but that might run into write access issues because the PR branch usually lives in the user's fork.

muenchnerkindl · 2023-02-10T10:51:40Z

.github/scripts/smoke_test_large_models.py

+    # Attempted to select nonexistent field "traces" from record
+    'specifications/ewd426/SimTokenRing.cfg',
+    # Initial error cannot find TLAPS; if fixed, cannot find property "Stable"
+    'specifications/ewd998/AsyncTerminationDetection_proof.cfg',


Thanks for catching that error: there is no reason to run TLC on AsyncTerminationDetection_proof. I added the properties that were checked here to the configuration file for module AsyncTerminationDetection and removed that configuration file.

muenchnerkindl · 2023-02-11T08:21:29Z

.github/scripts/smoke_test_large_models.py

+    # The following are bugs that should be fixed:
+
+    # Attempted to access index 0 of tuple <<>>
+    'specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.cfg',


Fixed the formula that raised the exception during liveness checking.

muenchnerkindl · 2023-02-11T09:17:37Z

.github/scripts/smoke_test_large_models.py

+    # Attempted to access index 0 of tuple <<>>
+    'specifications/SpecifyingSystems/AdvancedExamples/MCInnerSerial.cfg',
+    # Attempted to select nonexistent field "traces" from record
+    'specifications/ewd426/SimTokenRing.cfg',


This issue must be due to the evaluation of TLCGet("stats").traces. I couldn't find a documentation of what TLCGet("stats") returns. @lemmy?

@muenchnerkindl f6de57f and fca6a17 have taken care of TLCGet("stats"), which - by the way - exposes TLC's progress statistics.

ahelwer · 2023-02-12T00:19:35Z

@lemmy @muenchnerkindl so if the .ciignore feature is implemented will this be merged? If so I will implement it, but won't spend more time on this otherwise.

muenchnerkindl · 2023-02-13T08:01:36Z

@ahelwer I am afraid we didn't express ourselves clearly enough: we highly welcome your effort to raise the standard of the examples collection, and your work has already found a number of issues in existing contributions. So yes, we'll be happy to accept your PR. Experience will tell if installing the ancillary tools proves to be too burdensome for future contributors: adding the .ciignore feature as suggested by @lemmy will allow them to bail out. Of course, our hope is that not a lot of people will use it. We also hope that you'll be willing to maintain the Python scripts in case of problems.

Signed-off-by: Andrew Helwer <[email protected]>

Addresses Github issue #65 #65 [Bug] Signed-off-by: Andrew Helwer <[email protected]>

Addresses part of Github issue #65 #65 Also see comment #65 (comment) [Doc] Signed-off-by: Andrew Helwer <[email protected]>

Signed-off-by: Andrew Helwer <[email protected]>

…d spurious configuration file for AsyncTerminationDetection_proof Signed-off-by: Andrew Helwer <[email protected]>

Signed-off-by: merz <[email protected]> Signed-off-by: Andrew Helwer <[email protected]>

Signed-off-by: Andrew Helwer <[email protected]>

ahelwer · 2023-02-15T04:35:48Z

@lemmy @muenchnerkindl added .ciignore feature and updated README instructions. This is now good to be merged. I'm happy to maintain the python scripts.

lemmy · 2023-04-10T22:39:19Z

What is wrong here?

Run python $SCRIPT_DIR/check_manifest_schema.py
Traceback (most recent call last):
  File "D:\a\Examples\Examples\.github\scripts\check_manifest_schema.py", line 14, in <module>
    result = validate(instance=manifest, schema=schema)
             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "C:\hostedtoolcache\windows\Python\3.11.2\x64\Lib\site-packages\jsonschema\validators.py", line 1121, in validate
    raise error
jsonschema.exceptions.ValidationError: 'features' is a required property

Failed validating 'required' in schema['properties']['specifications']['items']['properties']['modules']['items']['properties']['models']['items']:
    {'additionalProperties': False,
     'properties': {'config': {'items': {'enum': ['ignore deadlock']},
                               'type': 'array'},
                    'features': {'items': {'enum': ['liveness',
                                                    'symmetry',
                                                    'view',
                                                    'alias',
                                                    'state constraint']},
                                 'type': 'array'},
                    'mode': {'oneOf': [{'enum': ['exhaustive search',
                                                 'generate']},
                                       {'additionalProperties': False,
                                        'properties': {'simulate': {'additionalProperties': False,
                                                                    'properties': {'traceCount': {'type': 'number'}},
                                                                    'required': ['traceCount'],
                                                                    'type': 'object'}},
                                        'required': ['simulate'],
                                        'type': 'object'}]},
                    'path': {'type': 'string'},
                    'result': {'enum': ['success',
                                        'safety failure',
                                        'liveness failure',
                                        'deadlock failure',
                                        'unknown']},
                    'runtime': {'pattern': '^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$',
                                'type': 'string'},
                    'size': {'enum': ['small',
                                      'medium',
                                      'large',
                                      'unknown']}},
     'required': ['path',
                  'runtime',
                  'size',
                  'mode',
                  'config',
                  'features',
                  'result'],
     'type': 'object'}

On instance['specifications'][50]['modules'][[15](https://github.com/tlaplus/Examples/actions/runs/4661865936/jobs/8251615026?pr=75#step:8:16)]['models'][0]:
    {'config': [],
     'mode': 'exhaustive search',
     'path': 'specifications/ewd998/EWD998ChanTrace.cfg',
     'result': 'unknown',
     'runtime': '00:00:01',
     'size': 'small'}
Error: Process completed with exit code 1.

https://github.com/tlaplus/Examples/actions/runs/4661865936/jobs/8251615026?pr=75

ahelwer · 2023-04-11T02:30:42Z

@lemmy missing the features property, it says that

lemmy · 2023-04-11T02:48:02Z

b2691f3#diff-ffa5b716b5a57837f7929dfcca4b4dfdeb97210a7fd5a12d2f1978846d6f1743R3151

lemmy · 2023-04-11T16:25:36Z

After adding one more empty features to the Json file, check_manifest_files.py fails with no error message:

Run python $SCRIPT_DIR/check_manifest_files.py
  python $SCRIPT_DIR/check_manifest_files.py
  shell: /usr/bin/bash --noprofile --norc -e -o pipefail {0}
  env:
    SCRIPT_DIR: .github/scripts
    TLAPS_VERSION: [2](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:2)02210041448
    pythonLocation: /opt/hostedtoolcache/Python/[3](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:3).11.2/x6[4](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:4)
    PKG_CONFIG_PATH: /opt/hostedtoolcache/Python/3.11.2/x[6](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:6)4/lib/pkgconfig
    Python_ROOT_DIR: /opt/hostedtoolcache/Python/3.11.2/x64
    Python2_ROOT_DIR: /opt/hostedtoolcache/Python/3.11.2/x64
    Python3_ROOT_DIR: /opt/hostedtoolcache/Python/3.11.2/x64
    LD_LIBRARY_PATH: /opt/hostedtoolcache/Python/3.11.2/x64/lib
    JAVA_HOME: /opt/hostedtoolcache/Java_Adopt_jdk/1[7](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:7).0.6-10/x64
    JAVA_HOME_17_X64: /opt/hostedtoolcache/Java_Adopt_jdk/17.0.6-10/x64
Ignored .tla paths present in manifest:
specifications/ewd99[8](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:8)/AsyncTerminationDetection_proof.tla
specifications/ewd[9](https://github.com/tlaplus/Examples/actions/runs/4663381584/jobs/8254656249?pr=75#step:9:9)98/EWD998ChanID.tla
specifications/ewd998/EWD998Chan_opts.tla
specifications/ewd998/EWD998ChanTrace.tla
specifications/ewd998/AsyncTerminationDetection.tla
specifications/ewd998/EWD998_anim.tla
specifications/ewd998/EWD998_optsSC.tla
specifications/ewd998/SmokeEWD998.tla
specifications/ewd998/EWD998_opts.tla
specifications/ewd998/SmokeEWD998_SC.tla
specifications/ewd998/EWD998ChanID_shiviz.tla
specifications/ewd998/EWD998Chan.tla
specifications/ewd998/EWD998ChanID_export.tla
specifications/ewd998/EWD998.tla
specifications/ewd998/Utils.tla
specifications/ewd998/EWD998_proof.tla
Ignored .cfg paths present in manifest:
specifications/ewd998/AsyncTerminationDetection.cfg
specifications/ewd998/EWD998ChanID.cfg
specifications/ewd998/EWD998ChanID_shiviz.cfg
specifications/ewd998/SmokeEWD998.cfg
specifications/ewd998/SmokeEWD998_SC.cfg
specifications/ewd998/EWD998ChanTrace.cfg
specifications/ewd998/EWD998Chan.cfg
specifications/ewd998/EWD998.cfg
specifications/ewd998/EWD998ChanID_export.cfg
specifications/ewd998/EWD998Small.cfg

ahelwer · 2023-04-11T19:39:53Z

You added the EWD998 directory to CI ignore but then kept those files in the manifest, that's why it's failing.

I don't think adding EWD998 to CI ignore is a good idea btw. It passes basically all the steps except the parse, for which it has a hardcoded exception.

lemmy · 2023-04-12T03:31:03Z

What is the CWD when TLC is invoked?

ahelwer · 2023-04-12T03:47:17Z

repo root

ahelwer marked this pull request as ready for review January 31, 2023 18:36

lemmy reviewed Jan 31, 2023

View reviewed changes

lemmy requested review from lemmy and removed request for lemmy January 31, 2023 19:28

ahelwer mentioned this pull request Feb 1, 2023

EWD998 spec fails parsing due to name collision between TLAPS and Community Modules #66

Closed

muenchnerkindl reviewed Feb 10, 2023

View reviewed changes

muenchnerkindl reviewed Feb 11, 2023

View reviewed changes

Added manifest.json

5ac6806

Signed-off-by: Andrew Helwer <[email protected]>

ahelwer and others added 20 commits February 14, 2023 23:04

Updated README instructions

3dcd3c1

Signed-off-by: Andrew Helwer <[email protected]>

Expanded README

f5e7ec5

Signed-off-by: Andrew Helwer <[email protected]>

Final README changes

e0d6a9d

Signed-off-by: Andrew Helwer <[email protected]>

Ignore deadlock in simulation script

1fced72

Signed-off-by: Andrew Helwer <[email protected]>

Also ignore deadlock here

784cbe2

Signed-off-by: Andrew Helwer <[email protected]>

Added note about .cfg names

4271a63

Signed-off-by: Andrew Helwer <[email protected]>

Models failing smoke testing #65

b286b65

Addresses Github issue #65 #65 [Bug] Signed-off-by: Andrew Helwer <[email protected]>

Models failing smoke testing #65

69372ba

Addresses part of Github issue #65 #65 Also see comment #65 (comment) [Doc] Signed-off-by: Andrew Helwer <[email protected]>

Blacklist tools/ folder created by .devcontainer.json.

201c7c6

Signed-off-by: Andrew Helwer <[email protected]>

Update smoke test after fixes

9f659aa

Signed-off-by: Andrew Helwer <[email protected]>

Ran MCInnerSerial, ignore SimTokenRing

8955d41

Signed-off-by: Andrew Helwer <[email protected]>

Implement .ciignore

fb80777

Signed-off-by: Andrew Helwer <[email protected]>

fixed TLC configuration file for AsyncTerminationDetection and remove…

a9a699d

…d spurious configuration file for AsyncTerminationDetection_proof Signed-off-by: Andrew Helwer <[email protected]>

fixed two issues in specifications/SpecifyingSystems

38161a9

Signed-off-by: merz <[email protected]> Signed-off-by: Andrew Helwer <[email protected]>

Add .ciignore

638dc01

Signed-off-by: Andrew Helwer <[email protected]>

Fixed .ciignore

056a066

Signed-off-by: Andrew Helwer <[email protected]>

Run model except on win

4eabb2e

Signed-off-by: Andrew Helwer <[email protected]>

Merge branch 'master' into json

b99f336

Update README instructions for .ciignore

791a245

Signed-off-by: Andrew Helwer <[email protected]>

Fixed bullets in readme

20d48dd

Signed-off-by: Andrew Helwer <[email protected]>

lemmy merged commit 4d227cd into tlaplus:master Feb 15, 2023

ahelwer deleted the json branch February 15, 2023 04:44

Added JSON manifest with CI validation #61

Added JSON manifest with CI validation #61

Conversation

ahelwer commented Jan 26, 2023 • edited Loading

lemmy commented Jan 26, 2023

ahelwer commented Jan 26, 2023 • edited Loading

lemmy commented Jan 26, 2023 • edited Loading

muenchnerkindl commented Jan 27, 2023

ahelwer commented Jan 27, 2023

muenchnerkindl commented Jan 27, 2023

lemmy commented Jan 27, 2023

lemmy commented Jan 27, 2023

ahelwer commented Jan 31, 2023

lemmy commented Jan 31, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ahelwer commented Jan 31, 2023

lemmy commented Jan 31, 2023

ahelwer commented Feb 1, 2023

lemmy commented Feb 6, 2023

ahelwer commented Feb 6, 2023 • edited Loading

lemmy commented Feb 7, 2023

lemmy commented Feb 7, 2023

ahelwer commented Feb 7, 2023

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

ahelwer commented Feb 12, 2023

muenchnerkindl commented Feb 13, 2023

ahelwer commented Feb 15, 2023

lemmy commented Apr 10, 2023

ahelwer commented Apr 11, 2023

lemmy commented Apr 11, 2023

lemmy commented Apr 11, 2023

ahelwer commented Apr 11, 2023 • edited Loading

lemmy commented Apr 12, 2023

ahelwer commented Apr 12, 2023

ahelwer commented Jan 26, 2023 •

edited

Loading

ahelwer commented Jan 26, 2023 •

edited

Loading

lemmy commented Jan 26, 2023 •

edited

Loading

ahelwer commented Feb 6, 2023 •

edited

Loading

ahelwer commented Apr 11, 2023 •

edited

Loading