Skip to content

Commit 9beb57f

Browse files
ahelwerahelwer
committed
JSON schema and validation script now check split manifest
Signed-off-by: Andrew Helwer <[email protected]>
1 parent 44751ef commit 9beb57f

File tree

4 files changed

+90
-5518
lines changed

4 files changed

+90
-5518
lines changed

‎.github/scripts/check_manifest_schema.py‎

Lines changed: 23 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,38 @@
11
"""
2-
Checks to ensure manifest.json is valid according to schema; this can also
3-
be done manually at https://www.jsonschemavalidator.net/
2+
Checks to ensure manifest.json in each specifications/ subdirectory is valid
3+
according to schema; this can also be done manually at
4+
https://www.jsonschemavalidator.net/
5+
46
Learn about the JSON schema format at
57
https://json-schema.org/understanding-json-schema/
68
"""
79

810
from argparse import ArgumentParser
911
from jsonschema import validate
10-
from os.path import normpath
12+
from jsonschema.exceptions import ValidationError
13+
from os.path import normpath, dirname, join
14+
from sys import stderr
1115
import tla_utils
1216

13-
parser = ArgumentParser(description='Checks tlaplus/examples manifest.json against JSON schema file.')
14-
parser.add_argument('--manifest_path', help='Path to the tlaplus/examples manifest.json file', required=True)
17+
parser = ArgumentParser(description='Checks tlaplus/examples manifest.json files against JSON schema file.')
1518
parser.add_argument('--schema_path', help='Path to the tlaplus/examples manifest-schema.json file', required=True)
1619
args = parser.parse_args()
1720

21+
examples_root = dirname(args.schema_path)
1822
schema = tla_utils.load_json(normpath(args.schema_path))
19-
manifest = tla_utils.load_json(normpath(args.manifest_path))
23+
failures = []
24+
for manifest in tla_utils.load_all_manifests(examples_root):
25+
manifest_path = join(manifest['path'], "manifest.json")
26+
try:
27+
validate(instance=manifest, schema=schema)
28+
except ValidationError as error:
29+
print(f'FAILURE: schema NOT matched by {manifest_path}', file=stderr)
30+
failures.append((manifest_path, error))
31+
else:
32+
print(f'SUCCESS: schema matched by {manifest_path}')
33+
34+
for (manifest_path, manifest_error) in failures:
35+
print(f'\nSchema failure in {manifest_path}:\n{manifest_error}\n', file=stderr)
2036

21-
result = validate(instance=manifest, schema=schema)
22-
if None == result:
23-
print('SUCCESS: Manifest correctly follows schema')
24-
exit(0)
25-
else:
26-
print('ERROR: Manifest does not follow schema')
27-
print(result)
28-
exit(1)
37+
exit(1 if any(failures) else 0)
2938

‎.github/scripts/tla_utils.py‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,7 @@
44
from os.path import join, normpath, pathsep
55
import subprocess
66
import re
7+
import glob
78

89
def from_cwd(root, path):
910
"""
@@ -44,6 +45,15 @@ def load_json(path):
4445
with open(normpath(path), 'r', encoding='utf-8') as file:
4546
return json.load(file)
4647

48+
def load_all_manifests(examples_root):
49+
"""
50+
Loads all manifest.json files in the specifications subdirectories.
51+
"""
52+
return [
53+
load_json(manifest_path)
54+
for manifest_path in glob.glob(f'specifications/*/manifest.json', root_dir=examples_root)
55+
]
56+
4757
def write_json(data, path):
4858
"""
4959
Writes the given json to the given file.

‎manifest-schema.json‎

Lines changed: 57 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -1,93 +1,83 @@
11
{
2-
"type" : "object",
3-
"required": ["specifications"],
2+
"type": "object",
3+
"required": ["title", "description", "sources", "authors", "path", "tags", "modules"],
44
"additionalProperties": false,
5-
"properties" : {
6-
"specifications" : {
5+
"properties": {
6+
"path": {"type": "string"},
7+
"title": {"type": "string"},
8+
"description": {"type": "string"},
9+
"sources": {
10+
"type": "array",
11+
"items": {"type": "string"}
12+
},
13+
"authors": {
14+
"type": "array",
15+
"items": {"type": "string"}
16+
},
17+
"tags": {
18+
"type": "array",
19+
"items": {"enum": ["beginner", "intermediate", "ewd"]}
20+
},
21+
"modules": {
722
"type": "array",
823
"items": {
924
"type": "object",
10-
"required": ["title", "description", "sources", "authors", "path", "tags", "modules"],
25+
"required": ["path", "communityDependencies", "tlaLanguageVersion", "features", "models"],
1126
"additionalProperties": false,
1227
"properties": {
1328
"path": {"type": "string"},
14-
"title": {"type": "string"},
15-
"description": {"type": "string"},
16-
"sources": {
29+
"communityDependencies": {
1730
"type": "array",
1831
"items": {"type": "string"}
1932
},
20-
"authors": {
33+
"tlaLanguageVersion": {"type": "number"},
34+
"features": {
2135
"type": "array",
22-
"items": {"type": "string"}
36+
"items": {"enum": ["pluscal", "proof", "action composition"]}
2337
},
24-
"tags": {
25-
"type": "array",
26-
"items": {"enum": ["beginner", "intermediate", "ewd"]}
27-
},
28-
"modules": {
38+
"models": {
2939
"type": "array",
3040
"items": {
3141
"type": "object",
32-
"required": ["path", "communityDependencies", "tlaLanguageVersion", "features", "models"],
3342
"additionalProperties": false,
43+
"required": ["path", "runtime", "size", "mode", "features", "result"],
3444
"properties": {
3545
"path": {"type": "string"},
36-
"communityDependencies": {
37-
"type": "array",
38-
"items": {"type": "string"}
46+
"runtime": {
47+
"type": "string",
48+
"pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$"
49+
},
50+
"size": {"enum": ["small", "medium", "large", "unknown"]},
51+
"distinctStates": {"type": "integer"},
52+
"totalStates": {"type": "integer"},
53+
"stateDepth": {"type": "integer"},
54+
"mode": {
55+
"oneOf": [
56+
{
57+
"enum": ["exhaustive search", "generate", "symbolic"]
58+
},
59+
{
60+
"type": "object",
61+
"additionalProperties": false,
62+
"required": ["simulate"],
63+
"properties": {
64+
"simulate": {
65+
"type": "object",
66+
"additionalProperties": false,
67+
"required": ["traceCount"],
68+
"properties": {
69+
"traceCount": {"type": "number"}
70+
}
71+
}
72+
}
73+
}
74+
]
3975
},
40-
"tlaLanguageVersion": {"type": "number"},
4176
"features": {
4277
"type": "array",
43-
"items": {"enum": ["pluscal", "proof", "action composition"]}
78+
"items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}
4479
},
45-
"models": {
46-
"type": "array",
47-
"items": {
48-
"type": "object",
49-
"additionalProperties": false,
50-
"required": ["path", "runtime", "size", "mode", "features", "result"],
51-
"properties": {
52-
"path": {"type": "string"},
53-
"runtime": {
54-
"type": "string",
55-
"pattern": "^(([0-9][0-9]:[0-9][0-9]:[0-9][0-9])|unknown)$"
56-
},
57-
"size": {"enum": ["small", "medium", "large", "unknown"]},
58-
"distinctStates": {"type": "integer"},
59-
"totalStates": {"type": "integer"},
60-
"stateDepth": {"type": "integer"},
61-
"mode": {
62-
"oneOf": [
63-
{
64-
"enum": ["exhaustive search", "generate", "symbolic"]
65-
},
66-
{
67-
"type": "object",
68-
"additionalProperties": false,
69-
"required": ["simulate"],
70-
"properties": {
71-
"simulate": {
72-
"type": "object",
73-
"additionalProperties": false,
74-
"required": ["traceCount"],
75-
"properties": {
76-
"traceCount": {"type": "number"}
77-
}
78-
}
79-
}
80-
}
81-
]
82-
},
83-
"features": {
84-
"type": "array",
85-
"items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]}
86-
},
87-
"result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]}
88-
}
89-
}
90-
}
80+
"result": {"enum": ["success", "assumption failure", "deadlock failure", "safety failure", "liveness failure", "unknown"]}
9181
}
9282
}
9383
}

0 commit comments

Comments
 (0)