Fixes a few dumb mistakes, adds ps example.

8 files changed, 298 insertions, 95 deletions

diff --git a/cfg-to-paths/Makefile b/cfg-to-paths/Makefile
index 6db785e..c4d71e2 100644
--- a/cfg-to-paths/Makefile
+++ b/cfg-to-paths/Makefile
@@ -1,17 +1,15 @@
 ## Target(s) Configuration #####################################################
-MODEL_FILE = "../data/instructions/example_1.sl"
-LEVEL_DIR = "../data/level/"
+MODEL_FILE = "../data/instructions/example_process.pl"
+ROOT_NODE = "237"
+ID_PREFIX = "p237_"
+OUTPUT_FILE = "$(MODEL_FILE).kk"
+
 ## Executables #################################################################
 JAVAC = javac
 JAVA = java
-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
+CLASSPATH = "./src/"
 
 ## Makefile Magic ##############################################################
 SOURCES = $(wildcard src/*.java)
@@ -24,13 +22,9 @@ all: $(CLASSES)
 clean:
 	rm -f $(CLASSES)
 
-run: $(CLASSES) $(REQUIRED_JARS)
-	$(JAVA) -cp $(CLASSPATH) Main $(LEVEL_DIR) $(MODEL_FILE)
+run: $(CLASSES)
+	$(JAVA) -cp $(CLASSPATH) Main $(MODEL_FILE) $(ROOT_NODE) $(ID_PREFIX) \
+		$(OUTPUT_FILE)
 
-%.class: %.java $(REQUIRED_JARS)
+%.class: %.java
 	$(JAVAC) -cp $(CLASSPATH) $<
-
-%.jar:
-	echo "Attempting to download missing jar '$@'"
-	$(DOWNLOADER) "$(JAR_SOURCE)/$@"
-
diff --git a/cfg-to-paths/src/ControlFlow.java b/cfg-to-paths/src/ControlFlow.java
index 629ac49..a0863d8 100644
--- a/cfg-to-paths/src/ControlFlow.java
+++ b/cfg-to-paths/src/ControlFlow.java
@@ -96,7 +96,7 @@ public class ControlFlow
          return false;
       }
 
-      if (input[1] != "node")
+      if (!input[1].equals("node"))
       {
          return true;
       }
diff --git a/cfg-to-paths/src/Main.java b/cfg-to-paths/src/Main.java
index ec55450..f81b22f 100644
--- a/cfg-to-paths/src/Main.java
+++ b/cfg-to-paths/src/Main.java
@@ -1,38 +1,14 @@
 /* FIXME: Finer imports */
-import kodkod.ast.*;
+import java.util.*;
 
-import kodkod.engine.*;
-import kodkod.engine.config.*;
-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;
-
-      w = Variable.unary("w");
-
-      return
-         w.join
-         (
-            model.get_predicate_as_relation("is_accessed_by")
-         ).no().forSome(w.oneOf(model.get_type_as_relation("waveform")));
-   }
-
    public static void main (final String... args)
    {
-      final VHDLModel model;
-
-      final Universe univ;
-      final TupleFactory tf;
-      final Bounds bounds;
-
-      final Solver solver;
-      final Solution sol;
+      final Collection<Path> all_paths;
+      final Collection<List<Node>> all_subpaths;
 
       PARAMETERS = new Parameters(args);
 
@@ -41,51 +17,31 @@ public class Main
          return;
       }
 
-      model = new VHDLModel();
-
       try
       {
-         VHDLLevel.add_to_model
-         (
-            model,
-            (
-               PARAMETERS.get_levels_directory()
-               + "/structural_level.data"
-            )
-         );
+         ControlFlow.load_file(PARAMETERS.get_model_file());
       }
       catch (final Exception e)
       {
-         System.err.println("[E] Could not load structural level:");
-         e.printStackTrace();
-
-         return;
-      }
+         System.err.println
+         (
+            "[E] Could not load model file \""
+            + PARAMETERS.get_model_file()
+            + "\":"
+         );
 
-      try
-      {
-         model.parse_file(PARAMETERS.get_model_file());
-      }
-      catch (final Exception e)
-      {
-         System.err.println("[E] Could not load instructions:");
          e.printStackTrace();
 
          return;
       }
 
-      univ = new Universe(model.get_atoms());
-      tf = univ.factory();
-      bounds = new Bounds(univ);
-
-      model.add_to_bounds(bounds, tf);
+      all_paths = Path.get_all_paths_from(PARAMETERS.get_root_node());
 
-      solver = new Solver();
-      solver.options().setSolver(SATFactory.DefaultSAT4J);
-      solver.options().setReporter(new ConsoleReporter());
+      all_subpaths = new ArrayList<List<Node>>();
 
-      sol = solver.solve(get_formula(model), bounds);
-
-      System.out.println(sol);
+      for (final Path p: all_paths)
+      {
+         all_subpaths.addAll(p.get_all_subpaths());
+      }
    }
 }
diff --git a/cfg-to-paths/src/Node.java b/cfg-to-paths/src/Node.java
index 6f9083d..5f82f64 100644
--- a/cfg-to-paths/src/Node.java
+++ b/cfg-to-paths/src/Node.java
@@ -51,6 +51,19 @@ public class Node
       n_a = NODE_FROM_STRING.get(a);
       n_b = NODE_FROM_STRING.get(b);
 
+      if ((n_a == null) || (n_b == null))
+      {
+         System.err.println
+         (
+            "[E] Causality issue: Nodes \""
+            + a
+            + "\" or \""
+            + b
+            + "\" used but not defined."
+         );
+
+         return false;
+      }
       n_a.next_nodes.add(n_b);
 
       return true;
diff --git a/cfg-to-paths/src/Parameters.java b/cfg-to-paths/src/Parameters.java
index 8d0331b..710b1f7 100644
--- a/cfg-to-paths/src/Parameters.java
+++ b/cfg-to-paths/src/Parameters.java
@@ -1,7 +1,9 @@
 public class Parameters
 {
-   private final String levels_dir;
    private final String model_file;
+   private final String root_node;
+   private final String id_prefix;
+   private final String output_file;
    private final boolean are_valid;
 
    public static void print_usage ()
@@ -10,42 +12,57 @@ public class Parameters
       (
          "Instr-to-kodkod\n"
          + "USAGE:\n"
-         + "\tjava Main <LEVELS_DIR> <INSTRUCTIONS>\n"
+         + "\tjava Main <INSTRUCTIONS> <ROOT_NODE> <ID_PREFIX> <OUTPUT_FILE>\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)."
+         + "\t<ROOT_NODE>\tID of the root node for this DAG.\n"
+         + "\t<ID_PREFIX>\tPrefix for the IDs of generated paths.\n"
+         + "\t<OUTPUT_FILE>\tFile in which to output the generated"
+         + " instructions."
       );
    }
 
    public Parameters (String... args)
    {
-      if (args.length != 2)
+      if (args.length != 4)
       {
          print_usage();
 
-         levels_dir = new String();
          model_file = new String();
+         root_node = new String();
+         id_prefix = new String();
+         output_file = new String();
+
          are_valid = false;
       }
       else
       {
-         levels_dir = args[0];
-         model_file = args[1];
+         model_file = args[0];
+         root_node = args[1];
+         id_prefix = args[2];
+         output_file = args[3];
          are_valid = true;
       }
    }
 
-   public String get_levels_directory ()
+   public String get_model_file ()
    {
-      return levels_dir;
+      return model_file;
    }
 
-   public String get_model_file ()
+   public String get_root_node ()
    {
-      return model_file;
+      return root_node;
+   }
+
+   public String get_id_prefix ()
+   {
+      return id_prefix;
+   }
+
+   public String get_output_file ()
+   {
+      return output_file;
    }
 
    public boolean are_valid ()
diff --git a/cfg-to-paths/src/Path.java b/cfg-to-paths/src/Path.java
index 80b433f..76ba28a 100644
--- a/cfg-to-paths/src/Path.java
+++ b/cfg-to-paths/src/Path.java
@@ -31,6 +31,21 @@ public class Path
    {
       final Collection<Path> result;
       final Stack<Path> waiting_list;
+      final Node root_node;
+
+      root_node = Node.get_node(root);
+
+      if (root_node == null)
+      {
+         System.err.println
+         (
+            "[E] Could not find root node \""
+            + root
+            + "\"."
+         );
+
+         return null;
+      }
 
       result = new ArrayList<Path>();
       waiting_list = new Stack<Path>();
@@ -63,17 +78,17 @@ public class Path
       return result;
    }
 
-   public static Collection<List<Node>> get_subpaths (final Path p)
+   public Collection<List<Node>> get_all_subpaths ()
    {
       final Collection<List<Node>> result;
       final int path_length;
 
       result = new ArrayList<List<Node>>();
-      path_length = p.nodes.size();
+      path_length = nodes.size();
 
       for (int i = 0; i < path_length; ++i)
       {
-         result.add(p.nodes.subList(i, path_length));
+         result.add(nodes.subList(i, path_length));
       }
 
       return result;
diff --git a/data/instructions/example_process.pl b/data/instructions/example_process.pl
new file mode 100644
index 0000000..17eb9f0
--- /dev/null
+++ b/data/instructions/example_process.pl
@@ -0,0 +1,208 @@
+(add_element node 237)
+(expr_reads 237 192)
+(add_element string 56)
+(set_attribute label 237 56)
+(add_element string 238)
+(set_attribute kind 237 238)
+(set_attribute depth 237 1)
+(add_element node 239)
+(node_connect 237 239)
+(add_element string 56)
+(set_attribute label 239 56)
+(add_element string 240)
+(set_attribute kind 239 240)
+(add_element string 241)
+(add_option 239 241)
+(set_attribute depth 239 2)
+(add_element node 242)
+(node_connect 239 242)
+(add_element string 56)
+(set_attribute label 242 56)
+(add_element string 59)
+(set_attribute kind 242 59)
+(add_element string 60)
+(add_option 242 60)
+(set_attribute depth 242 3)
+(expr_writes 242 243)
+(expr_reads 242 219)
+(add_element node 244)
+(node_connect 237 244)
+(add_element string 56)
+(set_attribute label 244 56)
+(add_element string 240)
+(set_attribute kind 244 240)
+(set_attribute depth 244 2)
+(add_element node 245)
+(node_connect 244 245)
+(add_element string 56)
+(set_attribute label 245 56)
+(add_element string 59)
+(set_attribute kind 245 59)
+(add_element string 60)
+(add_option 245 60)
+(set_attribute depth 245 3)
+(expr_writes 245 195)
+(expr_reads 245 198)
+(add_element node 246)
+(node_connect 237 246)
+(add_element string 56)
+(set_attribute label 246 56)
+(add_element string 240)
+(set_attribute kind 246 240)
+(set_attribute depth 246 2)
+(add_element node 247)
+(node_connect 246 247)
+(add_element string 56)
+(set_attribute label 247 56)
+(add_element string 59)
+(set_attribute kind 247 59)
+(add_element string 60)
+(add_option 247 60)
+(set_attribute depth 247 3)
+(expr_writes 247 243)
+(expr_reads 247 200)
+(add_element node 248)
+(node_connect 237 248)
+(add_element string 56)
+(set_attribute label 248 56)
+(add_element string 240)
+(set_attribute kind 248 240)
+(set_attribute depth 248 2)
+(add_element node 249)
+(node_connect 248 249)
+(add_element string 56)
+(set_attribute label 249 56)
+(add_element string 59)
+(set_attribute kind 249 59)
+(add_element string 60)
+(add_option 249 60)
+(set_attribute depth 249 3)
+(expr_writes 249 243)
+(expr_reads 249 202)
+(add_element node 250)
+(node_connect 237 250)
+(add_element string 56)
+(set_attribute label 250 56)
+(add_element string 240)
+(set_attribute kind 250 240)
+(set_attribute depth 250 2)
+(add_element node 251)
+(node_connect 250 251)
+(add_element string 56)
+(set_attribute label 251 56)
+(add_element string 59)
+(set_attribute kind 251 59)
+(add_element string 60)
+(add_option 251 60)
+(set_attribute depth 251 3)
+(expr_writes 251 243)
+(expr_reads 251 204)
+(add_element node 252)
+(node_connect 237 252)
+(add_element string 56)
+(set_attribute label 252 56)
+(add_element string 240)
+(set_attribute kind 252 240)
+(set_attribute depth 252 2)
+(add_element node 253)
+(node_connect 252 253)
+(add_element string 56)
+(set_attribute label 253 56)
+(add_element string 59)
+(set_attribute kind 253 59)
+(add_element string 60)
+(add_option 253 60)
+(set_attribute depth 253 3)
+(expr_writes 253 243)
+(expr_reads 253 206)
+(add_element node 254)
+(node_connect 237 254)
+(add_element string 56)
+(set_attribute label 254 56)
+(add_element string 240)
+(set_attribute kind 254 240)
+(set_attribute depth 254 2)
+(add_element node 255)
+(node_connect 254 255)
+(add_element string 56)
+(set_attribute label 255 56)
+(add_element string 59)
+(set_attribute kind 255 59)
+(add_element string 60)
+(add_option 255 60)
+(set_attribute depth 255 3)
+(expr_writes 255 243)
+(expr_reads 255 208)
+(add_element node 256)
+(node_connect 237 256)
+(add_element string 56)
+(set_attribute label 256 56)
+(add_element string 240)
+(set_attribute kind 256 240)
+(set_attribute depth 256 2)
+(add_element node 257)
+(node_connect 256 257)
+(add_element string 56)
+(set_attribute label 257 56)
+(add_element string 59)
+(set_attribute kind 257 59)
+(add_element string 60)
+(add_option 257 60)
+(set_attribute depth 257 3)
+(expr_writes 257 243)
+(expr_reads 257 210)
+(add_element node 258)
+(node_connect 237 258)
+(add_element string 56)
+(set_attribute label 258 56)
+(add_element string 240)
+(set_attribute kind 258 240)
+(set_attribute depth 258 2)
+(add_element node 259)
+(node_connect 258 259)
+(add_element string 56)
+(set_attribute label 259 56)
+(add_element string 59)
+(set_attribute kind 259 59)
+(add_element string 60)
+(add_option 259 60)
+(set_attribute depth 259 3)
+(expr_writes 259 243)
+(expr_reads 259 212)
+(add_element node 260)
+(node_connect 237 260)
+(add_element string 56)
+(set_attribute label 260 56)
+(add_element string 240)
+(set_attribute kind 260 240)
+(set_attribute depth 260 2)
+(add_element node 261)
+(node_connect 260 261)
+(add_element string 56)
+(set_attribute label 261 56)
+(add_element string 59)
+(set_attribute kind 261 59)
+(add_element string 60)
+(add_option 261 60)
+(set_attribute depth 261 3)
+(expr_writes 261 243)
+(expr_reads 261 214)
+(add_element node 262)
+(node_connect 237 262)
+(add_element string 56)
+(set_attribute label 262 56)
+(add_element string 240)
+(set_attribute kind 262 240)
+(set_attribute depth 262 2)
+(add_element node 263)
+(node_connect 262 263)
+(add_element string 56)
+(set_attribute label 263 56)
+(add_element string 59)
+(set_attribute kind 263 59)
+(add_element string 60)
+(add_option 263 60)
+(set_attribute depth 263 3)
+(expr_writes 263 243)
+(expr_reads 263 217)
+
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index 8d0331b..e9dc648 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -16,7 +16,7 @@ public class Parameters
          + "\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)."
+         + " source files (in Main.java)."
       );
    }