Removes repetitions, prepares for skol. of sol.

5 files changed, 536 insertions, 385 deletions

diff --git a/instr-to-kodkod/parser/PropertyParser.g4 b/instr-to-kodkod/parser/PropertyParser.g4
index 40cb2aa..8ac7b03 100644
--- a/instr-to-kodkod/parser/PropertyParser.g4
+++ b/instr-to-kodkod/parser/PropertyParser.g4
@@ -25,80 +25,17 @@ tag_existing
 
    (WS)* TAG_EXISTING_KW
       L_PAREN
-         tag_list
+      (tag_item)+
       R_PAREN
-   (WS)* sl_formula
+   (WS)* formula[null]
    (WS)* R_PAREN
 
    {
-      final List<String[]> tags;
-
-      $result = ($sl_formula.result);
-
-      tags = ($tag_list.list);
-
-      for (final String[] tag_var: tags)
-      {
-         final Relation type_as_relation;
-
-         type_as_relation = Main.get_model().get_type_as_relation(tag_var[1]);
-
-         if (type_as_relation == (Relation) null)
-         {
-            System.err.println
-            (
-               "[F] The property uses an unknown type: \""
-               + tag_var[1]
-               + "\" in its tag_existing (l."
-               + ($TAG_EXISTING_KW.getLine())
-               + " c."
-               + ($TAG_EXISTING_KW.getCharPositionInLine())
-               + ")."
-            );
-
-            System.exit(-1);
-         }
-
-         $result =
-            $result.forSome
-            (
-               Main.get_variable_manager().get_variable
-               (
-                  tag_var[0]
-               ).oneOf
-               (
-                  type_as_relation
-               )
-            );
-
-         Main.get_variable_manager().tag_variable(tag_var[0], tag_var[2]);
-      }
+      $result = ($formula.result);
    }
 ;
 
-tag_list
-   returns [List<String[]> list]
-
-   @init
-   {
-      final List<String[]> result = new ArrayList<String[]>();
-   }
-
-   :
-   (
-      tag_item
-      {
-         result.add(($tag_item.result));
-      }
-   )+
-
-   {
-      $list = result;
-   }
-;
-
-tag_item
-   returns [String[] result]:
+tag_item:
 
    (WS)* L_PAREN
    (WS)* var=ID
@@ -108,11 +45,47 @@ tag_item
    (WS)*
 
    {
-      $result = new String[3];
+      try
+      {
+         Main.get_variable_manager().add_tag
+         (
+            ($var.text),
+            ($type.text),
+            ($tag.text)
+         );
+      }
+      catch (final Exception e)
+      {
+         System.err.println
+         (
+            "[F] The following exception was raised during the parsing of the"
+            + " property (l."
+            + ($var.getLine())
+            + " c."
+            + ($var.getCharPositionInLine())
+            + "):\n"
+            + e.getMessage()
+         );
+
+         System.exit(-1);
+      }
+
+      if (!Main.get_model().type_exists(($type.text)))
+      {
+         System.err.println
+         (
+            "[F] The following exception was raised during the parsing of the"
+            + " property (l."
+            + ($var.getLine())
+            + " c."
+            + ($var.getCharPositionInLine())
+            + "):\n[F] No such type \""
+            + ($type.text)
+            + "\"."
+         );
 
-      $result[0] = ($var.text);
-      $result[1] = ($type.text);
-      $result[2] = ($tag.text);
+         System.exit(-1);
+      }
    }
 ;
 
@@ -122,13 +95,31 @@ id_or_string_or_fun [Variable current_node]
    :
    ID
    {
-     if (($ID.text).equals("_"))
+      if (($ID.text).equals("_"))
       {
          $value = null;
       }
       else
       {
-         $value = Main.get_variable_manager().get_variable(($ID.text));
+         try
+         {
+            $value = Main.get_variable_manager().get_variable(($ID.text));
+         }
+         catch (final Exception e)
+         {
+            System.err.println
+            (
+               "[F] The following exception was raised during the parsing of"
+               + " the property (l."
+               + ($ID.getLine())
+               + " c."
+               + ($ID.getCharPositionInLine())
+               + "):\n"
+               + e.getMessage()
+            );
+
+            System.exit(-1);
+         }
       }
    }
 
@@ -136,7 +127,6 @@ id_or_string_or_fun [Variable current_node]
    STRING
    {
       $value = Main.get_string_manager().get_string_as_relation(($STRING.text));
-      System.out.println("Using (STR \"" + ($STRING.text) + "\" " + ($value) + ")");
    }
 
    |
@@ -160,7 +150,7 @@ id_list [Variable current_node]
       (WS)+
       id_or_string_or_fun[current_node]
       {
-         if (($id_or_string_or_fun.value) == (Expression) null)
+         if (($id_or_string_or_fun.value) == null)
          {
             used_joker = true;
          }
@@ -286,7 +276,7 @@ function [Variable current_node]
       {
          System.err.println
          (
-            "[F] The property uses an unknown predicate: \""
+            "[F] The property uses an unknown function: \""
             + ($ID.text)
             + "\" (l."
             + ($ID.getLine())
@@ -302,7 +292,7 @@ function [Variable current_node]
       {
          System.err.println
          (
-            "[F] The property uses a joker inside a function: \""
+            "[F] The property uses a joker inside a function call at \""
             + ($ID.text)
             + "\" (l."
             + ($ID.getLine())
@@ -328,10 +318,7 @@ function [Variable current_node]
    }
 ;
 
-/******************************************************************************/
-/** Structural Level **********************************************************/
-/******************************************************************************/
-sl_non_empty_formula_list
+non_empty_formula_list [Variable current_node]
    returns [List<Formula> list]
 
    @init
@@ -341,10 +328,10 @@ sl_non_empty_formula_list
 
    :
    (
-      sl_formula
+      formula[current_node]
 
       {
-         result.add(($sl_formula.result));
+         result.add(($formula.result));
       }
    )+
 
@@ -354,62 +341,62 @@ sl_non_empty_formula_list
 ;
 
 /**** First Order Expressions *************************************************/
-sl_and_operator
+and_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* AND_OPERATOR_KW
-      sl_formula
-      sl_non_empty_formula_list
+      formula[current_node]
+      non_empty_formula_list[current_node]
    (WS)* R_PAREN
 
    {
       $result =
          (
-            ($sl_formula.result)
+            ($formula.result)
          ).and
          (
-            Formula.and(($sl_non_empty_formula_list.list))
+            Formula.and(($non_empty_formula_list.list))
          );
    }
 ;
 
-sl_or_operator
+or_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* OR_OPERATOR_KW
-      sl_formula
-      sl_non_empty_formula_list
+      formula[current_node]
+      non_empty_formula_list[current_node]
    (WS)* R_PAREN
 
    {
       $result =
          (
-            ($sl_formula.result)
+            ($formula.result)
          ).or
          (
-            Formula.or(($sl_non_empty_formula_list.list))
+            Formula.or(($non_empty_formula_list.list))
          );
    }
 ;
 
-sl_not_operator
+not_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* NOT_OPERATOR_KW
-      sl_formula
+      formula[current_node]
    (WS)* R_PAREN
 
    {
-      $result = ($sl_formula.result).not();
+      $result = ($formula.result).not();
    }
 ;
 
-sl_implies_operator
+implies_operator [Variable current_node]
    returns [Formula result]:
 
    (WS)* IMPLIES_OPERATOR_KW
-      a=sl_formula
-      b=sl_formula
+      a=formula[current_node]
+      b=formula[current_node]
    (WS)* R_PAREN
 
    {
@@ -418,31 +405,25 @@ sl_implies_operator
 ;
 
 /** Quantified Expressions ****************************************************/
-sl_exists_operator
-   returns [Formula result]:
+variable_declaration
+   returns [Variable var_as_var, Relation type_as_rel]:
 
-   (WS)* EXISTS_OPERATOR_KW
-         var=ID
-   (WS)+ type=ID
-         f=sl_formula
-   (WS*) R_PAREN
+   var=ID (WS)+ type=ID
 
    {
-      final Relation type_as_relation;
-
-      type_as_relation =
+      $type_as_rel =
          Main.get_model().get_type_as_relation
          (
             ($type.text)
          );
 
-      if (type_as_relation == (Relation) null)
+      if ($type_as_rel == (Relation) null)
       {
          System.err.println
          (
             "[F] The property uses an unknown type: \""
             + ($type.text)
-            + "\" in an \"exists\" at structural level (l."
+            + "\" at (l."
             + ($type.getLine())
             + " c."
             + ($type.getCharPositionInLine())
@@ -452,256 +433,203 @@ sl_exists_operator
          System.exit(-1);
       }
 
-      $result =
-         ($f.result).forSome
+      try
+      {
+         $var_as_var = Main.get_variable_manager().add_variable(($var.text));
+      }
+      catch (final Exception e)
+      {
+         System.err.println
          (
-            Main.get_variable_manager().get_variable
-            (
-               ($var.text)
-            ).oneOf
-            (
-               type_as_relation
-            )
+            "[F] The following exception was raised during the parsing of"
+            + " the property (l."
+            + ($var.getLine())
+            + " c."
+            + ($var.getCharPositionInLine())
+            + "):\n"
+            + e.getMessage()
          );
+
+         System.exit(-1);
+      }
    }
 ;
 
-sl_forall_operator
+exists_operator [Variable current_node]
    returns [Formula result]:
 
-   (WS)* FORALL_OPERATOR_KW
-         var=ID
-   (WS)+ type=ID
-         f=sl_formula
+   (WS)* EXISTS_OPERATOR_KW
+      variable_declaration
+      formula[current_node]
    (WS*) R_PAREN
 
    {
-      final Relation type_as_relation;
-
-      type_as_relation =
-         Main.get_model().get_type_as_relation
-         (
-            ($type.text)
-         );
-
-      if (type_as_relation == (Relation) null)
+      if (current_node != null)
       {
          System.err.println
          (
-            "[F] The property uses an unknown type: \""
-            + ($type.text)
-            + "\" in a \"forall\" at structural level (l."
-            + ($type.getLine())
+            "[W] Use of the existential operator inside a \"CTL_verifies\""
+            + " operator is not part of Tabellion's semantics and may not be"
+            + " available on other solving platforms. As a result, its use is"
+            + " discouraged (from l."
+            + ($EXISTS_OPERATOR_KW.getLine())
             + " c."
-            + ($type.getCharPositionInLine())
+            + ($EXISTS_OPERATOR_KW.getCharPositionInLine())
             + ")."
          );
-
-         System.exit(-1);
       }
 
       $result =
-         ($f.result).forAll
+         ($formula.result).forSome
          (
-            Main.get_variable_manager().get_variable
-            (
-               ($var.text)
-            ).oneOf
+            ($variable_declaration.var_as_var).oneOf
             (
-               type_as_relation
+               ($variable_declaration.type_as_rel)
             )
          );
    }
 ;
 
-/** Special Expressions *******************************************************/
-sl_ctl_verifies_operator
-   returns [Formula result]
-
-   @init
-   {
-      final Variable root_node;
-
-      root_node = Main.get_variable_manager().generate_new_variable();
-   }
+forall_operator [Variable current_node]
+   returns [Formula result]:
 
-   :
-   (WS)* CTL_VERIFIES_OPERATOR_KW
-         ps=ID
-         f=bl_formula[root_node]
-   (WS)* R_PAREN
+   (WS)* FORALL_OPERATOR_KW
+      variable_declaration
+      formula[current_node]
+   (WS*) R_PAREN
 
    {
+      if (current_node != null)
+      {
+         System.err.println
+         (
+            "[W] Use of the universal operator inside a \"CTL_verifies\""
+            + " operator is not part of Tabellion's semantics and may not be"
+            + " available on other solving platforms. As a result, its use is"
+            + " discouraged (from l."
+            + ($FORALL_OPERATOR_KW.getLine())
+            + " c."
+            + ($FORALL_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+      }
 
       $result =
-         ($f.result).forSome
+         ($formula.result).forAll
          (
-            root_node.oneOf
+            ($variable_declaration.var_as_var).oneOf
             (
-               Main.get_variable_manager().get_variable(($ps.text)).join
-               (
-                  Main.get_model().get_predicate_as_relation
-                  (
-                     "is_start_node"
-                  ).transpose()
-               )
+               ($variable_declaration.type_as_rel)
             )
          );
    }
 ;
 
-/**** Formula Definition ******************************************************/
-sl_formula
-   returns [Formula result]:
-
-   predicate[null]
-   {
-      $result = ($predicate.result);
-   }
-
-   | sl_and_operator
-   {
-      $result = ($sl_and_operator.result);
-   }
-
-   | sl_or_operator
-   {
-      $result = ($sl_or_operator.result);
-   }
-
-   | sl_not_operator
-   {
-      $result = ($sl_not_operator.result);
-   }
-
-   | sl_implies_operator
-   {
-      $result = ($sl_implies_operator.result);
-   }
-
-   | sl_exists_operator
-   {
-      $result = ($sl_exists_operator.result);
-   }
-
-   | sl_forall_operator
-   {
-      $result = ($sl_forall_operator.result);
-   }
-
-   | sl_ctl_verifies_operator
-   {
-      $result = ($sl_ctl_verifies_operator.result);
-   }
-;
-
-/******************************************************************************/
-/** Behavioral Level **********************************************************/
-/******************************************************************************/
-bl_formula_list [Variable current_node]
-   returns [List<Formula> list]
+/** Special Expressions *******************************************************/
+ctl_verifies_operator [Variable current_node]
+   returns [Formula result]
 
    @init
    {
-      final List<Formula> result = new ArrayList<Formula>();
-   }
-
-   :
-   (
-      bl_formula[current_node]
-      {
-         result.add(($bl_formula.result));
-      }
-   )+
+      final Variable root_node;
 
-   {
-      $list = result;
+      root_node = Main.get_variable_manager().generate_new_anonymous_variable();
    }
-;
-
-/**** First Order Expressions *************************************************/
-bl_and_operator [Variable current_node]
-   returns [Formula result]:
 
-   (WS)* AND_OPERATOR_KW
-      bl_formula[current_node]
-      bl_formula_list[current_node]
+   :
+   (WS)* CTL_VERIFIES_OPERATOR_KW
+         ps=ID
+         f=formula[root_node]
    (WS)* R_PAREN
 
    {
-      $result =
-         (
-            ($bl_formula.result)
-         ).and
+      if (current_node != null)
+      {
+         System.err.println
          (
-            Formula.and(($bl_formula_list.list))
+            "[F] The property uses a \"CTL_verifies\" inside a \"CTL_verifies\""
+            + " and we have not heard anything about you liking"
+            + " \"CTL_verifies\", so you can't CTL_verify while you CTL_verify"
+            + " (l."
+            + ($CTL_VERIFIES_OPERATOR_KW.getLine())
+            + " c."
+            + ($CTL_VERIFIES_OPERATOR_KW.getCharPositionInLine())
+            + ")."
          );
-   }
-;
-
-bl_or_operator [Variable current_node]
-   returns [Formula result]:
 
-   (WS)* OR_OPERATOR_KW
-      bl_formula[current_node]
-      bl_formula_list[current_node]
-   (WS)* R_PAREN
+         System.exit(-1);
+      }
 
-   {
-      $result =
-         (
-            ($bl_formula.result)
-         ).or
+      try
+      {
+         $result =
+            ($f.result).forSome
+            (
+               root_node.oneOf
+               (
+                  Main.get_variable_manager().get_variable(($ps.text)).join
+                  (
+                     Main.get_model().get_predicate_as_relation
+                     (
+                        "is_start_node"
+                     ).transpose()
+                  )
+               )
+            );
+      }
+      catch (final Exception e)
+      {
+         System.err.println
          (
-            Formula.or(($bl_formula_list.list))
+            "[F] The following exception was raised during the parsing of"
+            + " the property (l."
+            + ($ps.getLine())
+            + " c."
+            + ($ps.getCharPositionInLine())
+            + "):\n"
+            + e.getMessage()
          );
-   }
-;
-
-bl_not_operator [Variable current_node]
-   returns [Formula result]:
 
-   (WS)* NOT_OPERATOR_KW
-      bl_formula[current_node]
-   (WS)* R_PAREN
-
-   {
-      $result = ($bl_formula.result).not();
+         System.exit(-1);
+      }
    }
 ;
 
-bl_implies_operator [Variable current_node]
-   returns [Formula result]:
-
-   (WS)* IMPLIES_OPERATOR_KW
-      a=bl_formula[current_node]
-      b=bl_formula[current_node]
-   (WS)* R_PAREN
-
-   {
-      $result = ($a.result).implies(($b.result));
-   }
-;
 
 /**** Computation Tree Logic Expressions **************************************/
-bl_ax_operator [Variable current_node]
+ax_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable next_node;
 
-      next_node = Main.get_variable_manager().generate_new_variable();
+      next_node = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* AX_OPERATOR_KW
-      bl_formula[next_node]
+      formula[next_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($AX_OPERATOR_KW.getLine())
+            + " c."
+            + ($AX_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
-         ($bl_formula.result).forAll
+         ($formula.result).forAll
          (
             next_node.oneOf
             (
@@ -714,24 +642,39 @@ bl_ax_operator [Variable current_node]
    }
 ;
 
-bl_ex_operator [Variable current_node]
+ex_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable next_node;
 
-      next_node = Main.get_variable_manager().generate_new_variable();
+      next_node = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* EX_OPERATOR_KW
-      bl_formula[next_node]
+      formula[next_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($EX_OPERATOR_KW.getLine())
+            + " c."
+            + ($EX_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
-         ($bl_formula.result).forSome
+         ($formula.result).forSome
          (
             next_node.oneOf
             (
@@ -744,24 +687,39 @@ bl_ex_operator [Variable current_node]
    }
 ;
 
-bl_ag_operator [Variable current_node]
+ag_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable next_node;
 
-      next_node = Main.get_variable_manager().generate_new_variable();
+      next_node = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* AG_OPERATOR_KW
-      bl_formula[next_node]
+      formula[next_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($AG_OPERATOR_KW.getLine())
+            + " c."
+            + ($AG_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
-         ($bl_formula.result).forAll
+         ($formula.result).forAll
          (
             next_node.oneOf
             (
@@ -780,25 +738,40 @@ bl_ag_operator [Variable current_node]
    }
 ;
 
-bl_eg_operator [Variable current_node]
+eg_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable next_node, chosen_path;
 
-      next_node = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      next_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* EG_OPERATOR_KW
-      bl_formula[next_node]
+      formula[next_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($EG_OPERATOR_KW.getLine())
+            + " c."
+            + ($EG_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
-         ($bl_formula.result).forAll
+         ($formula.result).forAll
          (
             next_node.oneOf
             (
@@ -823,25 +796,40 @@ bl_eg_operator [Variable current_node]
    }
 ;
 
-bl_af_operator [Variable current_node]
+af_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable next_node, chosen_path;
 
-      next_node = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      next_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* AF_OPERATOR_KW
-      bl_formula[next_node]
+      formula[next_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($AF_OPERATOR_KW.getLine())
+            + " c."
+            + ($AF_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
-         ($bl_formula.result).forSome
+         ($formula.result).forSome
          (
             next_node.oneOf
             (
@@ -866,25 +854,40 @@ bl_af_operator [Variable current_node]
    }
 ;
 
-bl_ef_operator [Variable current_node]
+ef_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable next_node, chosen_path;
 
-      next_node = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      next_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* EF_OPERATOR_KW
-      bl_formula[next_node]
+      formula[next_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($EF_OPERATOR_KW.getLine())
+            + " c."
+            + ($EF_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
-         ($bl_formula.result).forSome
+         ($formula.result).forSome
          (
             next_node.oneOf
             (
@@ -909,25 +912,40 @@ bl_ef_operator [Variable current_node]
    }
 ;
 
-bl_au_operator [Variable current_node]
+au_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable f1_node, f2_node, chosen_path;
 
-      f1_node = Main.get_variable_manager().generate_new_variable();
-      f2_node = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      f1_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      f2_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* AU_OPERATOR_KW
-      f1=bl_formula[f1_node]
-      f2=bl_formula[f2_node]
+      f1=formula[f1_node]
+      f2=formula[f2_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($AU_OPERATOR_KW.getLine())
+            + " c."
+            + ($AU_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
          ($f1.result).forAll
          (
@@ -969,25 +987,40 @@ bl_au_operator [Variable current_node]
    }
 ;
 
-bl_eu_operator [Variable current_node]
+eu_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable f1_node, f2_node, chosen_path;
 
-      f1_node = Main.get_variable_manager().generate_new_variable();
-      f2_node = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      f1_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      f2_node = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* EU_OPERATOR_KW
-      f1=bl_formula[f1_node]
-      f2=bl_formula[f2_node]
+      f1=formula[f1_node]
+      f2=formula[f2_node]
    (WS)* R_PAREN
 
    {
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($EU_OPERATOR_KW.getLine())
+            + " c."
+            + ($EU_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
          ($f1.result).forAll
          (
@@ -1029,21 +1062,21 @@ bl_eu_operator [Variable current_node]
 ;
 
 /**** Depth Operators *********************************************************/
-bl_depth_no_parent_operator [Variable current_node]
+depth_no_parent_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable node_of_path, node_for_f, chosen_path;
 
-      node_of_path = Main.get_variable_manager().generate_new_variable();
-      node_for_f = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      node_of_path = Main.get_variable_manager().generate_new_anonymous_variable();
+      node_for_f = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
    (WS)* DEPTH_NO_PARENT_OPERATOR_KW
-      bl_formula[node_for_f]
+      formula[node_for_f]
    (WS)* R_PAREN
 
    {
@@ -1052,6 +1085,21 @@ bl_depth_no_parent_operator [Variable current_node]
       depth_relation = Main.get_model().get_predicate_as_relation("depth");
       lower_than_relation = Main.get_model().get_predicate_as_relation("depth");
 
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($DEPTH_NO_PARENT_OPERATOR_KW.getLine())
+            + " c."
+            + ($DEPTH_NO_PARENT_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
          node_of_path.join
          (
@@ -1079,7 +1127,7 @@ bl_depth_no_parent_operator [Variable current_node]
             )
          ).and
          (
-            ($bl_formula.result).and
+            ($formula.result).and
             (
                current_node.join
                (
@@ -1117,21 +1165,21 @@ bl_depth_no_parent_operator [Variable current_node]
    }
 ;
 
-bl_depth_no_change_operator [Variable current_node]
+depth_no_change_operator [Variable current_node]
    returns [Formula result]
 
    @init
    {
       final Variable node_of_path, node_for_f, chosen_path;
 
-      node_of_path = Main.get_variable_manager().generate_new_variable();
-      node_for_f = Main.get_variable_manager().generate_new_variable();
-      chosen_path = Main.get_variable_manager().generate_new_variable();
+      node_of_path = Main.get_variable_manager().generate_new_anonymous_variable();
+      node_for_f = Main.get_variable_manager().generate_new_anonymous_variable();
+      chosen_path = Main.get_variable_manager().generate_new_anonymous_variable();
    }
 
    :
-   (WS)* DEPTH_NO_PARENT_OPERATOR_KW
-      bl_formula[node_for_f]
+   (WS)* DEPTH_NO_CHANGE_OPERATOR_KW
+      formula[node_for_f]
    (WS)* R_PAREN
 
    {
@@ -1139,6 +1187,21 @@ bl_depth_no_change_operator [Variable current_node]
 
       depth_relation = Main.get_model().get_predicate_as_relation("depth");
 
+      if (current_node == null)
+      {
+         System.err.println
+         (
+            "[F] The property uses a CTL operator outside of a \"CTL_verifies\""
+            + " (l."
+            + ($DEPTH_NO_CHANGE_OPERATOR_KW.getLine())
+            + " c."
+            + ($DEPTH_NO_CHANGE_OPERATOR_KW.getCharPositionInLine())
+            + ")."
+         );
+
+         System.exit(-1);
+      }
+
       $result =
          node_of_path.join
          (
@@ -1161,7 +1224,7 @@ bl_depth_no_change_operator [Variable current_node]
             )
          ).and
          (
-            ($bl_formula.result)
+            ($formula.result)
          ).forSome
          (
             node_for_f.oneOf
@@ -1188,67 +1251,96 @@ bl_depth_no_change_operator [Variable current_node]
 ;
 
 /**** Formula Definition ******************************************************/
-bl_formula [Variable current_node]
+formula [Variable current_node]
    returns [Formula result]:
 
    predicate[current_node]
    {
       $result = ($predicate.result);
    }
-   | bl_and_operator[current_node]
+
+   | and_operator[current_node]
+   {
+      $result = ($and_operator.result);
+   }
+
+   | or_operator[current_node]
    {
-      $result = ($bl_and_operator.result);
+      $result = ($or_operator.result);
    }
-   | bl_or_operator[current_node]
+
+   | not_operator[current_node]
    {
-      $result = ($bl_or_operator.result);
+      $result = ($not_operator.result);
    }
-   | bl_not_operator[current_node]
+
+   | implies_operator[current_node]
+   {
+      $result = ($implies_operator.result);
+   }
+
+   | exists_operator[current_node]
+   {
+      $result = ($exists_operator.result);
+   }
+
+   | forall_operator[current_node]
    {
-      $result = ($bl_not_operator.result);
+      $result = ($forall_operator.result);
    }
-   | bl_implies_operator[current_node]
+
+   | ctl_verifies_operator[current_node]
    {
-      $result = ($bl_implies_operator.result);
+      $result = ($ctl_verifies_operator.result);
    }
-   | bl_ax_operator[current_node]
+
+   | ax_operator[current_node]
    {
-      $result = ($bl_ax_operator.result);
+      $result = ($ax_operator.result);
    }
-   | bl_ex_operator[current_node]
+
+   | ex_operator[current_node]
    {
-      $result = ($bl_ex_operator.result);
+      $result = ($ex_operator.result);
    }
-   | bl_ag_operator[current_node]
+
+   | ag_operator[current_node]
    {
-      $result = ($bl_ag_operator.result);
+      $result = ($ag_operator.result);
    }
-   | bl_eg_operator[current_node]
+
+   | eg_operator[current_node]
    {
-      $result = ($bl_eg_operator.result);
+      $result = ($eg_operator.result);
    }
-   | bl_af_operator[current_node]
+
+   | af_operator[current_node]
    {
-      $result = ($bl_af_operator.result);
+      $result = ($af_operator.result);
    }
-   | bl_ef_operator[current_node]
+
+   | ef_operator[current_node]
    {
-      $result = ($bl_ef_operator.result);
+      $result = ($ef_operator.result);
    }
-   | bl_au_operator[current_node]
+
+   | au_operator[current_node]
    {
-      $result = ($bl_au_operator.result);
+      $result = ($au_operator.result);
    }
-   | bl_eu_operator[current_node]
+
+   | eu_operator[current_node]
    {
-      $result = ($bl_eu_operator.result);
+      $result = ($eu_operator.result);
    }
-   | bl_depth_no_parent_operator[current_node]
+
+   | depth_no_parent_operator[current_node]
    {
-      $result = ($bl_depth_no_parent_operator.result);
+      $result = ($depth_no_parent_operator.result);
    }
-   | bl_depth_no_change_operator[current_node]
+
+   | depth_no_change_operator[current_node]
    {
-      $result = ($bl_depth_no_change_operator.result);
+      $result = ($depth_no_change_operator.result);
    }
 ;
diff --git a/instr-to-kodkod/src/Main.java b/instr-to-kodkod/src/Main.java
index b835c28..d8393bd 100644
--- a/instr-to-kodkod/src/Main.java
+++ b/instr-to-kodkod/src/Main.java
@@ -76,7 +76,7 @@ public class Main
             + "\"..."
          );
 
-         return pro.generate_formula();
+         return pro.generate_base_formula();
       }
       catch (final IOException e)
       {
diff --git a/instr-to-kodkod/src/VHDLModel.java b/instr-to-kodkod/src/VHDLModel.java
index 4b6e053..170ce12 100644
--- a/instr-to-kodkod/src/VHDLModel.java
+++ b/instr-to-kodkod/src/VHDLModel.java
@@ -345,6 +345,16 @@ public class VHDLModel
       }
    }
 
+   public boolean type_exists (final String name)
+   {
+      return types.containsKey(name);
+   }
+
+   public boolean predicate_exists (final String name)
+   {
+      return predicates.containsKey(name);
+   }
+
    public Relation get_atom_as_relation
    (
       final String type,
diff --git a/instr-to-kodkod/src/VHDLProperty.java b/instr-to-kodkod/src/VHDLProperty.java
index a91d25a..ac88e6e 100644
--- a/instr-to-kodkod/src/VHDLProperty.java
+++ b/instr-to-kodkod/src/VHDLProperty.java
@@ -9,13 +9,17 @@ import org.antlr.v4.runtime.*;
 public class VHDLProperty
 {
    private final String filename;
+   private final List<Variable> tagged_variables;
+   private final List<VHDLType> tagged_variables_types;
 
    public VHDLProperty (final String filename)
    {
       this.filename = filename;
+      tagged_variables = new ArrayList<Variable>();
+      tagged_variables_types = new ArrayList<VHDLType>();
    }
 
-   public Formula generate_formula ()
+   public Formula generate_base_formula ()
    throws IOException
    {
       final PropertyLexer lexer;
diff --git a/instr-to-kodkod/src/VariableManager.java b/instr-to-kodkod/src/VariableManager.java
index 381a774..eaa20d2 100644
--- a/instr-to-kodkod/src/VariableManager.java
+++ b/instr-to-kodkod/src/VariableManager.java
@@ -5,53 +5,98 @@ import kodkod.ast.*;
 
 public class VariableManager
 {
-   private final Map<String, Variable> from_string;
+   private final Map<String, Expression> from_string;
    private final Map<String, String> tags;
-   private final String var_prefix;
    private int next_id;
 
    public VariableManager (final String var_prefix)
    {
-      from_string = new HashMap<String, Variable>();
+      from_string = new HashMap<String, Expression>();
       tags = new HashMap<String, String>();
-
-      this.var_prefix = var_prefix;
    }
 
-   private String generate_new_id ()
+   private String generate_new_anonymous_variable_name ()
    {
       final String result;
 
-      result = var_prefix + next_id;
+      result = "_var" + next_id;
 
       next_id += 1;
 
       return result;
    }
 
-   public Variable get_variable (final String name)
+   public void add_tag
+   (
+      final String var_name,
+      final String var_type,
+      final String tag_name
+   )
+   throws Exception
    {
-      Variable result;
-
-      result = from_string.get(name);
+      System.out.println("[D] Skolemizing: " + var_name);
 
-      if (result == null)
+      if (from_string.containsKey(var_name))
       {
-         result = Variable.unary(name);
+         throw
+            new Exception
+            (
+               "[F] Invalid property: the variable name \""
+               + var_name
+               + "\" is bound multiple times in the \"tag_existing\""
+               + " operator."
+            );
+      }
 
-         from_string.put(name, result);
+      from_string.put(var_name, Variable.unary(var_name));
+   }
+
+   public Variable add_variable (final String var_name)
+   throws Exception
+   {
+      final Variable result;
+
+      if (from_string.containsKey(var_name))
+      {
+         throw
+            new Exception
+            (
+               "[F] Invalid property: the variable name \""
+               + var_name
+               + "\" is declared multiple times."
+            );
       }
 
+      result = Variable.unary(var_name);
+
+      from_string.put(var_name, result);
+
       return result;
    }
 
-   public Variable generate_new_variable ()
+   public Expression get_variable (final String var_name)
+   throws Exception
    {
-      return get_variable(generate_new_id());
+      final Expression result;
+
+      result = from_string.get(var_name);
+
+      if (result == null)
+      {
+         throw
+            new Exception
+            (
+               "[F] Variable \""
+               + var_name
+               + "\" is used, but not declared."
+            );
+      }
+
+      return result;
    }
 
-   public void tag_variable (final String name, final String tag)
+   public Variable generate_new_anonymous_variable ()
    {
-      tags.put(name, tag);
+      return Variable.unary(generate_new_anonymous_variable_name());
    }
 }