anchor.diff:     /* of the class */
   }
   
  -prog: tag_existing;
  -
  -tag_existing
  -   : TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN (WS)* sl_formula (WS)* R_PAREN
  -;
  -
  -tag_item
  -   : (WS)* L_PAREN (WS)* ID (WS)+ ID (WS)+ ID (WS)* R_PAREN (WS)*
  -;
  -
  -predicate: (WS)* L_PAREN ID ((WS)+ ID)* (WS)* R_PAREN;
  +prog:
  +   tag_existing
  +;
  +
  +tag_existing:
  +   (WS)* TAG_EXISTING_KW
  +      L_PAREN
  +         (tag_item)+
  +      R_PAREN
  +   (WS)* sl_formula
  +   (WS)* R_PAREN
  +;
  +
  +tag_item:
  +   (WS)* L_PAREN
  +   (WS)* var=ID
  +   (WS)+ type=ID
  +   (WS)+ tag=ID
  +   (WS)* R_PAREN
  +   (WS)*
  +;
  +
  +id_list
  +   returns [List<Variable> list]:
  +
  +   @init
  +   {
  +      final List<Variable> result = new ArrayList<Variable>();
  +   }
  +
  +   (
  +      (WS)+
  +      var=ID
  +      {
  +         result.add(VARIABLE_SET.get_variable($var.text));
  +      }
  +   )*
  +
  +   {
  +      $list = result;
  +   }
  +;
   
   /******************************************************************************/
   /** Structural Level **********************************************************/
   /******************************************************************************/
  +
  +sl_predicate
  +   return [Formula result]:
  +
  +   (WS)* L_PAREN
  +      ID
  +      id_list
  +   (WS)* R_PAREN
  +
  +   {
  +      /* TODO */
  +   }
  +;
  +
  +sl_non_empty_formula_list
  +   returns [List<Formula> list]:
  +
  +   @init
  +   {
  +      final List<Formula> result = new ArrayList<Formula>();
  +   }
  +
  +   (
  +      sl_formula
  +
  +      {
  +         result.add($sl_formula);
  +      }
  +   )+
  +
  +   {
  +      $list = result;
  +   }
  +;
  +
   /**** First Order Expressions *************************************************/
  -sl_and_operator returns [Formula result]:
  -   (WS)* AND_OPERATOR_KW a=sl_formula b=(sl_formula)+ (WS)* R_PAREN
  -   {
  -      /* TODO */
  -      $result = a.and(b);
  -   }
  -;
  -
  -sl_or_operator returns [Formula result]:
  -   (WS)* OR_OPERATOR_KW a=sl_formula b=(sl_formula)+ (WS)* R_PAREN
  -   {
  -      /* TODO */
  -      $result = a.or(b);
  -   }
  -;
  -
  -sl_not_operator returns [Formula result]:
  -   (WS)* NOT_OPERATOR_KW sl_formula (WS)* R_PAREN
  +sl_and_operator
  +   returns [Formula result]:
  +
  +   (WS)* AND_OPERATOR_KW
  +      sl_formula
  +      sl_non_empty_formula_list
  +   (WS)* R_PAREN
  +
  +   {
  +      /* TODO */
  +      $result = $sl_formula.and($sl_non_empty_formula_list);
  +   }
  +;
  +
  +sl_or_operator
  +   returns [Formula result]:
  +
  +   (WS)* OR_OPERATOR_KW
  +      sl_formula
  +      sl_non_empty_formula_list
  +   (WS)* R_PAREN
  +
  +   {
  +      /* TODO */
  +      $result = $sl_formula.or($sl_non_empty_formula_list);
  +   }
  +;
  +
  +sl_not_operator
  +   returns [Formula result]:
  +
  +   (WS)* NOT_OPERATOR_KW
  +      sl_formula
  +   (WS)* R_PAREN
  +
      {
         /* TODO */
         $result = $sl_formula.not();
      }
   ;
   
  -sl_implies_operator returns [Formula result]:
  -   (WS)* IMPLIES_OPERATOR_KW a=sl_formula b=sl_formula (WS)* R_PAREN
  +sl_implies_operator
  +   returns [Formula result]:
  +
  +   (WS)* IMPLIES_OPERATOR_KW
  +      a=sl_formula
  +      b=sl_formula
  +   (WS)* R_PAREN
  +
      {
         /* TODO */
         $result = $a.implies($b);
  
positive.code: ;
  
  /** Special Expressions *******************************************************/
  sl_ctl_verifies_operator returns [Formula result]:
     (WS)* CTL_VERIFIES_OPERATOR_KW ps=ID (WS)* f=bl_formula (WS)* R_PAREN
     {
        /* TODO */
        $result =
           $f.forSome
           (
              VARIABLE_SET.get_variable
              (
                 ???
              ).oneOf
              (
                 {n | <ps, n> \in start_node}
              )
           );
     }
  ;
  
  /**** Formula Definition ******************************************************/
  sl_formula returns [Formula result]:
     predicate
     {
        $result = $predicate;
     }
     | sl_and_operator
     {
        $result = $sl_and_operator;
     }
     | sl_or_operator
     {
        $result = $sl_or_operator;
     }
     | sl_not_operator
     {
        $result = $sl_not_operator;
     }
     | sl_implies_operator
     {
        $result = $sl_implies_operator;
     }
     | sl_exists_operator
     {
        $result = $sl_exists_operator;
     }
     | sl_forall_operator
     {
        $result = $sl_forall_operator;
     }
     | sl_ctl_verifies_operator
     {
        $result = $sl_ctl_verifies_operator;
  
negative.code:          (
              VARIABLE_SET.get_variable
              (
                 $var.text
              ).oneOf
              (
                 MODEL.get_type_as_relation($type)
  