diff --git a/Makefile b/Makefile
index 2491bc7..40d229f 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@ CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
 #CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
 LDLIBS = $(CUDD_INCLUDE) 
 
-OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctl.o 
+OBJ = rs.o ctx_aut.o symrs.o mc.o rsin_driver.o rsin_parser.o rsin_parser.lex.o formrsctlk.o 
 
 all: main
 
diff --git a/formrsctl.cc b/formrsctlk.cc
similarity index 77%
rename from formrsctl.cc
rename to formrsctlk.cc
index f85693a..5870709 100644
--- a/formrsctl.cc
+++ b/formrsctlk.cc
@@ -6,7 +6,7 @@
     without the author's permission is strictly prohibited.
 */
 
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
 
 
 std::string BoolContexts::toStr(void) const
@@ -73,12 +73,12 @@ BDD BoolContexts::getBDD(const SymRS *srs) const
   }
 }
 
-std::string FormRSCTL::toStr(void) const
+std::string FormRSCTLK::toStr(void) const
 {
-  if (oper == RSCTL_PV) {
+  if (oper == RSCTLK_PV) {
     return proc_name + "." + entity_name;
   }
-  else if (oper == RSCTL_TF) {
+  else if (oper == RSCTLK_TF) {
     if (tf) {
       return "true";
     }
@@ -86,69 +86,69 @@ std::string FormRSCTL::toStr(void) const
       return "false";
     }
   }
-  else if (oper == RSCTL_AND) {
+  else if (oper == RSCTLK_AND) {
     return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
   }
-  else if (oper == RSCTL_OR) {
+  else if (oper == RSCTLK_OR) {
     return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
   }
-  else if (oper == RSCTL_XOR) {
+  else if (oper == RSCTLK_XOR) {
     return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
   }
-  else if (oper == RSCTL_IMPL) {
+  else if (oper == RSCTLK_IMPL) {
     return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
   }
-  else if (oper == RSCTL_NOT) {
+  else if (oper == RSCTLK_NOT) {
     return "~" + arg[0]->toStr();
   }
-  else if (oper == RSCTL_EX) {
+  else if (oper == RSCTLK_EX) {
     return "EX(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_EG) {
+  else if (oper == RSCTLK_EG) {
     return "EG(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_EU) {
+  else if (oper == RSCTLK_EU) {
     return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
   }
-  else if (oper == RSCTL_EF) {
+  else if (oper == RSCTLK_EF) {
     return "EF(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_AX) {
+  else if (oper == RSCTLK_AX) {
     return "AX(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_AG) {
+  else if (oper == RSCTLK_AG) {
     return "AG(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_AU) {
+  else if (oper == RSCTLK_AU) {
     return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
   }
-  else if (oper == RSCTL_AF) {
+  else if (oper == RSCTLK_AF) {
     return "AF(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_EX_ACT) {
+  else if (oper == RSCTLK_EX_ACT) {
     return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_EG_ACT) {
+  else if (oper == RSCTLK_EG_ACT) {
     return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_EU_ACT) {
+  else if (oper == RSCTLK_EU_ACT) {
     return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
            + ")";
   }
-  else if (oper == RSCTL_EF_ACT) {
+  else if (oper == RSCTLK_EF_ACT) {
     return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_AX_ACT) {
+  else if (oper == RSCTLK_AX_ACT) {
     return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_AG_ACT) {
+  else if (oper == RSCTLK_AG_ACT) {
     return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
   }
-  else if (oper == RSCTL_AU_ACT) {
+  else if (oper == RSCTLK_AU_ACT) {
     return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
            + ")";
   }
-  else if (oper == RSCTL_AF_ACT) {
+  else if (oper == RSCTLK_AF_ACT) {
     return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
   }
 
@@ -158,7 +158,7 @@ std::string FormRSCTL::toStr(void) const
   }
 }
 
-bool FormRSCTL::hasOper(Oper op) const
+bool FormRSCTLK::hasOper(Oper op) const
 {
   if (oper == op) {
     return true;
@@ -178,28 +178,28 @@ bool FormRSCTL::hasOper(Oper op) const
   }
 }
 
-void FormRSCTL::encodeEntities(const SymRS *srs)
+void FormRSCTLK::encodeEntities(const SymRS *srs)
 {
-  if (RSCTL_COND_1ARG(oper)) {
+  if (RSCTLK_COND_1ARG(oper)) {
     arg[0]->encodeEntities(srs);
   }
-  else if (RSCTL_COND_2ARG(oper)) {
+  else if (RSCTLK_COND_2ARG(oper)) {
     arg[0]->encodeEntities(srs);
     arg[1]->encodeEntities(srs);
   }
-  else if (oper == RSCTL_PV) {
+  else if (oper == RSCTLK_PV) {
     bdd = new BDD(srs->encEntity(proc_name, entity_name));
   }
 }
 
-bool FormRSCTL::isERSCTL(void) const
+bool FormRSCTLK::isERSCTLK(void) const
 {
-  if (oper == RSCTL_PV) {
+  if (oper == RSCTLK_PV) {
     return true;
   }
 
-  if (oper == RSCTL_NOT) {
-    if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF) {
+  if (oper == RSCTLK_NOT) {
+    if (arg[0]->getOper() == RSCTLK_PV || arg[0]->getOper() == RSCTLK_TF) {
       return true;
     }
     else {
@@ -207,16 +207,16 @@ bool FormRSCTL::isERSCTL(void) const
     }
   }
 
-  if (RSCTL_COND_IS_UNIVERSAL(oper)) {
+  if (RSCTLK_COND_IS_UNIVERSAL(oper)) {
     return false;
   }
 
-  if (RSCTL_COND_1ARG(oper)) {
-    return arg[0]->isERSCTL();
+  if (RSCTLK_COND_1ARG(oper)) {
+    return arg[0]->isERSCTLK();
   }
 
-  if (RSCTL_COND_2ARG(oper)) {
-    return arg[0]->isERSCTL() && arg[1]->isERSCTL();
+  if (RSCTLK_COND_2ARG(oper)) {
+    return arg[0]->isERSCTLK() && arg[1]->isERSCTLK();
   }
 
   assert(0);
@@ -224,7 +224,7 @@ bool FormRSCTL::isERSCTL(void) const
   return false;
 }
 
-std::string FormRSCTL::getActionsStr(void) const
+std::string FormRSCTLK::getActionsStr(void) const
 {
   // if (actions != nullptr) {
   //   std::string r = "[ ";
@@ -267,9 +267,9 @@ std::string FormRSCTL::getActionsStr(void) const
   }
 }
 
-void FormRSCTL::encodeActions(const SymRS *srs)
+void FormRSCTLK::encodeActions(const SymRS *srs)
 {
-  if (RSCTL_COND_ACT(oper)) {
+  if (RSCTLK_COND_ACT(oper)) {
     if (actions_bdd != nullptr) {
       forgetActionsBDD();
     }
@@ -300,11 +300,11 @@ void FormRSCTL::encodeActions(const SymRS *srs)
     }
   }
 
-  if (RSCTL_COND_1ARG(oper)) {
+  if (RSCTLK_COND_1ARG(oper)) {
     arg[0]->encodeActions(srs);
   }
 
-  if (RSCTL_COND_2ARG(oper)) {
+  if (RSCTLK_COND_2ARG(oper)) {
     arg[0]->encodeActions(srs);
     arg[1]->encodeActions(srs);
   }
diff --git a/formrsctl.hh b/formrsctlk.hh
similarity index 67%
rename from formrsctl.hh
rename to formrsctlk.hh
index 58b2feb..008e5a1 100644
--- a/formrsctl.hh
+++ b/formrsctlk.hh
@@ -6,8 +6,8 @@
     without the author's permission is strictly prohibited.
 */
 
-#ifndef RS_FORMRSCTL_HH
-#define RS_FORMRSCTL_HH
+#ifndef RS_FORMRSCTLK_HH
+#define RS_FORMRSCTLK_HH
 
 #include <iostream>
 #include <string>
@@ -16,32 +16,32 @@
 #include "symrs.hh"
 #include "cudd.hh"
 
-#define RSCTL_PV      0 // propositional variable
-#define RSCTL_AND     1
-#define RSCTL_OR      2
-#define RSCTL_XOR  3
-#define RSCTL_NOT     4
-#define RSCTL_IMPL    5
-#define RSCTL_EG      11 // Existential...
-#define RSCTL_EU      12
-#define RSCTL_EX      13
-#define RSCTL_EF      14
-#define RSCTL_AG      21 // Universal...
-#define RSCTL_AU      22
-#define RSCTL_AX      23
-#define RSCTL_AF      24
-#define RSCTL_EG_ACT  31 // Existential...
-#define RSCTL_EU_ACT  32
-#define RSCTL_EX_ACT  33
-#define RSCTL_EF_ACT  34
-#define RSCTL_AG_ACT  41 // Universal...
-#define RSCTL_AU_ACT  42
-#define RSCTL_AX_ACT  43
-#define RSCTL_AF_ACT  44
-#define RSCTL_TF      50 // true/false
+#define RSCTLK_PV      0 // propositional variable
+#define RSCTLK_AND     1
+#define RSCTLK_OR      2
+#define RSCTLK_XOR  3
+#define RSCTLK_NOT     4
+#define RSCTLK_IMPL    5
+#define RSCTLK_EG      11 // Existential...
+#define RSCTLK_EU      12
+#define RSCTLK_EX      13
+#define RSCTLK_EF      14
+#define RSCTLK_AG      21 // Universal...
+#define RSCTLK_AU      22
+#define RSCTLK_AX      23
+#define RSCTLK_AF      24
+#define RSCTLK_EG_ACT  31 // Existential...
+#define RSCTLK_EU_ACT  32
+#define RSCTLK_EX_ACT  33
+#define RSCTLK_EF_ACT  34
+#define RSCTLK_AG_ACT  41 // Universal...
+#define RSCTLK_AU_ACT  42
+#define RSCTLK_AX_ACT  43
+#define RSCTLK_AF_ACT  44
+#define RSCTLK_TF      50 // true/false
 
-#define RSCTL_UK      60 // Epistemic operators
-#define RSCTL_NK      61
+#define RSCTLK_UK      60 // Epistemic operators
+#define RSCTLK_NK      61
 
 /* For Boolean contexts: */
 #define BCTX_PV   80
@@ -52,12 +52,12 @@
 #define BCTX_TF   90
 
 
-#define RSCTL_COND_1ARG(a) ((a) == RSCTL_NOT || (a) == RSCTL_EG || (a) == RSCTL_EF || (a) == RSCTL_EX || (a) == RSCTL_AG || (a) == RSCTL_AF || (a) == RSCTL_AX || (a) == RSCTL_EG_ACT || (a) == RSCTL_EF_ACT || (a) == RSCTL_EX_ACT || (a) == RSCTL_AG_ACT || (a) == RSCTL_AF_ACT || (a) == RSCTL_AX_ACT || (a) == RSCTL_UK || (a) == RSCTL_NK)
-#define RSCTL_COND_2ARG(a) ((a) == RSCTL_AND || (a) == RSCTL_OR || (a) == RSCTL_XOR || (a) == RSCTL_IMPL || (a) == RSCTL_EU || (a) == RSCTL_AU || (a) == RSCTL_EU_ACT || (a) == RSCTL_AU_ACT)
-#define RSCTL_COND_ACT(a) ((a) > 30 && (a) < 45)
-#define RSCTL_IS_VALID(a) (RSCTL_COND_1ARG(a) || RSCTL_COND_2ARG(a) || (a) == RSCTL_PV || (a) == RSCTL_TF)
+#define RSCTLK_COND_1ARG(a) ((a) == RSCTLK_NOT || (a) == RSCTLK_EG || (a) == RSCTLK_EF || (a) == RSCTLK_EX || (a) == RSCTLK_AG || (a) == RSCTLK_AF || (a) == RSCTLK_AX || (a) == RSCTLK_EG_ACT || (a) == RSCTLK_EF_ACT || (a) == RSCTLK_EX_ACT || (a) == RSCTLK_AG_ACT || (a) == RSCTLK_AF_ACT || (a) == RSCTLK_AX_ACT || (a) == RSCTLK_UK || (a) == RSCTLK_NK)
+#define RSCTLK_COND_2ARG(a) ((a) == RSCTLK_AND || (a) == RSCTLK_OR || (a) == RSCTLK_XOR || (a) == RSCTLK_IMPL || (a) == RSCTLK_EU || (a) == RSCTLK_AU || (a) == RSCTLK_EU_ACT || (a) == RSCTLK_AU_ACT)
+#define RSCTLK_COND_ACT(a) ((a) > 30 && (a) < 45)
+#define RSCTLK_IS_VALID(a) (RSCTLK_COND_1ARG(a) || RSCTLK_COND_2ARG(a) || (a) == RSCTLK_PV || (a) == RSCTLK_TF)
 
-#define RSCTL_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45))
+#define RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45))
 
 #define BCTX_COND_1ARG(a) ((a) == BCTX_NOT)
 #define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR)
@@ -155,10 +155,10 @@ class BoolContexts
     }
 };
 
-class FormRSCTL
+class FormRSCTLK
 {
     Oper oper;
-    FormRSCTL *arg[2];
+    FormRSCTLK *arg[2];
     std::string entity_name;
     std::string proc_name;
     bool tf;
@@ -174,9 +174,9 @@ class FormRSCTL
      * @param   varName variable name used mostly for printing the variable.
      * @param   varBDD  the BDD describing the set where the variable holds.
      */
-    FormRSCTL(std::string procName, std::string varName)
+    FormRSCTLK(std::string procName, std::string varName)
     {
-      oper = RSCTL_PV;
+      oper = RSCTLK_PV;
       proc_name = procName;
       entity_name = varName;
       arg[0] = nullptr;
@@ -192,9 +192,9 @@ class FormRSCTL
      *
      * @param   val value of the logical constant
      */
-    FormRSCTL(bool val)
+    FormRSCTLK(bool val)
     {
-      oper = RSCTL_TF;
+      oper = RSCTLK_TF;
       tf = val;
       arg[0] = nullptr;
       arg[1] = nullptr;
@@ -207,10 +207,10 @@ class FormRSCTL
     /**
      * @brief Constructor for two-argument formula.
      */
-    FormRSCTL(Oper op, FormRSCTL *form1, FormRSCTL *form2)
+    FormRSCTLK(Oper op, FormRSCTLK *form1, FormRSCTLK *form2)
     {
-      assert(RSCTL_COND_2ARG(op));
-      assert(!RSCTL_COND_ACT(op));
+      assert(RSCTLK_COND_2ARG(op));
+      assert(!RSCTLK_COND_ACT(op));
       oper = op;
       arg[0] = form1;
       arg[1] = form2;
@@ -223,11 +223,11 @@ class FormRSCTL
     /**
      * @brief Constructor for two-argument formula with action restrictions.
      */
-    // FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2)
+    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1, FormRSCTLK *form2)
     // {
     //   assert(acts != nullptr);
-    //   assert(RSCTL_COND_2ARG(op));
-    //   assert(RSCTL_COND_ACT(op));
+    //   assert(RSCTLK_COND_2ARG(op));
+    //   assert(RSCTLK_COND_ACT(op));
     //   oper = op;
     //   arg[0] = form1;
     //   arg[1] = form2;
@@ -240,11 +240,11 @@ class FormRSCTL
     /**
      * @brief Constructor for two-argument formula with Boolean context restrictions.
      */
-    FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2)
+    FormRSCTLK(Oper op, BoolContexts *bctx, FormRSCTLK *form1, FormRSCTLK *form2)
     {
       assert(bctx != nullptr);
-      assert(RSCTL_COND_2ARG(op));
-      assert(RSCTL_COND_ACT(op));
+      assert(RSCTLK_COND_2ARG(op));
+      assert(RSCTLK_COND_ACT(op));
       oper = op;
       arg[0] = form1;
       arg[1] = form2;
@@ -257,10 +257,10 @@ class FormRSCTL
     /**
      * @brief Constructor for one-argument formula.
      */
-    FormRSCTL(Oper op, FormRSCTL *form1)
+    FormRSCTLK(Oper op, FormRSCTLK *form1)
     {
-      assert(RSCTL_COND_1ARG(op));
-      assert(!RSCTL_COND_ACT(op));
+      assert(RSCTLK_COND_1ARG(op));
+      assert(!RSCTLK_COND_ACT(op));
       oper = op;
       arg[0] = form1;
       arg[1] = nullptr;
@@ -273,11 +273,11 @@ class FormRSCTL
     /**
      * @brief Constructor for one-argument formula with action restrictions.
      */
-    // FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1)
+    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1)
     // {
     //   assert(acts != nullptr);
-    //   assert(RSCTL_COND_1ARG(op));
-    //   assert(RSCTL_COND_ACT(op));
+    //   assert(RSCTLK_COND_1ARG(op));
+    //   assert(RSCTLK_COND_ACT(op));
     //   oper = op;
     //   arg[0] = form1;
     //   arg[1] = nullptr;
@@ -290,11 +290,11 @@ class FormRSCTL
     /**
      * @brief Constructor for one-argument formula with Boolean context restrictions.
      */
-    FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1)
+    FormRSCTLK(Oper op, BoolContexts *bctx, FormRSCTLK *form1)
     {
       assert(bctx != nullptr);
-      assert(RSCTL_COND_1ARG(op));
-      assert(RSCTL_COND_ACT(op));
+      assert(RSCTLK_COND_1ARG(op));
+      assert(RSCTLK_COND_ACT(op));
       oper = op;
       arg[0] = form1;
       arg[1] = nullptr;
@@ -304,9 +304,9 @@ class FormRSCTL
       boolCtx = bctx;
     }
 
-    FormRSCTL(Oper op, Agents_f agents_set, FormRSCTL *form1)
+    FormRSCTLK(Oper op, Agents_f agents_set, FormRSCTLK *form1)
     {
-      assert(RSCTL_COND_1ARG(op));
+      assert(RSCTLK_COND_1ARG(op));
       oper = op;
       arg[0] = form1;
       arg[1] = nullptr;
@@ -318,7 +318,7 @@ class FormRSCTL
     /**
      * @brief Destructor.
      */
-    ~FormRSCTL()
+    ~FormRSCTLK()
     {
       delete arg[0];
       delete arg[1];
@@ -331,36 +331,36 @@ class FormRSCTL
     bool hasOper(Oper op) const;
     const BDD *getBDD(void) const
     {
-      assert(oper == RSCTL_PV);
+      assert(oper == RSCTLK_PV);
       assert(bdd != nullptr);
       return bdd;
     }
     const BDD *getActionsBDD(void) const
     {
-      assert(RSCTL_COND_ACT(oper));
+      assert(RSCTLK_COND_ACT(oper));
       assert(actions_bdd != nullptr);
       return actions_bdd;
     }
     Oper getOper(void) const
     {
-      assert(RSCTL_IS_VALID(oper));
+      assert(RSCTLK_IS_VALID(oper));
       return oper;
     }
-    FormRSCTL *getLeftSF(void) const
+    FormRSCTLK *getLeftSF(void) const
     {
       assert(arg[0] != nullptr);
       return arg[0];
     }
-    FormRSCTL *getRightSF(void) const
+    FormRSCTLK *getRightSF(void) const
     {
-      assert(RSCTL_COND_2ARG(oper));
+      assert(RSCTLK_COND_2ARG(oper));
       assert(arg[1] != nullptr);
       return arg[1];
     }
     std::string getActionsStr(void) const;
     bool getTF(void) const
     {
-      assert(oper == RSCTL_TF);
+      assert(oper == RSCTLK_TF);
       return tf;
     }
     void encodeEntities(const SymRS *srs);
@@ -371,7 +371,7 @@ class FormRSCTL
         delete actions_bdd;
       }
     }
-    bool isERSCTL(void) const;
+    bool isERSCTLK(void) const;
 };
 
 #endif
diff --git a/main.cc b/main.cc
index bba2658..85d3f71 100644
--- a/main.cc
+++ b/main.cc
@@ -182,10 +182,10 @@ int main(int argc, char **argv)
     if (rstl_model_checking) {
       if (bmc) {
         cout << "Using BDD-based Bounded Model Checking" << endl;
-        mc.checkRSCTL(driver.getFormRSCTL());
+        mc.checkRSCTLK(driver.getFormRSCTLK());
       }
       else {
-        mc.checkRSCTLfull(driver.getFormRSCTL());
+        mc.checkRSCTLKfull(driver.getFormRSCTLK());
       }
     }
   }
@@ -233,7 +233,7 @@ void print_help(std::string path_str)
 #endif
        << " Usage: " << path_str << " [options] <inputfile>" << endl << endl
        << " TASKS:" << endl
-       << "  -c   -- perform RSCTL model checking" << endl
+       << "  -c   -- perform RSCTLK model checking" << endl
        //<< " -f K -- generate SMT input for the depth K" << endl
        << "  -P   -- print parsed system" << endl
        << "  -r   -- print reactions" << endl
diff --git a/mc.cc b/mc.cc
index d6da428..0ad65f6 100644
--- a/mc.cc
+++ b/mc.cc
@@ -233,15 +233,15 @@ bool ModelChecker::checkReach(const Entities testState)
   return false;
 }
 
-BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
+BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
 {
   assert(reach != nullptr);
   Oper oper = form->getOper();
 
-  if (oper == RSCTL_PV) {
+  if (oper == RSCTLK_PV) {
     return *form->getBDD() * *reach;
   }
-  else if (oper == RSCTL_TF) {
+  else if (oper == RSCTLK_TF) {
     if (form->getTF() == true) {
       return *reach;
     }
@@ -249,47 +249,47 @@ BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
       return cuddMgr->bddZero();
     }
   }
-  else if (oper == RSCTL_AND) {
-    return getStatesRSCTL(form->getLeftSF()) * getStatesRSCTL(form->getRightSF());
+  else if (oper == RSCTLK_AND) {
+    return getStatesRSCTLK(form->getLeftSF()) * getStatesRSCTLK(form->getRightSF());
   }
-  else if (oper == RSCTL_OR) {
-    return getStatesRSCTL(form->getLeftSF()) + getStatesRSCTL(form->getRightSF());
+  else if (oper == RSCTLK_OR) {
+    return getStatesRSCTLK(form->getLeftSF()) + getStatesRSCTLK(form->getRightSF());
   }
-  else if (oper == RSCTL_XOR) {
-    return getStatesRSCTL(form->getLeftSF()) ^ getStatesRSCTL(form->getRightSF());
+  else if (oper == RSCTLK_XOR) {
+    return getStatesRSCTLK(form->getLeftSF()) ^ getStatesRSCTLK(form->getRightSF());
   }
-  else if (oper == RSCTL_IMPL) {
-    return (!getStatesRSCTL(form->getLeftSF()) * *reach) + getStatesRSCTL(
+  else if (oper == RSCTLK_IMPL) {
+    return (!getStatesRSCTLK(form->getLeftSF()) * *reach) + getStatesRSCTLK(
              form->getRightSF());
   }
-  else if (oper == RSCTL_NOT) {
-    return !getStatesRSCTL(form->getLeftSF()) * *reach;
+  else if (oper == RSCTLK_NOT) {
+    return !getStatesRSCTLK(form->getLeftSF()) * *reach;
   }
-  else if (oper == RSCTL_EX) {
-    return getPreE(getStatesRSCTL(form->getLeftSF())) * *reach;
+  else if (oper == RSCTLK_EX) {
+    return getPreE(getStatesRSCTLK(form->getLeftSF())) * *reach;
   }
-  else if (oper == RSCTL_EG) {
-    return statesEG(getStatesRSCTL(form->getLeftSF()));
+  else if (oper == RSCTLK_EG) {
+    return statesEG(getStatesRSCTLK(form->getLeftSF()));
   }
-  else if (oper == RSCTL_EU) {
+  else if (oper == RSCTLK_EU) {
     return statesEU(
-             getStatesRSCTL(form->getLeftSF()),
-             getStatesRSCTL(form->getRightSF())
+             getStatesRSCTLK(form->getLeftSF()),
+             getStatesRSCTLK(form->getRightSF())
            );
   }
-  else if (oper == RSCTL_EF) {
-    return statesEF(getStatesRSCTL(form->getLeftSF()));
+  else if (oper == RSCTLK_EF) {
+    return statesEF(getStatesRSCTLK(form->getLeftSF()));
   }
-  else if (oper == RSCTL_AX) {
-    return !getPreE(!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
+  else if (oper == RSCTLK_AX) {
+    return !getPreE(!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
   }
-  else if (oper == RSCTL_AG) {
+  else if (oper == RSCTLK_AG) {
     return !statesEF(
-             !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
+             !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
   }
-  else if (oper == RSCTL_AU) {
-    BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach;
-    BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach;
+  else if (oper == RSCTLK_AU) {
+    BDD ng = !getStatesRSCTLK(form->getRightSF()) * *reach;
+    BDD nf = !getStatesRSCTLK(form->getLeftSF()) * *reach;
 
     BDD x = !statesEU(ng, ng * nf) * *reach;
 
@@ -299,40 +299,40 @@ BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
 
     return x;
   }
-  else if (oper == RSCTL_AF) {
+  else if (oper == RSCTLK_AF) {
     return !statesEG(
-             !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
+             !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
   }
   /***** CONTEXT RESTRICTIONS: ******/
-  else if (oper == RSCTL_EX_ACT) {
-    return getPreEctx(getStatesRSCTL(form->getLeftSF()),
+  else if (oper == RSCTLK_EX_ACT) {
+    return getPreEctx(getStatesRSCTLK(form->getLeftSF()),
                       form->getActionsBDD()) * *reach;
   }
-  else if (oper == RSCTL_EG_ACT) {
+  else if (oper == RSCTLK_EG_ACT) {
     return statesEGctx(form->getActionsBDD(),
-                       getStatesRSCTL(form->getLeftSF())); /***** EG? *****/
+                       getStatesRSCTLK(form->getLeftSF())); /***** EG? *****/
   }
-  else if (oper == RSCTL_EU_ACT) {
+  else if (oper == RSCTLK_EU_ACT) {
     return statesEUctx(
              form->getActionsBDD(),
-             getStatesRSCTL(form->getLeftSF()),
-             getStatesRSCTL(form->getRightSF())
+             getStatesRSCTLK(form->getLeftSF()),
+             getStatesRSCTLK(form->getRightSF())
            );
   }
-  else if (oper == RSCTL_EF_ACT) {
-    return statesEFctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF()));
+  else if (oper == RSCTLK_EF_ACT) {
+    return statesEFctx(form->getActionsBDD(), getStatesRSCTLK(form->getLeftSF()));
   }
-  else if (oper == RSCTL_AX_ACT) {
-    return !getPreEctx(!getStatesRSCTL(form->getLeftSF()) * *reach,
+  else if (oper == RSCTLK_AX_ACT) {
+    return !getPreEctx(!getStatesRSCTLK(form->getLeftSF()) * *reach,
                        form->getActionsBDD()) * *reach;
   }
-  else if (oper == RSCTL_AG_ACT) {
+  else if (oper == RSCTLK_AG_ACT) {
     return !statesEFctx(form->getActionsBDD(),
-                        !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
+                        !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
   }
-  else if (oper == RSCTL_AU_ACT) {
-    BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach;
-    BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach;
+  else if (oper == RSCTLK_AU_ACT) {
+    BDD ng = !getStatesRSCTLK(form->getRightSF()) * *reach;
+    BDD nf = !getStatesRSCTLK(form->getLeftSF()) * *reach;
 
     BDD x = !statesEUctx(form->getActionsBDD(), ng, ng * nf) * *reach;
 
@@ -342,9 +342,9 @@ BDD ModelChecker::getStatesRSCTL(const FormRSCTL *form)
 
     return x;
   }
-  else if (oper == RSCTL_AF_ACT) {
+  else if (oper == RSCTLK_AF_ACT) {
     return !statesEGctx(form->getActionsBDD(),
-                        !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
+                        !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
   }
 
   assert(0); // Should never happen
@@ -454,17 +454,17 @@ BDD ModelChecker::getIthOnly(Process proc_id)
   return bdd;
 }
 
-bool ModelChecker::checkRSCTL(FormRSCTL *form)
+bool ModelChecker::checkRSCTLK(FormRSCTLK *form)
 {
-  if (form->isERSCTL()) {
-    return checkRSCTLbmc(form);
+  if (form->isERSCTLK()) {
+    return checkRSCTLKbmc(form);
   }
   else {
-    return checkRSCTLfull(form);
+    return checkRSCTLKfull(form);
   }
 }
 
-bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
+bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form)
 {
   if (opts->measure) {
     opts->ver_time = cpuTime();
@@ -474,7 +474,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
 
   bool result = false;
 
-  VERB("Model checking for RSCTL formula: " << form->toStr());
+  VERB("Model checking for RSCTLK formula: " << form->toStr());
 
   VERB("Processing the formula: encoding entities");
   form->encodeEntities(srs);
@@ -514,8 +514,8 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
 
   VERB("Checking the formula");
 
-  //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero())
-  if (*initStates * getStatesRSCTL(form) == *initStates) {
+  //if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
+  if (*initStates * getStatesRSCTLK(form) == *initStates) {
     result = true;
   }
   else {
@@ -535,7 +535,7 @@ bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
   return result;
 }
 
-bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
+bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
 {
   if (opts->measure) {
     opts->ver_time = cpuTime();
@@ -543,14 +543,14 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
 
   assert(form != nullptr);
 
-  if (!form->isERSCTL()) {
+  if (!form->isERSCTLK()) {
     FERROR("Formula " << form->toStr() <<
-           " is not syntactically an ERSCTL formula");
+           " is not syntactically an ERSCTLK formula");
   }
 
   bool result = false;
 
-  VERB("Bounded model checking for RSCTL formula: " << form->toStr());
+  VERB("Bounded model checking for RSCTLK formula: " << form->toStr());
 
   VERB("Processing the formula: encoding entities");
   form->encodeEntities(srs);
@@ -572,8 +572,8 @@ bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
       cout << "\rIteration " << ++k << flush;
     }
 
-    //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero())
-    if (*initStates * getStatesRSCTL(form) == *initStates) {
+    //if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
+    if (*initStates * getStatesRSCTLK(form) == *initStates) {
       result = true;
       break;
     }
@@ -605,4 +605,4 @@ void ModelChecker::cleanup(void)
   reach = nullptr;
 }
 
-/** EOF **/
\ No newline at end of file
+/** EOF **/
diff --git a/mc.hh b/mc.hh
index 12497d9..9685c47 100644
--- a/mc.hh
+++ b/mc.hh
@@ -4,7 +4,7 @@
 #include "cudd.hh"
 #include "rs.hh"
 #include "symrs.hh"
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
 #include "macro.hh"
 #include "bdd_macro.hh"
 #include "options.hh"
@@ -53,7 +53,7 @@ class ModelChecker
     BDD getSucc(const BDD &states);
     BDD getPreE(const BDD &states);
     BDD getPreEctx(const BDD &states, const BDD *contexts);
-    BDD getStatesRSCTL(const FormRSCTL *form);
+    BDD getStatesRSCTLK(const FormRSCTLK *form);
     BDD statesEG(const BDD &states);
     BDD statesEU(const BDD &statesA, const BDD &statesB);
     BDD statesEF(const BDD &states);
@@ -71,9 +71,9 @@ class ModelChecker
     void printReach(void);
     void printReachWithSucc(void);
     bool checkReach(const Entities testState);
-    bool checkRSCTL(FormRSCTL *form);
-    bool checkRSCTLfull(FormRSCTL *form);
-    bool checkRSCTLbmc(FormRSCTL *form);
+    bool checkRSCTLK(FormRSCTLK *form);
+    bool checkRSCTLKfull(FormRSCTLK *form);
+    bool checkRSCTLKbmc(FormRSCTLK *form);
 };
 
 #endif
diff --git a/rs.hh b/rs.hh
index 39a89cb..1ac89b2 100644
--- a/rs.hh
+++ b/rs.hh
@@ -137,4 +137,4 @@ class RctSys
 
 #endif
 
-/** EOF **/
\ No newline at end of file
+/** EOF **/
diff --git a/rsin_driver.cc b/rsin_driver.cc
index ddc5352..5e6ccf5 100644
--- a/rsin_driver.cc
+++ b/rsin_driver.cc
@@ -17,7 +17,7 @@ rsin_driver::rsin_driver(RctSys *rs)
 void rsin_driver::initialise(void)
 {
   rs = nullptr;
-  rsctlform = nullptr;
+  rsctlkform = nullptr;
   opts = nullptr;
   use_ctx_aut = false;
   use_concentrations = false;
@@ -49,13 +49,13 @@ void rsin_driver::error(const std::string &m)
   std::cerr << m << std::endl;
 }
 
-FormRSCTL *rsin_driver::getFormRSCTL(void)
+FormRSCTLK *rsin_driver::getFormRSCTLK(void)
 {
-  if (rsctlform == nullptr) {
-    FERROR("RSCTL formula was not supplied!");
+  if (rsctlkform == nullptr) {
+    FERROR("RSCTLK formula was not supplied!");
   }
 
-  return rsctlform;
+  return rsctlkform;
 }
 
 //
diff --git a/rsin_driver.hh b/rsin_driver.hh
index 04a8aa2..5570960 100644
--- a/rsin_driver.hh
+++ b/rsin_driver.hh
@@ -4,7 +4,7 @@
 #include <map>
 #include "rsin_parser.hh"
 #include "rs.hh"
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
 #include "options.hh"
 
 // Tell Flex the lexer's prototype ...
@@ -25,7 +25,7 @@ class rsin_driver
     virtual ~rsin_driver();
 
     //std::map<std::string, int> variables;
-    FormRSCTL *rsctlform;
+    FormRSCTLK *rsctlkform;
     Options *opts;
 
     // options in configuration file:
@@ -45,11 +45,11 @@ class rsin_driver
     {
       this->opts = opts;
     };
-    void addFormRSCTL(FormRSCTL *f)
+    void addFormRSCTLK(FormRSCTLK *f)
     {
-      rsctlform = f;
+      rsctlkform = f;
     };
-    FormRSCTL *getFormRSCTL(void);
+    FormRSCTLK *getFormRSCTLK(void);
 
     void ensureOptionsAllowed(void);
     void useContextAutomaton(void);
diff --git a/rsin_parser.ll b/rsin_parser.ll
index 1abe2fc..a946223 100644
--- a/rsin_parser.ll
+++ b/rsin_parser.ll
@@ -48,7 +48,7 @@ blank [ \t]
 "transitions"			      return token::TRANSITIONS;
 "states"				        return token::STATES;
 "init-state"			      return token::INITSTATE;
-"rsctl-property"        return token::RSCTLFORM;
+"rsctlk-property"        return token::RSCTLKFORM;
 "{"                     return token::LCB;
 "}"                     return token::RCB;
 "("                     return token::LRB;
diff --git a/rsin_parser.yy b/rsin_parser.yy
index f308f65..827eda5 100644
--- a/rsin_parser.yy
+++ b/rsin_parser.yy
@@ -6,7 +6,7 @@
 %code requires {
 #include <string>
 #include <set>
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
 
 using std::set;
 using std::string;
@@ -33,7 +33,7 @@ class rsin_driver;
 {
     int ival;
     std::string *sval;
-    FormRSCTL *frsctl;
+    FormRSCTLK *frsctlk;
     // Entity_f *ent;
     // Action_f *act;
     // ActionsVec_f *actionsVec;
@@ -45,7 +45,7 @@ class rsin_driver;
 }
 
 %token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS
-%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM
+%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLKFORM
 %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
 %token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL DOT COMMA RARR
 %token AND OR XOR IMPLIES NOT
@@ -60,7 +60,7 @@ class rsin_driver;
 
 //%right SRB
 
-%type <frsctl> rsctl_form
+%type <frsctlk> rsctlk_form
 // %type <ent> f_entity
 // %type <act> action
 // %type <actionsVec> actions
@@ -81,8 +81,8 @@ system:
     | INITIALCONTEXTS LCB initstates RCB system
     | CONTEXTENTITIES LCB actionentities RCB system
 	| CONTEXTAUTOMATON LCB ctxaut RCB system
-    | RSCTLFORM LCB rsctl_form RCB system {
-        driver.addFormRSCTL($3);
+    | RSCTLKFORM LCB rsctlk_form RCB system {
+        driver.addFormRSCTLK($3);
     }
     ;
 
@@ -316,110 +316,110 @@ bool_contexts: IDENTIFIER DOT IDENTIFIER {
 //     }
 //     ;
 
-rsctl_form: 
+rsctlk_form: 
     IDENTIFIER DOT IDENTIFIER {
-        $$ = new FormRSCTL(*$1, *$3);
+        $$ = new FormRSCTLK(*$1, *$3);
         free($1);
         free($3);
     }
-    | NOT rsctl_form {
-        $$ = new FormRSCTL(RSCTL_NOT, $2);
+    | NOT rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_NOT, $2);
     }
-    | LRB rsctl_form RRB {
+    | LRB rsctlk_form RRB {
         $$ = $2;
     }
-    | rsctl_form AND rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AND, $1, $3);
+    | rsctlk_form AND rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AND, $1, $3);
     }
-    | rsctl_form OR rsctl_form {
-        $$ = new FormRSCTL(RSCTL_OR, $1, $3);
+    | rsctlk_form OR rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_OR, $1, $3);
     }
-    | rsctl_form XOR rsctl_form {
-        $$ = new FormRSCTL(RSCTL_XOR, $1, $3);
+    | rsctlk_form XOR rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_XOR, $1, $3);
     }
-    | rsctl_form IMPLIES rsctl_form {
-        $$ = new FormRSCTL(RSCTL_IMPL, $1, $3);
+    | rsctlk_form IMPLIES rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_IMPL, $1, $3);
     }
-    | EX rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EX, $2);
+    | EX rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EX, $2);
     }
-    | EU LRB rsctl_form COMMA rsctl_form RRB {
-        $$ = new FormRSCTL(RSCTL_EU, $3, $5);
+    | EU LRB rsctlk_form COMMA rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_EU, $3, $5);
     }
-    | EF rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EF, $2);
+    | EF rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EF, $2);
     }
-    | EG rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EG, $2);
+    | EG rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EG, $2);
     }
-    | AX rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AX, $2);
+    | AX rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AX, $2);
     }
-    | AU LRB rsctl_form COMMA rsctl_form RRB {
-        $$ = new FormRSCTL(RSCTL_AU, $3, $5);
+    | AU LRB rsctlk_form COMMA rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_AU, $3, $5);
     }
-    | AF rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AF, $2);
+    | AF rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AF, $2);
     }
-    | AG rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AG, $2);
+    | AG rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AG, $2);
     } 
-    | UK LSB IDENTIFIER RSB LRB rsctl_form RRB {
+    | UK LSB IDENTIFIER RSB LRB rsctlk_form RRB {
         Agents_f agents;
         agents.insert(*$3);
-        $$ = new FormRSCTL(RSCTL_UK, agents, $6);
+        $$ = new FormRSCTLK(RSCTLK_UK, agents, $6);
         free($3);
     }
 
-    // | E LSB actions RSB X rsctl_form {
-    //     $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
+    // | E LSB actions RSB X rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
     // }
-    // | E LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
-    //     $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
+    // | E LSB actions RSB U LRB rsctlk_form COMMA rsctlk_form RRB {
+    //     $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
     // }
-    // | E LSB actions RSB F rsctl_form {
-    //     $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
+    // | E LSB actions RSB F rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
     // }
-    // | E LSB actions RSB G rsctl_form {
-    //     $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
+    // | E LSB actions RSB G rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
     // }
-    // | A LSB actions RSB X rsctl_form {
-    //     $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
+    // | A LSB actions RSB X rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
     // }
-    // | A LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
-    //     $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
+    // | A LSB actions RSB U LRB rsctlk_form COMMA rsctlk_form RRB {
+    //     $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
     // }
-    // | A LSB actions RSB F rsctl_form {
-    //     $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
+    // | A LSB actions RSB F rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
     // }
-    // | A LSB actions RSB G rsctl_form {
-    //     $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
+    // | A LSB actions RSB G rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
     // }
 
 	  /* contexts as boolean formulae  */
-    | E LAB bool_contexts RAB X rsctl_form { 
-        $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
+    | E LAB bool_contexts RAB X rsctlk_form { 
+        $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB U LRB rsctl_form COMMA rsctl_form RRB {
-        $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
+    | E LAB bool_contexts RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
     }
-    | E LAB bool_contexts RAB F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
+    | E LAB bool_contexts RAB F rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
+    | E LAB bool_contexts RAB G rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
     }
-    | A LAB bool_contexts RAB X rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
+    | A LAB bool_contexts RAB X rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
     }
-    | A LAB bool_contexts RAB U LRB rsctl_form COMMA rsctl_form RRB {
-        $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
+    | A LAB bool_contexts RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
     }
-    | A LAB bool_contexts RAB F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
+    | A LAB bool_contexts RAB F rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
     }
-    | A LAB bool_contexts RAB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
+    | A LAB bool_contexts RAB G rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
     }
     ;
 %%
diff --git a/symrs.hh b/symrs.hh
index 5133420..cea2470 100644
--- a/symrs.hh
+++ b/symrs.hh
@@ -30,7 +30,7 @@ using std::map;
 class SymRS
 {
     friend class ModelChecker;
-    friend class FormRSCTL;
+    friend class FormRSCTLK;
 
   public:
     SymRS(RctSys *rs, Options *opts);