First shot at (logic, not VHDL) functions.

6 files changed, 155 insertions, 125 deletions

diff --git a/instr-to-kodkod/Makefile b/instr-to-kodkod/Makefile
index bb52959..1b59ccd 100644
--- a/instr-to-kodkod/Makefile
+++ b/instr-to-kodkod/Makefile
@@ -5,8 +5,9 @@ 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/incrementer.pro
 #PROPERTY_FILE = ../data/property/combinational_processes.pro
+PROPERTY_FILE = ../data/property/likely_a_clock.pro
 VAR_PREFIX = "_anon_"
 
 ## Executables #################################################################
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 46aa30f..9fcad29 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -4,6 +4,8 @@ fragment SEP: [ \t\r\n]+;
 
 L_PAREN : '(';
 R_PAREN : ')';
+L_BRAKT: ']';
+R_BRAKT: '[';
 
 TAG_EXISTING_KW: '(tag_existing' SEP;
 
diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 82eb429..29e91d2 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -116,7 +116,7 @@ tag_item
    }
 ;
 
-id_or_string
+id_or_string_or_fun [Variable current_node]
    returns [Expression value]
 
    :
@@ -138,9 +138,15 @@ id_or_string
       $value = Main.get_string_manager().get_string_as_relation(($STRING.text));
       System.out.println("Using (STR \"" + ($STRING.text) + "\" " + ($value) + ")");
    }
+
+   |
+   function[current_node]
+   {
+      $value = ($function.result);
+   }
 ;
 
-id_list
+id_list [Variable current_node]
    returns [List<Expression> list, boolean has_joker]
 
    @init
@@ -152,14 +158,14 @@ id_list
    :
    (
       (WS)+
-      id_or_string
+      id_or_string_or_fun[current_node]
       {
-         if (($id_or_string.value) == (Expression) null)
+         if (($id_or_string_or_fun.value) == (Expression) null)
          {
             used_joker = true;
          }
 
-         result.add(($id_or_string.value));
+         result.add(($id_or_string_or_fun.value));
       }
    )*
 
@@ -169,16 +175,12 @@ id_list
    }
 ;
 
-/******************************************************************************/
-/** Structural Level **********************************************************/
-/******************************************************************************/
-
-sl_predicate
+predicate [Variable current_node]
    returns [Formula result]:
 
    (WS)* L_PAREN
       ID
-      id_list
+      id_list[current_node]
    (WS)* R_PAREN
 
    {
@@ -198,7 +200,7 @@ sl_predicate
          (
             "[F] The property uses an unknown predicate: \""
             + ($ID.text)
-            + "\" at structural level. (l."
+            + "\" (l."
             + ($ID.getLine())
             + " c."
             + ($ID.getCharPositionInLine())
@@ -212,17 +214,30 @@ sl_predicate
       {
          final List<IntExpression> columns;
          final int params_length;
+         final int offset;
 
          ids = new ArrayList<Expression>();
          columns = new ArrayList<IntExpression>();
 
          params_length = ($id_list.list).size();
 
+         if (current_node == null)
+         {
+            offset = 0;
+         }
+         else
+         {
+            offset = 1;
+
+            ids.add(current_node);
+            columns.add(IntConstant.constant(0));
+         }
+
          for (int i = 0; i < params_length; ++i)
          {
             if (($id_list.list).get(i) != (Expression) null)
             {
-               columns.add(IntConstant.constant(i));
+               columns.add(IntConstant.constant(i + offset));
                ids.add(($id_list.list).get(i));
             }
          }
@@ -237,12 +252,85 @@ sl_predicate
       {
          predicate = predicate_as_relation;
          ids = ($id_list.list);
+
+         if (current_node != null)
+         {
+            ids.add(0, current_node);
+         }
       }
 
       $result = Expression.product(ids).in(predicate);
    }
 ;
 
+function [Variable current_node]
+   returns [Expression result]:
+
+   (WS)* L_BRAKT
+      ID
+      id_list[current_node]
+   (WS)* R_BRAKT
+
+   {
+      final Expression predicate;
+      final List<Expression> ids;
+      final Relation predicate_as_relation;
+
+      predicate_as_relation =
+         Main.get_model().get_predicate_as_relation
+         (
+            ($ID.text)
+         );
+
+      if (predicate_as_relation == (Relation) null)
+      {
+         System.err.println
+         (
+            "[F] The property uses an unknown predicate: \""
+            + ($ID.text)
+            + "\" (l."
+            + ($ID.getLine())
+            + " c."
+            + ($ID.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
+      if (($id_list.has_joker))
+      {
+         System.err.println
+         (
+            "[F] The property uses a joker inside a function: \""
+            + ($ID.text)
+            + "\" (l."
+            + ($ID.getLine())
+            + " c."
+            + ($ID.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+      else
+      {
+         predicate = predicate_as_relation;
+         ids = ($id_list.list);
+
+         if (current_node != null)
+         {
+            ids.add(0, current_node);
+         }
+
+         $result = Expression.product(ids).join(predicate);
+      }
+   }
+;
+
+/******************************************************************************/
+/** Structural Level **********************************************************/
+/******************************************************************************/
 sl_non_empty_formula_list
    returns [List<Formula> list]
 
@@ -466,9 +554,9 @@ sl_ctl_verifies_operator
 sl_formula
    returns [Formula result]:
 
-   sl_predicate
+   predicate[null]
    {
-      $result = ($sl_predicate.result);
+      $result = ($predicate.result);
    }
 
    | sl_and_operator
@@ -510,79 +598,6 @@ sl_formula
 /******************************************************************************/
 /** Behavioral Level **********************************************************/
 /******************************************************************************/
-bl_predicate [Variable current_node]
-   returns [Formula result]:
-
-   (WS)* L_PAREN
-      ID
-      id_list
-   (WS)* R_PAREN
-
-   {
-      final Expression predicate;
-      final List<Expression> ids;
-      final Relation predicate_as_relation;
-
-      predicate_as_relation =
-         Main.get_model().get_predicate_as_relation
-         (
-            ($ID.text)
-         );
-
-      if (predicate_as_relation == (Relation) null)
-      {
-         System.err.println
-         (
-            "[F] The property uses an unknown predicate: \""
-            + ($ID.text)
-            + "\" at behavioral level (l."
-            + ($ID.getLine())
-            + " c."
-            + ($ID.getCharPositionInLine())
-            + ")."
-         );
-
-         System.exit(-1);
-      }
-
-      if (($id_list.has_joker))
-      {
-         final List<IntExpression> columns;
-         final int params_length;
-
-         ids = new ArrayList<Expression>();
-         columns = new ArrayList<IntExpression>();
-
-         params_length = ($id_list.list).size();
-
-         /* We always keep the node id. */
-         columns.add(IntConstant.constant(0));
-
-         for (int i = 0; i < params_length; ++i)
-         {
-            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));
-            }
-         }
-
-         predicate =
-            predicate_as_relation.project
-            (
-               columns.toArray(new IntExpression[columns.size()])
-            );
-      }
-      else
-      {
-         predicate = predicate_as_relation;
-         ids = ($id_list.list);
-      }
-
-      $result = current_node.product(Expression.product(ids)).in(predicate);
-   }
-;
-
 bl_formula_list [Variable current_node]
    returns [List<Formula> list]
 
@@ -1017,9 +1032,9 @@ bl_eu_operator [Variable current_node]
 bl_formula [Variable current_node]
    returns [Formula result]:
 
-   bl_predicate[current_node]
+   predicate[current_node]
    {
-      $result = ($bl_predicate.result);
+      $result = ($predicate.result);
    }
    | bl_and_operator[current_node]
    {
diff --git a/instr-to-kodkod/src/VHDLLevel.java b/instr-to-kodkod/src/VHDLLevel.java
index 738adaf..57bb8c4 100644
--- a/instr-to-kodkod/src/VHDLLevel.java
+++ b/instr-to-kodkod/src/VHDLLevel.java
@@ -60,7 +60,11 @@ public class VHDLLevel
          }
          else if (input[0].equals("add_predicate"))
          {
-            success = handle_add_predicate(input, m);
+            success = handle_add_predicate(input, m, false);
+         }
+         else if (input[0].equals("add_function"))
+         {
+            success = handle_add_predicate(input, m, true);
          }
          else
          {
@@ -128,7 +132,8 @@ public class VHDLLevel
    private static boolean handle_add_predicate
    (
       final String[] cmd,
-      final VHDLModel m
+      final VHDLModel m,
+      final boolean is_function
    )
    {
       final String[] signature;
@@ -137,7 +142,8 @@ public class VHDLLevel
       {
          System.err.println
          (
-            "[E] Badly formed \"add_predicate\" instruction: \""
+            "[E] Badly formed \"add_predicate\" or \"add_function\""
+            + " instruction: \""
             + String.join(" ", cmd)
             + "\"."
          );
@@ -152,6 +158,6 @@ public class VHDLLevel
          signature[i - 2] = cmd[i];
       }
 
-      return m.add_predicate(cmd[1], signature);
+      return m.add_predicate(cmd[1], signature, is_function);
    }
 }
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index ea024b8..4b6e053 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -25,7 +25,12 @@ public class VHDLModel
       }
    }
 
-   public boolean add_predicate (final String name, final String[] signature)
+   public boolean add_predicate
+   (
+      final String name,
+      final String[] signature,
+      final boolean is_function
+   )
    {
       final VHDLPredicate p;
       final VHDLType[] true_signature;
@@ -55,7 +60,11 @@ public class VHDLModel
 
       if (p == null)
       {
-         predicates.put(name, new VHDLPredicate(name, true_signature));
+         predicates.put
+         (
+            name,
+            new VHDLPredicate(name, true_signature, false)
+         );
       }
       else
       {
@@ -113,7 +122,15 @@ public class VHDLModel
          }
          else if (input[0].equals("set_function"))
          {
-            success = handle_set_function(input);
+            if (input.length < 2)
+            {
+               success = false;
+            }
+            success =
+               handle_predicate
+               (
+                  Arrays.copyOfRange(input, 1, input.length)
+               );
          }
          else
          {
@@ -126,7 +143,9 @@ public class VHDLModel
             (
                "[E] An erroneous instruction was found in file \""
                + filename
-               + "\"."
+               + "\": \"("
+               + String.join(" ", input)
+               + ")\")"
             );
 
             try
@@ -186,30 +205,6 @@ public class VHDLModel
       return true;
    }
 
-   private boolean handle_set_function (final String... cmd)
-   {
-      if (cmd.length != 4)
-      {
-         System.err.println
-         (
-            "[E] Badly formed \"set_function\" instruction: \""
-            + String.join(" ", cmd)
-            + "\"."
-         );
-
-         return false;
-      }
-
-      /*
-      System.err.println
-      (
-         "[W] \"set_function\" instructions are ignored."
-      );
-      */
-
-      return true;
-   }
-
    private boolean handle_predicate (final String... cmd)
    {
       final VHDLPredicate p;
@@ -256,7 +251,6 @@ public class VHDLModel
 
       for (int i = 0; i < params.length; ++i)
       {
-         /* TODO: check if the IDs are registered in the corresponding type. */
          params[i] = cmd[i + 1];
 
          if (!p.accepts_as_nth_param(i, params[i]))
diff --git a/instr-to-kodkod/src/VHDLPredicate.java b/instr-to-kodkod/src/VHDLPredicate.java
index 3605e76..0ff388b 100644
--- a/instr-to-kodkod/src/VHDLPredicate.java
+++ b/instr-to-kodkod/src/VHDLPredicate.java
@@ -14,11 +14,18 @@ public class VHDLPredicate
    private final String name;
    private final int arity;
    private final Relation as_relation;
+   private final boolean is_function;
    private boolean is_used;
 
-   public VHDLPredicate (final String name, final VHDLType[] signature)
+   public VHDLPredicate
+   (
+      final String name,
+      final VHDLType[] signature,
+      final boolean is_function
+   )
    {
       this.name = name;
+      this.is_function = is_function;
       arity = signature.length;
 
       signatures = new ArrayList<VHDLType[]>();
@@ -45,6 +52,11 @@ public class VHDLPredicate
       return arity;
    }
 
+   public boolean is_function ()
+   {
+      return is_function;
+   }
+
    public Relation get_as_relation ()
    {
       if (!is_used)