From 7613bf1b2bc1e24f8f718b16427f835647d529be Mon Sep 17 00:00:00 2001 From: Markus Alexander Kuppe Date: Fri, 30 Jan 2026 13:38:33 -0800 Subject: [PATCH] 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 https://github.com/tlaplus/vscode-tlaplus/issues/483 [Bug] Signed-off-by: Markus Alexander Kuppe --- src/tla2tools.ts | 4 ++-- tests/suite/tla2tools.test.ts | 28 ++++++++++++++++++++++++++++ 2 files changed, 30 insertions(+), 2 deletions(-) diff --git a/src/tla2tools.ts b/src/tla2tools.ts index 3241e0b0..656b5e81 100644 --- a/src/tla2tools.ts +++ b/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 { 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); diff --git a/tests/suite/tla2tools.test.ts b/tests/suite/tla2tools.test.ts index f0a5e8fc..03ec5938 100644 --- a/tests/suite/tla2tools.test.ts +++ b/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(