Merge pull request #42 from sanctuuary/dev

Update APE to 1.1.3

pom.xml

@@ -4,7 +4,7 @@
 	<modelVersion>4.0.0</modelVersion>
 	<groupId>io.github.sanctuuary</groupId>
 	<artifactId>APE</artifactId>
-	<version>1.1.2</version>
+	<version>1.1.3</version>
 	<packaging>jar</packaging>
 	<name>io.github.sanctuuary:APE</name>
 	<description>APE is a command line tool and an API for the automated exploration of possible computational pipelines (workflows) from large collections of computational tools.</description>

src/main/java/nl/uu/cs/ape/sat/APE.java

@@ -306,7 +306,7 @@ private SATsolutionsList executeSynthesis(APERunConfig runConfig) throws IOExcep
 		APEUtils.timerStart(globalTimerID, true);
 		int solutionLength = runConfig.getSolutionLength().getMin();
 		while (allSolutions.getNumberOfSolutions() < allSolutions.getMaxNumberOfSolutions()
-				&& solutionLength <= runConfig.getSolutionLength().getMax()) {
+				&& solutionLength <= runConfig.getSolutionLength().getMax() && APEUtils.timerTimeLeft("globalTimer", runConfig.getTimeoutMs()) > 0) {
 
 			SAT_SynthesisEngine implSATsynthesis = new SAT_SynthesisEngine(apeDomainSetup, allSolutions, runConfig,
 					solutionLength);
@@ -319,17 +319,22 @@ private SATsolutionsList executeSynthesis(APERunConfig runConfig) throws IOExcep
 				return null;
 			}
 			/* Execution of the synthesis - updates the object allSolutions */
-			implSATsynthesis.synthesisExecution();
+			allSolutions.addSolutions(implSATsynthesis.synthesisExecution());
+			implSATsynthesis.deleteTempFiles();
 			allSolutions.addNoSolutionsForLength(solutionLength, allSolutions.getNumberOfSolutions());
 
-			if ((allSolutions.getNumberOfSolutions() >= allSolutions.getMaxNumberOfSolutions() - 1)
-					|| solutionLength == runConfig.getSolutionLength().getMax()) {
-				APEUtils.timerPrintSolutions(globalTimerID, allSolutions.getNumberOfSolutions());
-			}
-
 			/* Increase the size of the workflow for the next depth iteration */
 			solutionLength++;
 		}
+
+		if ((allSolutions.getNumberOfSolutions() >= allSolutions.getMaxNumberOfSolutions() - 1)) {
+			System.out.println("All required solutions found.");
+		} else if (solutionLength == runConfig.getSolutionLength().getMax()) {
+			System.out.println("Maximum solution length reached.");
+		} else if(APEUtils.timerTimeLeft("globalTimer", runConfig.getTimeoutMs()) <= 0) {
+			System.out.println("Timeout was reached.");
+		}
+		APEUtils.timerPrintSolutions(globalTimerID, allSolutions.getNumberOfSolutions());
 
 		return allSolutions;
 	}

src/main/java/nl/uu/cs/ape/sat/configuration/APERunConfig.java

@@ -75,6 +75,10 @@ public class APERunConfig {
      * Mode is true if debug mode is turned on.
      */
     public final APEConfigTag<Boolean> DEBUG_MODE = new APEConfigTagFactory.TAGS.DEBUG_MODE();
+    /**
+     * Synthesis timeout in seconds.
+     */
+    public final APEConfigTag<Integer> TIMEOUT_SEC = new APEConfigTagFactory.TAGS.TIMEOUT_SEC();
     /**
      * false iff the provided solutions should be distinguished based on the tool
      * sequences alone, i.e. tool sequences cannot repeat, ignoring the types in the
@@ -102,6 +106,7 @@ public class APERunConfig {
             this.USE_WORKFLOW_INPUT,
             this.USE_ALL_GENERATED_DATA,
             this.DEBUG_MODE,
+            this.TIMEOUT_SEC,
             this.TOOL_SEQ_REPEAT,
             this.PROGRAM_OUTPUTS,
             this.PROGRAM_INPUTS
@@ -120,6 +125,7 @@ public class APERunConfig {
             new USE_WORKFLOW_INPUT(),
             new USE_ALL_GENERATED_DATA(),
             new DEBUG_MODE(),
+            new TIMEOUT_SEC(),
             new TOOL_SEQ_REPEAT(),
             new PROGRAM_OUTPUTS(null),
             new PROGRAM_INPUTS(null)
@@ -153,6 +159,7 @@ private APERunConfig(Builder builder) {
         setUseWorkflowInput(builder.useWorkflowInput);
         setUseAllGeneratedData(builder.useAllGeneratedData);
         setDebugMode(builder.debugMode);
+        setTimeoutSec(builder.timeoutSec);
         setProgramInputs(builder.programInputs);
         setProgramOutputs(builder.programOutputs);
     }
@@ -467,6 +474,30 @@ public ConfigEnum getUseAllGeneratedData() {
     public void setUseAllGeneratedData(ConfigEnum useAllGeneratedData) {
         USE_ALL_GENERATED_DATA.setValue(useAllGeneratedData);
     }
+
+    /**
+     * Get timeout (in seconds) how long the execution should last.
+     * @return Timeout in seconds.
+     */
+    public int getTimeoutSec() {
+    	return TIMEOUT_SEC.getValue();
+    }
+
+    /**
+     * Get timeout (in ms) how long the execution should last.
+     * @return Timeout in seconds.
+     */
+    public int getTimeoutMs() {
+    	return TIMEOUT_SEC.getValue() * 1000;
+    }
+
+    /**
+     * Set the timeout in sec.
+     * @param timeoutSec
+     */
+    public void setTimeoutSec(int timeoutSec) {
+    	TIMEOUT_SEC.setValue(timeoutSec);
+    }
 
     /**
      * Gets debug mode.
@@ -524,7 +555,7 @@ public interface IApeDomainSetupStage {
     public interface IBuildStage {
         IBuildStage withConstraintsJSON(JSONObject constraintsJSON);
 
-        IBuildStage withToolSeqRepeat(boolean toolSeqRepeat);
+		IBuildStage withToolSeqRepeat(boolean toolSeqRepeat);
 
         IBuildStage withSolutionDirPath(String solutionPath);
 
@@ -541,6 +572,8 @@ public interface IBuildStage {
         IBuildStage withUseAllGeneratedData(ConfigEnum useAllGeneratedData);
 
         IBuildStage withDebugMode(boolean debugMode);
+
+        IBuildStage withTimeoutSec(int timeoutSec);
 
         APERunConfig build();
     }
@@ -564,6 +597,7 @@ public static final class Builder implements ISolutionMinLengthStage, ISolutionM
         private ConfigEnum useWorkflowInput;
         private ConfigEnum useAllGeneratedData;
         private boolean debugMode;
+        private int timeoutSec;
 
         private Builder() {
         }
@@ -652,6 +686,12 @@ public IBuildStage withDebugMode(boolean debugMode) {
             this.debugMode = debugMode;
             return this;
         }
+
+        @Override
+        public IBuildStage withTimeoutSec(int timeout) {
+            this.timeoutSec = timeout;
+            return this;
+        }
 
         @Override
         public APERunConfig build() {

src/main/java/nl/uu/cs/ape/sat/configuration/tags/APEConfigTagFactory.java

@@ -745,6 +745,39 @@ protected ValidationResults validate(Integer value, ValidationResults results) {
                 return results;
             }
         }
+
+        public static class TIMEOUT_SEC extends TYPES.Int {
+
+            public TIMEOUT_SEC() {
+                super(Range.of(0, Integer.MAX_VALUE));
+            }
+
+            @Override
+            public String getTagName() {
+                return "timeout(sec)";
+            }
+
+            @Override
+            public String getLabel() {
+                return "Timeout (in sec)";
+            }
+
+            @Override
+            public String getDescription() {
+                //TODO
+                return "";
+            }
+
+            @Override
+            protected ValidationResults validate(Integer value, ValidationResults results) {
+                return results;
+            }
+
+            @Override
+            public APEConfigDefaultValue<Integer> getDefault() {
+                return APEConfigDefaultValue.withDefault(300);
+            }
+        }
 
         public static class USE_WORKFLOW_INPUT extends TYPES.Option<ConfigEnum> {
 

src/main/java/nl/uu/cs/ape/sat/core/SynthesisEngine.java

@@ -1,6 +1,10 @@
 package nl.uu.cs.ape.sat.core;
 
+import java.io.FileNotFoundException;
 import java.io.IOException;
+import java.util.List;
+
+import nl.uu.cs.ape.sat.core.solutionStructure.SolutionWorkflow;
 
 /**
  * The {@code SynthesisEngine} interface is used as a template in order to implement different synthesis approaches over the given input.
@@ -21,7 +25,8 @@ public interface SynthesisEngine {
      * Synthesis execution boolean.
      *
      * @return the boolean
+     * @throws IOException sat encoding not defined 
      */
-    public boolean synthesisExecution();
+    public List<SolutionWorkflow> synthesisExecution() throws FileNotFoundException, IOException;
 
 }

src/main/java/nl/uu/cs/ape/sat/core/implSAT/SAT_SynthesisEngine.java

@@ -22,6 +22,7 @@
 
 import java.io.File;
 import java.io.FileInputStream;
+import java.io.FileNotFoundException;
 import java.io.IOException;
 import java.io.InputStream;
 import java.io.RandomAccessFile;
@@ -64,12 +65,11 @@ public class SAT_SynthesisEngine implements SynthesisEngine {
      * CNF encoding of the problem.
      */
     private File cnfEncoding;
-//    private StringBuilder cnfEncoding;
 
     /**
-     * String used as an input for the SAT solver.
+     * File used as an input for the SAT solver.
      */
-    private InputStream tmpSatInput;
+    private File satInputFile;
 
     /**
      * Representation of the tool part of the automaton used to encode the structure of the solution.
@@ -97,9 +97,8 @@ public SAT_SynthesisEngine(APEDomainSetup domainSetup, SATsolutionsList allSolut
         this.runConfig = runConfig;
         allSolutions.newEncoding();
         this.mappings = allSolutions.getMappings();
-        this.tmpSatInput = null;
+        this.satInputFile = null;
         this.cnfEncoding = File.createTempFile("satCNF" + workflowLength, null);
-        cnfEncoding.deleteOnExit();
 
         int maxNoToolInputs = Math.max(domainSetup.getMaxNoToolInputs(), runConfig.getProgramOutputs().size());
         int maxNoToolOutputs = Math.max(domainSetup.getMaxNoToolOutputs(), runConfig.getProgramInputs().size());
@@ -133,7 +132,7 @@ public boolean synthesisEncoding() throws IOException {
         APEUtils.timerRestartAndPrint(currLengthTimer, "Tool I/O constraints");
 
         /*
-         * The constraints preserve the memory structure (e.g. shared memory structure), i.e. preserve the data available in memory and the
+         * The constraints preserve the memory structure, i.e. preserve the data available in memory and the
          * logic of referencing data from memory in case of tool inputs.
          */
         APEUtils.appendToFile(cnfEncoding, SATModuleUtils.encodeMemoryStructure(this));
@@ -209,14 +208,11 @@ public boolean synthesisEncoding() throws IOException {
         APEUtils.timerRestartAndPrint(currLengthTimer, "Reading rows");
         System.out.println();
 
-        File satInputFile = APEUtils.concatIntoFile(sat_input_header, cnfEncoding);
+        satInputFile = APEUtils.concatIntoFile(sat_input_header, cnfEncoding);
+        cnfEncoding.delete();
 //		APEUtils.write2file(mknfEncoding.toString(), new File("/home/vedran/Desktop/tmp"+ problemSetupStartTime), false);
 
 
-
-        tmpSatInput = new FileInputStream(satInputFile);
-
-
         /* testing sat input */
 //		InputStream tmpSat = IOUtils.toInputStream(mknfEncoding.toString(), "ASCII");
 //		tmpSat.close();
@@ -233,15 +229,17 @@ public boolean synthesisEncoding() throws IOException {
     /**
      * Using the SAT input generated from SAT encoding and running MiniSAT solver to find the solutions.
      *
-     * @return true if the synthesis execution results in new candidate solutions, otherwise false.
+     * @return The list of new solutions.
+     * @throws IOException  Error if the sat encoding file does not exist.
      */
-    public boolean synthesisExecution() {
+    public List<SolutionWorkflow> synthesisExecution() throws IOException {
 
+    	InputStream tmpSatInput = new FileInputStream(satInputFile);
         List<SolutionWorkflow> currSolutions = runMiniSAT(tmpSatInput,
                 allSolutions.getNumberOfSolutions(), allSolutions.getMaxNumberOfSolutions());
-
+        tmpSatInput.close();
         /* Add current solutions to list of all solutions. */
-        return allSolutions.addSolutions(currSolutions);
+        return currSolutions;
     }
 
     /**
@@ -263,9 +261,14 @@ public String getCnfEncoding() {
     private List<SolutionWorkflow> runMiniSAT(InputStream sat_input, int solutionsFound, int solutionsFoundMax) {
         List<SolutionWorkflow> solutions = new ArrayList<SolutionWorkflow>();
         ISolver solver = SolverFactory.newDefault();
-        int timeout = 3600;
-        // 1 hour timeout
-        solver.setTimeout(timeout);
+        long globalTimeoutMs = runConfig.getTimeoutMs();
+		long currTimeout = APEUtils.timerTimeLeft("globalTimer", globalTimeoutMs);
+		if (currTimeout <= 0) {
+			System.err.println("Timeout. Total solving took longer than the timeout: " + globalTimeoutMs + " ms.");
+			return solutions;
+		}
+        // set timeout (in ms)
+        solver.setTimeoutMs(currTimeout);
         long realStartTime = 0;
         long realTimeElapsedMillis;
         Reader reader = new DimacsReader(solver);
@@ -297,7 +300,7 @@ private List<SolutionWorkflow> runMiniSAT(InputStream sat_input, int solutionsFo
                 System.err.println("Unsatisfiable");
             }
         } catch (TimeoutException e) {
-            System.err.println("Timeout. Solving took longer than the default timeout: " + timeout + " seconds.");
+            System.err.println("Timeout. Total solving took longer than the timeout: " + globalTimeoutMs + " ms.");
         } catch (IOException e) {
             System.err.println("Internal error while parsing the encoding.");
         }
@@ -384,4 +387,13 @@ public int getSolutionSize() {
         return moduleAutomaton.size();
     }
 
+    /**
+     * Delete all temporary files created.
+     */
+	public void deleteTempFiles() {
+		cnfEncoding.delete();
+		satInputFile.delete();
+
+	}
+
 }

src/main/java/nl/uu/cs/ape/sat/models/SATEncodingUtils/SATModuleUtils.java

@@ -202,7 +202,7 @@ private static String inputDependencyCons(TypeAutomaton typeAutomaton, AtomMappi
 
         // setting up input constraints (Shared Memory Approach)
         StringBuilder constraints = new StringBuilder();
-
+        /** For each input state...*/
         for (Block currBlock : typeAutomaton.getUsedTypesBlocks()) {
             int blockNumber = currBlock.getBlockNumber();
             for (State currInputState : currBlock.getStates()) {

src/main/java/nl/uu/cs/ape/sat/utils/APEUtils.java

@@ -524,7 +524,7 @@ public static String readFile(String path, Charset encoding) throws IOException
 	}
 
 	/**
-	 * Timer start.
+	 * Timer start if in debug mode.
 	 *
 	 * @param timerID   the timer id
 	 * @param debugMode the debug mode
@@ -536,6 +536,17 @@ public static void timerStart(String timerID, Boolean debugMode) {
 			timers.put(timerID, (long) -1);
 		}
 	}
+
+	public static long timerTimeLeft(String timerID, long timeout) {
+		if(timers.get(timerID) == -1) {
+			return 0;
+		}
+
+		long elapsedTimeMs = System.currentTimeMillis() - timers.get(timerID);
+		long timeLeftMs = timeout - elapsedTimeMs;
+		return timeLeftMs;
+
+	}
 
 	/**
 	 * Timer restart and print.
@@ -805,7 +816,8 @@ public static void appendToFile(File file, String content) throws IOException {
 	}
 
 	/**
-	 * Prepend text to the existing file. It adds the text at the beginning, before the existing content of the file.
+	 * Prepend text to the existing file content and create a new file out of it.
+	 * It adds the text at the beginning, before the existing content of the file.
 	 * @param file
 	 * @param prefix
 	 * @throws IOException