Fix filename variable substitution to strip any extension

When using ${modelName} or ${specName} in TLC custom options, the
variables now correctly resolve to the base filename without extension,
regardless of whether the file has a .cfg or .tla extension.

Previously, path.basename(file, '.ext') would only strip the specified
extension, causing ${modelName}.dot to expand to "Model.tla.dot" when
the config was embedded in a .tla file instead of the expected
"Model.dot".

Now using path.parse(file).name which properly strips any extension.

Fixes Github issue #483
#483

[Bug]

Signed-off-by: Markus Alexander Kuppe <github.com@lemmster.de>

Author: lemmy

src/tla2tools.ts

@@ -484,8 +484,8 @@ export function extractFingerprintFromTrace(traceFilePath: string): number | und
 export async function buildTlcOptions(tlaFilePath: string, cfgFilePath: string, customOptions: string[]): Promise<string[]> {
     const custOpts = customOptions.map((opt) => {
         return opt
-            .replace(VAR_TLC_SPEC_NAME, path.basename(tlaFilePath, '.tla'))
-            .replace(VAR_TLC_MODEL_NAME, path.basename(cfgFilePath, '.cfg'));
+            .replace(VAR_TLC_SPEC_NAME, path.parse(tlaFilePath).name)
+            .replace(VAR_TLC_MODEL_NAME, path.parse(cfgFilePath).name);
     });
     const opts = [path.basename(tlaFilePath), '-tool', '-modelcheck'];
     addValueOrDefault('-config', cfgFilePath, custOpts, opts);

tests/suite/tla2tools.test.ts

@@ -103,6 +103,34 @@ suite('TLA+ Tools Test Suite', () => {
         assert.strictEqual(result[dumpIdx + 2], 'bar.dot');
     });
 
+    test('Strips .tla extension from modelName when CONFIG is embedded (regression for #483)', async () => {
+        const result = await buildTlcOptions(
+            '/path/to/HourClock.tla',
+            '/path/to/HourClock.tla',
+            ['-dump', 'dot,colorize,actionlabels', '${modelName}.dot']
+        );
+        assert.strictEqual(result[0], 'HourClock.tla');
+        assert.ok(result.includes('-dump'));
+        const dumpIdx = result.indexOf('-dump');
+        assert.strictEqual(result[dumpIdx + 1], 'dot,colorize,actionlabels');
+        assert.strictEqual(result[dumpIdx + 2], 'HourClock.dot',
+            'modelName should expand to HourClock.dot, not HourClock.tla.dot');
+    });
+
+    test('Strips .tla extension from specName when CONFIG is embedded', async () => {
+        const result = await buildTlcOptions(
+            '/path/to/HourClock.tla',
+            '/path/to/HourClock.tla',
+            ['-dump', 'dot', '${specName}.dot']
+        );
+        assert.strictEqual(result[0], 'HourClock.tla');
+        assert.ok(result.includes('-dump'));
+        const dumpIdx = result.indexOf('-dump');
+        assert.strictEqual(result[dumpIdx + 1], 'dot');
+        assert.strictEqual(result[dumpIdx + 2], 'HourClock.dot',
+            'specName should expand to HourClock.dot, not HourClock.tla.dot');
+    });
+
     test('Provides default classpath and GC in Java options', async () => {
         assert.deepEqual(
             buildJavaOptions(