3 files changed, 85 insertions, 10 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index fb2662a..6db785e 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -1,20 +1,31 @@
+## Target(s) Configuration #####################################################
+MODEL_FILE = "../data/instructions/example_1.sl"
+LEVEL_DIR = "../data/level/"
+## Executables #################################################################
 JAVAC = javac
 JAVA = java
-SOURCES = $(wildcard src/*.java)
-CLASSES = $(SOURCES:.java=.class)
-CLASSPATH = "kodkod.jar:./src/:org.sat4j.core.jar"
-TEST_FILE = "./system_minus_fun.sl"
 DOWNLOADER = wget
+
+## Java Config #################################################################
+CLASSPATH = "kodkod.jar:./src/:org.sat4j.core.jar"
+
+## Dependencies ################################################################
 JAR_SOURCE = https://noot-noot.org/onera_2017/jar/
 REQUIRED_JARS = kodkod.jar org.sat4j.core.jar
 
+## Makefile Magic ##############################################################
+SOURCES = $(wildcard src/*.java)
+CLASSES = $(SOURCES:.java=.class)
+
+## Makefile Rules ##############################################################
+
 all: $(CLASSES)
 
 clean:
 	rm -f $(CLASSES)
 
 run: $(CLASSES) $(REQUIRED_JARS)
-	$(JAVA) -cp $(CLASSPATH) Main $(TEST_FILE)
+	$(JAVA) -cp $(CLASSPATH) Main $(LEVEL_DIR) $(MODEL_FILE)
 
 %.class: %.java $(REQUIRED_JARS)
 	$(JAVAC) -cp $(CLASSPATH) $<
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index d692ecd..ec55450 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -8,6 +8,8 @@ import kodkod.engine.satlab.*;
 import kodkod.instance.*;
 public class Main
 {
+   private static Parameters PARAMETERS;
+
    private static Formula get_formula (final VHDLModel model)
    {
       final Variable w;
@@ -32,10 +34,10 @@ public class Main
       final Solver solver;
       final Solution sol;
 
-      if (args.length != 1)
-      {
-         System.out.println("Use: java Main <instructions_file>");
+      PARAMETERS = new Parameters(args);
 
+      if (!PARAMETERS.are_valid())
+      {
          return;
       }
 
@@ -43,7 +45,14 @@ public class Main
 
       try
       {
-         VHDLLevel.add_to_model(model, "./structural_level.data");
+         VHDLLevel.add_to_model
+         (
+            model,
+            (
+               PARAMETERS.get_levels_directory()
+               + "/structural_level.data"
+            )
+         );
       }
       catch (final Exception e)
       {
@@ -55,7 +64,7 @@ public class Main
 
       try
       {
-         model.parse_file(args[0]);
+         model.parse_file(PARAMETERS.get_model_file());
       }
       catch (final Exception e)
       {
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
new file mode 100644
index 0000000..8d0331b
--- /dev/null
+++ b/instr-to-kodkod/src/Parameters.java
@@ -0,0 +1,55 @@
+public class Parameters
+{
+   private final String levels_dir;
+   private final String model_file;
+   private final boolean are_valid;
+
+   public static void print_usage ()
+   {
+      System.out.println
+      (
+         "Instr-to-kodkod\n"
+         + "USAGE:\n"
+         + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS>\n"
+         + "PARAMETERS:\n"
+         + "\t<LEVELS_DIR>\tDirectory containing the level definitions.\n"
+         + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n"
+         + "NOTES:\n"
+         + "\tThe properties to be verified still have to be hand coded in the"
+         + "source files (in Main.java)."
+      );
+   }
+
+   public Parameters (String... args)
+   {
+      if (args.length != 2)
+      {
+         print_usage();
+
+         levels_dir = new String();
+         model_file = new String();
+         are_valid = false;
+      }
+      else
+      {
+         levels_dir = args[0];
+         model_file = args[1];
+         are_valid = true;
+      }
+   }
+
+   public String get_levels_directory ()
+   {
+      return levels_dir;
+   }
+
+   public String get_model_file ()
+   {
+      return model_file;
+   }
+
+   public boolean are_valid ()
+   {
+      return are_valid;
+   }
+}