6 files changed, 592 insertions, 0 deletions
diff --git a/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java b/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java
new file mode 100644
index 0000000..93d20ba
--- /dev/null
+++ b/instr-to-kodkod/cfg-to-paths/src/ControlFlow.java
@@ -0,0 +1,142 @@
+import java.io.*;
+
+public class ControlFlow
+{
+   public static boolean load_file
+   (
+      final String filename
+   )
+   throws FileNotFoundException
+   {
+      final QuickParser qp;
+      String[] input;
+      boolean success;
+
+      qp = new QuickParser(filename);
+
+      for (;;)
+      {
+         try
+         {
+            input = qp.parse_line();
+
+            if (input == null)
+            {
+               qp.finalize();
+
+               return false;
+            }
+            else if (input.length == 0)
+            {
+               qp.finalize();
+
+               break;
+            }
+         }
+         catch (final IOException e)
+         {
+            System.err.println
+            (
+               "[E] IO error while parsing file \""
+               + filename
+               + "\":"
+               /* FIXME: can be null */
+               + e.getMessage()
+            );
+
+            return false;
+         }
+
+         if (input[0].equals("add_element"))
+         {
+            success = handle_add_element(input);
+         }
+         else if (input[0].equals("node_connect"))
+         {
+            success = handle_add_connect_to(input);
+         }
+         else if (input[0].equals("is_terminal"))
+         {
+            success = handle_is_terminal(input);
+         }
+         else
+         {
+            continue;
+         }
+
+         if (!success)
+         {
+            System.err.println
+            (
+               "[E] An erroneous instruction was found in file \""
+               + filename
+               + "\"."
+            );
+
+            try
+            {
+               qp.finalize();
+            }
+            catch (final Exception e)
+            {
+               System.err.println("[E] Additionally:");
+               e.printStackTrace();
+            }
+
+            return false;
+         }
+      }
+
+      return true;
+   }
+
+   private static boolean handle_add_element
+   (
+      final String[] input
+   )
+   {
+      if (input.length != 3)
+      {
+         return false;
+      }
+
+      if (!input[1].equals("node"))
+      {
+         return true;
+      }
+
+      Node.handle_add_node(input[2]);
+
+      return true;
+   }
+
+   private static boolean handle_is_terminal
+   (
+      final String[] input
+   )
+   {
+      if (input.length != 2)
+      {
+         return false;
+      }
+
+      Node.handle_is_terminal(input[1]);
+
+      return true;
+   }
+
+   private static boolean handle_add_connect_to
+   (
+      final String[] input
+   )
+   {
+      if ((input.length != 3))
+      {
+         return false;
+      }
+
+      return Node.handle_connect_to(input[1], input[2]);
+   }
+
+   private ControlFlow () {} /* Utility Class */
+}
diff --git a/instr-to-kodkod/cfg-to-paths/src/Main.java b/instr-to-kodkod/cfg-to-paths/src/Main.java
new file mode 100644
index 0000000..d5cc650
--- /dev/null
+++ b/instr-to-kodkod/cfg-to-paths/src/Main.java
@@ -0,0 +1,114 @@
+/* FIXME: Finer imports */
+import java.util.*;
+
+import java.io.*;
+
+public class Main
+{
+   private static Parameters PARAMETERS;
+   private static int path_counter = 0;
+
+   public static void main (final String... args)
+   {
+      final FileWriter output;
+      final Collection<Path> all_paths;
+      final Collection<List<Node>> all_subpaths;
+
+      PARAMETERS = new Parameters(args);
+
+      if (!PARAMETERS.are_valid())
+      {
+         return;
+      }
+
+      try
+      {
+         ControlFlow.load_file(PARAMETERS.get_model_file());
+      }
+      catch (final Exception e)
+      {
+         System.err.println
+         (
+            "[E] Could not load model file \""
+            + PARAMETERS.get_model_file()
+            + "\":"
+         );
+
+         e.printStackTrace();
+
+         return;
+      }
+
+      all_paths = Path.get_all_paths_from(PARAMETERS.get_root_node());
+
+      all_subpaths = new ArrayList<List<Node>>();
+
+      for (final Path p: all_paths)
+      {
+         all_subpaths.addAll(p.get_all_subpaths());
+      }
+
+      try
+      {
+         output = new FileWriter(PARAMETERS.get_output_file());
+
+         for (final List<Node> tuple: all_subpaths)
+         {
+            node_tuple_to_predicates(tuple, output);
+         }
+
+         output.close();
+      }
+      catch (final Exception e)
+      {
+         System.err.println
+         (
+            "[E] Could not write to output file \""
+            + PARAMETERS.get_model_file()
+            + "\":"
+         );
+
+         e.printStackTrace();
+
+         return;
+      }
+   }
+
+   private static void node_tuple_to_predicates
+   (
+      final List<Node> tuple,
+      final FileWriter out
+   )
+   throws IOException
+   {
+      final String id;
+      final int tuple_size;
+
+      tuple_size = tuple.size();
+
+      id = (PARAMETERS.get_id_prefix() + path_counter);
+      path_counter += 1;
+
+      out.write("(add_element path " + id + ")\n");
+      out.write("(is_path_of " + id + " " + tuple.get(0) + ")\n");
+
+      for (int i = 0; i < tuple_size; ++i)
+      {
+         out.write("(contains_node " + id + " " + tuple.get(i) + ")\n");
+
+         for (int j = (i + 1); j < tuple_size; ++j)
+         {
+            out.write
+            (
+               "(is_before "
+               + id
+               + " "
+               + tuple.get(i)
+               + " "
+               + tuple.get(j)
+               + ")\n"
+            );
+         }
+      }
+   }
+}
diff --git a/instr-to-kodkod/cfg-to-paths/src/Node.java b/instr-to-kodkod/cfg-to-paths/src/Node.java
new file mode 100644
index 0000000..3b6f2c1
--- /dev/null
+++ b/instr-to-kodkod/cfg-to-paths/src/Node.java
@@ -0,0 +1,104 @@
+import java.util.*;
+
+public class Node
+{
+   /** Static *****************************************************************/
+   private static final Map<String, Node> NODE_FROM_STRING;
+
+   static
+   {
+      NODE_FROM_STRING = new HashMap<String, Node>();
+   }
+
+   public static Node get_node (final String s)
+   {
+      return NODE_FROM_STRING.get(s);
+   }
+
+   public static boolean handle_add_node (final String a)
+   {
+      if (!NODE_FROM_STRING.containsKey(a))
+      {
+         NODE_FROM_STRING.put(a, new Node(a));
+      }
+
+      return true;
+   }
+
+   public static boolean handle_is_terminal (final String a)
+   {
+      Node n;
+
+      n = NODE_FROM_STRING.get(a);
+
+      if (n == (Node) null)
+      {
+         n = new Node(a);
+
+         NODE_FROM_STRING.put(a, n);
+      }
+
+      n.set_as_terminal();
+
+      return true;
+   }
+
+   public static boolean handle_connect_to (final String a, final String b)
+   {
+      final Node n_a, n_b;
+
+      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;
+   }
+
+   /** Non-Static *************************************************************/
+   private final Collection<Node> next_nodes;
+   private final String name;
+   private boolean is_terminal;
+
+   private Node (final String name)
+   {
+      this.name = name;
+
+      next_nodes = new ArrayList<Node>();
+      is_terminal = false;
+   }
+
+   private void set_as_terminal ()
+   {
+      is_terminal = true;
+   }
+
+   public Collection<Node> next_nodes ()
+   {
+      return next_nodes;
+   }
+
+   public boolean is_terminal ()
+   {
+      return is_terminal;
+   }
+
+   @Override
+   public String toString ()
+   {
+      return name;
+   }
+}
diff --git a/instr-to-kodkod/cfg-to-paths/src/Parameters.java b/instr-to-kodkod/cfg-to-paths/src/Parameters.java
new file mode 100644
index 0000000..91303d2
--- /dev/null
+++ b/instr-to-kodkod/cfg-to-paths/src/Parameters.java
@@ -0,0 +1,72 @@
+public class Parameters
+{
+   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 ()
+   {
+      System.out.println
+      (
+         "Instr-to-kodkod\n"
+         + "USAGE:\n"
+         + "\tjava Main <INSTRUCTIONS> <ROOT_NODE> <ID_PREFIX> <OUTPUT_FILE>\n"
+         + "PARAMETERS:\n"
+         + "\t<INSTRUCTIONS>\tInstruction file describing the model.\n"
+         + "\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 (final String... args)
+   {
+      if (args.length != 4)
+      {
+         print_usage();
+
+         model_file = new String();
+         root_node = new String();
+         id_prefix = new String();
+         output_file = new String();
+
+         are_valid = false;
+      }
+      else
+      {
+         model_file = args[0];
+         root_node = args[1];
+         id_prefix = args[2];
+         output_file = args[3];
+         are_valid = true;
+      }
+   }
+
+   public String get_model_file ()
+   {
+      return model_file;
+   }
+
+   public String get_root_node ()
+   {
+      return root_node;
+   }
+
+   public String get_id_prefix ()
+   {
+      return id_prefix;
+   }
+
+   public String get_output_file ()
+   {
+      return output_file;
+   }
+
+   public boolean are_valid ()
+   {
+      return are_valid;
+   }
+}
diff --git a/instr-to-kodkod/cfg-to-paths/src/Path.java b/instr-to-kodkod/cfg-to-paths/src/Path.java
new file mode 100644
index 0000000..9e0897f
--- /dev/null
+++ b/instr-to-kodkod/cfg-to-paths/src/Path.java
@@ -0,0 +1,102 @@
+import java.util.*;
+
+public class Path
+{
+   private final ArrayList<Node> nodes;
+   private final Node last_node;
+
+   public static Collection<Path> get_all_paths_from (final String root)
+   {
+      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>();
+
+      waiting_list.push((new Path(Node.get_node(root))));
+
+      while (!waiting_list.empty())
+      {
+         final Path current_path;
+         final Node current_node;
+         final Collection<Node> next_nodes;
+
+         current_path = waiting_list.pop();
+         current_node = current_path.last_node;
+         next_nodes = current_node.next_nodes();
+
+         if (next_nodes.isEmpty())
+         {
+            result.add(current_path);
+         }
+         else
+         {
+            if (current_node.is_terminal())
+            {
+               result.add(current_path);
+            }
+            for (final Node next: next_nodes)
+            {
+               waiting_list.push(current_path.add_step(next));
+            }
+         }
+      }
+
+      return result;
+   }
+
+   private Path (final Node start)
+   {
+      nodes = new ArrayList<Node>();
+
+      nodes.add(start);
+
+      last_node = start;
+   }
+
+   private Path (final ArrayList<Node> nodes, final Node last_node)
+   {
+      this.nodes = nodes;
+      this.last_node = last_node;
+
+      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);
+   }
+
+   public Collection<List<Node>> get_all_subpaths ()
+   {
+      final Collection<List<Node>> result;
+      final int path_length;
+
+      result = new ArrayList<List<Node>>();
+      path_length = nodes.size();
+
+      for (int i = 0; i < path_length; ++i)
+      {
+         result.add(nodes.subList(i, path_length));
+      }
+
+      return result;
+   }
+}
diff --git a/instr-to-kodkod/cfg-to-paths/src/QuickParser.java b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java
new file mode 100644
index 0000000..47cea27
--- /dev/null
+++ b/instr-to-kodkod/cfg-to-paths/src/QuickParser.java
@@ -0,0 +1,58 @@
+/* FIXME: Finer imports */
+import java.io.*;
+import java.util.regex.*;
+import java.util.*;
+
+public class QuickParser
+{
+   private static final Pattern instr_pattern;
+   private final BufferedReader buffered_reader;
+
+   static
+   {
+      instr_pattern = Pattern.compile("\\((?<list>[a-z_0-9 \"]+)\\)");
+   }
+   public QuickParser (final String filename)
+   throws FileNotFoundException
+   {
+      buffered_reader = new BufferedReader(new FileReader(filename));
+   }
+
+   public void finalize ()
+   throws IOException
+   {
+      buffered_reader.close();
+   }
+
+   public String[] parse_line ()
+   throws IOException
+   {
+      final List<String> result;
+      final Matcher matcher;
+      String line;
+
+      do
+      {
+         line = buffered_reader.readLine();
+
+         if (line == null)
+         {
+            return new String[0];
+         }
+
+         line = line.replaceAll("\\s+"," ");
+      }
+      while (line.length() < 3 || line.startsWith(";"));
+
+      matcher = instr_pattern.matcher(line);
+
+      if (!matcher.find())
+      {
+         System.err.println("[E] Invalid instruction \"" + line + "\"");
+
+         return null;
+      }
+
+      return matcher.group(1).split(" |\t");
+   }
+}