Added TLC models for all viable specs (tlaplus#110)

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

Author: ahelwer

.github/scripts/check_markdown_table.py

@@ -180,6 +180,7 @@ def from_json(spec):
     for path, json, md in different_tlc_flag:
         print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' a TLC Model flag in README.md table')
 
+'''
 # Ensure Apalache flag is correct
 different_apalache_flag = [
     (manifest_spec.path, manifest_spec.apalache, table_spec.apalache)
@@ -191,6 +192,7 @@ def from_json(spec):
     print('ERROR: Apalache Model flags in README.md table differ from model records in manifest.json:')
     for path, json, md in different_tlc_flag:
         print(f'Spec {path} ' + ('incorrectly has' if md else 'is missing') + ' an Apalache Model flag in README.md table')
+'''
 
 if success:
     print('SUCCESS: manifest.json concords with README.md table')

.github/scripts/check_small_models.py

@@ -17,6 +17,7 @@
 parser.add_argument('--community_modules_jar_path', help='Path to the CommunityModules-deps.jar file', required=True)
 parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
 parser.add_argument('--skip', nargs='+', help='Space-separated list of models to skip checking', required=False, default=[])
+parser.add_argument('--only', nargs='+', help='If provided, only check models in this space-separated list', required=False, default=[])
 args = parser.parse_args()
 
 logging.basicConfig(level=logging.INFO)
@@ -27,6 +28,7 @@
 manifest_path = normpath(args.manifest_path)
 examples_root = dirname(manifest_path)
 skip_models = [normpath(path) for path in args.skip]
+only_models = [normpath(path) for path in args.only]
 
 def check_model(module_path, model, expected_runtime):
     module_path = tla_utils.from_cwd(examples_root, module_path)
@@ -72,6 +74,7 @@ def check_model(module_path, model, expected_runtime):
         for model in module['models']
             if model['size'] == 'small'
             and normpath(model['path']) not in skip_models
+            and (only_models == [] or normpath(model['path']) in only_models)
     ],
     key = lambda m: m[2],
     reverse=True

.github/scripts/format_markdown_table.py

@@ -16,10 +16,6 @@
 parser.add_argument('--readme_path', help='Path to the tlaplus/examples README.md file', required=True)
 args = parser.parse_args()
 
-readme = None
-with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
-    readme = mistletoe.Document(readme_file)
-
 columns = ['name', 'authors', 'beginner', 'proof', 'tlc', 'pcal', 'apalache']
 
 def get_column(row, index):
@@ -64,11 +60,21 @@ def format_table(table):
     '''
     return
 
-table = next((child for child in readme.children if isinstance(child, Table)))
-format_table(table)
+def format_document(document):
+    '''
+    All document transformations should go here.
+    '''
+    # Gets table of local specs
+    table = next((child for child in document.children if isinstance(child, Table)))
+    format_table(table)
 
-# Write formatted markdown to README.md
-with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file:
-    with MarkdownRenderer() as renderer:
+# Read, format, write
+# Need to both parse & render within same MarkdownRenderer context to preserve other formatting
+with MarkdownRenderer() as renderer:
+    readme = None
+    with open(normpath(args.readme_path), 'r', encoding='utf-8') as readme_file:
+        readme = mistletoe.Document(readme_file)
+    format_document(readme)
+    with open(normpath(args.readme_path), 'w', encoding='utf-8') as readme_file:
         readme_file.write(renderer.render(readme))
 

.github/scripts/generate_manifest.py

@@ -52,15 +52,20 @@ def get_cfg_files(examples_root, tla_path):
     Assume a .cfg file in the same directory as the .tla file and with the
     same name is a model of that .tla file; also assume this of any .cfg
     files where the .tla file name is only a prefix of the .cfg file name,
-    unless there are other .tla file names in the directory that exactly
-    match the .cfg file name.
+    unless there are other .tla file names in the directory that are longer
+    prefixes of the .cfg file name.
     """
     parent_dir = dirname(tla_path)
     module_name, _ = splitext(basename(tla_path))
     other_module_names = [other for other in get_module_names_in_dir(examples_root, parent_dir) if other != module_name]
     return [
-        path for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg', root_dir=examples_root)
-        if splitext(basename(path))[0] not in other_module_names
+        path
+        for path in glob.glob(f'{join(parent_dir, module_name)}*.cfg', root_dir=examples_root)
+        if not any([
+            splitext(basename(path))[0].startswith(other_module_name)
+            for other_module_name in other_module_names
+            if len(other_module_name) > len(module_name)
+        ])
     ]
 
 def generate_new_manifest(examples_root, ignored_dirs, parser, queries):

.github/scripts/tla_utils.py

@@ -108,6 +108,7 @@ def resolve_tlc_exit_code(code):
     """
     tlc_exit_codes = {
         0   : 'success',
+        10  : 'assumption failure',
         11  : 'deadlock failure',
         12  : 'safety failure',
         13  : 'liveness failure'

.github/workflows/CI.yml

@@ -28,13 +28,13 @@ jobs:
         shell: bash
     steps:
       - name: Clone repo
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
       - name: Install python
-        uses: actions/setup-python@v4
+        uses: actions/setup-python@v5
         with:
           python-version: '3.11'
       - name: Install Java
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           distribution: adopt
           java-version: 17

.gitignore

@@ -38,9 +38,11 @@ pyvenv.cfg
 
 ## Ignore directories used for local CI testing
 deps/
+tree-sitter-tlaplus/
 
 # Ignore TTrace specs
 *_TTrace_*.tla
 
 ## Blacklist tools/ folder created by .devcontainer.json
 tools/
+