✨Start alloy-app migration from meteor to react

frontend/src/api/alloyApi.js

@@ -0,0 +1,34 @@
+import axios from "axios";
+import { saveCode } from "./playgroundApi";
+
+const ALLOY_API_URL = import.meta.env.VITE_ALLOY_API_URL;
+const MAX_INSTANCES = import.meta.env.VITE_ALLOY_MAX_INSTANCES;
+
+/**
+ * Method to execute the current model and get model instances.
+ * This will call the Alloy API (webService). If the model contains
+ * secrets and the previous didn't (if any), will become a new derivation
+ * root (although it still registers the derivation).
+ *
+ * @param {String} code the Alloy model to execute
+ * @param {Number} commandIndex the index of the command to execute
+ * @param {String} currentModelId the id of the current model (from which the new will derive)
+ *
+ * @returns the instance data and the id of the new saved model
+ */
+export async function getInstances(code, commandIndex, currentModelId) {
+  let url = `${ALLOY_API_URL}/getInstances`;
+  // saveCode(code);
+  try {
+    const response = await axios.post(url, {
+      model: code,
+      numberOfInstances: MAX_INSTANCES,
+      commandIndex: commandIndex,
+      sessionId: currentModelId,
+    });
+    return response.data;
+  } catch (error) {
+    console.log(error);
+  }
+}
+

frontend/src/assets/js/runZ3.js

@@ -1,54 +1,9 @@
-import { init } from 'z3-solver';
+import { Z3HighLevel, Z3LowLevel } from 'z3-solver';
 
+window.Z3LoadedPromise = new Promise((resolve, reject) => {
+  window.Processors = [
+    new StdinToStdoutProcessor(Z3HighLevel, resolve, reject),
+    new StdinToStdoutProcessor(Z3LowLevel, resolve, reject),
+  ];
+});
 
-let evalZ3JSPromise = null;
-async function loadEvalZ3() {
-  if (evalZ3JSPromise != null) {
-    return evalZ3JSPromise;
-  }
-  evalZ3JSPromise = new Promise((res, rej) => {
-    const script = document.createElement('script');
-    script.src = '/z3guide/eval-z3.js';
-    script.onload = () => {
-      res(window.evalZ3Mod.evalZ3JS);
-    };
-    script.onerror = rej;
-    document.head.appendChild(script);
-  });
-  return evalZ3JSPromise;
-}
-
-let Z3Promise = null;
-async function loadZ3() {
-  if (Z3Promise != null) {
-    return Z3Promise;
-  }
-  Z3Promise = init();
-  return Z3Promise;
-}
-
-export default async function runZ3JSWeb(input) {
-  let output = '';
-  let error = '';
-  let timeStart, timeEnd;
-
-  const Z3 = await loadZ3();
-  const timeout = 10000;
-
-  try {
-    Z3.Z3.global_param_set('timeout', String(timeout));
-    timeStart = new Date().getTime();
-    const evalZ3JS = await loadEvalZ3();
-    output = (await evalZ3JS(Z3, input)) ?? '';
-  } catch (e) {
-    error = e.message ?? 'Error message is empty';
-    if (timeStart) {
-      timeEnd = new Date().getTime();
-      if (timeEnd - timeStart >= timeout) {
-        error = error + '\nZ3 timeout\n';
-      }
-    }
-  }
-
-  return JSON.stringify({ output: String(output), error: error });
-}