Adds a verbosity parameter.

8 files changed, 209 insertions, 60 deletions

diff --git a/cfg-to-paths/src/Path.java b/cfg-to-paths/src/Path.java
index 6015d53..9e0897f 100644
--- a/cfg-to-paths/src/Path.java
+++ b/cfg-to-paths/src/Path.java
@@ -77,6 +77,8 @@ public class Path
       this.nodes.add(last_node);
    }
 
+   @SuppressWarnings("unchecked")
+   /* 'nodes' is an ArrayList<Node>, and so should be its clone. */
    private Path add_step (final Node n)
    {
       return new Path((ArrayList<Node>) nodes.clone(), n);
diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index 7232a6e..bdc7324 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -7,13 +7,10 @@ MODEL_FILES = \
 	$(wildcard ../cfg-to-paths/*.mod)
 MAP_FILES = $(wildcard ../ast-to-instr/*.map)
 LEVEL_DIR = $(wildcard ../data/level/*.lvl)
-#PROPERTY_FILE = ../data/property/unread_waveforms.pro
-#PROPERTY_FILE = ../data/property/impossible_processes.pro
-#PROPERTY_FILE = ../data/property/incrementer.pro
-PROPERTY_FILE = ../data/property/combinational_processes.pro
-#PROPERTY_FILE = ../data/property/likely_a_clock.pro
-#PROPERTY_FILE = ../data/property/cnes/CNE*.pro
-VAR_PREFIX = "_anon_"
+
+PROPERTIES = \
+	../data/property/combinational_processes.pro \
+	../data/property/likely_a_clock.pro
 
 ## Executables #################################################################
 JAVAC = javac
@@ -28,12 +25,14 @@ JAR_SOURCE = https://noot-noot.org/onera_2017/jar/
 REQUIRED_JARS = kodkod.jar org.sat4j.core.jar antlr-4.7-complete.jar
 
 ## Makefile Magic ##############################################################
-INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(PROPERTY_FILE) $(MAP_FILES)
+GLOBAL_INPUT_FILES = $(MODEL_FILES) $(LEVEL_DIR) $(MAP_FILES)
 SOURCES = $(wildcard src/*.java parser/*.java)
 GRAMMARS = $(wildcard parser/*.g4)
 CLASSES = $(SOURCES:.java=.class)
+SOLUTIONS = $(PROPERTIES:.pro=.sol)
 
 ## Makefile Rules ##############################################################
+run: $(SOLUTIONS)
 
 all: parser/PropertyParser.java $(CLASSES)
 	$(MAKE) -C parser
@@ -46,12 +45,13 @@ clean:
 	$(MAKE) -C ../ast-to-instr clean
 	$(MAKE) -C ../cfg-to-paths clean
 
-run: parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS)
+%.sol: %.pro parser/PropertyParser.java $(CLASSES) $(REQUIRED_JARS)
+	echo "Solving \"$<\"..."
 	$(MAKE) -C ../ast-to-instr
 	$(MAKE) -C ../cfg-to-paths
-	$(JAVA) -cp $(CLASSPATH) Main $(VAR_PREFIX) $(INPUT_FILES)
+	$(JAVA) -cp $(CLASSPATH) Main $@ $< $(GLOBAL_INPUT_FILES)
 
-%.class: %.java $(REQUIRED_JARS)
+%.class: %.java $(REQUIRED_JARS) parser/PropertyParser.java
 	$(JAVAC) -cp $(CLASSPATH) $<
 
 %.jar:
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index d6528cd..6a2445b 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -1,4 +1,7 @@
+import java.io.BufferedWriter;
+import java.io.File;
 import java.io.FileNotFoundException;
+import java.io.FileWriter;
 import java.io.IOException;
 
 import java.util.Iterator;
@@ -20,6 +23,11 @@ public class Main
    private static VariableManager VARIABLE_MANAGER;
    private static StringManager STRING_MANAGER;
 
+   public static Parameters get_parameters ()
+   {
+      return PARAMETERS;
+   }
+
    public static VHDLModel get_model ()
    {
       return MODEL;
@@ -41,7 +49,10 @@ public class Main
       {
          try
          {
-            System.out.println("Loading level file \"" + lvl + "\"...");
+            if (PARAMETERS.be_verbose())
+            {
+               System.out.println("Loading level file \"" + lvl + "\"...");
+            }
 
             VHDLLevel.add_to_model(MODEL, lvl);
          }
@@ -71,12 +82,15 @@ public class Main
 
       try
       {
-         System.out.println
-         (
-            "Loading property file \""
-            + PARAMETERS.get_property_file()
-            + "\"..."
-         );
+         if (PARAMETERS.be_verbose())
+         {
+            System.out.println
+            (
+               "Loading property file \""
+               + PARAMETERS.get_property_file()
+               + "\"..."
+            );
+         }
 
          return pro.generate_base_formula();
       }
@@ -100,7 +114,10 @@ public class Main
       {
          try
          {
-            System.out.println("Loading model file \"" + mod + "\"...");
+            if (PARAMETERS.be_verbose())
+            {
+               System.out.println("Loading model file \"" + mod + "\"...");
+            }
 
             MODEL.parse_file(mod);
          }
@@ -219,6 +236,29 @@ public class Main
       return true;
    }
 
+   private static BufferedWriter get_output_file (final String filename)
+   {
+      try
+      {
+         return new BufferedWriter(new FileWriter(new File(filename)));
+      }
+      catch (final Exception e)
+      {
+         System.err.println
+         (
+            "[F] Could not create/open output file \""
+            + filename
+            + "\":"
+         );
+
+         e.printStackTrace();
+
+         System.exit(-1);
+      }
+
+      return null;
+   }
+
    public static void main (final String... args)
    {
       /*
@@ -238,6 +278,7 @@ public class Main
       final Iterator<Solution> solutions;
       final Solver solver;
       final Formula property;
+      final BufferedWriter solution_output;
 
       PARAMETERS = new Parameters(args);
 
@@ -246,7 +287,14 @@ public class Main
          return;
       }
 
-      VARIABLE_MANAGER = new VariableManager(PARAMETERS.get_variables_prefix());
+      solution_output = get_output_file(PARAMETERS.get_output_file());
+
+      if (solution_output == null)
+      {
+         return;
+      }
+
+      VARIABLE_MANAGER = new VariableManager();
 
       MODEL = new VHDLModel();
 
@@ -271,7 +319,7 @@ public class Main
       {
          return;
       }
-      else
+      else if (PARAMETERS.be_verbose())
       {
          System.out.println
          (
@@ -320,8 +368,46 @@ public class Main
 
          if (sol.sat())
          {
-            VARIABLE_MANAGER.print_solution(sol.instance().relationTuples());
+            try
+            {
+               VARIABLE_MANAGER.print_solution
+               (
+                  sol.instance().relationTuples(),
+                  solution_output
+               );
+            }
+            catch (final IOException e)
+            {
+               System.err.println
+               (
+                  "[F] Unable to write solution to file \""
+                  + PARAMETERS.get_output_file()
+                  + "\":"
+               );
+
+               e.printStackTrace();
+
+               System.exit(-1);
+            }
          }
       }
+
+      try
+      {
+         solution_output.close();
+      }
+      catch (final IOException e)
+      {
+         System.err.println
+         (
+            "[F] Unable to properly close solution file \""
+            + PARAMETERS.get_output_file()
+            + "\":"
+         );
+
+         e.printStackTrace();
+
+         System.exit(-1);
+      }
    }
 }
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index d3bc0f1..7c80474 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -7,7 +7,8 @@ public class Parameters
    private final List<String> model_files;
    private final List<String> map_files;
    private final String property_file;
-   private final String var_prefix;
+   private final String output_file;
+   private final boolean be_verbose;
 
    private final boolean are_valid;
 
@@ -17,12 +18,14 @@ public class Parameters
       (
          "Instr-to-kodkod\n"
          + "USAGE:\n"
-         + "\tjava Main <VAR_PREFIX> <FILES>+\n"
+         + "\tjava Main <OUTPUT_FILE> <FILES|OPTIONS>+\n"
          + "PARAMETERS:\n"
-         + "\t- <VAR_PREFIX>\tPrefix for anonymous variables (e.g. \"_anon_\").\n"
+         + "\t- <OUTPUT_FILE>\tFile to write the solutions in.\n"
          + "\t- <FILES>\tList of files to be loaded.\n"
+         + "OPTIONS:\n"
+         + "\t- -v|--verbose\tPrint informative messages to STDOUT.\n"
          + "NOTES:\n"
-         + "\t- One, single, property file MUST be in <FILES>.\n"
+         + "\t- Exactly one property file must be in <FILES>.\n"
          + "\t- Property files have a \".pro\" extension.\n"
          + "\t- Model files have a \".mod\" extension.\n"
          + "\t- Level files have a \".lvl\" extension.\n"
@@ -31,23 +34,26 @@ public class Parameters
       );
    }
 
-   public Parameters (String... args)
+   public Parameters (final String... args)
    {
-      boolean has_pro_file, has_error;
+      boolean has_pro_file, has_error, should_be_verbose;
       String prop_file;
 
       level_files = new ArrayList<String>();
       model_files = new ArrayList<String>();
       map_files = new ArrayList<String>();
 
+      should_be_verbose = false;
+
       if (args.length < 2)
       {
          print_usage();
 
          property_file = new String();
-         var_prefix = new String();
+         output_file = new String();
 
          are_valid = false;
+         be_verbose = false;
 
          return;
       }
@@ -55,7 +61,48 @@ public class Parameters
       has_pro_file = false;
       has_error = false;
 
-      var_prefix = args[0];
+      output_file = args[0];
+
+      if
+      (
+         (output_file.equals("-v") || output_file.equals("--verbose"))
+         /* || ... */
+      )
+      {
+         print_usage();
+
+         System.err.println
+         (
+            "[F] An option was found in lieu of the output file."
+         );
+
+         System.exit(-1);
+      }
+
+      if
+      (
+         output_file.endsWith(".lvl")
+         || output_file.endsWith(".mod")
+         || output_file.endsWith(".map")
+         || output_file.endsWith(".pro")
+      )
+      {
+         print_usage();
+
+         System.err.println
+         (
+            "[F] The output file has an extension that could be used in an"
+            + " input file. It is most likely that you did not indicate an"
+            + " output file, meaning that one of the input files was about to"
+            + " be written over. So likely, in fact, that we'll abort here. The"
+            + " output file you indicated was \""
+            + output_file
+            + "\"."
+         );
+
+         System.exit(-1);
+      }
+
       prop_file = new String();
 
       for (int i = 1; i < args.length; ++i)
@@ -65,7 +112,7 @@ public class Parameters
             level_files.add(args[i]);
          }
          else if (args[i].endsWith(".mod"))
-         {
+          {
             model_files.add(args[i]);
          }
          else if (args[i].endsWith(".map"))
@@ -93,6 +140,10 @@ public class Parameters
                prop_file = args[i];
             }
          }
+         else if (output_file.equals("-v") || output_file.equals("--verbose"))
+         {
+            should_be_verbose = true;
+         }
          else
          {
             System.err.println
@@ -115,6 +166,7 @@ public class Parameters
          has_error = true;
       }
 
+      be_verbose = should_be_verbose;
       are_valid = !has_error;
    }
 
@@ -138,9 +190,14 @@ public class Parameters
       return property_file;
    }
 
-   public String get_variables_prefix ()
+   public String get_output_file ()
+   {
+      return output_file;
+   }
+
+   public boolean be_verbose ()
    {
-      return var_prefix;
+      return be_verbose;
    }
 
    public boolean are_valid ()
diff --git a/instr-to-kodkod/src/StringManager.java b/instr-to-kodkod/src/StringManager.java
index c0a2fa4..247d8e3 100644
--- a/instr-to-kodkod/src/StringManager.java
+++ b/instr-to-kodkod/src/StringManager.java
@@ -41,17 +41,6 @@ public class StringManager
 
          TO_ID.put(str, id);
       }
-      else
-      {
-         System.out.println
-         (
-            "[D] Using string \""
-            + str
-            + "\" (id: "
-            + id
-            + ")"
-         );
-      }
 
       return string_type.get_member_as_relation(id);
    }
diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java
index 821a044..1b4d16d 100644
--- a/instr-to-kodkod/src/VHDLPredicate.java
+++ b/instr-to-kodkod/src/VHDLPredicate.java
@@ -71,7 +71,10 @@ public class VHDLPredicate
 
          is_used = true;
 
-         System.out.println("Enabling predicate: " + name);
+         if (Main.get_parameters().be_verbose())
+         {
+            System.out.println("Enabling predicate: " + name);
+         }
       }
 
       return as_relation;
diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java
index d8ae9ed..e38af5e 100644
--- a/instr-to-kodkod/src/VHDLType.java
+++ b/instr-to-kodkod/src/VHDLType.java
@@ -44,7 +44,10 @@ public class VHDLType
    {
       if (!is_used)
       {
-         System.out.println("Enabling type: " + name);
+         if (Main.get_parameters().be_verbose())
+         {
+            System.out.println("Enabling type: " + name);
+         }
 
          is_used = true;
       }
diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java
index cf7229e..249b183 100644
--- a/instr-to-kodkod/src/VariableManager.java
+++ b/instr-to-kodkod/src/VariableManager.java
@@ -1,3 +1,6 @@
+import java.io.BufferedWriter;
+import java.io.IOException;
+
 import java.util.HashMap;
 import java.util.Map;
 
@@ -16,7 +19,7 @@ public class VariableManager
    private final Map<String, TaggedVariable> tagged_variables;
    private int next_id;
 
-   public VariableManager (final String var_prefix)
+   public VariableManager ()
    {
       from_string = new HashMap<String, Expression>();
       tagged_variables = new HashMap<String, TaggedVariable>();
@@ -43,8 +46,6 @@ public class VariableManager
    {
       final TaggedVariable tg;
 
-      System.out.println("[D] Skolemizing: " + var_name);
-
       if (from_string.containsKey(var_name))
       {
          throw
@@ -149,25 +150,33 @@ public class VariableManager
       return result;
    }
 
-   public void print_solution (final Map<Relation, TupleSet> solution)
+   public void print_solution
+   (
+      final Map<Relation, TupleSet> solution,
+      final BufferedWriter output
+   )
+   throws IOException
    {
-      System.out.print("(solution");
+      output.write("(solution");
 
       for (final TaggedVariable tg: tagged_variables.values())
       {
-         System.out.print("\n   (");
-         System.out.print(tg.name);
-         System.out.print(" ");
-         System.out.print
+         output.newLine();
+         output.write("   (");
+         output.write(tg.name);
+         output.write(" ");
+         output.write
          (
-            solution.get(tg.as_relation).iterator().next().atom(0)
+            solution.get(tg.as_relation).iterator().next().atom(0).toString()
          );
-         System.out.print(" ");
-         System.out.print(tg.tag);
-         System.out.print(")");
+         output.write(" ");
+         output.write(tg.tag);
+         output.write(")");
       }
 
-      System.out.println("\n)");
+      output.newLine();
+      output.write(")");
+      output.newLine();
    }
 
    private static class TaggedVariable