Mostly complete proof of concept for state generation in web worker

js/app.js

@@ -64,6 +64,7 @@ let model = {
     specEditorChanges: [],
     enableAnimationView: false,
     explodedConstantExpr: null,
+    generatingInitStates: false,
     // Special definition that will enable animation feature.
     animViewDefName: "AnimView"
 }
@@ -921,6 +922,12 @@ function reloadSpec() {
     let interp = new TlaInterpreter();
     const start = performance.now();
 
+    // TODO: Can work on this more to consider web workers for off-thread state generation.
+    // console.log("Starting web worker for state generation.");
+    // model.generatingInitStates = true;
+    // startWebWorker();   
+    // return;
+
     // let allInitStates;
     let initStates;
     try {
@@ -1363,8 +1370,20 @@ function componentTraceViewer(hidden) {
 // TODO: Think about more fully fledged worker execution framework.
 function startWebWorker(){
     const myWorker = new Worker("js/worker.js");
-    myWorker.postMessage([{a:1,b:2}, {c:4,d:5, spec: model.specTreeObjs}]);
+    myWorker.postMessage({
+        newText: model.specText,
+        specPath: model.specPath,
+        constValInputs: model.specConstInputVals
+    });
     console.log("Message posted to worker");
+
+    myWorker.onmessage = function(e) {
+        console.log("Message received from worker");
+        let response = e.data;
+        console.log("Response from worker:", response);
+        model.generatingInitStates = false;
+        m.redraw();
+    };
 }
 
 // Called when an updated spec is finished being re-parsed.
@@ -2184,6 +2203,10 @@ async function loadApp() {
 
             let spinner = fetchingInProgress ? m("div", {class:"spinner-border spinner-border-sm"}) : m("span");
             let fetchingText = fetchingInProgress ? "Fetching spec... " : "";
+            if(model.generatingInitStates){
+                fetchingText = "(Generating initial states...) ";
+                spinner = m("div", {class:"spinner-border spinner-border-sm"});
+            }
             let parseError = isParseErr ? m("span", {class:"bi-exclamation-triangle", style:{"color":"red", "margin-left":"5px"}}, " Parse error.") : m("span");
 
             return [

js/worker.js

@@ -2,10 +2,97 @@
 
 console.log("Worker is running...")
 
-onmessage = (e) => {
+self.importScripts('tree-sitter.js');
+self.importScripts('eval.js');
+self.importScripts('https://cdn.jsdelivr.net/npm/lodash@4.17.21/lodash.min.js');
+self.importScripts('hash-sum/hash-sum.js');
+
+let parser;
+let languageName = "tlaplus";
+let enableEvalTracing = false;
+
+onmessage = async (e) => {
+
+
+    let newText = e.data.newText;
+    let specPath = e.data.specPath;
+    let constValInputs = e.data.constValInputs;
+
+    await TreeSitter.init();
+    parser = new TreeSitter();
+
+    let tree = null;
+    var ASSIGN_PRIMED = false;
+
+
+    // Load the tree-sitter TLA+ parser.
+    let language;
+    LANGUAGE_BASE_URL = "js";
+    const url = `/${LANGUAGE_BASE_URL}/tree-sitter-${languageName}.wasm`;
+    try {
+        console.log("Loading language from", url);
+        language = await TreeSitter.Language.load(url);
+    } catch (e) {
+        console.error(e);
+        return;
+    }
+
+    tree = null;
+    parser.setLanguage(language);
+
     console.log("Message received from main script");
     const workerResult = `Result: ${e.data}`;
     console.log(e.data);
     console.log("Posting message back to main script");
-    postMessage(workerResult);
+
+    let spec = new TLASpec(newText, specPath);
+    return spec.parse().then(function(){
+        console.log("SPEC WAS PARSED IN WEBWORKER.", spec);
+
+        let constVals = {};
+        let constTlaVals = {};
+
+        // Evaluate each CONSTANT value expression.
+        for (var constDecl in constValInputs) {
+            let constValText = constValInputs[constDecl];
+            if (constValText === undefined) {
+                throw "no constant value given for " + constDecl;
+            }
+            console.log("constDecl:", constDecl, constValText);
+            constVals[constDecl] = constValText;
+
+            let model = {};
+            model.specDefs = spec.spec_obj["op_defs"]
+
+            let ctx = new Context(null, new TLAState({}), model.specDefs, {}, constTlaVals);
+            // Flag so that we treat unknown identifiers as model values during evaluation.
+            ctx.evalModelVals = true;
+            let cVal = evalExprStrInContext(ctx, constValText);
+            console.log("cval:", cVal);
+            constTlaVals[constDecl] = cVal;
+        }
+
+        console.log("constTlaVals:", constTlaVals);
+
+
+        // Generate initial states.
+        let interp = new TlaInterpreter();
+
+        let start = performance.now();
+        let initStates = interp.computeInitStates(spec.spec_obj, constTlaVals, false);
+        const duration = (performance.now() - start).toFixed(1);
+        console.log("INIT STATES IN WEBWORKER.", initStates, `duration: ${duration}ms`);
+
+        // Seems it is fine to serialize TLAState objects back through the web worker.
+        postMessage(initStates[0]);
+
+
+    }).catch(function(e){
+        console.log("Error parsing and loading spec.", e);
+        // model.errorObj = {parseError: true, obj: e, message: "Error parsing spec."};
+    });
+
+
+
+
 };