From d0ca8f0e0678ed1c72ec2ce5c4723059a15a298b Mon Sep 17 00:00:00 2001 From: Andrew Helwer <2n8rn1w1f@mozmail.com> Date: Sun, 14 Jan 2024 10:31:23 -0500 Subject: [PATCH] Use CHECK_DEADLOCK config file parameter Signed-off-by: Andrew Helwer <2n8rn1w1f@mozmail.com> --- .github/scripts/check_manifest_features.py | 27 +-- .github/scripts/check_small_models.py | 1 - .github/scripts/generate_manifest.py | 4 +- .github/scripts/smoke_test_large_models.py | 1 - .github/scripts/tla_utils.py | 11 +- README.md | 5 +- manifest-schema.json | 8 +- manifest.json | 164 ++++-------------- specifications/Huang/Huang.cfg | 5 +- .../N-Queens/Queens.toolbox/FourQueens/MC.cfg | 1 + specifications/Paxos/MCConsensus.cfg | 2 + specifications/Paxos/MCVoting.cfg | 2 + .../SDP_Attack_New_Solution_Spec/MC.cfg | 4 +- .../SDP_Verification/SDP_Attack_Spec/MC.cfg | 2 + specifications/ewd687a/EWD687a_anim.cfg | 6 +- specifications/ewd840/EWD840.cfg | 2 + specifications/ewd840/EWD840_anim.cfg | 6 +- specifications/ewd840/EWD840_json.cfg | 5 +- specifications/ewd998/EWD998.cfg | 4 + specifications/ewd998/EWD998Chan.cfg | 6 +- specifications/ewd998/EWD998ChanID.cfg | 6 +- specifications/ewd998/EWD998Small.cfg | 4 + 22 files changed, 104 insertions(+), 172 deletions(-) diff --git a/.github/scripts/check_manifest_features.py b/.github/scripts/check_manifest_features.py index e6d59e80..15d425e5 100644 --- a/.github/scripts/check_manifest_features.py +++ b/.github/scripts/check_manifest_features.py @@ -12,6 +12,7 @@ import glob from os.path import basename, dirname, join, normpath, splitext from typing import Any +import re import tla_utils from tree_sitter import Language, Parser @@ -89,21 +90,22 @@ def get_module_features(examples_root, path, parser, queries): tree, _, _ = parse_module(examples_root, parser, path) return get_tree_features(tree, queries) -# Keywords mapping to features for models +# Regexes mapping to features for models model_features = { - 'PROPERTY': 'liveness', - 'PROPERTIES': 'liveness', - 'SYMMETRY': 'symmetry', - 'ALIAS': 'alias', - 'VIEW': 'view', - 'CONSTRAINT': 'state constraint', - 'CONSTRAINTS': 'state constraint', + re.compile('^PROPERTY', re.MULTILINE) : 'liveness', + re.compile('^PROPERTIES', re.MULTILINE): 'liveness', + re.compile('^SYMMETRY', re.MULTILINE): 'symmetry', + re.compile('^ALIAS', re.MULTILINE): 'alias', + re.compile('^VIEW', re.MULTILINE): 'view', + re.compile('^CONSTRAINT', re.MULTILINE): 'state constraint', + re.compile('^CONSTRAINTS', re.MULTILINE): 'state constraint', + re.compile('^CHECK_DEADLOCK\\s+FALSE', re.MULTILINE) : 'ignore deadlock' } def get_model_features(examples_root, path): """ Finds features present in the given .cfg model file. - This will be a best-effort text search until a tree-sitter grammar is + This will be a best-effort regex search until a tree-sitter grammar is created for .cfg files. """ path = tla_utils.from_cwd(examples_root, path) @@ -111,10 +113,9 @@ def get_model_features(examples_root, path): model_text = None with open(path, 'rt') as model_file: model_text = model_file.read() - for line in model_text.split('\n'): - tokens = line.split() - if len(tokens) > 0 and tokens[0] in model_features: - features.append(model_features[tokens[0]]) + for regex, feature in model_features.items(): + if regex.search(model_text): + features.append(feature) return set(features) # All the standard modules available when using TLC diff --git a/.github/scripts/check_small_models.py b/.github/scripts/check_small_models.py index 081e1c84..e1fd4c31 100644 --- a/.github/scripts/check_small_models.py +++ b/.github/scripts/check_small_models.py @@ -41,7 +41,6 @@ def check_model(module_path, model, expected_runtime): tlapm_lib_path, community_jar_path, model['mode'], - model['config'], hard_timeout_in_seconds ) end_time = timer() diff --git a/.github/scripts/generate_manifest.py b/.github/scripts/generate_manifest.py index d3fb6631..3c55f388 100644 --- a/.github/scripts/generate_manifest.py +++ b/.github/scripts/generate_manifest.py @@ -14,7 +14,6 @@ from pathlib import PureWindowsPath import glob import tla_utils -from tree_sitter import Language, Parser def to_posix(path): """ @@ -89,7 +88,6 @@ def generate_new_manifest(examples_root, ignored_dirs, parser, queries): 'runtime': 'unknown', 'size': 'unknown', 'mode': 'exhaustive search', - 'config': [], 'features': sorted(list(get_model_features(examples_root, cfg_path))), 'result': 'unknown' } @@ -138,7 +136,7 @@ def find_corresponding_model(old_model, new_module): return models[0] if any(models) else None def integrate_model_info(old_model, new_model): - fields = ['runtime', 'size', 'mode', 'config', 'result'] + fields = ['runtime', 'size', 'mode', 'result'] for field in fields: new_model[field] = old_model[field] diff --git a/.github/scripts/smoke_test_large_models.py b/.github/scripts/smoke_test_large_models.py index 38792ff3..bcd9d901 100644 --- a/.github/scripts/smoke_test_large_models.py +++ b/.github/scripts/smoke_test_large_models.py @@ -38,7 +38,6 @@ def check_model(module_path, model): tlapm_lib_path, community_jar_path, model['mode'], - model['config'], smoke_test_timeout_in_seconds ) match tlc_result: diff --git a/.github/scripts/tla_utils.py b/.github/scripts/tla_utils.py index 6c99263d..f10b765f 100644 --- a/.github/scripts/tla_utils.py +++ b/.github/scripts/tla_utils.py @@ -67,14 +67,7 @@ def get_run_mode(mode): else: raise NotImplementedError(f'Undefined model-check mode {mode}') -def get_config(config): - """ - Converts the model config found in manifest.json into TLC CLI - parameters. - """ - return ['-deadlock'] if 'ignore deadlock' in config else [] - -def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, config, hard_timeout_in_seconds): +def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, community_jar_path, mode, hard_timeout_in_seconds): """ Model-checks the given model against the given module. """ @@ -98,7 +91,7 @@ def check_model(tools_jar_path, module_path, model_path, tlapm_lib_path, communi '-workers', 'auto', '-lncheck', 'final', '-cleanup' - ] + get_config(config) + get_run_mode(mode), + ] + get_run_mode(mode), timeout=hard_timeout_in_seconds, stdout=subprocess.PIPE, stderr=subprocess.STDOUT, diff --git a/README.md b/README.md index 069f7fd1..3683ec65 100644 --- a/README.md +++ b/README.md @@ -10,6 +10,8 @@ It serves as: All TLA+ specs can be found in the `specifications` directory. A central manifest of specs with descriptions and accounts of their various models and features can be found in the [`manifest.json`](manifest.json) file. +Beginner-friendly specs can be found by searching for the "beginner" tag in that file. +Similarly, PlusCal specs can be found by searching for the "pluscal" feature, or "proof" for specs with proofs. ## List of Examples @@ -171,8 +173,6 @@ Otherwise, follow these directions: - `"exhaustive search"` by default - `{"simulate": {"traceCount": N}}` for a simulation model - `"generate"` for model trace generation - - Model config: - - `"ignore deadlock"` if your model should ignore deadlock - Model result: - `"success"` if the model completes successfully - `"safety failure"` if the model violates an invariant @@ -181,3 +181,4 @@ Otherwise, follow these directions: - Other fields are auto-generated by the script; if you are adding an entry manually, ensure their values are present and correct (see other entries or the [`manifest-schema.json`](manifest-schema.json) file) Before submitted your changes to run in the CI, you can quickly check your [`manifest.json`](manifest.json) for errors and also check it against [`manifest-schema.json`](manifest-schema.json) at https://www.jsonschemavalidator.net/. + diff --git a/manifest-schema.json b/manifest-schema.json index d483f8df..776efa5d 100644 --- a/manifest-schema.json +++ b/manifest-schema.json @@ -44,7 +44,7 @@ "items": { "type": "object", "additionalProperties": false, - "required": ["path", "runtime", "size", "mode", "config", "features", "result"], + "required": ["path", "runtime", "size", "mode", "features", "result"], "properties": { "path": {"type": "string"}, "runtime": { @@ -74,13 +74,9 @@ } ] }, - "config": { - "type": "array", - "items": {"enum": ["ignore deadlock"]} - }, "features": { "type": "array", - "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint"]} + "items": {"enum": ["liveness", "symmetry", "view", "alias", "state constraint", "ignore deadlock"]} }, "result": {"enum": ["success", "safety failure", "liveness failure", "deadlock failure", "unknown"]} } diff --git a/manifest.json b/manifest.json index d06e5b6d..ccad3aff 100644 --- a/manifest.json +++ b/manifest.json @@ -70,7 +70,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -94,7 +93,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -118,7 +116,6 @@ "runtime": "unknown", "size": "large", "mode": "exhaustive search", - "config": [], "features": [], "result": "unknown" } @@ -173,7 +170,6 @@ "runtime": "00:01:00", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "state constraint", "symmetry" @@ -185,7 +181,6 @@ "runtime": "00:00:10", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "state constraint", "symmetry" @@ -238,7 +233,6 @@ "runtime": "00:00:15", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -249,7 +243,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -260,7 +253,6 @@ "runtime": "00:02:30", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -293,7 +285,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "safety failure" } @@ -317,7 +308,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "safety failure" } @@ -350,7 +340,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -381,7 +370,6 @@ "runtime": "unknown", "size": "large", "mode": "exhaustive search", - "config": [], "features": [], "result": "safety failure" } @@ -409,39 +397,37 @@ "models": [] }, { - "path": "specifications/FiniteMonotonic/Finitize_CRDT.tla", + "path": "specifications/FiniteMonotonic/Constrain_CRDT.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], "models": [ { - "path": "specifications/FiniteMonotonic/Finitize_CRDT.cfg", + "path": "specifications/FiniteMonotonic/Constrain_CRDT.cfg", "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ - "liveness" + "liveness", + "state constraint" ], "result": "success" } ] }, { - "path": "specifications/FiniteMonotonic/Constrain_CRDT.tla", + "path": "specifications/FiniteMonotonic/Finitize_CRDT.tla", "communityDependencies": [], "tlaLanguageVersion": 2, "features": [], "models": [ { - "path": "specifications/FiniteMonotonic/Constrain_CRDT.cfg", + "path": "specifications/FiniteMonotonic/Finitize_CRDT.cfg", "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ - "liveness", - "state constraint" + "liveness" ], "result": "success" } @@ -458,7 +444,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -519,11 +504,9 @@ "runtime": "00:00:40", "size": "medium", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ "alias", + "ignore deadlock", "liveness", "state constraint" ], @@ -578,7 +561,6 @@ "runtime": "07:16:00", "size": "large", "mode": "exhaustive search", - "config": [], "features": [ "symmetry" ], @@ -589,7 +571,6 @@ "runtime": "00:04:30", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "symmetry" ], @@ -600,7 +581,6 @@ "runtime": "00:00:40", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -617,7 +597,6 @@ "runtime": "00:00:50", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "symmetry" @@ -680,8 +659,8 @@ "runtime": "unknown", "size": "unknown", "mode": "generate", - "config": [], "features": [ + "ignore deadlock", "state constraint" ], "result": "unknown" @@ -733,7 +712,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "state constraint" ], @@ -773,7 +751,6 @@ "runtime": "00:01:00", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" }, @@ -782,7 +759,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -881,10 +857,9 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [ + "features": [ "ignore deadlock" ], - "features": [], "result": "success" } ] @@ -1001,7 +976,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "safety failure" } @@ -1030,7 +1004,6 @@ "runtime": "00:11:00", "size": "large", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -1041,7 +1014,6 @@ "runtime": "00:00:30", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -1052,7 +1024,6 @@ "runtime": "00:10:00", "size": "large", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" }, @@ -1061,7 +1032,6 @@ "runtime": "00:03:00", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" }, @@ -1070,7 +1040,6 @@ "runtime": "00:00:15", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -1108,10 +1077,9 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [ + "features": [ "ignore deadlock" ], - "features": [], "result": "safety failure" } ] @@ -1143,7 +1111,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -1183,7 +1150,6 @@ "runtime": "00:20:00", "size": "large", "mode": "exhaustive search", - "config": [], "features": [ "view" ], @@ -1194,7 +1160,6 @@ "runtime": "00:00:30", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "view" ], @@ -1205,7 +1170,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "view" ], @@ -1252,10 +1216,9 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [ + "features": [ "ignore deadlock" ], - "features": [], "result": "success" } ] @@ -1271,7 +1234,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "symmetry" @@ -1291,10 +1253,8 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "liveness", "symmetry" ], @@ -1387,7 +1347,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -1418,7 +1377,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -1457,10 +1415,8 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "liveness" ], "result": "success" @@ -1488,10 +1444,8 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "liveness" ], "result": "safety failure" @@ -1532,7 +1486,6 @@ "runtime": "00:00:30", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "symmetry" @@ -1552,7 +1505,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "symmetry" @@ -1584,7 +1536,6 @@ "runtime": "00:00:10", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -1622,7 +1573,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "safety failure" } @@ -1653,7 +1603,6 @@ "runtime": "00:50:00", "size": "large", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" }, @@ -1662,7 +1611,6 @@ "runtime": "00:01:00", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" }, @@ -1671,7 +1619,6 @@ "runtime": "00:00:15", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -1768,7 +1715,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "state constraint" @@ -1788,7 +1734,6 @@ "runtime": "00:01:30", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "state constraint" @@ -1822,7 +1767,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -1839,7 +1783,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -1856,7 +1799,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -1880,7 +1822,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -1897,7 +1838,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2028,7 +1968,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "state constraint" ], @@ -2047,7 +1986,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -2064,7 +2002,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2097,7 +2034,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2137,7 +2073,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2156,7 +2091,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2217,7 +2151,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2285,7 +2218,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -2372,7 +2304,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -2410,7 +2341,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "state constraint" @@ -2470,7 +2400,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2533,7 +2462,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -2621,7 +2549,6 @@ "runtime": "00:00:15", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2640,7 +2567,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2659,7 +2585,6 @@ "runtime": "00:00:10", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2678,7 +2603,6 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2911,7 +2835,6 @@ "runtime": "00:00:50", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -2939,7 +2862,6 @@ "runtime": "00:02:00", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -3011,7 +2933,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "success" } @@ -3051,8 +2972,8 @@ "runtime": "unknown", "size": "large", "mode": "generate", - "config": [], "features": [ + "ignore deadlock", "state constraint" ], "result": "unknown" @@ -3070,9 +2991,9 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "alias", + "ignore deadlock", "liveness" ], "result": "success" @@ -3129,11 +3050,9 @@ "traceCount": 100 } }, - "config": [ - "ignore deadlock" - ], "features": [ "alias", + "ignore deadlock", "liveness" ], "result": "safety failure" @@ -3151,8 +3070,8 @@ "runtime": "00:01:00", "size": "medium", "mode": "exhaustive search", - "config": [], "features": [ + "ignore deadlock", "liveness", "state constraint" ], @@ -3183,10 +3102,9 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [ + "features": [ "ignore deadlock" ], - "features": [], "result": "success" } ] @@ -3208,11 +3126,9 @@ "traceCount": 100 } }, - "config": [ - "ignore deadlock" - ], "features": [ - "alias" + "alias", + "ignore deadlock" ], "result": "safety failure" } @@ -3229,10 +3145,9 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [ + "features": [ "ignore deadlock" ], - "features": [], "result": "success" } ] @@ -3257,7 +3172,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness" ], @@ -3298,7 +3212,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [ "liveness", "state constraint" @@ -3330,10 +3243,8 @@ "runtime": "00:50:00", "size": "large", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "state constraint" ], "result": "success" @@ -3343,10 +3254,8 @@ "runtime": "00:05:00", "size": "medium", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "state constraint" ], "result": "success" @@ -3364,10 +3273,8 @@ "runtime": "00:05:00", "size": "medium", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "liveness", "state constraint" ], @@ -3386,10 +3293,8 @@ "runtime": "00:00:05", "size": "small", "mode": "exhaustive search", - "config": [ - "ignore deadlock" - ], "features": [ + "ignore deadlock", "liveness", "state constraint", "view" @@ -3411,8 +3316,9 @@ "runtime": "unknown", "size": "large", "mode": "exhaustive search", - "config": [], - "features": [], + "features": [ + "ignore deadlock" + ], "result": "unknown" } ] @@ -3428,9 +3334,9 @@ "runtime": "unknown", "size": "large", "mode": "exhaustive search", - "config": [], "features": [ - "alias" + "alias", + "ignore deadlock" ], "result": "unknown" } @@ -3503,8 +3409,8 @@ "traceCount": 100 } }, - "config": [], "features": [ + "ignore deadlock", "liveness", "state constraint" ], @@ -3526,7 +3432,6 @@ "runtime": "unknown", "size": "unknown", "mode": "exhaustive search", - "config": [], "features": [], "result": "unknown" } @@ -3787,7 +3692,6 @@ "runtime": "00:00:01", "size": "small", "mode": "exhaustive search", - "config": [], "features": [], "result": "safety failure" } @@ -3837,4 +3741,4 @@ ] } ] -} +} \ No newline at end of file diff --git a/specifications/Huang/Huang.cfg b/specifications/Huang/Huang.cfg index bdbf414c..8c19b748 100644 --- a/specifications/Huang/Huang.cfg +++ b/specifications/Huang/Huang.cfg @@ -16,4 +16,7 @@ CONSTANT CONSTRAINT StateConstraint ALIAS - Alias \ No newline at end of file + Alias +CHECK_DEADLOCK + FALSE + diff --git a/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg b/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg index 2b79a3d7..bb61dedc 100644 --- a/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg +++ b/specifications/N-Queens/Queens.toolbox/FourQueens/MC.cfg @@ -10,4 +10,5 @@ inv_129269484700018000 inv_129269484701019000 \* Generated at Sat Dec 18 18:54:07 CET 2010 INVARIANT NoSolutions +CHECK_DEADLOCK FALSE diff --git a/specifications/Paxos/MCConsensus.cfg b/specifications/Paxos/MCConsensus.cfg index b90fee05..ee3a85d5 100644 --- a/specifications/Paxos/MCConsensus.cfg +++ b/specifications/Paxos/MCConsensus.cfg @@ -1,3 +1,5 @@ CONSTANTS Value = {"a", "b", "c"} SPECIFICATION ISpec INVARIANT Inv +CHECK_DEADLOCK FALSE + diff --git a/specifications/Paxos/MCVoting.cfg b/specifications/Paxos/MCVoting.cfg index 61554c48..c7866e5a 100644 --- a/specifications/Paxos/MCVoting.cfg +++ b/specifications/Paxos/MCVoting.cfg @@ -8,3 +8,5 @@ SPECIFICATION Spec \* MCSpec INVARIANT Inv \* MCInv PROPERTY ConsensusSpecBar SYMMETRY MCSymmetry +CHECK_DEADLOCK FALSE + diff --git a/specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.cfg b/specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.cfg index e6fbd76d..2430a94d 100644 --- a/specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.cfg +++ b/specifications/SDP_Verification/SDP_Attack_New_Solution_Spec/MC.cfg @@ -49,4 +49,6 @@ UserAccessAvailProperty SvrHidenProperty FwRuleConsistentProperty FwCorrectProperty -\* Generated on Fri Feb 18 16:28:57 CST 2022 \ No newline at end of file +\* Generated on Fri Feb 18 16:28:57 CST 2022 +CHECK_DEADLOCK FALSE + diff --git a/specifications/SDP_Verification/SDP_Attack_Spec/MC.cfg b/specifications/SDP_Verification/SDP_Attack_Spec/MC.cfg index df875a37..26445eb9 100644 --- a/specifications/SDP_Verification/SDP_Attack_Spec/MC.cfg +++ b/specifications/SDP_Verification/SDP_Attack_Spec/MC.cfg @@ -50,3 +50,5 @@ SvrHidenProperty FwRuleConsistentProperty FwCorrectProperty \* Generated on Mon Jan 16 20:59:44 CST 2023 +CHECK_DEADLOCK FALSE + diff --git a/specifications/ewd687a/EWD687a_anim.cfg b/specifications/ewd687a/EWD687a_anim.cfg index 37f4a1fc..e347ee2e 100644 --- a/specifications/ewd687a/EWD687a_anim.cfg +++ b/specifications/ewd687a/EWD687a_anim.cfg @@ -36,4 +36,8 @@ CHECK_DEADLOCK FALSE ACTION_CONSTRAINT - NoSuperfluousIdleSteps \ No newline at end of file + NoSuperfluousIdleSteps + +CHECK_DEADLOCK + FALSE + diff --git a/specifications/ewd840/EWD840.cfg b/specifications/ewd840/EWD840.cfg index f8e94798..726b8a66 100644 --- a/specifications/ewd840/EWD840.cfg +++ b/specifications/ewd840/EWD840.cfg @@ -4,3 +4,5 @@ CONSTANTS INIT Init NEXT Next INVARIANT Inv +CHECK_DEADLOCK FALSE + diff --git a/specifications/ewd840/EWD840_anim.cfg b/specifications/ewd840/EWD840_anim.cfg index e8e70ea8..5ce67c18 100644 --- a/specifications/ewd840/EWD840_anim.cfg +++ b/specifications/ewd840/EWD840_anim.cfg @@ -8,4 +8,8 @@ ALIAS Alias INVARIANT - AnimInv \ No newline at end of file + AnimInv + +CHECK_DEADLOCK + FALSE + diff --git a/specifications/ewd840/EWD840_json.cfg b/specifications/ewd840/EWD840_json.cfg index be4afac1..a21b5511 100644 --- a/specifications/ewd840/EWD840_json.cfg +++ b/specifications/ewd840/EWD840_json.cfg @@ -2,4 +2,7 @@ CONSTANTS N = 4 SPECIFICATION Spec -INVARIANT JsonInv \ No newline at end of file +INVARIANT JsonInv + +CHECK_DEADLOCK FALSE + diff --git a/specifications/ewd998/EWD998.cfg b/specifications/ewd998/EWD998.cfg index 7a975c97..c0caebdb 100644 --- a/specifications/ewd998/EWD998.cfg +++ b/specifications/ewd998/EWD998.cfg @@ -15,3 +15,7 @@ INVARIANT \* PROPERTIES \* \* Liveness \* TDSpec + +CHECK_DEADLOCK + FALSE + diff --git a/specifications/ewd998/EWD998Chan.cfg b/specifications/ewd998/EWD998Chan.cfg index 63342323..9ebfc976 100644 --- a/specifications/ewd998/EWD998Chan.cfg +++ b/specifications/ewd998/EWD998Chan.cfg @@ -11,4 +11,8 @@ INVARIANT TypeOK PROPERTIES - EWD998Spec \ No newline at end of file + EWD998Spec + +CHECK_DEADLOCK + FALSE + diff --git a/specifications/ewd998/EWD998ChanID.cfg b/specifications/ewd998/EWD998ChanID.cfg index 570fa641..cfa3ee5e 100644 --- a/specifications/ewd998/EWD998ChanID.cfg +++ b/specifications/ewd998/EWD998ChanID.cfg @@ -16,4 +16,8 @@ PROPERTIES EWD998Live VIEW - View \ No newline at end of file + View + +CHECK_DEADLOCK + FALSE + diff --git a/specifications/ewd998/EWD998Small.cfg b/specifications/ewd998/EWD998Small.cfg index 57656f73..0d664ddb 100644 --- a/specifications/ewd998/EWD998Small.cfg +++ b/specifications/ewd998/EWD998Small.cfg @@ -15,3 +15,7 @@ INVARIANT \* PROPERTIES \* \* Liveness \* TDSpec + +CHECK_DEADLOCK + FALSE +