Don't use JVM assertions by default in scripts

Expose --enable_assertions flag

Signed-off-by: Andrew Helwer <ahelwer@pm.me>

.github/scripts/check_small_models.py

@@ -20,6 +20,7 @@
 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=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
+parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')
 args = parser.parse_args()
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
@@ -32,6 +33,7 @@
 examples_root = dirname(manifest_path)
 skip_models = args.skip
 only_models = args.only
+enable_assertions = args.enable_assertions
 
 def check_model(module, model, expected_runtime):
     module_path = tla_utils.from_cwd(examples_root, module['path'])
@@ -49,6 +51,7 @@ def check_model(module, model, expected_runtime):
         model['mode'],
         module['features'],
         model['features'],
+        enable_assertions,
         hard_timeout_in_seconds
     )
     end_time = timer()

.github/scripts/parse_modules.py

@@ -19,6 +19,7 @@
 parser.add_argument('--skip', nargs='+', help='Space-separated list of .tla modules to skip parsing', required=False, default=[])
 parser.add_argument('--only', nargs='+', help='If provided, only parse models in this space-separated list', required=False, default=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
+parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')
 args = parser.parse_args()
 
 logging.basicConfig(level = logging.DEBUG if args.verbose else logging.INFO)
@@ -31,27 +32,26 @@
 examples_root = dirname(manifest_path)
 skip_modules = args.skip
 only_modules = args.only
+enable_assertions = args.enable_assertions
 
 def parse_module(path):
     """
     Parse the given module using SANY.
     """
     logging.info(path)
     # Jar paths must go first
-    search_paths = pathsep.join([
-        tools_jar_path,
-        apalache_jar_path,
-        dirname(path),
-        community_modules,
-        tlaps_modules
-    ])
-    sany = subprocess.run([
-            'java',
-            '-cp', search_paths,
-            'tla2sany.SANY',
-            '-error-codes',
-            path
-        ],
+    jvm_parameters = [
+        '-cp', pathsep.join([
+            tools_jar_path,
+            apalache_jar_path,
+            dirname(path),
+            community_modules,
+            tlaps_modules
+        ])
+    ] + (['-enableassertions'] if enable_assertions else [])
+    sany_parameters = ['-error-codes', path]
+    sany = subprocess.run(
+        ['java'] + jvm_parameters + ['tla2sany.SANY'] + sany_parameters,
         stdout=subprocess.PIPE,
         stderr=subprocess.STDOUT,
         text=True

.github/scripts/smoke_test_large_models.py

@@ -20,6 +20,7 @@
 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=[])
 parser.add_argument('--verbose', help='Set logging output level to debug', action='store_true')
+parser.add_argument('--enable_assertions', help='Enable Java assertions (pass -enableassertions to JVM)', action='store_true')
 args = parser.parse_args()
 
 tools_jar_path = normpath(args.tools_jar_path)
@@ -30,6 +31,7 @@
 examples_root = dirname(manifest_path)
 skip_models = args.skip
 only_models = args.only
+enable_assertions = args.enable_assertions
 
 def check_model(module, model):
     module_path = tla_utils.from_cwd(examples_root, module['path'])
@@ -46,6 +48,7 @@ def check_model(module, model):
         model['mode'],
         module['features'],
         model['features'],
+        enable_assertions,
         smoke_test_timeout_in_seconds
     )
     match tlc_result:

.github/scripts/tla_utils.py

@@ -123,6 +123,7 @@ def check_model(
         mode,
         module_features,
         model_features,
+        enable_assertions,
         hard_timeout_in_seconds
     ):
     """
@@ -149,8 +150,7 @@ def check_model(
             )
             return apalache
         else:
-            jvm_parameters = [
-                '-enableassertions',
+            jvm_parameters = (['-enableassertions'] if enable_assertions else []) + [
                 '-Dtlc2.TLC.ide=Github',
                 '-Dutil.ExecutionStatisticsCollector.id=abcdef60f238424fa70d124d0c77ffff',
                 '-XX:+UseParallelGC',