Fixed failing test by readding generation guard in vampire

Author: ShaunRose

src/java/com/articulate/sigma/tp/Vampire.java

@@ -21,6 +21,7 @@ portions copyright Teknowledge (c) 2003 and reused under the terms of the GNU li
 import com.articulate.sigma.trans.SessionTPTPManager;
 import com.articulate.sigma.trans.THFnew;
 import com.articulate.sigma.trans.TPTP3ProofProcessor;
+import com.articulate.sigma.trans.TPTPGenerationManager;
 import com.articulate.sigma.trans.TPTPutil;
 import com.articulate.sigma.utils.FileUtil;
 import com.articulate.sigma.utils.StringUtil;
@@ -181,6 +182,13 @@ else if ("tff".equalsIgnoreCase(requestedTptpLang)){
         this.timeout = timeout;
         this.maxAnswers = maxAnswers;
         this.inferenceFilePath = KBmanager.getMgr().getPref("kbDir") + File.separator + KBmanager.getMgr().getPref("sumokbname") + "." + this.inferenceFileExtension;
+        if (!(new File(this.inferenceFilePath).exists()) || KBmanager.getMgr().infBaseFileOldIgnoringUserAssertions(this.inferenceFileExtension)) {
+            System.out.println("INFO in KB.loadVampire(): this.inferenceFilePath=" + !(new File(this.inferenceFilePath).exists()));
+            System.out.println("INFO in KB.loadVampire(): managerInfFileOld " + KBmanager.getMgr().infFileOld());
+            synchronized (kb.baseGenLock) {
+                TPTPGenerationManager.generateProperFile(kb, this.requestedTptpLanguage);
+            }
+        }
     }
 
     /***************************************************************
@@ -371,6 +379,18 @@ public void askVampireHOL(String stmt, boolean useModals) {
             File thfAxioms = new File(kbThfPath);
             if (!thfAxioms.exists()) {
                 System.out.println("Vampire.askVampireHOL(): no such file: " + kbThfPath + ". Waiting for background generation or creating it.");
+                // Wait for background THF generation if in progress, otherwise generate synchronously
+                if (useModals) {
+                    if (!TPTPGenerationManager.waitForTHFModal(600)) {
+                        System.out.println("Vampire.askVampireHOL(): Background generation not ready, generating THF Modal synchronously");
+                        THFnew.transModalTHF(this.kb);
+                    }
+                } else {
+                    if (!TPTPGenerationManager.waitForTHFPlain(600)) {
+                        System.out.println("Vampire.askVampireHOL(): Background generation not ready, generating THF Plain synchronously");
+                        THFnew.transPlainTHF(this.kb);
+                    }
+                }
             }
             // -------- 2. Prepare temp-stmt.thf and temp-comb.thf (mirrors FOF/TFF run() pattern) --------
             String stmtFile = dir + "temp-stmt." + this.inferenceFileExtension;