Model checking: deterministic config resolution + embedded .tla config picking

Author: younes-io

src/commands/checkModel.ts

@@ -1,9 +1,7 @@
 import { ChildProcess } from 'child_process';
-import { copyFile } from 'fs';
 import * as path from 'path';
 import * as vscode from 'vscode';
-import { Utils } from 'vscode-uri';
-import { LANG_TLAPLUS, LANG_TLAPLUS_CFG, exists, listFiles, replaceExtension } from '../common';
+import { LANG_TLAPLUS, LANG_TLAPLUS_CFG } from '../common';
 import { applyDCollection } from '../diagnostic';
 import { ModelCheckResult, ModelCheckResultSource, SpecFiles } from '../model/check';
 import { ToolOutputChannel } from '../outputChannels';
@@ -15,6 +13,7 @@ import {
 } from '../panels/checkResultView';
 import { TlcModelCheckerStdoutParser } from '../parsers/tlc';
 import { runTlc, stopProcess } from '../tla2tools';
+import { ModelResolveMode, resolveModelForUri } from './modelResolver';
 import { TlcCoverageDecorationProvider } from '../tlcCoverage';
 
 export const CMD_CHECK_MODEL_RUN = 'tlaplus.model.check.run';
@@ -27,8 +26,6 @@ export const CTX_TLC_RUNNING = 'tlaplus.tlc.isRunning';
 export const CTX_TLC_CAN_RUN_AGAIN = 'tlaplus.tlc.canRunAgain';
 
 const CFG_CREATE_OUT_FILES = 'tlaplus.tlc.modelChecker.createOutFiles';
-const TEMPLATE_CFG_PATH = path.resolve(__dirname, '../tools/template.cfg');
-
 let checkProcess: ChildProcess | undefined;
 let lastCheckFiles: SpecFiles | undefined;
 let coverageProvider: TlcCoverageDecorationProvider | undefined;
@@ -89,26 +86,14 @@ export async function checkModelCustom(
         return;
     }
     const doc = editor.document;
-    if (doc.languageId !== LANG_TLAPLUS) {
-        vscode.window.showWarningMessage('File in the active editor is not a .tla, it cannot be checked as a model');
+    if (doc.languageId !== LANG_TLAPLUS && doc.languageId !== LANG_TLAPLUS_CFG) {
+        vscode.window.showWarningMessage('File in the active editor is not a .tla or .cfg, it cannot be checked as a model');
         return;
     }
-    // Accept .tla files here because TLC configs and TLA+ modules can share the same file:
-    // https://github.com/tlaplus/vscode-tlaplus/issues/220
-    const configFiles = await listFiles(path.dirname(doc.uri.fsPath),
-        (fName) => fName.endsWith('.cfg') || fName.endsWith('.tla'));
-    configFiles.sort();
-    const cfgFileName = await vscode.window.showQuickPick(
-        configFiles,
-        { canPickMany: false, placeHolder: 'Select a model config file', matchOnDetail: true }
-    );
-    if (!cfgFileName || cfgFileName.length === 0) {
+    const specFiles = await getSpecFiles(doc.uri, true, true, 'customPick');
+    if (!specFiles) {
         return;
     }
-    const specFiles = new SpecFiles(
-        doc.uri.fsPath,
-        path.join(path.dirname(doc.uri.fsPath), cfgFileName)
-    );
     await doCheckModel(specFiles, true, extContext, diagnostic, true);
 }
 
@@ -186,7 +171,7 @@ export async function doCheckModel(
 ): Promise<ModelCheckResult | undefined> {
     try {
         const procInfo = await runTlc(
-            specFiles.tlaFilePath, path.basename(specFiles.cfgFilePath), showOptionsPrompt, extraOpts);
+            specFiles.tlaFilePath, specFiles.cfgFilePath, showOptionsPrompt, extraOpts);
         if (procInfo === undefined) {
             // Command cancelled by user, make sure UI state is reset
             vscode.commands.executeCommand('setContext', CTX_TLC_CAN_RUN_AGAIN, !!lastCheckFiles);
@@ -203,7 +188,7 @@ export async function doCheckModel(
             updateStatusBarItem(false, lastCheckFiles);
         });
         if (showCheckResultView) {
-            attachFileSaver(specFiles.tlaFilePath, checkProcess);
+            attachFileSaver(specFiles, checkProcess);
             revealEmptyCheckResultView(extContext);
         }
         const resultHolder = new CheckResultHolder();
@@ -242,116 +227,47 @@ export async function doCheckModel(
     return undefined;
 }
 
-function attachFileSaver(tlaFilePath: string, proc: ChildProcess) {
+function attachFileSaver(specFiles: SpecFiles, proc: ChildProcess) {
     const createOutFiles = vscode.workspace.getConfiguration().get<boolean>(CFG_CREATE_OUT_FILES);
     if (typeof(createOutFiles) === 'undefined' || createOutFiles) {
-        const outFilePath = replaceExtension(tlaFilePath, 'out');
+        const outFilePath = path.join(specFiles.outputDir, `${specFiles.modelName}.out`);
         saveStreamToFile(proc.stdout, outFilePath);
     }
 }
 
 /**
  * Finds all files that needed to run model check.
  */
-export async function getSpecFiles(fileUri: vscode.Uri, warn = true, prefix = 'MC'): Promise<SpecFiles | undefined> {
-    let specFiles;
-
-    // a) Check the given input if it exists.
-    specFiles = await checkSpecFiles(fileUri, false);
-    if (specFiles) {
-        return specFiles;
-    }
-    // b) Check alternatives:
-    // Unless the given filePath already starts with 'MC', prepend MC to the name
-    // and check if it exists. If yes, it becomes the spec file.  If not, fall back
-    // to the original file.  The assumptions is that a user usually has  Spec.tla
-    // open in the editor and doesn't want to switch to  MC.tla  before model-checking.
-    // TODO: Ideally, we wouldn't just check filenames here but check the parse result
-    // TODO: if the module in  MCSpec.tla  actually extends the module in  Spec.
-    const b = Utils.basename(fileUri);
-    if (!b.startsWith(prefix) && !b.endsWith('.cfg')) {
-        const str = fileUri.toString();
-        const n = str.substr(0, str.lastIndexOf(b)) + prefix + b;
-        const filePath = vscode.Uri.parse(n).fsPath;
-        specFiles = new SpecFiles(filePath, replaceExtension(filePath, 'cfg'));
-        // Here, we make sure that the .cfg *and* the .tla exist.
-        let canRun = true;
-        canRun = await checkModelExists(specFiles.cfgFilePath, warn);
-        canRun = canRun && await checkModuleExists(specFiles.tlaFilePath, warn);
-        if (canRun) {
-            return specFiles;
-        }
-    }
-    // c) Deliberately trigger the warning dialog by checking the given input again
-    // knowing that it doesn't exist.
-    return await checkSpecFiles(fileUri, warn);
-}
-
-async function checkSpecFiles(fileUri: vscode.Uri, warn = true): Promise<SpecFiles | undefined> {
-    const filePath = fileUri.fsPath;
-    let specFiles;
-    let canRun = true;
-    if (filePath.endsWith('.cfg')) {
-        specFiles = new SpecFiles(replaceExtension(filePath, 'tla'), filePath);
-        canRun = await checkModuleExists(specFiles.tlaFilePath, warn);
-    } else if (filePath.endsWith('.tla')) {
-        specFiles = new SpecFiles(filePath, replaceExtension(filePath, 'cfg'));
-        canRun = await checkModelExists(specFiles.cfgFilePath, warn);
-    }
-    return canRun ? specFiles : undefined;
-}
-
-async function checkModuleExists(modulePath: string, warn = true): Promise<boolean> {
-    const moduleExists = await exists(modulePath);
-    if (!moduleExists && warn) {
-        const moduleFile = path.basename(modulePath);
-        vscode.window.showWarningMessage(`Corresponding TLA+ module file ${moduleFile} doesn't exist.`);
-    }
-    return moduleExists;
-}
-
-async function checkModelExists(cfgPath: string, warn = true): Promise<boolean> {
-    const cfgExists = await exists(cfgPath);
-    if (!cfgExists && warn) {
-        showConfigAbsenceWarning(cfgPath);
+export async function getSpecFiles(
+    fileUri: vscode.Uri,
+    warn = true,
+    interactive = true,
+    mode: ModelResolveMode = 'adjacent'
+): Promise<SpecFiles | undefined> {
+    const resolved = await resolveModelForUri(fileUri, warn, interactive, mode);
+    if (!resolved) {
+        return undefined;
     }
-    return cfgExists;
+    return new SpecFiles(
+        resolved.tlaPath,
+        resolved.cfgPath,
+        resolved.modelName,
+        resolved.outputDir
+    );
 }
 
 function updateStatusBarItem(active: boolean, specFiles: SpecFiles | undefined) {
     statusBarItem.text = 'TLC' + (active ?
-        (specFiles === undefined ? '' : ' (' + specFiles.tlaFileName + '/' + specFiles.cfgFileName + ')')
+        (specFiles === undefined ? '' : ` (Model: ${specFiles.modelName})`)
         + ' $(gear~spin)' : '');
     statusBarItem.tooltip = 'TLA+ model checking' + (active ?
-        (specFiles === undefined ? '' : ' of ' + specFiles.tlaFileName + '/' + specFiles.cfgFileName)
+        (specFiles === undefined ? '' : ` of model ${specFiles.modelName}`)
         + ' is running' : ' result');
     statusBarItem.command = CMD_CHECK_MODEL_DISPLAY;
     statusBarItem.show();
     vscode.commands.executeCommand('setContext', CTX_TLC_RUNNING, active);
 }
 
-function showConfigAbsenceWarning(cfgPath: string) {
-    const fileName = path.basename(cfgPath);
-    const createOption = 'Create model file';
-    vscode.window.showWarningMessage(`Model file ${fileName} doesn't exist. Cannot check model.`, createOption)
-        .then((option) => {
-            if (option === createOption) {
-                createModelFile(cfgPath);
-            }
-        });
-}
-
-async function createModelFile(cfgPath: string) {
-    copyFile(TEMPLATE_CFG_PATH, cfgPath, (err) => {
-        if (err) {
-            console.warn(`Error creating config file: ${err}`);
-            vscode.window.showWarningMessage(`Cannot create model file: ${err}`);
-            return;
-        }
-        vscode.workspace.openTextDocument(cfgPath)
-            .then(doc => vscode.window.showTextDocument(doc));
-    });
-}
 
 export function mapTlcOutputLine(line: string): string | undefined {
     if (line === '') {