Gets the strings seemingly working.

8 files changed, 187 insertions, 20 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index c25c95f..bb52959 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -5,7 +5,8 @@ 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/combinational_processes.pro
+PROPERTY_FILE = ../data/property/incrementer.pro
+#PROPERTY_FILE = ../data/property/combinational_processes.pro
 VAR_PREFIX = "_anon_"
 
 ## Executables #################################################################
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 159dec1..46aa30f 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -29,3 +29,4 @@ EU_OPERATOR_KW: '(EU' SEP;
 WS: SEP;
 
 ID: [a-zA-Z0-9_]+;
+STRING: '"' ~('\r' | '\n' | '"')* '"';
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 70e672f..82eb429 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -116,29 +116,50 @@ tag_item
    }
 ;
 
+id_or_string
+   returns [Expression value]
+
+   :
+   ID
+   {
+     if (($ID.text).equals("_"))
+      {
+         $value = null;
+      }
+      else
+      {
+         $value = Main.get_variable_manager().get_variable(($ID.text));
+      }
+   }
+
+   |
+   STRING
+   {
+      $value = Main.get_string_manager().get_string_as_relation(($STRING.text));
+      System.out.println("Using (STR \"" + ($STRING.text) + "\" " + ($value) + ")");
+   }
+;
+
 id_list
-   returns [List<Variable> list, boolean has_joker]
+   returns [List<Expression> list, boolean has_joker]
 
    @init
    {
-      final List<Variable> result = new ArrayList<Variable>();
+      final List<Expression> result = new ArrayList<Expression>();
       boolean used_joker = false;
    }
 
    :
    (
       (WS)+
-      ID
+      id_or_string
       {
-         if (($ID.text).equals("_"))
+         if (($id_or_string.value) == (Expression) null)
          {
             used_joker = true;
-            result.add((Variable) null);
-         }
-         else
-         {
-            result.add(Main.get_variable_manager().get_variable(($ID.text)));
          }
+
+         result.add(($id_or_string.value));
       }
    )*
 
@@ -162,7 +183,7 @@ sl_predicate
 
    {
       final Expression predicate;
-      final List<Variable> ids;
+      final List<Expression> ids;
       final Relation predicate_as_relation;
 
       predicate_as_relation =
@@ -192,14 +213,14 @@ sl_predicate
          final List<IntExpression> columns;
          final int params_length;
 
-         ids = new ArrayList<Variable>();
+         ids = new ArrayList<Expression>();
          columns = new ArrayList<IntExpression>();
 
          params_length = ($id_list.list).size();
 
          for (int i = 0; i < params_length; ++i)
          {
-            if (($id_list.list).get(i) != (Variable) null)
+            if (($id_list.list).get(i) != (Expression) null)
             {
                columns.add(IntConstant.constant(i));
                ids.add(($id_list.list).get(i));
@@ -499,7 +520,7 @@ bl_predicate [Variable current_node]
 
    {
       final Expression predicate;
-      final List<Variable> ids;
+      final List<Expression> ids;
       final Relation predicate_as_relation;
 
       predicate_as_relation =
@@ -529,7 +550,7 @@ bl_predicate [Variable current_node]
          final List<IntExpression> columns;
          final int params_length;
 
-         ids = new ArrayList<Variable>();
+         ids = new ArrayList<Expression>();
          columns = new ArrayList<IntExpression>();
 
          params_length = ($id_list.list).size();
@@ -539,7 +560,7 @@ bl_predicate [Variable current_node]
 
          for (int i = 0; i < params_length; ++i)
          {
-            if (($id_list.list).get(i) != (Variable) null)
+            if (($id_list.list).get(i) != (Expression) null)
             {
                columns.add(IntConstant.constant(i + 1)); // Offset for the node
                ids.add(($id_list.list).get(i));
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index 5b0e9b5..b835c28 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -8,6 +8,7 @@ import kodkod.engine.satlab.*;
 import kodkod.instance.*;
 
 import java.io.IOException;
+import java.io.FileNotFoundException;
 import java.util.Iterator;
 
 public class Main
@@ -15,6 +16,7 @@ public class Main
    private static Parameters PARAMETERS;
    private static VHDLModel MODEL;
    private static VariableManager VARIABLE_MANAGER;
+   private static StringManager STRING_MANAGER;
 
    public static VHDLModel get_model ()
    {
@@ -26,6 +28,11 @@ public class Main
       return VARIABLE_MANAGER;
    }
 
+   public static StringManager get_string_manager ()
+   {
+      return STRING_MANAGER;
+   }
+
    private static boolean load_levels ()
    {
       for (final String lvl: PARAMETERS.get_level_files())
@@ -113,6 +120,103 @@ public class Main
       return true;
    }
 
+   private static boolean load_mapping_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
+         (
+            (!STRING_MANAGER.handle_mapping_instruction(input))
+            /* && (!_____.handle_mapping_instruction(input)) */
+            /* Yeah, we don't handle those */
+            && (!input[0].equals("xml->instr"))
+         )
+         {
+            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 load_mappings ()
+   {
+      try
+      {
+         for (final String file: PARAMETERS.get_mapping_files())
+         {
+            if (!load_mapping_file(file))
+            {
+               return false;
+            }
+         }
+      }
+      catch (final Exception e)
+      {
+         System.err.println("[F] Could not load mappings:");
+         e.printStackTrace();
+
+         System.exit(-1);
+      }
+
+      return true;
+   }
+
    public static void main (final String... args)
    {
       /*
@@ -147,6 +251,14 @@ public class Main
          return;
       }
 
+      /* 2/ Load Mappings (to allow references in the property). */
+      STRING_MANAGER = new StringManager();
+
+      if (!load_mappings())
+      {
+         return;
+      }
+
       /* 2/ Load Properties (will change 'is_used()' on predicates) */
       /* FIXME? Currently only one property, due to the 'is_used' */
       property = load_property();
diff --git a/instr-to-kodkod/src/Parameters.java b/instr-to-kodkod/src/Parameters.java
index c3fcd51..d3bc0f1 100644
--- a/instr-to-kodkod/src/Parameters.java
+++ b/instr-to-kodkod/src/Parameters.java
@@ -128,9 +128,9 @@ public class Parameters
       return model_files;
    }
 
-   public List<String> get_map_files ()
+   public List<String> get_mapping_files ()
    {
-      return model_files;
+      return map_files;
    }
 
    public String get_property_file ()
diff --git a/instr-to-kodkod/src/QuickParser.java b/instr-to-kodkod/src/QuickParser.java
index 47cea27..7a63c43 100644
--- a/instr-to-kodkod/src/QuickParser.java
+++ b/instr-to-kodkod/src/QuickParser.java
@@ -10,7 +10,11 @@ public class QuickParser
 
    static
    {
-      instr_pattern = Pattern.compile("\\((?<list>[a-z_0-9 \"]+)\\)");
+      instr_pattern =
+         Pattern.compile
+         (
+            "\\(([a-z_0-9\\->]+ .*)\\)"
+         );
    }
    public QuickParser (final String filename)
    throws FileNotFoundException
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index 7a9671e..ea024b8 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -350,4 +350,29 @@ public class VHDLModel
          return t.get_as_relation();
       }
    }
+
+   public Relation get_atom_as_relation
+   (
+      final String type,
+      final String id
+   )
+   {
+      final VHDLType t;
+
+      t = types.get(type);
+
+      if (t == null)
+      {
+         return null;
+      }
+      else
+      {
+         return t.get_member_as_relation(id);
+      }
+   }
+
+   public VHDLType get_string_type ()
+   {
+      return types.get("string");
+   }
 }
diff --git a/instr-to-kodkod/src/VHDLType.java b/instr-to-kodkod/src/VHDLType.java
index 58b0d1e..46d7cd9 100644
--- a/instr-to-kodkod/src/VHDLType.java
+++ b/instr-to-kodkod/src/VHDLType.java
@@ -25,7 +25,10 @@ public class VHDLType
 
    public void add_member (final String id)
    {
-      members.put(id, Relation.unary(id));
+      if (!members.containsKey(id))
+      {
+         members.put(id, Relation.unary(id));
+      }
    }
 
    public String get_name ()