diff --git a/Makefile b/Makefile
index a75b776..4235476 100644
--- a/Makefile
+++ b/Makefile
@@ -4,21 +4,22 @@ CUDD_INCLUDE=cudd/lib/libcudd.a
 INCLUDES=-Icudd/include
 CPPFLAGS_SILENT = $(INCLUDES)
 CPPFLAGS = -Wall $(CPPFLAGS_SILENT) #-Werror
-#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG 
+#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG
 CXXFLAGS_SILENT = -O3 -g
 CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
-#CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
-LDLIBS = $(CUDD_INCLUDE) 
+CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
+CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE #-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 stateconstr.o
 
-all: main
+all: reactics
 
 cleanly:
 	rm -f *.lex.cc *.lex.o location.hh stack.hh position.hh rsin_parser.cc rsin_parser.hh
 
 clean: cleanly
-	rm -f *.o main *~ makefile.dep tags
+	rm -f *.o reactics *.orig *~ makefile.dep tags
 
 cleanall: clean
 
@@ -27,7 +28,7 @@ makefile.dep: *.cc *.hh
 
 include makefile.dep
 
-main: main.o $(OBJ)
+reactics: reactics.o $(OBJ)
 
 rsin_parser.hh: rsin_parser.cc
 
@@ -43,3 +44,8 @@ rsin_parser.lex.cc: rsin_parser.ll
 	flex rsin_parser.ll
 	mv lex.yy.c rsin_parser.lex.cc
 
+style:
+	astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh
+
+commit: style
+	git commit -a
diff --git a/bdd_macro.hh b/bdd_macro.hh
index 43136af..c39bf1e 100644
--- a/bdd_macro.hh
+++ b/bdd_macro.hh
@@ -1,11 +1,13 @@
 #ifndef __BDD_MACRO_HH__
 #define __BDD_MACRO_HH__
 
-#define BDD_IFF(p,q)	(!(p+q)+(p*q))
-#define BDD_TRUE		(cuddMgr->bddOne())
-#define BDD_FALSE		(cuddMgr->bddZero())
+#include "cudd.hh"
 
-#define BDD_PRINT(t)	((t).PrintMinterm())
+#define BDD_IFF(p,q)  (!(p+q)+(p*q))
+#define BDD_TRUE    (cuddMgr->bddOne())
+#define BDD_FALSE   (cuddMgr->bddZero())
+
+#define BDD_PRINT(t)  ((t).PrintMinterm())
 
 #endif
 
diff --git a/ctx_aut.cc b/ctx_aut.cc
index a77e21c..edc0f8a 100644
--- a/ctx_aut.cc
+++ b/ctx_aut.cc
@@ -1,108 +1,186 @@
 
 #include "ctx_aut.hh"
+#include "rs.hh"
+#include "macro.hh"
+#include "stateconstr.hh"
 
-CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys) 
-{ 
-	setOptions(opts);
-	this->parent_rctsys = parent_rctsys;
+CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys)
+{
+  setOptions(opts);
+  this->parent_rctsys = parent_rctsys;
+  made_progressive = false;
 }
 
 bool CtxAut::hasState(std::string name)
 {
-    if (states_names.find(name) == states_names.end())
-        return false;
-    else
-        return true;
+  if (states_names.find(name) == states_names.end()) {
+    return false;
+  }
+  else {
+    return true;
+  }
 }
 
 State CtxAut::getStateID(std::string name)
 {
-    if (!hasState(name))
-    {
-        FERROR("No such state: " << name);
-    }
-    return states_names[name];
+  if (!hasState(name)) {
+    FERROR("No such state: " << name);
+  }
+
+  return states_names[name];
 }
 
 std::string CtxAut::getStateName(State state_id)
 {
-	assert(state_id < states_ids.size());
-	return states_ids[state_id];
+  assert(state_id < states_ids.size());
+  return states_ids[state_id];
 }
 
 void CtxAut::addState(std::string name)
 {
-    if (!hasState(name))
-    {
-        State new_state_id = states_ids.size();
+  if (!hasState(name)) {
+    State new_state_id = states_ids.size();
 
-        VERB_L2("Adding state: " << name << " index=" << new_state_id);
+    VERB_L2("Adding state: " << name << " index=" << new_state_id);
 
-        states_ids.push_back(name);
-        states_names[name] = new_state_id;
-		
-		if (!init_state_defined)
-		{
-			setInitState(name);
-		}
+    states_ids.push_back(name);
+    states_names[name] = new_state_id;
+
+    if (!init_state_defined) {
+      setInitState(name);
     }
+  }
 }
 
 void CtxAut::setInitState(std::string name)
 {
-	VERB_L2("Setting initial CA state: " << name);
-	State state_id = getStateID(name);
-	VERB_L2("Got initial CA state ID: index=" << state_id);
-	init_state_id = state_id;
-	init_state_defined = true;
+  VERB_L2("Setting initial CA state: " << name);
+  State state_id = getStateID(name);
+  VERB_L2("Got initial CA state ID: index=" << state_id);
+  init_state_id = state_id;
+  init_state_defined = true;
 }
 
 State CtxAut::getInitState(void)
 {
-	assert(init_state_defined);
-	return init_state_id;
+  assert(init_state_defined);
+  return init_state_id;
 }
 
 void CtxAut::printAutomaton(void)
 {
-	showStates();
-	showTransitions();
+  showStates();
+  showTransitions();
 }
 
 void CtxAut::showStates(void)
 {
-	cout << "# Context Automaton States:" << endl;
-	cout << " = Init state: " << getStateName(init_state_id) << endl;
-	for (const auto &s : states_ids)
-		cout << " * " << s << endl;
+  cout << "# Context Automaton States:" << endl;
+  cout << " = Init state: " << getStateName(init_state_id) << endl;
+
+  for (const auto &s : states_ids) {
+    cout << " * " << s << endl;
+  }
 }
 
-void CtxAut::pushContextEntity(Entity entity_id) 
+void CtxAut::pushContextEntity(Entity entity_id)
 {
-	tmpEntities.insert(entity_id);
+  tmpEntities.insert(entity_id);
 }
 
-void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) 
+void CtxAut::saveCurrentContextSet(Process proc_id)
 {
-    VERB_L3("Saving transition");
-	
-	CtxAutTransition new_transition;
-	
-	new_transition.src_state = getStateID(srcStateName);
-	new_transition.ctx = tmpEntities; 
-	tmpEntities.clear();
-	new_transition.dst_state = getStateID(dstStateName);
-	transitions.push_back(new_transition);
+  if (!parent_rctsys->hasProcess(proc_id)) {
+    FERROR("No such process: ID=" << proc_id);
+  }
+
+  tmpProcEntities[proc_id] = tmpEntities;
+  tmpEntities.clear();
+}
+
+void CtxAut::addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr)
+{
+  VERB_L3("Saving transition");
+
+  CtxAutTransition new_transition;
+
+  new_transition.src_state = getStateID(srcStateName);
+  new_transition.ctx = tmpProcEntities;
+  // tmpEntities.clear();
+  tmpProcEntities.clear();
+  new_transition.state_constr = stateConstr;
+  new_transition.dst_state = getStateID(dstStateName);
+  transitions.push_back(new_transition);
 }
 
 void CtxAut::showTransitions(void)
 {
-	cout << "# Context Automaton Transitions:" << endl;
-	for (const auto &t : transitions)
-	{
-		cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(t.dst_state) 
-			 << "]: {" << parent_rctsys->entitiesToStr(t.ctx) << "}" << endl;
-	}
+  cout << "# Context Automaton Transitions:" << endl;
+
+  for (const auto &t : transitions) {
+    cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(
+           t.dst_state)
+         << "]: { " << parent_rctsys->procEntitiesToStr(t.ctx) << "}";
+
+    if (t.state_constr != nullptr) {
+      cout << " " << t.state_constr->toStr();
+    }
+
+    cout << endl;
+  }
+}
+
+void CtxAut::makeProgressive(void)
+{
+  VERB_LN(2, "Calculating progressive closure of CA");
+  assert(!made_progressive);
+
+  std::string special_loc = "T";
+
+  while (hasState(special_loc)) {
+    special_loc += "T";
+  }
+
+  addState(special_loc);
+  State special_loc_id = getLastStateID();
+
+  std::map<State, StateConstr *> constrs;
+
+  for (State s = 0; s < states_ids.size(); ++s) {
+    if (s == special_loc_id) {
+      continue;
+    }
+
+    if (constrs.count(s) == 0) {
+      constrs[s] = new StateConstr(true);
+    }
+  }
+
+  constrs[special_loc_id] = new StateConstr(true);
+
+  for (const auto &t : transitions) {
+    State curr_st = t.src_state;
+
+    if (t.state_constr != nullptr) {
+      constrs[curr_st] = new StateConstr(
+        STC_OR, constrs[curr_st], t.state_constr);
+    }
+  }
+
+  for (const auto &s : states_ids) {
+    StateConstr *state_constr = nullptr;
+
+    if (!constrs[getStateID(s)]->isTrue()) {
+      state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]);
+      addTransition(s, special_loc, state_constr);
+    }
+
+  }
+
+  addTransition(special_loc, special_loc, nullptr);
+
+  made_progressive = true;
+
 }
 
 /** EOF **/
diff --git a/ctx_aut.hh b/ctx_aut.hh
index a2e2f6f..164d4c7 100644
--- a/ctx_aut.hh
+++ b/ctx_aut.hh
@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_CTX_AUT_HH
@@ -15,45 +12,61 @@
 #include <vector>
 #include <string>
 #include <cstdlib>
-#include "rs.hh"
+// #include "rs.hh"
 #include "types.hh"
-#include "macro.hh"
-#include "options.hh"
+// #include "options.hh"
+// #include "stateconstr.hh"
 
 using std::cout;
 using std::endl;
 
 class RctSys;
+class Options;
+class StateConstr;
 
 class CtxAut
 {
     friend class SymRS;
-	
-	public:
-		CtxAut(Options *opts, RctSys *parent_rctsys);
-		bool hasState(std::string name);
-		void addState(std::string stateName);
-		void setInitState(std::string stateName);
-		State getInitState(void);
-		State getStateID(std::string name);
-		std::string getStateName(State state_id);
-		void printAutomaton(void);
-		void showStates(void);
-		void addTransition(std::string srcStateName, std::string dstStateName);
-		void showTransitions(void);
-		void pushContextEntity(Entity entity_id);	
-	    void setOptions(Options *opts) { this->opts = opts; }
-		size_t statesCount(void) { return states_ids.size(); }
-		
-	private:
-		RctSys *parent_rctsys;
-	    Options *opts;
-		StatesById states_ids;
-		StatesByName states_names;
-		State init_state_id;
-		bool init_state_defined;
-		Entities tmpEntities;
-		CtxAutTransitions transitions;
+
+  public:
+    CtxAut(Options *opts, RctSys *parent_rctsys);
+    bool hasState(std::string name);
+    void addState(std::string stateName);
+    void setInitState(std::string stateName);
+    State getInitState(void);
+    State getStateID(std::string name);
+    State getLastStateID(void)
+    {
+      return states_ids.size();
+    }
+    std::string getStateName(State state_id);
+    void printAutomaton(void);
+    void showStates(void);
+    void addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr);
+    void showTransitions(void);
+    void makeProgressive(void);
+    void pushContextEntity(Entity entity_id);
+    void saveCurrentContextSet(Process proc_id);
+    void setOptions(Options *opts)
+    {
+      this->opts = opts;
+    }
+    size_t statesCount(void)
+    {
+      return states_ids.size();
+    }
+
+  private:
+    RctSys *parent_rctsys;
+    Options *opts;
+    StatesById states_ids;
+    StatesByName states_names;
+    State init_state_id;
+    bool init_state_defined;
+    EntitiesForProc tmpProcEntities;
+    Entities tmpEntities;
+    CtxAutTransitions transitions;
+    bool made_progressive;
 };
 
 #endif /* RS_CTX_AUT_HH */
diff --git a/drs_benchmark.sh b/drs_benchmark.sh
new file mode 100755
index 0000000..b7ad43d
--- /dev/null
+++ b/drs_benchmark.sh
@@ -0,0 +1,70 @@
+#!/bin/sh
+
+TMPINPUT="tmp_$RANDOM$RANDOM.rs"
+
+CMD="./reactics -B"
+
+timelimit="$((30*60))" # 30 minutes
+timelimit="$((5*60))" # 5 minutes
+
+form_tgc_sc="`seq 1 4`"
+form_asm="`seq 1 2`"
+
+for benchmark in "tgc_sc" "asm"; do
+
+    eval formulae=\$form_${benchmark}
+
+    for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
+
+        for f in $formulae; do
+
+            done=0
+
+            for i in `seq 2 20`;do
+
+                if [[ $done -eq 1 ]];then
+                    echo "Skipping f=$f i=$i for $opt"
+                    continue
+                fi
+
+                echo "[i] n=$i; generating input file (${benchmark})"
+                in/scripts/gen_${benchmark}.py $i > $TMPINPUT
+
+                echo "[i] Testing formula f$f"
+
+                if [[ "$opt" = "" ]];then
+                    opt_str="NoOpt"
+                    CMDOPT=""
+                else
+                    opt_str="$opt"
+                    CMDOPT="-$opt"
+                fi
+
+                TMPCMD="$CMD $CMDOPT -c f$f $TMPINPUT"
+                echo "[i] running reactics: $TMPCMD"
+
+                res=$(timeout $timelimit $TMPCMD | grep STAT)
+                if [[ $? -ne 0 ]];then
+                    done=1
+                    continue
+                fi
+                mem=$(echo $res | cut -d';' -f 5)
+                time=$(echo $res | cut -d';' -f 6)
+
+                echo "[.] Finished. time:$time, mem:$mem"
+
+                echo "$i $time $mem" >> bench_drs_${benchmark}_${opt_str}_f$f.dat
+
+            done
+
+            echo 
+            
+        done
+
+    done
+
+done
+
+rm -f $TMPINPUT
+
+# EOF
diff --git a/formrsctl.cc b/formrsctl.cc
deleted file mode 100644
index 45a9a5d..0000000
--- a/formrsctl.cc
+++ /dev/null
@@ -1,323 +0,0 @@
-/*
-    Copyright (c) 2012, 2013
-    Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
-*/
-
-#include "formrsctl.hh"
-
-
-std::string BoolContexts::toStr(void) const
-{
-    if (oper == BCTX_PV)
-    {
-        return name;
-    }
-    else if (oper == BCTX_TF)
-    {
-        if (tf) return "true";
-        else return "false";
-    }
-    else if (oper == BCTX_AND)
-    {
-        return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
-    }
-    else if (oper == BCTX_OR)
-    {
-        return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == BCTX_XOR)
-    {
-        return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == BCTX_NOT)
-    {
-        return "~" + arg[0]->toStr();
-    }
-	
-	else
-    {
-        return "??";
-        assert(0);
-    }
-}
-
-BDD BoolContexts::getBDD(const SymRS *srs) const
-{
-	if (oper == BCTX_PV)
-	{
-		return srs->encActStrEntity(name);
-	}
-	else if (oper == BCTX_TF)
-	{
-		if (tf) return srs->getBDDtrue();
-		else return srs->getBDDfalse();
-	}
-	else if (oper == BCTX_AND)
-	{
-		return arg[0]->getBDD(srs) * arg[1]->getBDD(srs);
-	}
-	else if (oper == BCTX_OR)
-	{
-		return arg[0]->getBDD(srs) + arg[1]->getBDD(srs);
-	}
-	else if (oper == BCTX_XOR)
-	{
-		return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs);
-	}
-	else if (oper == BCTX_NOT)
-	{
-		return !arg[0]->getBDD(srs);
-	}
-	else
-	{
-		assert(0);
-		FERROR("Undefined operator used in Boolean context definition. This should not happen.");
-		return srs->getBDDfalse();
-	}
-}
-
-std::string FormRSCTL::toStr(void) const
-{
-    if (oper == RSCTL_PV)
-    {
-        return name;
-    }
-    else if (oper == RSCTL_TF)
-    {
-        if (tf) return "true";
-        else return "false";
-    }
-    else if (oper == RSCTL_AND)
-    {
-        return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_OR)
-    {
-        return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_XOR)
-    {
-        return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_IMPL)
-    {
-        return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_NOT)
-    {
-        return "~" + arg[0]->toStr();
-    }
-    else if (oper == RSCTL_EX)
-    {
-        return "EX(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EG)
-    {
-        return "EG(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EU)
-    {
-        return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EF)
-    {
-        return "EF(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AX)
-    {
-        return "AX(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AG)
-    {
-        return "AG(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AU)
-    {
-        return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AF)
-    {
-        return "AF(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EX_ACT)
-    {
-        return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EG_ACT)
-    {
-        return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EU_ACT)
-    {
-        return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EF_ACT)
-    {
-        return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AX_ACT)
-    {
-        return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AG_ACT)
-    {
-        return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AU_ACT)
-    {
-        return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AF_ACT)
-    {
-        return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
-    }
-
-    else
-    {
-        return "??";
-        assert(0);
-    }
-}
-
-bool FormRSCTL::hasOper(Oper op) const
-{
-    if (oper == op)
-        return true;
-    else
-    {
-        bool result = false;
-        if (arg[0] != nullptr) result = arg[0]->hasOper(op);
-        if (!result && arg[1] != nullptr) result = arg[1]->hasOper(op);
-        return result;
-    }
-}
-
-void FormRSCTL::encodeEntities(const SymRS *srs)
-{
-    if (RSCTL_COND_1ARG(oper))
-    {
-        arg[0]->encodeEntities(srs);
-    }
-    else if (RSCTL_COND_2ARG(oper))
-    {
-        arg[0]->encodeEntities(srs);
-        arg[1]->encodeEntities(srs);
-    }
-    else if (oper == RSCTL_PV)
-    {
-        bdd = new BDD(srs->encEntity(name));
-    }
-}
-
-bool FormRSCTL::isERSCTL(void) const
-{
-    if (oper == RSCTL_PV)
-    {
-        return true;
-    }
-
-    if (oper == RSCTL_NOT)
-    {
-        if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF)
-            return true;
-        else
-            return false;
-    }
-
-    if (RSCTL_COND_IS_UNIVERSAL(oper))
-    {
-        return false;
-    }
-
-    if (RSCTL_COND_1ARG(oper))
-    {
-        return arg[0]->isERSCTL();
-    }
-
-    if (RSCTL_COND_2ARG(oper))
-    {
-        return arg[0]->isERSCTL() && arg[1]->isERSCTL();
-    }
-
-    assert(0);
-
-    return false;
-}
-
-std::string FormRSCTL::getActionsStr(void) const
-{
-	if (actions != nullptr)
-	{
-	    std::string r = "[ ";
-	    bool firstact = true;
-
-	    for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
-	    {
-	        if (!firstact) r += ",";
-	        else firstact = false;
-	        r += "{";
-	        bool firstent = true;
-	        for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent)
-	        {
-	            if (!firstent) r += ",";
-	            else firstent = false;
-	            r += *ent; 
-	        }
-	        r += "}";
-	    }
-		r += " ]";		
-	    return r;
-	}
-	else if (boolCtx != nullptr)
-	{
-		return "< " + boolCtx->toStr() + " >";
-	}
-	else
-	{
-		FERROR("Context not specified. This should not happen.");
-	}
-}
-
-void FormRSCTL::encodeActions(const SymRS *srs)
-{
-    if (RSCTL_COND_ACT(oper))
-    {
-        if (actions_bdd != nullptr) forgetActionsBDD();
-        actions_bdd = new BDD(srs->getBDDfalse());
-        assert(actions != nullptr || boolCtx != nullptr);
-		assert(!(actions != nullptr && boolCtx != nullptr));
-		if (actions != nullptr)
-		{
-	        for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
-	        {
-	            BDD single_action = srs->getBDDtrue();
-	            for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent)
-	            {
-	                single_action *= srs->encActStrEntity(*ent); 
-	            }
-	            single_action = srs->compContext(single_action);
-	            *actions_bdd += single_action;
-	        }
-		}
-		else if (boolCtx != nullptr)
-		{
-			*actions_bdd = boolCtx->getBDD(srs);
-		}
-		else
-			assert(0);
-    }
-
-    if (RSCTL_COND_1ARG(oper))
-    {
-        arg[0]->encodeActions(srs);
-    }
-
-    if (RSCTL_COND_2ARG(oper))
-    {
-        arg[0]->encodeActions(srs);
-        arg[1]->encodeActions(srs);
-    }
-}
diff --git a/formrsctl.hh b/formrsctl.hh
deleted file mode 100644
index eac1723..0000000
--- a/formrsctl.hh
+++ /dev/null
@@ -1,332 +0,0 @@
-/*
-    Copyright (c) 2012-2015
-    Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
-*/
-
-#ifndef RS_FORMRSCTL_HH
-#define RS_FORMRSCTL_HH
-
-#include <iostream>
-#include <string>
-#include <cassert>
-#include "rs.hh"
-#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
-
-/* For Boolean contexts: */
-#define BCTX_PV		60
-#define BCTX_AND 	61
-#define BCTX_OR 	62
-#define BCTX_XOR 	63
-#define BCTX_NOT	64
-#define BCTX_TF		70
-
-
-#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)
-#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 RSCTL_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)
-#define BCTX_IS_VALID(a) (BCTX_COND_1ARG(a) || BCTX_COND_2ARG(a) || (a) == BCTX_PV || (a) == BCTX_TF)
-
-using std::cout;
-using std::endl;
-
-typedef unsigned char Oper;
-
-typedef std::string Entity_f;
-typedef std::set<Entity_f> Action_f;
-typedef vector<Action_f> ActionsVec_f;
-
-class BoolContexts
-{
-	Oper oper;
-	BoolContexts *arg[2];
-	std::string name;
-	bool tf;
-	
-public:
-		
-	BoolContexts(std::string varName)
-	{
-		oper = BCTX_PV;
-		name = varName;
-        arg[0] = nullptr;
-        arg[1] = nullptr;
-	}
-	
-   /**
-    * @brief Constructor for true/false.
-    *
-    * @param   val value of the logical constant
-    */
-   BoolContexts(bool val) {
-       oper = BCTX_TF;
-       tf = val;
-       arg[0] = nullptr;
-       arg[1] = nullptr;
-   }
-
-   /**
-    * @brief Constructor for one-argument formula.
-    */
-   BoolContexts(Oper op, BoolContexts *form1) {
-       assert(op == BCTX_NOT);
-       oper = op;
-       arg[0] = form1;
-       arg[1] = nullptr;
-   }
-
-   /**
-    * @brief Constructor for two-argument formula.
-    */
-   BoolContexts(Oper op, BoolContexts *form1, BoolContexts *form2) {
-       assert(BCTX_COND_2ARG(op));
-       oper = op;
-       arg[0] = form1;
-       arg[1] = form2;
-   }
-   
-   ~BoolContexts() {
-       delete arg[0];
-       delete arg[1];
-   }
-   
-   std::string toStr(void) const;
-   
-   BDD getBDD(const SymRS *srs) const;
-   
-   Oper getOper(void) const {
-       assert(BCTX_IS_VALID(oper));
-       return oper;
-   }
-   BoolContexts *getLeftSF(void) const {
-       assert(arg[0] != nullptr);
-       return arg[0];
-   }
-   BoolContexts *getRightSF(void) const {
-       assert(BCTX_COND_2ARG(oper));
-       assert(arg[1] != nullptr);
-       return arg[1];
-   }
-};
-
-class FormRSCTL
-{
-    Oper oper;
-    FormRSCTL *arg[2];
-    std::string name;
-    bool tf;
-    BDD *bdd;
-    ActionsVec_f *actions;
-    BDD *actions_bdd;
-	BoolContexts *boolCtx;
-public:
-    /**
-     * @brief Constructor for propositional variable.
-     *
-     * @param   varName variable name used mostly for printing the variable.
-     * @param   varBDD  the BDD describing the set where the variable holds.
-     */
-    FormRSCTL(std::string varName) {
-        oper = RSCTL_PV;
-        name = varName;
-        arg[0] = nullptr;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for true/false.
-     *
-     * @param   val value of the logical constant
-     */
-    FormRSCTL(bool val) {
-        oper = RSCTL_TF;
-        tf = val;
-        arg[0] = nullptr;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for two-argument formula.
-     */
-    FormRSCTL(Oper op, FormRSCTL *form1, FormRSCTL *form2) {
-        assert(RSCTL_COND_2ARG(op));
-        assert(!RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = form2;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for two-argument formula with action restrictions.
-     */
-    FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) {
-        assert(acts != nullptr);
-        assert(RSCTL_COND_2ARG(op));
-        assert(RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = form2;
-        bdd = nullptr;
-        actions = acts;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-   /**
-    * @brief Constructor for two-argument formula with Boolean context restrictions.
-    */
-   FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2) {
-       assert(bctx != nullptr);
-       assert(RSCTL_COND_2ARG(op));
-       assert(RSCTL_COND_ACT(op));
-       oper = op;
-       arg[0] = form1;
-       arg[1] = form2;
-       bdd = nullptr;
-       actions = nullptr;
-       actions_bdd = nullptr;
-	   boolCtx = bctx;
-   }
-
-    /**
-     * @brief Constructor for one-argument formula.
-     */
-    FormRSCTL(Oper op, FormRSCTL *form1) {
-        assert(RSCTL_COND_1ARG(op));
-        assert(!RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for one-argument formula with action restrictions.
-     */
-    FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) {
-        assert(acts != nullptr);
-        assert(RSCTL_COND_1ARG(op));
-        assert(RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = acts;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-   /**
-    * @brief Constructor for one-argument formula with Boolean context restrictions.
-    */
-   FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1) {
-       assert(bctx != nullptr);
-       assert(RSCTL_COND_1ARG(op));
-       assert(RSCTL_COND_ACT(op));
-       oper = op;
-       arg[0] = form1;
-       arg[1] = nullptr;
-       bdd = nullptr;
-       actions = nullptr;
-       actions_bdd = nullptr;
-	   boolCtx = bctx;
-	}
-
-    /**
-     * @brief Destructor.
-     */
-    ~FormRSCTL() {
-        delete arg[0];
-        delete arg[1];
-        delete bdd;
-        delete actions;
-        delete actions_bdd;
-		delete boolCtx;
-    }
-    std::string toStr(void) const;
-    bool hasOper(Oper op) const;
-    const BDD *getBDD(void) const {
-        assert(oper == RSCTL_PV);
-        assert(bdd != nullptr);
-        return bdd;
-    }
-    const BDD *getActionsBDD(void) const {
-        assert(RSCTL_COND_ACT(oper));
-        assert(actions_bdd != nullptr);
-        return actions_bdd;
-    }
-    Oper getOper(void) const {
-        assert(RSCTL_IS_VALID(oper));
-        return oper;
-    }
-    FormRSCTL *getLeftSF(void) const {
-        assert(arg[0] != nullptr);
-        return arg[0];
-    }
-    FormRSCTL *getRightSF(void) const {
-        assert(RSCTL_COND_2ARG(oper));
-        assert(arg[1] != nullptr);
-        return arg[1];
-    }
-    std::string getActionsStr(void) const;
-    bool getTF(void) const {
-        assert(oper == RSCTL_TF);
-        return tf;
-    }
-    void encodeEntities(const SymRS *srs);
-    void encodeActions(const SymRS *srs);
-    void forgetActionsBDD(void) {
-        if (actions_bdd != nullptr) delete actions_bdd;
-    }
-    bool isERSCTL(void) const;
-};
-
-#endif
diff --git a/formrsctlk.cc b/formrsctlk.cc
new file mode 100644
index 0000000..fd56f3a
--- /dev/null
+++ b/formrsctlk.cc
@@ -0,0 +1,290 @@
+/*
+    Copyright (c) 2012, 2013
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "formrsctlk.hh"
+#include "rs.hh"
+
+std::string FormRSCTLK::toStr(void) const
+{
+  if (oper == RSCTLK_PV) {
+    return proc_name + "." + entity_name;
+  }
+  else if (oper == RSCTLK_TF) {
+    if (tf) {
+      return "true";
+    }
+    else {
+      return "false";
+    }
+  }
+  else if (oper == RSCTLK_AND) {
+    return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_OR) {
+    return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_XOR) {
+    return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_IMPL) {
+    return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_NOT) {
+    return "~" + arg[0]->toStr();
+  }
+  else if (oper == RSCTLK_EX) {
+    return "EX(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EG) {
+    return "EG(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EU) {
+    return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EF) {
+    return "EF(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AX) {
+    return "AX(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AG) {
+    return "AG(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AU) {
+    return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AF) {
+    return "AF(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EX_ACT) {
+    return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EG_ACT) {
+    return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EU_ACT) {
+    return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
+           + ")";
+  }
+  else if (oper == RSCTLK_EF_ACT) {
+    return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AX_ACT) {
+    return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AG_ACT) {
+    return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AU_ACT) {
+    return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
+           + ")";
+  }
+  else if (oper == RSCTLK_AF_ACT) {
+    return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_NK) {
+    return "NK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_UK) {
+    return "K[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_NC) {
+    return "NC[" + getAgentsStr() + "](" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_UC) {
+    return "C[" + getAgentsStr() + "](" + arg[0]->toStr() + ")";
+  }
+
+
+  else {
+    return "??";
+    assert(0);
+  }
+}
+
+bool FormRSCTLK::hasOper(Oper op) const
+{
+  if (oper == op) {
+    return true;
+  }
+  else {
+    bool result = false;
+
+    if (arg[0] != nullptr) {
+      result = arg[0]->hasOper(op);
+    }
+
+    if (!result && arg[1] != nullptr) {
+      result = arg[1]->hasOper(op);
+    }
+
+    return result;
+  }
+}
+
+void FormRSCTLK::encodeEntities(const SymRS *srs)
+{
+  if (RSCTLK_COND_1ARG(oper)) {
+    arg[0]->encodeEntities(srs);
+  }
+  else if (RSCTLK_COND_2ARG(oper)) {
+    arg[0]->encodeEntities(srs);
+    arg[1]->encodeEntities(srs);
+  }
+  else if (oper == RSCTLK_PV) {
+    bdd = new BDD(srs->encEntity(proc_name, entity_name));
+  }
+}
+
+bool FormRSCTLK::isERSCTLK(void) const
+{
+  if (oper == RSCTLK_PV) {
+    return true;
+  }
+
+  if (oper == RSCTLK_NOT) {
+    if (arg[0]->getOper() == RSCTLK_PV || arg[0]->getOper() == RSCTLK_TF) {
+      return true;
+    }
+    else {
+      return false;
+    }
+  }
+
+  if (RSCTLK_COND_IS_UNIVERSAL(oper)) {
+    return false;
+  }
+
+  if (RSCTLK_COND_1ARG(oper)) {
+    return arg[0]->isERSCTLK();
+  }
+
+  if (RSCTLK_COND_2ARG(oper)) {
+    return arg[0]->isERSCTLK() && arg[1]->isERSCTLK();
+  }
+
+  assert(0);
+
+  return false;
+}
+
+std::string FormRSCTLK::getActionsStr(void) const
+{
+  // if (actions != nullptr) {
+  //   std::string r = "[ ";
+  //   bool firstact = true;
+  //
+  //   for (ActionsVec_f::iterator act = actions->begin(); act != actions->end();
+  //        ++act) {
+  //     if (!firstact) {
+  //       r += ",";
+  //     }
+  //     else {
+  //       firstact = false;
+  //     }
+  //
+  //     r += "{";
+  //     bool firstent = true;
+  //
+  //     for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) {
+  //       if (!firstent) {
+  //         r += ",";
+  //       }
+  //       else {
+  //         firstent = false;
+  //       }
+  //
+  //       r += *ent;
+  //     }
+  //
+  //     r += "}";
+  //   }
+  //
+  //   r += " ]";
+  //   return r;
+  // }
+  if (boolCtx != nullptr) {
+    return "< " + boolCtx->toStr() + " >";
+  }
+  else {
+    FERROR("Context not specified. This should not happen.");
+  }
+}
+
+void FormRSCTLK::encodeActions(const SymRS *srs)
+{
+  if (RSCTLK_COND_ACT(oper)) {
+    if (actions_bdd != nullptr) {
+      forgetActionsBDD();
+    }
+
+    actions_bdd = new BDD(srs->getBDDfalse());
+    assert(boolCtx != nullptr);
+    // assert(actions != nullptr || boolCtx != nullptr);
+    // assert(!(actions != nullptr && boolCtx != nullptr));
+
+    // if (actions != nullptr) {
+    //   for (ActionsVec_f::iterator act = actions->begin(); act != actions->end();
+    //        ++act) {
+    //     BDD single_action = srs->getBDDtrue();
+    //
+    //     for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) {
+    //       single_action *= srs->encActStrEntity(*ent);
+    //     }
+    //
+    //     single_action = srs->compContext(single_action);
+    //     *actions_bdd += single_action;
+    //   }
+    // }
+    if (boolCtx != nullptr) {
+      *actions_bdd = boolCtx->getBDDforContext(srs);
+    }
+    else {
+      assert(0);
+    }
+  }
+
+  if (RSCTLK_COND_1ARG(oper)) {
+    arg[0]->encodeActions(srs);
+  }
+
+  if (RSCTLK_COND_2ARG(oper)) {
+    arg[0]->encodeActions(srs);
+    arg[1]->encodeActions(srs);
+  }
+}
+
+std::string FormRSCTLK::getAgentsStr(void) const
+{
+  std::string r = "";
+  bool first = true;
+
+  for (const auto &a : agents) {
+    if (first) {
+      first = false;
+    }
+    else {
+      r += " ";
+    }
+
+    r += a;
+  }
+
+  return r;
+}
+
+ProcSet FormRSCTLK::getAgentsAsProcSet(RctSys *rs) const
+{
+  ProcSet processes;
+
+  for (auto &a : agents) {
+    processes.insert(rs->getProcessID(a));
+  }
+
+  return processes;
+}
diff --git a/formrsctlk.hh b/formrsctlk.hh
new file mode 100644
index 0000000..95ee49a
--- /dev/null
+++ b/formrsctlk.hh
@@ -0,0 +1,299 @@
+/*
+    Copyright (c) 2012-2015
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#ifndef RS_FORMRSCTLK_HH
+#define RS_FORMRSCTLK_HH
+
+#include <iostream>
+#include <string>
+#include <cassert>
+// #include "rs.hh"
+#include "symrs.hh"
+#include "cudd.hh"
+#include "types.hh"
+#include "stateconstr.hh"
+
+#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 RSCTLK_NK      61 // Epistemic operators
+#define RSCTLK_NE      62
+#define RSCTLK_NC      63
+#define RSCTLK_UK      71
+#define RSCTLK_UE      72
+#define RSCTLK_UC      73
+
+#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 || (a) == RSCTLK_UE || (a) == RSCTLK_NE || (a) == RSCTLK_UC || (a) == RSCTLK_NC)
+#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 RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45) || ((a) > 70 && (a) < 75))
+
+using std::cout;
+using std::endl;
+
+// typedef std::string Entity_f;
+// typedef std::set<Entity_f> Action_f;
+// typedef vector<Action_f> ActionsVec_f;
+typedef std::set<std::string> Agents_f;
+
+class StateConstr;
+
+class FormRSCTLK
+{
+    Oper oper;
+    FormRSCTLK *arg[2];
+    std::string entity_name;
+    std::string proc_name;
+    bool tf;
+    BDD *bdd;
+    // ActionsVec_f *actions;
+    BDD *actions_bdd;
+    StateConstr *boolCtx;
+    Agents_f agents;
+  public:
+    /**
+     * @brief Constructor for propositional variable.
+     *
+     * @param   varName variable name used mostly for printing the variable.
+     * @param   varBDD  the BDD describing the set where the variable holds.
+     */
+    FormRSCTLK(std::string procName, std::string varName)
+    {
+      oper = RSCTLK_PV;
+      proc_name = procName;
+      entity_name = varName;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for true/false.
+     *
+     * @param   val value of the logical constant
+     */
+    FormRSCTLK(bool val)
+    {
+      oper = RSCTLK_TF;
+      tf = val;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula.
+     */
+    FormRSCTLK(Oper op, FormRSCTLK *form1, FormRSCTLK *form2)
+    {
+      assert(RSCTLK_COND_2ARG(op));
+      assert(!RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula with action restrictions.
+     */
+    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1, FormRSCTLK *form2)
+    // {
+    //   assert(acts != nullptr);
+    //   assert(RSCTLK_COND_2ARG(op));
+    //   assert(RSCTLK_COND_ACT(op));
+    //   oper = op;
+    //   arg[0] = form1;
+    //   arg[1] = form2;
+    //   bdd = nullptr;
+    //   actions = acts;
+    //   actions_bdd = nullptr;
+    //   boolCtx = nullptr;
+    // }
+
+    /**
+     * @brief Constructor for two-argument formula with Boolean context restrictions.
+     */
+    FormRSCTLK(Oper op, StateConstr *bctx, FormRSCTLK *form1, FormRSCTLK *form2)
+    {
+      assert(bctx != nullptr);
+      assert(RSCTLK_COND_2ARG(op));
+      assert(RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = bctx;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula.
+     */
+    FormRSCTLK(Oper op, FormRSCTLK *form1)
+    {
+      assert(RSCTLK_COND_1ARG(op));
+      assert(!RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula with action restrictions.
+     */
+    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1)
+    // {
+    //   assert(acts != nullptr);
+    //   assert(RSCTLK_COND_1ARG(op));
+    //   assert(RSCTLK_COND_ACT(op));
+    //   oper = op;
+    //   arg[0] = form1;
+    //   arg[1] = nullptr;
+    //   bdd = nullptr;
+    //   // actions = acts;
+    //   actions_bdd = nullptr;
+    //   boolCtx = nullptr;
+    // }
+
+    /**
+     * @brief Constructor for one-argument formula with Boolean context restrictions.
+     */
+    FormRSCTLK(Oper op, StateConstr *bctx, FormRSCTLK *form1)
+    {
+      assert(bctx != nullptr);
+      assert(RSCTLK_COND_1ARG(op));
+      assert(RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = bctx;
+    }
+
+    FormRSCTLK(Oper op, Agents_f agents_set, FormRSCTLK *form1)
+    {
+      assert(RSCTLK_COND_1ARG(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      actions_bdd = nullptr;
+      agents = agents_set;
+    }
+
+    /**
+     * @brief Destructor.
+     */
+    ~FormRSCTLK()
+    {
+      delete arg[0];
+      delete arg[1];
+      delete bdd;
+      // delete actions;
+      delete actions_bdd;
+      delete boolCtx;
+    }
+    std::string toStr(void) const;
+    bool hasOper(Oper op) const;
+    const BDD *getBDD(void) const
+    {
+      assert(oper == RSCTLK_PV);
+      assert(bdd != nullptr);
+      return bdd;
+    }
+    const BDD *getActionsBDD(void) const
+    {
+      assert(RSCTLK_COND_ACT(oper));
+      assert(actions_bdd != nullptr);
+      return actions_bdd;
+    }
+    Oper getOper(void) const
+    {
+      assert(RSCTLK_IS_VALID(oper));
+      return oper;
+    }
+    FormRSCTLK *getLeftSF(void) const
+    {
+      assert(arg[0] != nullptr);
+      return arg[0];
+    }
+    FormRSCTLK *getRightSF(void) const
+    {
+      assert(RSCTLK_COND_2ARG(oper));
+      assert(arg[1] != nullptr);
+      return arg[1];
+    }
+    std::string getActionsStr(void) const;
+    bool getTF(void) const
+    {
+      assert(oper == RSCTLK_TF);
+      return tf;
+    }
+    void encodeEntities(const SymRS *srs);
+    void encodeActions(const SymRS *srs);
+    void forgetActionsBDD(void)
+    {
+      if (actions_bdd != nullptr) {
+        delete actions_bdd;
+      }
+    }
+    bool isERSCTLK(void) const;
+    Agents_f getAgents(void) const
+    {
+      return agents;
+    }
+    std::string getSingleAgent(void) const
+    {
+      assert(oper == RSCTLK_NK || oper == RSCTLK_UK);
+      return *(agents.begin());
+    }
+    std::string getAgentsStr(void) const;
+    ProcSet getAgentsAsProcSet(RctSys *rs) const;
+};
+
+#endif
diff --git a/in/hsr_drs.rs b/in/hsr_drs.rs
new file mode 100644
index 0000000..51c33af
--- /dev/null
+++ b/in/hsr_drs.rs
@@ -0,0 +1,64 @@
+options { use-context-automaton; }
+
+reactions {
+    mainA {
+        {{hsf},{hsp} -> {hsf3}}; #10
+        {{hsf,hsp,mfp},{dI} -> {hsf3}}; #11
+        {{hsf3},{hse,hsp} -> {hsf}}; #12
+        {{hsf3,hsp,mfp},{hse} -> {hsf}}; #13
+        {{hsf3,hse},{hsp} -> {hsf3:hse}}; #14
+        {{hsf3,hse,hsp,mfp},{dI} -> {hsf3:hse}}; #15
+        {{hse},{hsf3} -> {hse}}; #16
+        {{hse,hsf3,hsp},{mfp} -> {hse}}; #17
+        {{hsf3:hse},{hsp} -> {hsf3:hse,hsp}}; #18
+        {{hsf3:hse,hsp,mfp},{dI} -> {hsf3:hse,hsp}}; #19
+        {{hsp,hsf},{mfp} -> {hsp:hsf}}; #20
+        {{hsp:hsf,stress},{nostress} -> {hsp,hsf}}; #21
+        {{hsp:hsf,nostress},{stress} -> {hsp:hsf}}; #22
+        {{hsp,hsf3},{mfp} -> {hsp:hsf}}; #23
+        {{hsp,hsf3:hse},{mfp} -> {hsp:hsf,hse}}; 
+        {{prot,stress},{nostress} -> {prot,mfp}};
+        {{prot,nostress},{stress} -> {prot}};
+        {{hsp,mfp},{dI} -> {hsp:mfp}};
+        {{mfp},{hsp} -> {mfp}};
+        {{hsp:mfp},{dI} -> {hsp,prot}};
+    };
+
+    dummy {
+        {{mfp},{hsp} -> {mfp}};
+    };
+    
+}
+
+context-automaton {
+	states { s0, s1 }
+    init-state { s0 }
+	transitions {
+		{ mainA={hsf,prot,hse,nostress} }: s0 -> s1;
+		{ mainA={hsf,prot,hsp:hsf,stress} }: s0 -> s1;
+		{ mainA={hsp,prot,hsf3:hse,mfp,hsp:mfp,nostress} }: s0 -> s1;
+		{ mainA={stress} }: s1 -> s1;
+		{ mainA={nostress} }: s1 -> s1;
+		{ mainA={stress,nostress} }: s1 -> s1;
+	}
+}
+
+# P1
+rsctlk-property { A<mainA.stress XOR mainA.nostress>G(mainA.hse OR mainA.hsf3:hse IMPLIES A<mainA.stress XOR mainA.nostress>X(mainA.hse OR NK[mainA]( mainA.hsf3:hse ))) }
+
+# P2
+#rsctlk-property { A[{stress},{nostress}]G(~(hse AND hsf3:hse) IMPLIES A[{stress},{nostress}]X(~(hse AND hsf3:hse))) }
+
+# P3
+#rsctlk-property { A[{stress},{nostress}]G(prot IMPLIES A[{stress},{nostress}]X(prot)) }
+
+# P4
+#rsctlk-property { A[{stress},{nostress}]G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
+#rsctlk-property { A< stress XOR nostress >G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
+
+# P5
+#rsctlk-property { A[{stress},{nostress}]G( ((hsf XOR hsf3 XOR hsf3:hse XOR hsp:hsf) OR ~(hsf OR hsf3 OR hsf3:hse OR hsp:hsf)) IMPLIES A[{stress},{nostress}]X( (hsf XOR hsf3 XOR hsf3:hse XOR hsp:hsf) OR ~(hsf OR hsf3 OR hsf3:hse OR hsp:hsf) ) )  }
+
+# P6
+#rsctlk-property { A[{nostress}]G(hsp:hsf IMPLIES A[{nostress}]X (hsp:hsf)) }
+
diff --git a/in/bench_bc.sh b/in/scripts/bench_bc.sh
similarity index 100%
rename from in/bench_bc.sh
rename to in/scripts/bench_bc.sh
diff --git a/in/bench_mutex.sh b/in/scripts/bench_mutex.sh
similarity index 100%
rename from in/bench_mutex.sh
rename to in/scripts/bench_mutex.sh
diff --git a/in/bench_pipe.sh b/in/scripts/bench_pipe.sh
similarity index 100%
rename from in/bench_pipe.sh
rename to in/scripts/bench_pipe.sh
diff --git a/in/benchmark.sh b/in/scripts/benchmark.sh
similarity index 100%
rename from in/benchmark.sh
rename to in/scripts/benchmark.sh
diff --git a/in/benchmark_abs1.sh b/in/scripts/benchmark_abs1.sh
similarity index 100%
rename from in/benchmark_abs1.sh
rename to in/scripts/benchmark_abs1.sh
diff --git a/in/benchmark_abs1_PT.sh b/in/scripts/benchmark_abs1_PT.sh
similarity index 100%
rename from in/benchmark_abs1_PT.sh
rename to in/scripts/benchmark_abs1_PT.sh
diff --git a/in/benchmark_bc.sh b/in/scripts/benchmark_bc.sh
similarity index 100%
rename from in/benchmark_bc.sh
rename to in/scripts/benchmark_bc.sh
diff --git a/in/benchmark_mutex.sh b/in/scripts/benchmark_mutex.sh
similarity index 100%
rename from in/benchmark_mutex.sh
rename to in/scripts/benchmark_mutex.sh
diff --git a/in/benchmark_mutex_PT.sh b/in/scripts/benchmark_mutex_PT.sh
similarity index 100%
rename from in/benchmark_mutex_PT.sh
rename to in/scripts/benchmark_mutex_PT.sh
diff --git a/in/gen_abstract1.py b/in/scripts/gen_abstract1.py
old mode 100644
new mode 100755
similarity index 100%
rename from in/gen_abstract1.py
rename to in/scripts/gen_abstract1.py
diff --git a/in/scripts/gen_asm.py b/in/scripts/gen_asm.py
new file mode 100755
index 0000000..7ba76ef
--- /dev/null
+++ b/in/scripts/gen_asm.py
@@ -0,0 +1,93 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; make-progressive; }
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{a}}, {{s}} -> {{y}}}};
+        {{{{y}}, {{s}} -> {{y}}}};
+        {{{{a}}, {{s}} -> {{b}}}};
+        {{{{b}}, {{s}} -> {{c}}}};
+        {{{{c}}, {{s}} -> {{d}}}};
+        {{{{d,y}}, {{s}} -> {{dy}}}};
+    }};
+"""
+
+FINAL_PROC = """
+    procFinal {
+        {{done}, {s} -> {done}};
+    };
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ init, act }}
+    init-state {{ init }}
+    transitions {{
+{:s}
+    }}
+}}
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }}
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+for i in range(1, n+1):
+    out += PROC_STR.format(i)
+
+out += FINAL_PROC
+out += "}\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ proc1={a} }: init -> act;\n"
+transitions += init_trans
+
+for i in range(1, n+1):
+    transitions += "{:s}{{ proc{:d}={{}} }}: act -> act : ~proc{:d}.dy;\n".format(8*" ", i, i, i)
+
+for i in range(2, n+1):
+    transitions += "{:s}{{ proc{:d}={{a}} }}: act -> act : proc{:d}.dy;\n".format(8*" ", i, i-1)
+
+final_cond = "proc1.dy"
+for i in range(2, n+1):
+     final_cond += " AND proc{:d}.dy".format(i)
+
+transitions += "{:s}{{ procFinal={{done}} }}: act -> act : {:s};\n".format(8*" ", final_cond)
+
+out += CA_STR.format(transitions)
+
+# f1
+formula = "EF( procFinal.done )"
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+formula = "AG( proc{:d}.d IMPLIES K[proc{:d}]( proc{:d}.y ) )".format(n, n, n-1)
+out += PROPERTY_STR.format("f2",formula)
+
+# x1
+formula = "EF( ~procFinal.done )"
+out += PROPERTY_STR.format("x1",formula)
+
+print(out)
+
diff --git a/in/gen_bc.py b/in/scripts/gen_bc.py
similarity index 100%
rename from in/gen_bc.py
rename to in/scripts/gen_bc.py
diff --git a/in/scripts/gen_drs_mutex.py b/in/scripts/gen_drs_mutex.py
new file mode 100755
index 0000000..5cf3dd9
--- /dev/null
+++ b/in/scripts/gen_drs_mutex.py
@@ -0,0 +1,89 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; }
+"""
+CONTROLLER_STR = """
+    ct {
+        {{lock},{leave} -> {lock}};
+        {{req},{} -> {lock}};
+    };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{req}}, {{lock}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ s0, s1 }}
+    init-state {{ s0 }}
+    transitions {{
+{:s}
+    }}
+}}
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }}
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+out += CONTROLLER_STR
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "}\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ ct={} "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+
+init_trans += "}: s0 -> s1;\n"
+
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
+
+out += CA_STR.format(transitions)
+
+# f1
+formula = "EF( proc0.in )"
+for i in range(1, n):
+    formula += " AND EF( proc{:d}.in )".format(i)
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+
+out += PROPERTY_STR.format("f2",formula)
+
+print(out)
+
diff --git a/in/gen_mutex.py b/in/scripts/gen_mutex.py
similarity index 100%
rename from in/gen_mutex.py
rename to in/scripts/gen_mutex.py
diff --git a/in/scripts/gen_tgc_sc.py b/in/scripts/gen_tgc_sc.py
new file mode 100755
index 0000000..d4bfcf0
--- /dev/null
+++ b/in/scripts/gen_tgc_sc.py
@@ -0,0 +1,117 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; make-progressive; };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{allowed}}, {{}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ init, green, red }};
+    init-state {{ init }};
+    transitions {{
+{:s}
+    }};
+}};
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }};
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "};\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+init_trans += "}: init -> green;\n"
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i)
+
+no_req_cond = "~proc0.req"
+for i in range(1, n):
+     no_req_cond += " AND ~proc{:d}.req".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i)
+
+no_leave_cond = "~proc0.leave"
+for i in range(1, n):
+     no_leave_cond += " AND ~proc{:d}.leave".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond)
+
+out += CA_STR.format(transitions)
+
+## f1
+#formula = "EF( proc0.in )"
+#out += PROPERTY_STR.format("f1",formula)
+
+# f1
+formula = "EF( E<proc0.allowed>X( proc0.in ) )"
+for i in range(1, n):
+    formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+formula = "EF( proc0.approach"
+for i in range(1, n):
+    formula += " AND proc{:d}.approach".format(i)
+formula += " )"
+out += PROPERTY_STR.format("f2",formula)
+
+# f3
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+out += PROPERTY_STR.format("f3",formula)
+
+# f4
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+all_agents = "proc0"
+for i in range(1, n):
+    all_agents += ",proc{:d}".format(i)
+formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
+out += PROPERTY_STR.format("f4",formula)
+
+print(out)
+
diff --git a/in/get_results.sh b/in/scripts/get_results.sh
similarity index 100%
rename from in/get_results.sh
rename to in/scripts/get_results.sh
diff --git a/in/tgc.rs b/in/tgc.rs
new file mode 100644
index 0000000..924e331
--- /dev/null
+++ b/in/tgc.rs
@@ -0,0 +1,48 @@
+
+options { use-context-automaton; }
+reactions {
+
+    proc0 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc1 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc2 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+}
+
+context-automaton {
+    states { init, green, red }
+    init-state { init }
+    transitions {
+        { proc0={out} proc1={out} proc2={out} }: init -> green;
+        { proc0={} proc1={} proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc0={allowed} }: green -> red : proc0.req;
+        { proc1={allowed} }: green -> red : proc1.req;
+        { proc2={allowed} }: green -> red : proc2.req;
+        { proc0={} }: red -> green : proc0.leave;
+        { proc1={} }: red -> green : proc1.leave;
+        { proc2={} }: red -> green : proc2.leave;
+        { proc0={} proc1={} proc2={} } : red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+    }
+}
+
+rsctlk-property { f1 : EF( proc0.in ) AND EF( proc1.in ) AND EF( proc2.in ) }
+
+rsctlk-property { f2 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) }
diff --git a/macro.hh b/macro.hh
index dc44207..b4305a7 100644
--- a/macro.hh
+++ b/macro.hh
@@ -2,13 +2,15 @@
 #define __MY_MACROS__
 
 #include <cassert>
+#include <iostream>
+
 
 #define LINENUM std::cout << __FILE__ <<  " (function " << __func__ << "), line " << __LINE__ << std::endl;
 /* Fatal error */
 #define FERROR(s) \
 { \
-	std::cerr << "EE: " << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << ": " << s << std::endl; \
-	exit(1); \
+  std::cerr << "EE: " << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << ": " << s << std::endl; \
+  exit(1); \
 }
 #define WARNING(s) \
 { \
@@ -18,25 +20,28 @@
 #define VERB(s) \
 assert(opts != nullptr); \
 if (opts->verbose > 0) { \
-	std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
 #define VERB_L2(s) \
 assert(opts != nullptr); \
 if (opts->verbose > 1) { \
-	std::cerr << "ii VERBOSE(2): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(2): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
 #define VERB_L3(s) \
 assert(opts != nullptr); \
 if (opts->verbose > 2) { \
-	std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
 #define VERB_LN(n,s) \
 assert(opts != nullptr); \
 if (opts->verbose >= (n)) { \
-	std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
+
+#define SET_ADD(set1, set2) (set1).insert((set2).begin(), (set2).end())
+
 #endif
diff --git a/main.cc b/main.cc
deleted file mode 100644
index afc90f7..0000000
--- a/main.cc
+++ /dev/null
@@ -1,236 +0,0 @@
-/*
-    Copyright (c) 2012-2014
-    Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
-*/
-
-#include "main.hh"
-
-int main(int argc, char **argv)
-{
-    rsin_driver driver;
-
-    Options *opts = new Options;
-	driver.setOptions(opts);
-
-    bool show_reactions = false;
-    bool rstl_model_checking = false;
-    bool reach_states = false;
-    bool reach_states_succ = false;
-    bool bmc = true;
-    bool benchmarking = false;
-    bool usage_error = false;
-    bool print_parsed_sys = false;
-
-    static struct option long_options[] = 
-    {
-        {"trace-parsing",   no_argument,    0, 0   },
-        {"trace-scanning",  no_argument,    0, 0   },
-        {0,                 0,              0, 0   }
-    };
-
-    int c;
-    int option_index = 0;
-
-    while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxz", long_options, &option_index)) != -1)
-    {
-        switch (c) {
-            case 0:
-                printf("option %s", long_options[option_index].name);
-                if (optarg)
-                    printf(" with arg %s", optarg);
-                printf("\n");
-
-                if (strcmp(long_options[option_index].name, "trace-parsing"))
-                    driver.trace_parsing = true;
-                else if (strcmp(long_options[option_index].name, "trace-scanning"))
-                    driver.trace_scanning = true;
-
-                break;
-            //case 'b':
-            //    printf("-b with %s\n", optarg);
-            //    break;
-            case 'b':
-                bmc = false;
-                break;
-            case 'p':
-                opts->show_progress = true;
-                break;
-            case 'P':
-                print_parsed_sys = true;
-                break;
-            case 'r':
-                show_reactions = true;
-                break;
-            case 'c':
-                rstl_model_checking = true;
-                break;
-            case 'm':
-                opts->measure = true;
-                break;
-            case 'B':
-                benchmarking = true;
-                opts->measure = true;
-                break;
-            case 's':
-                reach_states = true;
-                break;
-            case 't':
-                reach_states_succ = true;
-                break;
-            case 'v':
-                opts->verbose++;
-                break;
-            case 'x':
-                opts->part_tr_rel = true;
-                break;
-            case 'z':
-                opts->reorder_reach = true;
-                opts->reorder_trans = true;
-                break;
-            default:
-                usage_error = true;
-        }
-    }	
-	
-    std::string inputfile;
-    if (optind < argc)
-    {
-        inputfile = argv[optind];
-    }
-    else
-    {
-        cout << "Missing input file" << endl;
-        usage_error = true;
-    }
-
-    if (usage_error)
-    {
-        cout << endl
-             << " ------------------------------------" << endl
-             << " -- Reaction Systems Model Checker --" << endl
-             << " ------------------------------------" << endl
-             << endl
-             << "   Version:   " << VERSION << endl
-             << "   Contact:   " << AUTHOR << endl
-             << endl
-#ifndef PUBLIC_RELEASE
-             << " ###################################" << endl
-             << "  THIS IS A PRIVATE VERSION OF RSMC " << endl
-             << "     PLEASE, DO NOT DISTRIBUTE      " << endl
-             << " ###################################" << endl
-             << endl
-#endif
-             << " Usage: " << argv[0] << " [options] <inputfile>" << endl << endl
-			 << " TASKS:" << endl	 
-             << "  -c   -- perform RSCTL model checking" << endl
-             //<< " -f K -- generate SMT input for the depth K" << endl
-             << "  -P   -- print parsed system" << endl
-             << "  -r   -- print reactions" << endl
-             << "  -s   -- print the set of all the reachable states" << endl
-             << "  -t   -- print the set of all the reachable states with their successors" << endl
-			 << endl << " OTHER:" << endl 
-	         << "  -b   -- disable bounded model checking (BMC) heuristic" << endl
-             << "  -x   -- use partitioned transition relation (may use less memory)" << endl
-             << "  -z   -- use reordering of the BDD variables" << endl
-             << "  -v   -- verbose (can be used more than once to increase verbosity)" << endl
-             << "  -p   -- show progress (where possible)" << endl
-             << endl
-             << " Benchmarking options:" << endl
-             << "  -m   -- measure and display time and memory usage" << endl
-             << "  -B   -- display an easy to parse summary (enables -m)" << endl
-             << endl;
-        return 100;
-    }
-
-    if (!(reach_states || reach_states_succ || rstl_model_checking || show_reactions || print_parsed_sys))
-    {
-        FERROR("No task specified: -c, -P, -r, or -s needs to be used");
-    }
-
-    if (opts->verbose > 0) 
-    {
-        cout << "Verbose level: " << opts->verbose << endl;
-    }
-
-    VERB("Parsing " << inputfile);
-
-    if (driver.parse(inputfile))
-    {
-        FERROR("Parse error");
-    }
-	
-	//
-	// Here we retrieve the reaction system from the parser
-	//
-	// We decide which RS will be used at the parser level.
-	// This decision depends on whether we use concentrations,
-	// context automaton, etc.
-	//
-	auto rs = *driver.getReactionSystem();
-	
-    rs.setOptions(opts); // these need to be passed to the driver
-
-    if (show_reactions)
-        rs.showReactions();
-
-    if (print_parsed_sys)
-        rs.printSystem();
-
-    if (reach_states || reach_states_succ || rstl_model_checking)
-    {
-        SymRS srs(&rs, opts);
-
-        ModelChecker mc(&srs, opts);
-
-        if (reach_states)
-		{
-			mc.printReach();
-		}
-        if (reach_states_succ)
-		{
-			mc.printReachWithSucc();	
-		}
-
-        if (rstl_model_checking)
-        {
-            if (bmc)
-			{
-				cout << "Using BDD-based Bounded Model Checking" << endl;
-				mc.checkRSCTL(driver.getFormRSCTL());	
-			}
-            else 
-			{
-				mc.checkRSCTLfull(driver.getFormRSCTL());	
-			}
-        }
-    }
-
-    if (opts->measure) 
-    {
-        cout << endl << std::setprecision(4)
-             << "Encoding time: " << opts->enc_time << " sec" << endl
-             << "Verification time: " << opts->ver_time << " sec" << endl
-             << "Encoding memory: " << opts->enc_mem << " MB" << endl
-             << "Memory (total): " << opts->ver_mem << " MB" << endl
-             << "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl;
-        if (benchmarking)
-        {
-            cout << std::setprecision(4)
-                << "STAT; " << opts->enc_time
-                << " ; " << opts->ver_time 
-                << " ; " << opts->enc_mem
-                << " ; " << opts->ver_mem
-                << " ; " << opts->enc_time+opts->ver_time << endl;
-
-        }
-    }
-
-    delete opts;
-
-    return 0;
-}
-
-/** EOF **/
diff --git a/mc.cc b/mc.cc
index 2ec8873..76f1128 100644
--- a/mc.cc
+++ b/mc.cc
@@ -1,572 +1,688 @@
 #include "mc.hh"
 
 ModelChecker::ModelChecker(SymRS *srs, Options *opts)
-	: using_ctx_aut(false) 
+  : using_ctx_aut(false)
 {
-    this->srs = srs;
-    this->opts = opts;
-    
-	cuddMgr = srs->getCuddMgr();
-	
-	initStates = srs->getEncInitStates();
-	
-    totalStateVars = srs->getTotalStateVars();
-    
-	pv = srs->getEncPV();
-    pv_succ = srs->getEncPVsucc();
-    pv_E = srs->getEncPV_E();
-    pv_succ_E = srs->getEncPVsucc_E();
-    pv_act_E = srs->getEncPVact_E();
+  this->srs = srs;
+  this->opts = opts;
 
-    //
-	// Transition relations
-	//
-	//	trp -- partitioned TR
-	//	trm -- monolithic TR
-	//
-	// If we use trp, then trm is nullptr (same for trm)
-	//
-	trp = srs->getEncPartTrans();
-    if (trp == nullptr) 
-		trp_size = 0;
-    else 
-		trp_size = trp->size();	
-    trm = srs->getEncMonoTrans();
-    
-	if (srs->usingContextAutomaton())
-	{
-		using_ctx_aut = true;
-		pv_ca = srs->getEncCtxAutPV();
-		pv_ca_succ = srs->getEncCtxAutPVsucc();
-		pv_ca_E = srs->getEncCtxAutPV_E();
-		pv_ca_succ_E = srs->getEncCtxAutPVsucc_E();
-	}
-	else
-	{
-		using_ctx_aut = false;
-		pv_ca = nullptr;
-		pv_ca_succ = nullptr;
-		pv_ca_E = nullptr;
-		pv_ca_succ_E = nullptr;
-	}
-	
-	// Initialise the set of reachable states
-	reach = nullptr;
+  cuddMgr = srs->getCuddMgr();
+
+  initStates = srs->getEncInitStates();
+
+  totalStateVars = srs->getTotalStateVars();
+
+  pv = srs->getEncPV();
+  pv_succ = srs->getEncPVsucc();
+  pv_E = srs->getEncPV_E();
+  pv_succ_E = srs->getEncPVsucc_E();
+  pv_ctx_E = srs->getEncPVctx_E();
+  pv_proc_enab_E = srs->getEncPVproc_enab_E();
+  pv_drs_E = srs->getEncPVdrs_E();
+
+  assert(pv != nullptr);
+  assert(pv_succ != nullptr);
+  assert(pv_E != nullptr);
+  assert(pv_succ_E != nullptr);
+  assert(pv_ctx_E != nullptr);
+  assert(pv_proc_enab_E != nullptr);
+  assert(pv_drs_E != nullptr);
+
+  //
+  // Transition relations
+  //
+  //  trp -- partitioned TR
+  //  trm -- monolithic TR
+  //
+  // If we use trp, then trm is nullptr (same for trm)
+  //
+  trp = srs->getEncPartTrans();
+
+  if (trp == nullptr) {
+    trp_size = 0;
+  }
+  else {
+    trp_size = trp->size();
+  }
+
+  trm = srs->getEncMonoTrans();
+
+  if (srs->usingContextAutomaton()) {
+    using_ctx_aut = true;
+    pv_ca = srs->getEncCtxAutPV();
+    pv_ca_succ = srs->getEncCtxAutPVsucc();
+    pv_ca_E = srs->getEncCtxAutPV_E();
+    pv_ca_succ_E = srs->getEncCtxAutPVsucc_E();
+  }
+  else {
+    using_ctx_aut = false;
+    pv_ca = nullptr;
+    pv_ca_succ = nullptr;
+    pv_ca_E = nullptr;
+    pv_ca_succ_E = nullptr;
+  }
+
+  // Initialise the set of reachable states
+  reach = nullptr;
 }
 
 inline BDD ModelChecker::getSucc(const BDD &states)
 {
-    BDD q = BDD_TRUE;
+  BDD q = BDD_TRUE;
 
-    VERB_L2("Computing successors");
-    if (opts->part_tr_rel)
-    {
-        for (unsigned int i = 0; i < trp_size; ++i)
-        {
-            q *= states * (*trp)[i];
-        }
+  VERB_L2("Computing successors");
+
+  if (opts->part_tr_rel) {
+    for (const auto &trans : *trp) {
+      q *= states * trans;
+      reorder();
     }
-    else
-    {
-        q *= states * *trm;
-    }
-    q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv);
-    q = q.ExistAbstract(*pv_act_E);
-	
-    return q;
+  }
+  else {
+    q *= states * *trm;
+  }
+
+  q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv);
+
+  // we should have one BDD for cleaning up
+  // it should be calculated at the very beginning
+
+  q = q.ExistAbstract(*pv_ctx_E);
+  q = q.ExistAbstract(*pv_proc_enab_E);
+
+  return q;
 }
 
 inline BDD ModelChecker::getPreE(const BDD &states)
 {
-    BDD q = BDD_TRUE;
-    VERB_L2("Computing preE");
-    BDD x = states.SwapVariables(*pv, *pv_succ);
-    if (opts->part_tr_rel)
-    {
-        for (unsigned int i = 0; i < trp_size; ++i)
-            q *= x * (*trp)[i];
+  BDD q = BDD_TRUE;
+  VERB_L2("Computing preE");
+  BDD x = states.SwapVariables(*pv, *pv_succ);
+
+  if (opts->part_tr_rel) {
+    for (const auto &trans : *trp) {
+      q *= x * trans;
+      reorder();
     }
-    else
-    {
-        q *= x * *trm;
-    }
-    q = q.ExistAbstract(*pv_succ_E);
-    q = q.ExistAbstract(*pv_act_E);
-    return q;
+  }
+  else {
+    q *= x * *trm;
+  }
+
+  q = q.ExistAbstract(*pv_succ_E);
+  q = q.ExistAbstract(*pv_ctx_E);
+  q = q.ExistAbstract(*pv_proc_enab_E);
+
+  return q;
 }
 
 inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
 {
-    BDD q = BDD_TRUE;
-    VERB_L2("Computing (context-restricted) preE");
-    BDD x = states.SwapVariables(*pv, *pv_succ);
-    if (opts->part_tr_rel)
-    {
-        for (unsigned int i = 0; i < trp_size; ++i)
-            q *= x * (*trp)[i] * *contexts;
+  BDD q = BDD_TRUE;
+  VERB_L2("Computing (context-restricted) preE");
+  BDD x = states.SwapVariables(*pv, *pv_succ);
+
+  if (opts->part_tr_rel) {
+    for (const auto &trans : *trp) {
+      q *= x * trans;
+      reorder();
     }
-    else
-    {
-        q *= x * *trm * *contexts;
-    }
-    q = q.ExistAbstract(*pv_succ_E);
-    q = q.ExistAbstract(*pv_act_E);
-    return q;
+
+    q *= *contexts;
+  }
+  else {
+    q *= x * *trm * *contexts;
+  }
+
+  q = q.ExistAbstract(*pv_succ_E);
+  q = q.ExistAbstract(*pv_ctx_E);
+  q = q.ExistAbstract(*pv_proc_enab_E);
+  return q;
 }
 
 void ModelChecker::dropCtxAutStatePart(BDD &states)
 {
-	states = states.ExistAbstract(*pv_ca_E);
+  states = states.ExistAbstract(*pv_ca_E);
 }
 
 void ModelChecker::printReach(void)
 {
-	VERB_LN(2, "Printing/generating reachable states");
-	
-    if (opts->measure)
-        opts->ver_time = cpuTime();
+  VERB_LN(2, "Printing/generating reachable states");
 
-	assert(initStates != nullptr);
-	
-    BDD *reach = new BDD(*initStates);
-    BDD reach_p = BDD_FALSE;
+  if (opts->measure) {
+    opts->ver_time = cpuTime();
+  }
 
-    unsigned int k = 0;
+  assert(initStates != nullptr);
 
-    while (*reach != reach_p)
-    {
-        if (opts->show_progress)
-        {
-            cout << "\rIteration " << ++k << flush;
-        }
-        reach_p = *reach;
-        *reach += getSucc(*reach);
+  BDD *reach = new BDD(*initStates);
+  BDD reach_p = BDD_FALSE;
+
+  unsigned int k = 0;
+
+  while (*reach != reach_p) {
+    if (opts->show_progress) {
+      cout << "\rIteration " << ++k << flush;
     }
-	
-	dropCtxAutStatePart(*reach);
 
-    srs->printDecodedRctSysStates(*reach);
+    reach_p = *reach;
+    *reach += getSucc(*reach);
+  }
 
-    cleanup();
+  dropCtxAutStatePart(*reach);
+  srs->printDecodedRctSysStates(*reach);
+  cleanup();
 
-    if (opts->measure)
-    {
-        opts->ver_time = cpuTime() - opts->ver_time;
-        opts->ver_mem = memUsed();
-    }
+  if (opts->measure) {
+    opts->ver_time = cpuTime() - opts->ver_time;
+    opts->ver_mem = memUsed();
+  }
 }
 
 void ModelChecker::printReachWithSucc(void)
 {
-	VERB_LN(2, "Printing/generating reachable states (with successors)");
-	
-    BDD *reach = new BDD(*initStates);
-    BDD reach_p = cuddMgr->bddZero();
+  VERB_LN(2, "Printing/generating reachable states (with successors)");
 
-    while (*reach != reach_p)
-    {
-        reach_p = *reach;
-        BDD newStates = getSucc(*reach) - *reach;
-        *reach += newStates;
+  BDD *reach = new BDD(*initStates);
+  BDD reach_p = cuddMgr->bddZero();
 
-    }
+  while (*reach != reach_p) {
+    reach_p = *reach;
+    BDD newStates = getSucc(*reach) - *reach;
+    *reach += newStates;
 
-    BDD unproc = *reach;
-    while (!unproc.IsZero())
-    {
-        BDD t;
-        t = unproc.PickOneMinterm(*pv);
-        cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
-        srs->printDecodedRctSysStates(getSucc(t));
-        unproc -= t;
-    }
-    
-	cleanup();
+  }
+
+  BDD unproc = *reach;
+
+  while (!unproc.IsZero()) {
+    BDD t;
+    t = unproc.PickOneMinterm(*pv);
+    cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
+    srs->printDecodedRctSysStates(getSucc(t));
+    unproc -= t;
+  }
+
+  cleanup();
 }
 
 bool ModelChecker::checkReach(const Entities testState)
 {
-    if (opts->measure)
-        opts->ver_time = cpuTime();
+  if (opts->measure) {
+    opts->ver_time = cpuTime();
+  }
 
-    BDD st = srs->getEncState(testState);
+  // BDD st = srs->getEncState(testState);
+  BDD st = BDD_FALSE;
+  assert(0);
 
-    BDD reach = *initStates;
-    BDD reach_p = cuddMgr->bddZero();
+  BDD reach = *initStates;
+  BDD reach_p = cuddMgr->bddZero();
 
-    while (reach != reach_p)
-    {
-        if (reach * st != cuddMgr->bddZero())
-        {
-            cleanup();
-            return true;
-        }
-        reach_p = reach;
-        reach += getSucc(reach);
+  while (reach != reach_p) {
+    if (reach * st != cuddMgr->bddZero()) {
+      cleanup();
+      return true;
     }
 
-    cleanup();
+    reach_p = reach;
+    reach += getSucc(reach);
+  }
 
-    if (opts->measure)
-    {
-        opts->ver_time = cpuTime() - opts->ver_time;
-        opts->ver_mem = memUsed();
-    }
+  cleanup();
 
-    return false;
+  if (opts->measure) {
+    opts->ver_time = cpuTime() - opts->ver_time;
+    opts->ver_mem = memUsed();
+  }
+
+  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)
-    {
-        return *form->getBDD() * *reach;
-    }
-    else if (oper == RSCTL_TF)
-    {
-        if (form->getTF() == true)
-            return *reach;
-        else
-            return cuddMgr->bddZero();
-    }
-    else if (oper == RSCTL_AND)
-    {
-        return getStatesRSCTL(form->getLeftSF()) * getStatesRSCTL(form->getRightSF());
-    }
-    else if (oper == RSCTL_OR)
-    {
-        return getStatesRSCTL(form->getLeftSF()) + getStatesRSCTL(form->getRightSF());
-    }
-    else if (oper == RSCTL_XOR)
-    {
-        return getStatesRSCTL(form->getLeftSF()) ^ getStatesRSCTL(form->getRightSF());
-    }
-    else if (oper == RSCTL_IMPL)
-    {
-        return (!getStatesRSCTL(form->getLeftSF()) * *reach) + getStatesRSCTL(form->getRightSF());
-    }
-    else if (oper == RSCTL_NOT)
-    {
-        return !getStatesRSCTL(form->getLeftSF()) * *reach;
-    }
-    else if (oper == RSCTL_EX)
-    {
-        return getPreE(getStatesRSCTL(form->getLeftSF())) * *reach;
-    }
-    else if (oper == RSCTL_EG)
-    {
-        return statesEG(getStatesRSCTL(form->getLeftSF()));
-    }
-    else if (oper == RSCTL_EU)
-    {
-        return statesEU(
-                getStatesRSCTL(form->getLeftSF()),
-                getStatesRSCTL(form->getRightSF())
-                );
-    }
-    else if (oper == RSCTL_EF)
-    {
-        return statesEF(getStatesRSCTL(form->getLeftSF()));
-    }
-    else if (oper == RSCTL_AX)
-    {
-        return !getPreE(!getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
-    }
-    else if (oper == RSCTL_AG)
-    {
-        return !statesEF(
-                !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
-    }
-    else if (oper == RSCTL_AU)
-    {
-        BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach;
-        BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach;
+  assert(reach != nullptr);
+  Oper oper = form->getOper();
 
-        BDD x = !statesEU(ng, ng * nf) * *reach;
-        if (!x.IsZero()) 
-            x = x * !statesEG(ng) * *reach;
+  if (oper == RSCTLK_PV) {
+    return *form->getBDD() * *reach;
+  }
+  else if (oper == RSCTLK_TF) {
+    if (form->getTF() == true) {
+      return *reach;
+    }
+    else {
+      return cuddMgr->bddZero();
+    }
+  }
+  else if (oper == RSCTLK_AND) {
+    return getStatesRSCTLK(form->getLeftSF()) * getStatesRSCTLK(form->getRightSF());
+  }
+  else if (oper == RSCTLK_OR) {
+    return getStatesRSCTLK(form->getLeftSF()) + getStatesRSCTLK(form->getRightSF());
+  }
+  else if (oper == RSCTLK_XOR) {
+    return getStatesRSCTLK(form->getLeftSF()) ^ getStatesRSCTLK(form->getRightSF());
+  }
+  else if (oper == RSCTLK_IMPL) {
+    return (!getStatesRSCTLK(form->getLeftSF()) * *reach) + getStatesRSCTLK(
+             form->getRightSF());
+  }
+  else if (oper == RSCTLK_NOT) {
+    return !getStatesRSCTLK(form->getLeftSF()) * *reach;
+  }
+  else if (oper == RSCTLK_EX) {
+    return getPreE(getStatesRSCTLK(form->getLeftSF())) * *reach;
+  }
+  else if (oper == RSCTLK_EG) {
+    return statesEG(getStatesRSCTLK(form->getLeftSF()));
+  }
+  else if (oper == RSCTLK_EU) {
+    return statesEU(
+             getStatesRSCTLK(form->getLeftSF()),
+             getStatesRSCTLK(form->getRightSF())
+           );
+  }
+  else if (oper == RSCTLK_EF) {
+    return statesEF(getStatesRSCTLK(form->getLeftSF()));
+  }
+  else if (oper == RSCTLK_AX) {
+    return !getPreE(!getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
+  }
+  else if (oper == RSCTLK_AG) {
+    return !statesEF(
+             !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
+  }
+  else if (oper == RSCTLK_AU) {
+    BDD ng = !getStatesRSCTLK(form->getRightSF()) * *reach;
+    BDD nf = !getStatesRSCTLK(form->getLeftSF()) * *reach;
 
-        return x; 
-    }
-    else if (oper == RSCTL_AF)
-    {
-        return !statesEG(
-                !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
-    }
-    /***** CONTEXT RESTRICTIONS: ******/
-    else if (oper == RSCTL_EX_ACT) 
-    {
-        return getPreEctx(getStatesRSCTL(form->getLeftSF()), form->getActionsBDD()) * *reach;
-    }
-    else if (oper == RSCTL_EG_ACT)
-    {
-        return statesEGctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF())); /***** EG? *****/
-    }
-    else if (oper == RSCTL_EU_ACT)
-    {
-        return statesEUctx(
-                    form->getActionsBDD(),
-                    getStatesRSCTL(form->getLeftSF()),
-                    getStatesRSCTL(form->getRightSF())
-                );
-    }
-    else if (oper == RSCTL_EF_ACT)
-    {
-        return statesEFctx(form->getActionsBDD(), getStatesRSCTL(form->getLeftSF()));
-    }
-    else if (oper == RSCTL_AX_ACT)
-    {
-        return !getPreEctx(!getStatesRSCTL(form->getLeftSF()) * *reach, form->getActionsBDD()) * *reach;
-    }
-    else if (oper == RSCTL_AG_ACT)
-    {
-        return !statesEFctx(form->getActionsBDD(),
-                !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
-    }
-    else if (oper == RSCTL_AU_ACT)
-    {
-        BDD ng = !getStatesRSCTL(form->getRightSF()) * *reach;
-        BDD nf = !getStatesRSCTL(form->getLeftSF()) * *reach;
+    BDD x = !statesEU(ng, ng * nf) * *reach;
 
-        BDD x = !statesEUctx(form->getActionsBDD(), ng, ng * nf) * *reach; 
-        if (!x.IsZero()) 
-            x = x * !statesEGctx(form->getActionsBDD(), ng) * *reach;
-
-        return x; 
-    }
-    else if (oper == RSCTL_AF_ACT)
-    {
-        return !statesEGctx(form->getActionsBDD(),
-               !getStatesRSCTL(form->getLeftSF()) * *reach) * *reach;
+    if (!x.IsZero()) {
+      x = x * !statesEG(ng) * *reach;
     }
 
-    assert(0); // Should never happen
-    return BDD_FALSE;
+    return x;
+  }
+  else if (oper == RSCTLK_AF) {
+    return !statesEG(
+             !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
+  }
+  /***** CONTEXT RESTRICTIONS: ******/
+  else if (oper == RSCTLK_EX_ACT) {
+    return getPreEctx(getStatesRSCTLK(form->getLeftSF()),
+                      form->getActionsBDD()) * *reach;
+  }
+  else if (oper == RSCTLK_EG_ACT) {
+    return statesEGctx(form->getActionsBDD(),
+                       getStatesRSCTLK(form->getLeftSF())); /***** EG? *****/
+  }
+  else if (oper == RSCTLK_EU_ACT) {
+    return statesEUctx(
+             form->getActionsBDD(),
+             getStatesRSCTLK(form->getLeftSF()),
+             getStatesRSCTLK(form->getRightSF())
+           );
+  }
+  else if (oper == RSCTLK_EF_ACT) {
+    return statesEFctx(form->getActionsBDD(), getStatesRSCTLK(form->getLeftSF()));
+  }
+  else if (oper == RSCTLK_AX_ACT) {
+    return !getPreEctx(!getStatesRSCTLK(form->getLeftSF()) * *reach,
+                       form->getActionsBDD()) * *reach;
+  }
+  else if (oper == RSCTLK_AG_ACT) {
+    return !statesEFctx(form->getActionsBDD(),
+                        !getStatesRSCTLK(form->getLeftSF()) * *reach) * *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;
+
+    if (!x.IsZero()) {
+      x = x * !statesEGctx(form->getActionsBDD(), ng) * *reach;
+    }
+
+    return x;
+  }
+  else if (oper == RSCTLK_AF_ACT) {
+    return !statesEGctx(form->getActionsBDD(),
+                        !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
+  }
+  else if (oper == RSCTLK_NK) {
+    auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
+    return statesNK(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_id) * *reach;
+  }
+  else if (oper == RSCTLK_UK) {
+    auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
+    return *reach - (statesNK(*reach - getStatesRSCTLK(form->getLeftSF()), proc_id) * *reach);
+  }
+  else if (oper == RSCTLK_NE) {
+    auto proc_set = form->getAgentsAsProcSet(srs->rs);
+    return statesNE(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_set) * *reach;
+  }
+  else if (oper == RSCTLK_UE) {
+    auto proc_set = form->getAgentsAsProcSet(srs->rs);
+    return *reach - (statesNE(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
+  }
+  else if (oper == RSCTLK_NC) {
+    auto proc_set = form->getAgentsAsProcSet(srs->rs);
+    return statesNC(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_set) * *reach;
+  }
+  else if (oper == RSCTLK_UC) {
+    auto proc_set = form->getAgentsAsProcSet(srs->rs);
+    return *reach - (statesNC(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
+  }
+
+  assert(0); // Should never happen
+  return BDD_FALSE;
 }
 
 BDD ModelChecker::statesEG(const BDD &states)
 {
-    BDD x = states;
-    BDD x_p = cuddMgr->bddZero();
-    while (x != x_p)
-    {
-        x_p = x;
-        x = x * getPreE(x);
-    }
-    return x;
+  BDD x = states;
+  BDD x_p = cuddMgr->bddZero();
+
+  while (x != x_p) {
+    x_p = x;
+    x = x * getPreE(x);
+  }
+
+  return x;
 }
 
 BDD ModelChecker::statesEU(const BDD &statesA, const BDD &statesB)
 {
-    BDD x = statesA;
-    BDD x_p = *reach;
-    while (x != x_p)
-    {
-        x_p = x;
-        x = x + (statesA * getPreE(x));
-    }
-    return x;
+  BDD x = statesA;
+  BDD x_p = *reach;
+
+  while (x != x_p) {
+    x_p = x;
+    x = x + (statesA * getPreE(x));
+  }
+
+  return x;
 }
 
 BDD ModelChecker::statesEF(const BDD &states)
 {
-    BDD x = states;
-    BDD x_p = *reach;
-    while (x != x_p)
-    {
-        x_p = x;
-        x = x + (*reach * getPreE(x));
-    }
-    return x;
+  BDD x = states;
+  BDD x_p = *reach;
+
+  while (x != x_p) {
+    x_p = x;
+    x = x + (*reach * getPreE(x));
+  }
+
+  return x;
 }
 
 BDD ModelChecker::statesEGctx(const BDD *contexts, const BDD &states)
 {
-    BDD x = states;
-    BDD x_p = cuddMgr->bddZero();
-    while (x != x_p)
-    {
-        x_p = x;
-        x = x * getPreEctx(x, contexts);
-    }
-    return x;
+  BDD x = states;
+  BDD x_p = cuddMgr->bddZero();
+
+  while (x != x_p) {
+    x_p = x;
+    x = x * getPreEctx(x, contexts);
+  }
+
+  return x;
 }
 
-BDD ModelChecker::statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB)
+BDD ModelChecker::statesEUctx(const BDD *contexts, const BDD &statesA,
+                              const BDD &statesB)
 {
-    BDD x = statesA;
-    BDD x_p = *reach;
-    while (x != x_p)
-    {
-        x_p = x;
-        x = x + (statesA * getPreEctx(x, contexts));
-    }
-    return x;
+  BDD x = statesA;
+  BDD x_p = *reach;
+
+  while (x != x_p) {
+    x_p = x;
+    x = x + (statesA * getPreEctx(x, contexts));
+  }
+
+  return x;
 }
 
 BDD ModelChecker::statesEFctx(const BDD *contexts, const BDD &states)
 {
-    BDD x = states;
-    BDD x_p = *reach;
-    while (x != x_p)
-    {
-        x_p = x;
-        x = x + (*reach * getPreEctx(x, contexts));
-    }
-    return x;
+  BDD x = states;
+  BDD x_p = *reach;
+
+  while (x != x_p) {
+    x_p = x;
+    x = x + (*reach * getPreEctx(x, contexts));
+  }
+
+  return x;
 }
 
-bool ModelChecker::checkRSCTL(FormRSCTL *form)
+BDD ModelChecker::statesNK(const BDD &states, Process proc_id)
 {
-    if (form->isERSCTL())
-        return checkRSCTLbmc(form);
-    else
-        return checkRSCTLfull(form);
+  // bdd = new BDD((arg[0]->satStates(reach) * reach).ExistAbstract(bddOnlyIth(getAgent())) * reach);
+  BDD x = states;
+
+  x = x.ExistAbstract(getIthOnly(proc_id));
+
+  return x;
 }
 
-bool ModelChecker::checkRSCTLfull(FormRSCTL *form)
+BDD ModelChecker::statesNE(const BDD &states, ProcSet processes)
 {
-    if (opts->measure)
-        opts->ver_time = cpuTime();
+  BDD x = BDD_FALSE;
 
-    assert(form != nullptr);
+  for (auto const &proc_id : processes) {
+    x += states.ExistAbstract(getIthOnly(proc_id));
+  }
 
-    bool result = false;
-
-    VERB("Model checking for RSCTL formula: " << form->toStr());
-
-    VERB("Processing the formula: encoding entities");
-    form->encodeEntities(srs);
-    VERB("Entities encoded");
-
-    VERB("Processing the formula: encoding actions/contexts");
-    form->encodeActions(srs);
-    VERB("Contexts encoded");
-
-    assert(reach == nullptr);
-
-    reach = new BDD(*initStates);
-    BDD reach_p = cuddMgr->bddZero();
-
-    VERB("Generating state space");
-
-    unsigned int k = 0;
-
-    while (*reach != reach_p)
-    {
-
-        if (opts->show_progress)
-        {
-            cout << "\rIteration " << ++k << flush;
-        }
-
-        if (opts->reorder_reach)
-        {
-            VERB_L2("Reordering")
-            Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
-        }
-
-        reach_p = *reach;
-        *reach += getSucc(*reach);
-    }
-
-    if (opts->show_progress) cout << endl;
-
-    VERB("Checking the formula");
-
-    //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero())
-	if (*initStates * getStatesRSCTL(form) == *initStates)
-    {
-        result = true;
-    }
-    else
-    {
-        result = false;
-    }
-
-    cleanup(); 
-
-    cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold") << endl;
-
-    if (opts->measure)
-    {
-        opts->ver_time = cpuTime() - opts->ver_time;
-        opts->ver_mem = memUsed();
-    }
-
-    return result;
+  return x;
 }
 
-bool ModelChecker::checkRSCTLbmc(FormRSCTL *form)
+BDD ModelChecker::statesNC(const BDD &states, ProcSet processes)
 {
-    if (opts->measure)
-        opts->ver_time = cpuTime();
+  BDD x = BDD_FALSE;
+  BDD x_p = *reach;
 
-    assert(form != nullptr);
+  while (x != x_p) {
+    x_p = x;
+    BDD t = BDD_FALSE;
 
-    if (!form->isERSCTL())
-    {
-        FERROR("Formula " << form->toStr() << " is not syntactically an ERSCTL formula");
+    for (auto const &proc_id : processes) {
+      t += x.ExistAbstract(getIthOnly(proc_id));
     }
 
-    bool result = false;
+    x = t;
+  }
 
-    VERB("Bounded model checking for RSCTL formula: " << form->toStr());
+  return x;
+}
 
-    VERB("Processing the formula: encoding entities");
-    form->encodeEntities(srs);
-    VERB("Entities encoded");
+BDD ModelChecker::getIthOnly(Process proc_id)
+{
+  /* if possible, we return the BDD from cache */
+  if (ith_only_E.count(proc_id) == 1) {
+    return ith_only_E[proc_id];
+  }
 
-    VERB("Processing the formula: encoding actions/contexts");
-    form->encodeActions(srs);
-    VERB("Contexts encoded");
+  /* nothing has been found in the cache */
+  BDD bdd = BDD_TRUE;
 
-    assert(reach == nullptr);
+  for (auto i = 0; i < pv_drs_E->size(); ++i) {
 
-    reach = new BDD(*initStates);
-    BDD reach_p = cuddMgr->bddZero();
-
-    unsigned int k = 0;
-
-    while (*reach != reach_p)
-    {
-        if (opts->show_progress)
-        {
-            cout << "\rIteration " << ++k << flush;
-        }
-
-        //if (*initStates * getStatesRSCTL(form) != cuddMgr->bddZero())
-	    if (*initStates * getStatesRSCTL(form) == *initStates)
-        {
-            result = true;
-            break;
-        }
-
-        reach_p = *reach;
-        *reach += getSucc(*reach);
+    if (i == proc_id) {
+      continue;
     }
 
-    if (opts->show_progress) cout << endl;
+    bdd *= (*pv_drs_E)[i];
+  }
 
-    cleanup(); 
+  ith_only_E[proc_id] = bdd;
 
-    cout << "Formula " << form->toStr() << " " << (result ? "holds" : "does not hold") << endl;
+  return bdd;
+}
 
-    if (opts->measure)
-    {
-        opts->ver_time = cpuTime() - opts->ver_time;
-        opts->ver_mem = memUsed();
+bool ModelChecker::checkRSCTLK(FormRSCTLK *form)
+{
+  if (form->isERSCTLK()) {
+    return checkRSCTLKbmc(form);
+  }
+  else {
+    return checkRSCTLKfull(form);
+  }
+}
+
+bool ModelChecker::checkRSCTLKfull(FormRSCTLK *form)
+{
+  if (opts->measure) {
+    opts->ver_time = cpuTime();
+  }
+
+  assert(form != nullptr);
+
+  bool result = false;
+
+  VERB("Model checking for RSCTLK formula: " << form->toStr());
+
+  VERB("Processing the formula: encoding entities");
+  form->encodeEntities(srs);
+  VERB("Entities encoded");
+
+  VERB("Processing the formula: encoding actions/contexts");
+  form->encodeActions(srs);
+  VERB("Contexts encoded");
+
+  assert(reach == nullptr);
+
+  reach = new BDD(*initStates);
+  BDD reach_p = cuddMgr->bddZero();
+
+  VERB("Generating state space");
+
+  unsigned int k = 0;
+
+  while (*reach != reach_p) {
+
+    if (opts->show_progress) {
+      cout << "\rIteration " << ++k << flush;
     }
 
-    return result;
+    if (opts->reorder_reach) {
+      VERB_L2("Reordering")
+      Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+    }
+
+    reach_p = *reach;
+    *reach += getSucc(*reach);
+  }
+
+  if (opts->show_progress) {
+    cout << endl;
+  }
+
+  VERB("Checking the formula");
+
+  //if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
+  if (*initStates * getStatesRSCTLK(form) == *initStates) {
+    result = true;
+  }
+  else {
+    result = false;
+  }
+
+  cleanup();
+
+  cout << "Formula " << form->toStr() << (result ? " holds" : " does not hold")
+       << endl;
+
+  if (opts->measure) {
+    opts->ver_time = cpuTime() - opts->ver_time;
+    opts->ver_mem = memUsed();
+  }
+
+  return result;
+}
+
+bool ModelChecker::checkRSCTLKbmc(FormRSCTLK *form)
+{
+  if (opts->measure) {
+    opts->ver_time = cpuTime();
+  }
+
+  assert(form != nullptr);
+
+  if (!form->isERSCTLK()) {
+    FERROR("Formula " << form->toStr() <<
+           " is not syntactically an ERSCTLK formula");
+  }
+
+  bool result = false;
+
+  VERB("Bounded model checking for RSCTLK formula: " << form->toStr());
+
+  VERB("Processing the formula: encoding entities");
+  form->encodeEntities(srs);
+  VERB("Entities encoded");
+
+  VERB("Processing the formula: encoding actions/contexts");
+  form->encodeActions(srs);
+  VERB("Contexts encoded");
+
+  assert(reach == nullptr);
+
+  reach = new BDD(*initStates);
+  BDD reach_p = cuddMgr->bddZero();
+
+  unsigned int k = 0;
+
+  while (*reach != reach_p) {
+    if (opts->show_progress) {
+      cout << "\rIteration " << ++k << flush;
+    }
+
+    //if (*initStates * getStatesRSCTLK(form) != cuddMgr->bddZero())
+    if (*initStates * getStatesRSCTLK(form) == *initStates) {
+      result = true;
+      break;
+    }
+
+    reach_p = *reach;
+    *reach += getSucc(*reach);
+  }
+
+  if (opts->show_progress) {
+    cout << endl;
+  }
+
+  cleanup();
+
+  cout << "Formula " << form->toStr() << " " << (result ? "holds" :
+       "does not hold") << endl;
+
+  if (opts->measure) {
+    opts->ver_time = cpuTime() - opts->ver_time;
+    opts->ver_mem = memUsed();
+  }
+
+  return result;
+}
+
+void ModelChecker::reorder(void)
+{
+  if (opts->reorder_trans) {
+    VERB_L2("Reordering START");
+    // Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 100000);
+    cuddMgr->ReduceHeap(CUDD_REORDER_GROUP_SIFT);
+    VERB_L2("Reordering DONE");
+  }
 }
 
 void ModelChecker::cleanup(void)
 {
-    delete reach;
-    reach = nullptr;
+  delete reach;
+  reach = nullptr;
 }
 
-/** EOF **/
\ No newline at end of file
+/** EOF **/
diff --git a/mc.hh b/mc.hh
index 20d22fb..a331bb0 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"
@@ -20,52 +20,65 @@ class ModelChecker
     SymRS *srs;
     Options *opts;
     Cudd *cuddMgr;
-    BDD *initStates; 
+    BDD *initStates;
     vector<BDD> *pv;
     vector<BDD> *pv_succ;
     BDD *pv_E;
     BDD *pv_succ_E;
-    BDD *pv_act_E;
+    BDD *pv_ctx_E;
+    BDDvec *pv_drs_E;
     BDD *reach;
     vector<BDD> *trp;
     BDD *trm;
-	
-	// Context Automaton
-	bool using_ctx_aut;
-	vector<BDD> *pv_ca;
-	vector<BDD> *pv_ca_succ;
-	BDD *pv_ca_E;	
-	BDD *pv_ca_succ_E;
-		
+
+    std::map<Process, BDD> ith_only_E;
+
+    // Context Automaton
+    bool using_ctx_aut;
+    vector<BDD> *pv_ca;
+    vector<BDD> *pv_ca_succ;
+    BDD *pv_ca_E;
+    BDD *pv_ca_succ_E;
+
+    BDD *pv_proc_enab_E;
+
     unsigned int trp_size;
     unsigned int totalStateVars;
-	
+
     /**
      * @brief Abstracts away (in-place!) the context automaton states
      */
-	void dropCtxAutStatePart(BDD &states);
+    void dropCtxAutStatePart(BDD &states);
 
     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);
     BDD statesEGctx(const BDD *contexts, const BDD &states);
     BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB);
     BDD statesEFctx(const BDD *contexts, const BDD &states);
+    BDD statesNK(const BDD &states, Process proc_id);
+    BDD statesNE(const BDD &states, ProcSet processes);
+    BDD statesNC(const BDD &states, ProcSet processes);
+
+    BDD getIthOnly(Process proc_id);
+
     void cleanup(void);
 
-public:
+    void reorder(void);
+
+  public:
     ModelChecker(SymRS *srs, Options *opts);
 
     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/memtime.hh b/memtime.hh
index 1bcef66..086fd6c 100644
--- a/memtime.hh
+++ b/memtime.hh
@@ -21,47 +21,69 @@
 
 #include <sys/time.h>
 #include <sys/resource.h>
+#if defined(__APPLE__)
+#include <malloc/malloc.h>
+#endif
 #include <stdio.h>
 #include <unistd.h>
 #include "macro.hh"
 
+using namespace std;
+
 typedef long long int64;
 
 static inline double cpuTime(void)
 {
-    struct rusage ru;
-    getrusage(RUSAGE_SELF, &ru);
-    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
+  struct rusage ru;
+  getrusage(RUSAGE_SELF, &ru);
+  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
 }
 
 static inline int memReadStat(void)
 {
-    char name[256];
-    pid_t pid = getpid();
-    sprintf(name, "/proc/%d/statm", pid);
-    FILE* in = fopen(name, "rb");
-    if (in == nullptr)
-    {
-        return 0;
+  char name[256];
+  pid_t pid = getpid();
+  sprintf(name, "/proc/%d/statm", pid);
+  FILE *in = fopen(name, "rb");
+
+  if (in == nullptr) {
+    return 0;
+  }
+
+  int value;
+
+  for (int field = 0; field >= 0; --field) {
+    if (fscanf(in, "%d", &value) == EOF) {
+      FERROR("EOF")
     }
-    int value;
-    for (int field = 0; field >= 0; --field)
-    {
-        if (fscanf(in, "%d", &value) == EOF)
-            FERROR("EOF");
-    }
-    fclose(in);
-    return value;
+  }
+
+  fclose(in);
+  return value;
 }
 
 static inline int64 memUsedInt64()
 {
-    return (int64)memReadStat() * (int64)getpagesize();
+  return (int64)memReadStat() * (int64)getpagesize();
 }
 
+#if defined(__APPLE__)
+
 static inline double memUsed()
 {
-    return memUsedInt64() / 1048576.0;
+  malloc_statistics_t t;
+  malloc_zone_statistics(NULL, &t);
+  return (double)t.max_size_in_use / (1024 * 1024);
+}
+
+#else
+
+static inline double memUsed()
+{
+  return memUsedInt64() / (1024 * 1024);
 }
 
 #endif
+
+#endif
+
diff --git a/options.hh b/options.hh
index 0f494a0..e33af84 100644
--- a/options.hh
+++ b/options.hh
@@ -1,9 +1,10 @@
 #ifndef RS_OPTIONS_HH
 #define RS_OPTIONS_HH
 
-class Options {
+class Options
+{
 
-public:
+  public:
     unsigned int verbose;
     bool show_progress;
     bool measure;
@@ -18,19 +19,19 @@ public:
 
     Options(void)
     {
-        verbose = 0;
-        show_progress = false;
-        measure = false;
+      verbose = 0;
+      show_progress = false;
+      measure = false;
 
-        part_tr_rel = false;
+      part_tr_rel = false;
 
-        reorder_reach = false; 
-        reorder_trans = false;
+      reorder_reach = false;
+      reorder_trans = false;
 
-        enc_time = 0;
-        enc_mem = 0;
-        ver_time = 0;
-        ver_mem = 0;
+      enc_time = 0;
+      enc_mem = 0;
+      ver_time = 0;
+      ver_mem = 0;
     }
 };
 
diff --git a/reactics.cc b/reactics.cc
new file mode 100644
index 0000000..06aeab4
--- /dev/null
+++ b/reactics.cc
@@ -0,0 +1,271 @@
+/*
+    Copyright (c) 2012-2014
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "reactics.hh"
+
+int main(int argc, char **argv)
+{
+  rsin_driver driver;
+
+  Options *opts = new Options;
+  driver.setOptions(opts);
+
+  bool show_reactions = false;
+  bool rstl_model_checking = false;
+  bool reach_states = false;
+  bool reach_states_succ = false;
+  bool bmc = true;
+  bool benchmarking = false;
+  bool dump_help_message = false;
+  bool print_parsed_sys = false;
+  std::string property_name = "default";
+
+  static struct option long_options[] = {
+    {"trace-parsing",   no_argument,    0, 0   },
+    {"trace-scanning",  no_argument,    0, 0   },
+    {0,                 0,              0, 0   }
+  };
+
+  int c;
+  int option_index = 0;
+
+  while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzh", long_options,
+                          &option_index)) != -1) {
+    switch (c) {
+      case 0:
+        printf("option %s", long_options[option_index].name);
+
+        if (optarg) {
+          printf(" with arg %s", optarg);
+        }
+
+        printf("\n");
+
+        if (strcmp(long_options[option_index].name, "trace-parsing")) {
+          driver.trace_parsing = true;
+        }
+        else if (strcmp(long_options[option_index].name, "trace-scanning")) {
+          driver.trace_scanning = true;
+        }
+
+        break;
+
+      //case 'b':
+      //    printf("-b with %s\n", optarg);
+      //    break;
+      case 'b':
+        bmc = false;
+        break;
+
+      case 'p':
+        opts->show_progress = true;
+        break;
+
+      case 'P':
+        print_parsed_sys = true;
+        break;
+
+      case 'r':
+        show_reactions = true;
+        break;
+
+      case 'c':
+        rstl_model_checking = true;
+        property_name = optarg;
+        break;
+
+      case 'm':
+        opts->measure = true;
+        break;
+
+      case 'B':
+        benchmarking = true;
+        opts->measure = true;
+        break;
+
+      case 's':
+        reach_states = true;
+        break;
+
+      case 't':
+        reach_states_succ = true;
+        break;
+
+      case 'v':
+        opts->verbose++;
+        break;
+
+      case 'x':
+        opts->part_tr_rel = true;
+        break;
+
+      case 'z':
+        opts->reorder_reach = true;
+        opts->reorder_trans = true;
+        break;
+
+      case 'h':
+        dump_help_message = true;
+        break;
+
+      default:
+        dump_help_message = true;
+        break;
+    }
+  }
+
+  std::string inputfile;
+
+  if (optind < argc) {
+    inputfile = argv[optind];
+  }
+  else if (!dump_help_message) {
+    cout << "Missing input file" << endl;
+    dump_help_message = true;
+  }
+
+  if (dump_help_message) {
+    print_help(std::string(argv[0]));
+    return 100;
+  }
+
+  if (!(reach_states || reach_states_succ || rstl_model_checking
+        || show_reactions || print_parsed_sys)) {
+    FERROR("No task specified: -c, -P, -r, or -s needs to be used");
+  }
+
+  if (opts->verbose > 0) {
+    cout << "Verbose level: " << opts->verbose << endl;
+  }
+
+  VERB("Parsing " << inputfile);
+
+  if (driver.parse(inputfile)) {
+    FERROR("Parse error");
+  }
+
+  //
+  // Here we retrieve the reaction system from the parser
+  //
+  // We decide which RS will be used at the parser level.
+  // This decision depends on whether we use concentrations,
+  // context automaton, etc.
+  //
+  auto rs = *driver.getReactionSystem();
+
+  bool result = true;
+
+  rs.setOptions(opts); // these need to be passed to the driver
+
+  if (show_reactions) {
+    rs.showReactions();
+  }
+
+  if (print_parsed_sys) {
+    rs.printSystem();
+  }
+
+  if (reach_states || reach_states_succ || rstl_model_checking) {
+    SymRS srs(&rs, opts);
+
+    ModelChecker mc(&srs, opts);
+
+    if (reach_states) {
+      mc.printReach();
+    }
+
+    if (reach_states_succ) {
+      mc.printReachWithSucc();
+    }
+
+    if (rstl_model_checking) {
+      if (bmc) {
+        cout << "Using BDD-based Bounded Model Checking" << endl;
+        result = mc.checkRSCTLK(driver.getFormRSCTLK(property_name));
+      }
+      else {
+        result = mc.checkRSCTLKfull(driver.getFormRSCTLK(property_name));
+      }
+    }
+  }
+
+  if (opts->measure) {
+    cout << endl << std::setprecision(4)
+         << "Encoding time: " << opts->enc_time << " sec" << endl
+         << "Verification time: " << opts->ver_time << " sec" << endl
+         << "Encoding memory: " << opts->enc_mem << " MB" << endl
+         << "Memory (total): " << opts->ver_mem << " MB" << endl
+         << "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl;
+
+    if (benchmarking) {
+      cout << std::setprecision(4)
+           << "STAT; " << opts->enc_time
+           << " ; " << opts->ver_time
+           << " ; " << opts->enc_mem
+           << " ; " << opts->ver_mem
+           << " ; " << opts->enc_time + opts->ver_time << endl;
+
+    }
+  }
+
+  delete opts;
+
+  int ret_val;
+
+  if (result) {
+    ret_val = 0;
+  }
+  else {
+    ret_val = 1;
+  }
+
+  return ret_val;
+}
+
+void print_help(std::string path_str)
+{
+  cout << endl
+       << " ------------------------------------------------" << endl
+       << " -- ReactICS -- Reaction Systems Model Checker --" << endl
+       << " ------------------------------------------------" << endl
+       << endl
+       << "   Version:   " << VERSION << endl
+       << "   Contact:   " << AUTHOR << endl
+       << endl
+#ifndef PUBLIC_RELEASE
+       << " ###################################" << endl
+       << "  THIS IS A PRIVATE VERSION OF RSMC " << endl
+       << "     PLEASE, DO NOT DISTRIBUTE      " << endl
+       << " ###################################" << endl
+       << endl
+#endif
+       << " Usage: " << path_str << " [options] <input file>" << endl << endl
+       << " TASKS:" << endl
+       << "  -c form  -- perform RSCTLK model checking (form: formula identifier)" << endl
+       //<< " -f K -- generate SMT input for the depth K" << endl
+       << "  -P       -- print parsed system" << endl
+       << "  -r       -- print reactions" << endl
+       << "  -s       -- print all the reachable states" << endl
+       << "  -t       -- print all the reachable states with their successors"
+       << endl
+       << endl << " OTHER:" << endl
+       << "  -b       -- disable bounded model checking (BMC) heuristic" << endl
+       << "  -x       -- use partitioned transition relation" <<
+       endl
+       << "  -z       -- use reordering of the BDD variables" << endl
+       << "  -v       -- verbose (use more than once to increase verbosity)" <<
+       endl
+       << "  -p       -- show progress (where possible)" << endl
+       << endl
+       << " Benchmarking options:" << endl
+       << "  -m       -- measure and display time and memory usage" << endl
+       << "  -B       -- display an easy to parse summary (enables -m)" << endl
+       << endl;
+}
+
+/** EOF **/
diff --git a/main.hh b/reactics.hh
similarity index 55%
rename from main.hh
rename to reactics.hh
index 5a7b11b..c1e0d7c 100644
--- a/main.hh
+++ b/reactics.hh
@@ -1,13 +1,10 @@
 /*
-    Copyright (c) 2012, 2013
+    Copyright (c) 2012, 2013, 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
-#ifndef RS_MAIN_HH
-#define RS_MAIN_HH
+#ifndef REACTICS_HH
+#define REACTICS_HH
 
 #include <iostream>
 #include <string>
@@ -22,9 +19,12 @@
 #include "options.hh"
 #include "memtime.hh"
 
-#define VERSION     "1.0alpha"
-#define AUTHOR      "Artur Męski <meski@ipipan.waw.pl>"
+#define VERSION     "2.0"
+//#define AUTHOR      "Artur Meski <artur.meski@gmail.com>"
+#define AUTHOR      "Artur Meski <meski@ipipan.waw.pl>"
 using std::cout;
 using std::endl;
 
+void print_help(std::string path_str);
+
 #endif
diff --git a/rs.cc b/rs.cc
index 9ed9d26..f04c578 100644
--- a/rs.cc
+++ b/rs.cc
@@ -1,233 +1,371 @@
 /*
-    Copyright (c) 2012-2014
+    Copyright (c) 2012-2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "rs.hh"
 
 RctSys::RctSys(void)
+  : current_process_defined(false)
 {
-	ctx_aut = nullptr;
+  ctx_aut = nullptr;
+  gen_ctxaut_progressive_closure = false;
 }
 
 bool RctSys::hasEntity(std::string name)
 {
-    if (entities_names.find(name) == entities_names.end())
-        return false;
-    else
-        return true;
+  if (entities_names.find(name) == entities_names.end()) {
+    return false;
+  }
+  else {
+    return true;
+  }
 }
 
 void RctSys::addEntity(std::string name)
 {
-    if (!hasEntity(name))
-    {
-        Entity new_entity_id = entities_ids.size();
+  if (!hasEntity(name)) {
+    Entity new_entity_id = entities_ids.size();
 
-        VERB_L2("Adding entity: " << name << " index=" << new_entity_id);
+    VERB_L2("Adding entity: " << name << " index=" << new_entity_id);
 
-        entities_ids.push_back(name);		
-        entities_names[name] = new_entity_id;
-    }
+    entities_ids.push_back(name);
+    entities_names[name] = new_entity_id;
+  }
 }
 
 std::string RctSys::getEntityName(Entity entityID)
 {
-    if (entityID < entities_ids.size())
-        return entities_ids[entityID];
-    else
-    {
-        FERROR("No such entity ID: " << entityID);
-        return "??";
-    }
+  if (entityID < entities_ids.size()) {
+    return entities_ids[entityID];
+  }
+  else {
+    FERROR("No such entity ID: " << entityID);
+    return "??";
+  }
 }
 
 Entity RctSys::getEntityID(std::string name)
 {
-    if (!hasEntity(name))
-    {
-        FERROR("No such entity: " << name);
-    }
-    return entities_names[name];
+  if (!hasEntity(name)) {
+    FERROR("No such entity: " << name);
+  }
+
+  return entities_names[name];
+}
+
+void RctSys::setCurrentProcess(std::string processName)
+{
+  VERB_LN(2, "Current Process: " << processName);
+
+  if (!hasProcess(processName)) {
+    addProcess(processName);
+  }
+
+  current_proc_id = getProcessID(processName);
+  current_process_defined = true;
+}
+
+void RctSys::addProcess(std::string processName)
+{
+  if (!hasProcess(processName)) {
+    Process new_proc_id = processes_ids.size();
+
+    VERB_L2("Adding process: " << processName << " index=" << new_proc_id);
+
+    processes_ids.push_back(processName);
+    processes_names[processName] = new_proc_id;
+
+    // reactions for the new process
+    proc_reactions[new_proc_id] = Reactions();
+    assert(proc_reactions.size() == new_proc_id + 1);
+  }
+}
+
+bool RctSys::hasProcess(std::string processName)
+{
+  if (processes_names.find(processName) == processes_names.end()) {
+    return false;
+  }
+  else {
+    return true;
+  }
+}
+
+bool RctSys::hasProcess(Process processID)
+{
+  if (processID >= processes_ids.size()) {
+    return false;
+  }
+
+  return true;
+}
+
+Process RctSys::getProcessID(std::string processName)
+{
+  if (!hasProcess(processName)) {
+    FERROR("No such process: " << processName);
+  }
+
+  return processes_names[processName];
+}
+
+std::string RctSys::getProcessName(Process processID)
+{
+  if (hasProcess(processID)) {
+    return processes_ids[processID];
+  }
+  else {
+    FERROR("No such process ID: " << processID);
+  }
 }
 
 void RctSys::pushReactant(std::string entityName)
 {
-    if (!hasEntity(entityName))
-        addEntity(entityName);
-    tmpReactants.insert(getEntityID(entityName));
+  if (!hasEntity(entityName)) {
+    addEntity(entityName);
+  }
+
+  tmpReactants.insert(getEntityID(entityName));
 }
 void RctSys::pushInhibitor(std::string entityName)
 {
-    if (!hasEntity(entityName))
-        addEntity(entityName);
-    tmpInhibitors.insert(getEntityID(entityName));
+  if (!hasEntity(entityName)) {
+    addEntity(entityName);
+  }
+
+  tmpInhibitors.insert(getEntityID(entityName));
 }
 void RctSys::pushProduct(std::string entityName)
 {
-    if (!hasEntity(entityName))
-        addEntity(entityName);
-    tmpProducts.insert(getEntityID(entityName));
+  if (!hasEntity(entityName)) {
+    addEntity(entityName);
+  }
+
+  tmpProducts.insert(getEntityID(entityName));
+}
+
+void RctSys::addReactionForCurrentProcess(Reaction reaction)
+{
+  if (!current_process_defined) {
+    FERROR("Internal error. Current process is not set!");
+  }
+
+  proc_reactions[current_proc_id].push_back(reaction);
 }
 
 void RctSys::commitReaction(void)
 {
-    VERB_L3("Saving reaction");
+  VERB_L3("Saving reaction");
 
-    Reaction r;
+  Reaction r;
 
-    r.rctt = tmpReactants;
-    r.inhib = tmpInhibitors;
-    r.prod = tmpProducts;
+  r.rctt = tmpReactants;
+  r.inhib = tmpInhibitors;
+  r.prod = tmpProducts;
 
-    reactions.push_back(r);
+  addReactionForCurrentProcess(r);
 
-    tmpReactants.clear();
-    tmpInhibitors.clear();
-    tmpProducts.clear();
+  tmpReactants.clear();
+  tmpInhibitors.clear();
+  tmpProducts.clear();
 }
 
 std::string RctSys::entitiesToStr(const Entities &entities)
 {
-    std::string s = " ";
-    for (auto a = entities.begin(); a != entities.end(); ++a)
-    {
-        s += entityToStr(*a) + " ";
-    }
-    return s;
+  std::string s = " ";
+
+  for (auto a = entities.begin(); a != entities.end(); ++a) {
+    s += entityToStr(*a) + " ";
+  }
+
+  return s;
+}
+
+std::string RctSys::procEntitiesToStr(const EntitiesForProc &procEntities)
+{
+  std::string s = "";
+
+  for (auto const &p : procEntities) {
+    s += getProcessName(p.first) + "={" + entitiesToStr(p.second) + "} ";
+  }
+
+  return s;
 }
 
 void RctSys::showReactions(void)
 {
-    cout << "# Reactions:" << endl;
-    for (auto r = reactions.begin(); r != reactions.end(); ++r)
-    {
-        cout << " * (R={" << entitiesToStr(r->rctt) << "},"
-             << "I={" << entitiesToStr(r->inhib) << "}," 
-             << "P={" << entitiesToStr(r->prod) << "})" << endl;
-    } 
+  cout << "# Reactions:" << endl;
+
+  for (unsigned int proc_id = 0; proc_id < processes_ids.size(); ++proc_id) {
+    cout << endl;
+    cout << "  . proc = \"" << getProcessName(proc_id) << "\":" << endl;
+
+    for (const auto &r : proc_reactions[proc_id]) {
+      cout << "     * (R={" << entitiesToStr(r.rctt) << "},"
+           << "I={" << entitiesToStr(r.inhib) << "},"
+           << "P={" << entitiesToStr(r.prod) << "})" << endl;
+    }
+  }
+
+  cout << endl;
 }
 
 void RctSys::pushStateEntity(std::string entityName)
 {
-    if (!hasEntity(entityName))
-    {
-        FERROR("No such entity: " << entityName);
-    }
-    tmpState.insert(getEntityID(entityName)); 
+  if (!hasEntity(entityName)) {
+    FERROR("No such entity: " << entityName);
+  }
+
+  tmpState.insert(getEntityID(entityName));
 }
 
 void RctSys::commitInitState(void)
 {
-	if (ctx_aut != nullptr)
-	{
-		FERROR("Initial RS states must not be used with context automaton");
-	}
-    initStates.insert(tmpState); 
-    tmpState.clear();
+  if (ctx_aut != nullptr) {
+    FERROR("Initial RS states must not be used with context automaton");
+  }
+
+  initStates.insert(tmpState);
+  tmpState.clear();
 }
 
 void RctSys::addActionEntity(std::string entityName)
 {
-    if (!hasEntity(entityName))
-        addEntity(entityName);
-    actionEntities.insert(getEntityID(entityName));
+  if (!hasEntity(entityName)) {
+    addEntity(entityName);
+  }
+
+  actionEntities.insert(getEntityID(entityName));
 }
 
 void RctSys::addActionEntity(Entity entity)
 {
-	if (!isActionEntity(entity))
-	    actionEntities.insert(entity);
+  if (!isActionEntity(entity)) {
+    actionEntities.insert(entity);
+  }
 }
 
 bool RctSys::isActionEntity(Entity entity)
 {
-    if (actionEntities.count(entity) > 0)
-        return true;
-    else
-        return false;
+  if (actionEntities.count(entity) > 0) {
+    return true;
+  }
+  else {
+    return false;
+  }
 }
 
 void RctSys::showActionEntities(void)
 {
-    cout << "# Context entities:";
-    for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a)
-    {
-        cout << " " << getEntityName(*a);
-    }
-    cout << endl;
+  cout << "# Context entities:";
+
+  for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a) {
+    cout << " " << getEntityName(*a);
+  }
+
+  cout << endl;
 }
 
 void RctSys::showInitialStates(void)
 {
-    cout << "# Initial states:" << endl;
-    for (auto s = initStates.begin(); s != initStates.end(); ++s)
-    {
-        cout << " *";
-        for (auto a = s->begin(); a != s->end(); ++a)
-        {
-            cout << " " << getEntityName(*a);
-        }
-        cout << endl;
+  cout << "# Initial states:" << endl;
+
+  for (auto s = initStates.begin(); s != initStates.end(); ++s) {
+    cout << " *";
+
+    for (auto a = s->begin(); a != s->end(); ++a) {
+      cout << " " << getEntityName(*a);
     }
+
+    cout << endl;
+  }
 }
 
 void RctSys::printSystem(void)
 {
-	if (!usingContextAutomaton())
-	    showInitialStates();
-    showActionEntities();
-    showReactions();
-	
-	if (ctx_aut != nullptr) ctx_aut->printAutomaton();
+  if (!usingContextAutomaton()) {
+    showInitialStates();
+  }
+
+  showActionEntities();
+  showReactions();
+
+  if (ctx_aut != nullptr) {
+    ctx_aut->printAutomaton();
+  }
 }
 
 void RctSys::ctxAutEnable(void)
 {
-	assert(ctx_aut == nullptr);
-	if (initStatesDefined())
-	{
-		FERROR("Initial states must not be defined if using context automaton");
-	}
-	ctx_aut = new CtxAut(opts, this);
+  assert(ctx_aut == nullptr);
+
+  if (initStatesDefined()) {
+    FERROR("Initial states must not be defined if using context automaton");
+  }
+
+  ctx_aut = new CtxAut(opts, this);
+}
+
+void RctSys::ctxAutEnableProgressiveClosure(void)
+{
+  gen_ctxaut_progressive_closure = true;
 }
 
 void RctSys::ctxAutAddState(std::string stateName)
 {
-	assert(ctx_aut != nullptr);
-	ctx_aut->addState(stateName);
+  assert(ctx_aut != nullptr);
+  ctx_aut->addState(stateName);
 }
 
 void RctSys::ctxAutSetInitState(std::string stateName)
 {
-	assert(ctx_aut != nullptr);
-	ctx_aut->setInitState(stateName);
+  assert(ctx_aut != nullptr);
+  ctx_aut->setInitState(stateName);
 }
 
-void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateName)
+void RctSys::ctxAutAddTransition(std::string srcStateName,
+                                 std::string dstStateName)
 {
-	assert(ctx_aut != nullptr);
-	ctx_aut->addTransition(srcStateName, dstStateName);
+  assert(ctx_aut != nullptr);
+  ctx_aut->addTransition(srcStateName, dstStateName, nullptr);
+}
+
+void RctSys::ctxAutAddTransition(std::string srcStateName,
+                                 std::string dstStateName, StateConstr *stateConstr)
+{
+  assert(ctx_aut != nullptr);
+  ctx_aut->addTransition(srcStateName, dstStateName, stateConstr);
 }
 
 void RctSys::ctxAutPushNamedContextEntity(std::string entityName)
 {
-	assert(ctx_aut != nullptr);
-	
-	Entity entity_id = getEntityID(entityName);
+  assert(ctx_aut != nullptr);
 
-	//
-	// We mark the entity as an action entity
-	//
-	// 	This step is required to ensure the minimal number of
-	//  BDD variables used in the encoding of the context sets
-	//
-	addActionEntity(entity_id);
-	
-	ctx_aut->pushContextEntity(entity_id);
+  Entity entity_id = getEntityID(entityName);
+
+  //
+  // We mark the entity as an action entity
+  //
+  //  This step is required to ensure the minimal number of
+  //  BDD variables used in the encoding of the context sets
+  //
+  addActionEntity(entity_id);
+
+  ctx_aut->pushContextEntity(entity_id);
+}
+
+void RctSys::ctxAutSaveCurrentContextSet(std::string processName)
+{
+  Process processID = getProcessID(processName);
+  ctx_aut->saveCurrentContextSet(processID);
+}
+
+void RctSys::ctxAutFinalise(void)
+{
+  if (gen_ctxaut_progressive_closure) {
+    ctx_aut->makeProgressive();
+  }
 }
 
 /** EOF **/
diff --git a/rs.hh b/rs.hh
index 00bf7fa..e872da3 100644
--- a/rs.hh
+++ b/rs.hh
@@ -25,83 +25,122 @@ using std::cout;
 using std::endl;
 
 class CtxAut;
+class StateConstr;
 
 class RctSys
 {
-	    friend class SymRS;
-	    friend class SymRSstate;
+    friend class SymRS;
+    friend class SymRSstate;
 
-	public:
-		RctSys(void);
-	    void setOptions(Options *opts)
-	    {
-	        this->opts = opts;
-	    }
-	    bool hasEntity(std::string entityName);
-	    void addEntity(std::string entityName);
-	    std::string getEntityName(Entity entityID);
-	    void pushReactant(std::string entityName);
-	    void pushInhibitor(std::string entityName);
-	    void pushProduct(std::string entityName);
-	    void commitReaction(void);
-	    std::string entityToStr(const Entity entity) {
-	        return entities_ids[entity];
-	    }
-	    std::string entitiesToStr(const Entities &entities);
-	    void showReactions(void);
-	    void pushStateEntity(std::string entityName);
-	    void commitInitState(void);
-	    void addActionEntity(std::string entityName);
-	    void addActionEntity(Entity entity);
-	    bool isActionEntity(Entity entity);
-	    void resetInitStates(void) {
-	        initStates.clear();
-	    }
-	    unsigned int getEntitiesSize(void) {
-	        return entities_ids.size();
-	    }
-	    unsigned int getReactionsSize(void) {
-	        return reactions.size();
-	    }
-	    unsigned int getActionsSize(void) {
-	        return actionEntities.size();
-	    }
-	    void showInitialStates(void);
-	    void showActionEntities(void);
-	    void printSystem(void);
+  public:
+    RctSys(void);
 
-		void ctxAutEnable(void);		
-		void ctxAutAddState(std::string stateName);
-		void ctxAutSetInitState(std::string stateName);
-		void ctxAutAddTransition(std::string srcStateName, std::string dstStateName);
-		void ctxAutPushNamedContextEntity(std::string entity_name);
-		
-		bool initStatesDefined(void) { return initStates.size() != 0; }
-		bool usingContextAutomaton(void) { return ctx_aut != nullptr; }
-		
-	private:
-	    Reactions reactions;
-	    EntitiesSets initStates;
+    void setOptions(Options *opts)
+    {
+      this->opts = opts;
+    }
+    bool hasEntity(std::string entityName);
+    void addEntity(std::string entityName);
+    std::string getEntityName(Entity entityID);
 
-	    Entities actionEntities;
+    void setCurrentProcess(std::string processName);
+    void addProcess(std::string processName);
+    bool hasProcess(Process processID);
+    bool hasProcess(std::string processName);
+    Process getProcessID(std::string processName);
+    std::string getProcessName(Process processID);
 
-		CtxAut *ctx_aut;
+    void addReactionForCurrentProcess(Reaction reaction);
 
-	    EntitiesByIds entities_ids;
-	    EntitiesByName entities_names;
+    void pushReactant(std::string entityName);
+    void pushInhibitor(std::string entityName);
+    void pushProduct(std::string entityName);
+    void commitReaction(void);
+    std::string entityToStr(const Entity entity)
+    {
+      return entities_ids[entity];
+    }
+    std::string entitiesToStr(const Entities &entities);
+    std::string procEntitiesToStr(const EntitiesForProc &procEntities);
+    void showReactions(void);
+    void pushStateEntity(std::string entityName);
+    void commitInitState(void);
+    void addActionEntity(std::string entityName);
+    void addActionEntity(Entity entity);
+    bool isActionEntity(Entity entity);
+    void resetInitStates(void)
+    {
+      initStates.clear();
+    }
+    unsigned int getEntitiesSize(void)
+    {
+      return entities_ids.size();
+    }
+    unsigned int getActionsSize(void)
+    {
+      return actionEntities.size();
+    }
+    void showInitialStates(void);
+    void showActionEntities(void);
+    void printSystem(void);
 
-	    Entities tmpReactants;
-	    Entities tmpInhibitors;
-	    Entities tmpProducts;
+    void ctxAutEnable(void);
+    void ctxAutEnableProgressiveClosure(void);
+    void ctxAutAddState(std::string stateName);
+    void ctxAutSetInitState(std::string stateName);
+    void ctxAutAddTransition(std::string srcStateName, std::string dstStateName);
+    void ctxAutAddTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr);
+    void ctxAutPushNamedContextEntity(std::string entity_name);
+    void ctxAutSaveCurrentContextSet(std::string processName);
+    void ctxAutFinalise(void);
 
-	    Entities tmpState;
+    bool initStatesDefined(void)
+    {
+      return initStates.size() != 0;
+    }
+    bool usingContextAutomaton(void)
+    {
+      return ctx_aut != nullptr;
+    }
 
-	    Options *opts;
+    size_t getNumberOfProcesses(void)
+    {
+      return processes_ids.size();
+    }
 
-	    Entity getEntityID(std::string entityName);
+  private:
+
+    ReactionsForProc proc_reactions;
+
+    EntitiesSets initStates;
+
+    Entities actionEntities;
+
+    CtxAut *ctx_aut;
+
+    bool gen_ctxaut_progressive_closure;
+
+    EntitiesById entities_ids;
+    EntitiesByName entities_names;
+
+    ProcessesById processes_ids;
+    ProcessesByName processes_names;
+
+    Process current_proc_id;
+    bool current_process_defined;
+
+    Entities tmpReactants;
+    Entities tmpInhibitors;
+    Entities tmpProducts;
+
+    Entities tmpState;
+
+    Options *opts;
+
+    Entity getEntityID(std::string entityName);
 
 };
 
 #endif
 
-/** EOF **/
\ No newline at end of file
+/** EOF **/
diff --git a/rsin_driver.cc b/rsin_driver.cc
index c78679a..0c50b29 100644
--- a/rsin_driver.cc
+++ b/rsin_driver.cc
@@ -1,62 +1,68 @@
 #include "rsin_driver.hh"
 #include "rsin_parser.hh"
 
+#include "rs.hh"
+
 rsin_driver::rsin_driver(void)
-: trace_scanning(false), trace_parsing(false)
+  : trace_scanning(false), trace_parsing(false)
 {
-	initialise();
+  initialise();
 }
 
 rsin_driver::rsin_driver(RctSys *rs)
-: trace_scanning(false), trace_parsing(false)
+  : trace_scanning(false), trace_parsing(false)
 {
-	initialise();
-	this->rs = rs;
+  initialise();
+  this->rs = rs;
 }
 
 void rsin_driver::initialise(void)
 {
-    rs = nullptr;
-    rsctlform = nullptr;
-	opts = nullptr;
-	use_ctx_aut = false;
-	use_concentrations = false;
+  rs = nullptr;
+  opts = nullptr;
+  use_ctx_aut = false;
+  use_concentrations = false;
+  make_progressive = false;
 }
 
 rsin_driver::~rsin_driver ()
 {
-	// placeholder
+  // placeholder
 }
 
 int rsin_driver::parse(const std::string &f)
 {
-    file = f;
-    scan_begin();
-    yy::rsin_parser parser(*this);
-    parser.set_debug_level(trace_parsing);
-    int res = parser.parse();
-    scan_end();
-    return res;
+  file = f;
+  scan_begin();
+  yy::rsin_parser parser(*this);
+  parser.set_debug_level(trace_parsing);
+  int res = parser.parse();
+  scan_end();
+  return res;
 }
 
 void rsin_driver::error(const yy::location &l, const std::string &m)
 {
-    std::cerr << l << ": " << m << std::endl;
+  std::cerr << l << ": " << m << std::endl;
 }
 
 void rsin_driver::error(const std::string &m)
 {
-    std::cerr << m << std::endl;
+  std::cerr << m << std::endl;
 }
 
-FormRSCTL *rsin_driver::getFormRSCTL(void)
+void rsin_driver::addFormRSCTLK(std::string propertyName, FormRSCTLK *f)
 {
-    if (rsctlform == nullptr)
-    {
-        FERROR("RSCTL formula was not supplied!");
-    }
+  properties[propertyName] = f;
+};
 
-    return rsctlform;
+FormRSCTLK *rsin_driver::getFormRSCTLK(std::string propertyName)
+{
+  if (properties.count(propertyName) == 0) {
+    FERROR("Property/formula label does not exist: " << propertyName);
+  }
+
+  return properties[propertyName];
 }
 
 //
@@ -64,40 +70,53 @@ FormRSCTL *rsin_driver::getFormRSCTL(void)
 //
 void rsin_driver::ensureOptionsAllowed(void)
 {
-	if (rs != nullptr)
-	{
-		FERROR("Options cannot be set/modified after the reaction system is initialised")
-	}
+  if (rs != nullptr) {
+    FERROR("Options cannot be set/modified after the reaction system is initialised")
+  }
 }
 
 void rsin_driver::ensureReactionSystemReady(void)
 {
-	if (rs == nullptr)
-		setupReactionSystem();
+  if (rs == nullptr) {
+    setupReactionSystem();
+  }
 }
 
 void rsin_driver::setupReactionSystem(void)
 {
-	assert(rs == nullptr);
-	rs = new RctSys;
-	
-	if (use_ctx_aut) VERB("Using RS with CA")
-	else VERB("Using ordinary RS")
+  assert(rs == nullptr);
+  rs = new RctSys;
 
-	rs->setOptions(opts);
+  if (use_ctx_aut) VERB("Using RS with CA")
+    else VERB("Using ordinary RS")
+
+      rs->setOptions(opts);
 }
 
 RctSys *rsin_driver::getReactionSystem(void)
 {
-	ensureReactionSystemReady();
-	assert(rs != nullptr);
-	return rs;
+  ensureReactionSystemReady();
+  assert(rs != nullptr);
+  return rs;
 }
 
 void rsin_driver::useContextAutomaton(void)
 {
-	ensureOptionsAllowed(); 
-	use_ctx_aut = true; 
-	getReactionSystem()->ctxAutEnable();
+  ensureOptionsAllowed();
+  use_ctx_aut = true;
+  getReactionSystem()->ctxAutEnable();
 }
 
+void rsin_driver::makeProgressive(void)
+{
+  make_progressive = true;
+
+  if (use_ctx_aut) {
+    getReactionSystem()->ctxAutEnableProgressiveClosure();
+  }
+  else {
+    FERROR("Context automaton not enabled");
+  }
+}
+
+// EOF
diff --git a/rsin_driver.hh b/rsin_driver.hh
index f150146..7661ff9 100644
--- a/rsin_driver.hh
+++ b/rsin_driver.hh
@@ -3,8 +3,8 @@
 #include <string>
 #include <map>
 #include "rsin_parser.hh"
-#include "rs.hh"
-#include "formrsctl.hh"
+// #include "rs.hh"
+#include "formrsctlk.hh"
 #include "options.hh"
 
 // Tell Flex the lexer's prototype ...
@@ -16,21 +16,26 @@
 // ... and declare it for the parser's sake.
 YY_DECL;
 
+class RctSys;
+class CtxAut;
+
 // Conducting the whole scanning an parsing of RS
 class rsin_driver
 {
-public:
+  public:
     rsin_driver(void);
     rsin_driver(RctSys *rs);
     virtual ~rsin_driver();
 
     //std::map<std::string, int> variables;
-    FormRSCTL *rsctlform;
     Options *opts;
-	
-	// options in configuration file:
-	bool use_ctx_aut;
-	bool use_concentrations;
+
+    std::map<std::string, FormRSCTLK *> properties;
+
+    // options in configuration file:
+    bool use_ctx_aut;
+    bool use_concentrations;
+    bool make_progressive;
 
     // Handling the scanner
     void scan_begin();
@@ -41,29 +46,36 @@ public:
     std::string file;
     bool trace_parsing;
 
-	void setOptions(Options *opts) 		{ this->opts = opts; };
-    void addFormRSCTL(FormRSCTL *f) 	{ rsctlform = f; };
-    FormRSCTL *getFormRSCTL(void);
+    void setOptions(Options *opts)
+    {
+      this->opts = opts;
+    };
+    void addFormRSCTLK(std::string propertyName, FormRSCTLK *f);
 
-	void ensureOptionsAllowed(void);
-	void useContextAutomaton(void);
-	void useConcentrations(void)		{ ensureOptionsAllowed(); use_concentrations = true; };
-	
-	void ensureReactionSystemReady(void);
-	void setupReactionSystem(void);
-	
-	RctSys *getReactionSystem(void);
-	CtxAut *getCtxAut(void);
+    FormRSCTLK *getFormRSCTLK(std::string propertyName);
+
+    void ensureOptionsAllowed(void);
+    void useContextAutomaton(void);
+    void useConcentrations(void)
+    {
+      ensureOptionsAllowed();
+      use_concentrations = true;
+    };
+    void makeProgressive(void);
+    void ensureReactionSystemReady(void);
+    void setupReactionSystem(void);
+
+    RctSys *getReactionSystem(void);
+    CtxAut *getCtxAut(void);
 
     // Error handling.
     void error(const yy::location &l, const std::string &m);
     void error(const std::string &m);
-	
-private:
+
+  private:
     RctSys *rs;
 
-	void initialise(void);
+    void initialise(void);
 };
 
 #endif
-
diff --git a/rsin_parser.ll b/rsin_parser.ll
index ba2cbf8..668a117 100644
--- a/rsin_parser.ll
+++ b/rsin_parser.ll
@@ -38,34 +38,39 @@ blank [ \t]
   typedef yy::rsin_parser::token token;
 %}
 
-"options"				return token::OPTIONS;
+"options"				        return token::OPTIONS;
 "use-context-automaton"	return token::USE_CTX_AUT;
-"use-concentrations"	return token::USE_CONCENTRATIONS;
+"use-concentrations"	  return token::USE_CONCENTRATIONS;
+"make-progressive"      return token::MAKE_PROGRESSIVE;
 "reactions"             return token::REACTIONS;
 "initial-contexts"      return token::INITIALCONTEXTS;
 "context-entities"      return token::CONTEXTENTITIES;
-"context-automaton"		return token::CONTEXTAUTOMATON;
-"transitions"			return token::TRANSITIONS;
-"states"				return token::STATES;
-"init-state"			return token::INITSTATE;
-"rsctl-property"        return token::RSCTLFORM;
+"context-automaton"		  return token::CONTEXTAUTOMATON;
+"transitions"			      return token::TRANSITIONS;
+"states"				        return token::STATES;
+"init-state"			      return token::INITSTATE;
+"rsctlk-property"        return token::RSCTLKFORM;
 "{"                     return token::LCB;
 "}"                     return token::RCB;
 "("                     return token::LRB;
 ")"                     return token::RRB;
 "["                     return token::LSB;
 "]"                     return token::RSB;
-"<"						return token::LAB;
-">"						return token::RAB;
-":"						return token::COL;
+"="						          return token::EQ;
+"<"						          return token::LAB;
+">"						          return token::RAB;
+":"						          return token::COL;
 ";"                     return token::SEMICOL;
+"."                     return token::DOT;
 ","                     return token::COMMA;
 "->"                    return token::RARR;
 "AND"                   return token::AND;
 "OR"                    return token::OR;
-"XOR"					return token::XOR;
+"XOR"					          return token::XOR;
 "IMPLIES"               return token::IMPLIES;
 "~"                     return token::NOT;
+"A"                     return token::A;
+"E"                     return token::E;
 "EX"                    return token::EX;
 "EU"                    return token::EU;
 "EF"                    return token::EF;
@@ -74,12 +79,18 @@ blank [ \t]
 "AU"                    return token::AU;
 "AF"                    return token::AF;
 "AG"                    return token::AG;
-"E"                     return token::E;
-"A"                     return token::A;
 "X"                     return token::X;
 "U"                     return token::U;
 "F"                     return token::F;
 "G"                     return token::G;
+"K"                     return token::UK;
+"C"                     return token::UC;
+"D"                     return token::UD;
+"UE"                    return token::UE;
+"NK"                    return token::NK;
+"NC"                    return token::NC;
+"ND"                    return token::ND;
+"NE"                    return token::NE;
 "empty"                 return token::EMPTY;
 "#".*                   ;
 
@@ -118,4 +129,3 @@ rsin_driver::scan_end()
 {
   fclose(yyin);
 }
-
diff --git a/rsin_parser.yy b/rsin_parser.yy
index 1038cec..0f1ad96 100644
--- a/rsin_parser.yy
+++ b/rsin_parser.yy
@@ -6,7 +6,9 @@
 %code requires {
 #include <string>
 #include <set>
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
+#include "rs.hh"
+// #include "stateconstr.hh"
 
 using std::set;
 using std::string;
@@ -33,38 +35,40 @@ class rsin_driver;
 {
     int ival;
     std::string *sval;
-    FormRSCTL *frsctl;
-    Entity_f *ent;
-    Action_f *act;
-    ActionsVec_f *actionsVec;
-	BoolContexts *fboolctx;
+    FormRSCTLK *frsctlk;
+    // Entity_f *ent;
+    // Action_f *act;
+    // ActionsVec_f *actionsVec;
+    StateConstr *fstc;
+    Agents_f *agents;
 };
 
 %code {
 #include "rsin_driver.hh"
 }
 
-%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS
-%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM
+%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS MAKE_PROGRESSIVE
+%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLKFORM
 %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
-%token LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR
+%token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL DOT COMMA RARR
 %token AND OR XOR IMPLIES NOT
-%token EX EU EF EG AX AU AF AG E A X U F G EMPTY
+%token EX EU EF EG AX AU AF AG E A X U F G UK UC UD UE NK NC ND NE EMPTY
 
 %token        END      0 "end of file"
 %token <sval> IDENTIFIER "identifier"
 %token <ival> NUMBER     "number"
 
 %left AND OR XOR IMPLIES NOT
-%left EX EU EF EG AX AU AF AG E A X U F G
+%left EX EU EF EG AX AU AF AG E A X U F G UK UC UD UE NK NC ND NE
 
 //%right SRB
 
-%type <frsctl> rsctl_form
-%type <ent> f_entity
-%type <act> action
-%type <actionsVec> actions
-%type <fboolctx> bool_contexts
+%type <frsctlk> rsctlk_form
+// %type <ent> f_entity
+// %type <act> action
+// %type <actionsVec> actions
+%type <fstc> state_constr
+%type <agents> agents;
 
 //%printer    { yyoutput << *$$; } "identifier"
 %destructor { delete $$; } "identifier"
@@ -75,35 +79,54 @@ class rsin_driver;
 
 %start system;
 
-system: 
-	| OPTIONS LCB options RCB system
-    | REACTIONS LCB reactions RCB 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);
-    }
-    ;
+system:
+	| OPTIONS LCB options RCB SEMICOL system
+  | REACTIONS LCB reactionsets RCB SEMICOL system
+  | INITIALCONTEXTS LCB initstates RCB SEMICOL system
+  | CONTEXTENTITIES LCB actionentities RCB SEMICOL system
+	| CONTEXTAUTOMATON LCB ctxaut RCB SEMICOL system
+  {
+    driver.getReactionSystem()->ctxAutFinalise();
+  }
+  | RSCTLKFORM LCB IDENTIFIER COL rsctlk_form RCB SEMICOL system {
+    driver.addFormRSCTLK(*$3, $5);
+    free($3);
+  }
+  ;
 
 options:
 	| options option SEMICOL
 	;
 
 option:
-	| USE_CTX_AUT { 
-		driver.useContextAutomaton(); 
+	| USE_CTX_AUT {
+		driver.useContextAutomaton();
 	}
 	| USE_CONCENTRATIONS {
 		driver.useConcentrations();
 	}
+  | MAKE_PROGRESSIVE {
+    driver.makeProgressive();
+  }
 	;
 
-/* 
+/*
  * -------------------------
- *         REACTIONS 
+ *         REACTIONS
  * -------------------------
  */
+
+reactionsets:
+	| reactionsets process_reactions
+	;
+
+process_reactions: processname LCB reactions RCB SEMICOL
+
+processname: IDENTIFIER {
+		driver.getReactionSystem()->setCurrentProcess(*$1);
+		free($1);
+	}
+
 reactions:
     | reactions reaction SEMICOL
     ;
@@ -131,7 +154,7 @@ reactant: IDENTIFIER {
 
 inhibitors:
     inhibitor
-    | inhibitors COMMA inhibitor 
+    | inhibitors COMMA inhibitor
     ;
 
 inhibitor:
@@ -165,7 +188,7 @@ initstates:
 
 initstate:
     | entity
-    | initstate COMMA entity 
+    | initstate COMMA entity
     ;
 
 entity: IDENTIFIER {
@@ -176,7 +199,7 @@ entity: IDENTIFIER {
 
 /*******************************************/
 
-actionentities: 
+actionentities:
     | actentity
     | actionentities COMMA actentity
     ;
@@ -186,13 +209,13 @@ actentity: IDENTIFIER {
         free($1);
     }
     ;
-	
+
 /*******************************************/
 
 ctxaut:
-	| STATES LCB autstates RCB ctxaut
-	| INITSTATE LCB autinitstate RCB ctxaut
-	| TRANSITIONS LCB auttransitions RCB ctxaut
+	| STATES LCB autstates RCB SEMICOL ctxaut
+	| INITSTATE LCB autinitstate RCB SEMICOL ctxaut
+	| TRANSITIONS LCB auttransitions RCB SEMICOL ctxaut
 	;
 
 autstate: IDENTIFIER {
@@ -211,24 +234,39 @@ autinitstate: IDENTIFIER {
 		free($1);
 	}
 	;
-	
+
 auttransitions:
 	| auttrans
 	| auttrans SEMICOL auttransitions
-	;	
+	;
 
-auttrans: LCB contextset RCB COL IDENTIFIER RARR IDENTIFIER {
+auttrans: LCB proc_ctxsets RCB COL IDENTIFIER RARR IDENTIFIER {
 		driver.getReactionSystem()->ctxAutAddTransition(*$5, *$7);
 		free($5);
 		free($7);
 	}
+    | LCB proc_ctxsets RCB COL IDENTIFIER RARR IDENTIFIER COL state_constr {
+        driver.getReactionSystem()->ctxAutAddTransition(*$5, *$7, $9);
+        free($5);
+        free($7);
+    }
 	;
-	
+
+proc_ctxsets:
+  | proc_ctxsets single_proc_ctxset
+  ;
+
+single_proc_ctxset: IDENTIFIER EQ LCB contextset RCB {
+  driver.getReactionSystem()->ctxAutSaveCurrentContextSet(*$1);
+		free($1);
+	}
+	;
+
 contextset:
-	ctxentity
+	| ctxentity
 	| contextset COMMA ctxentity
 	;
-		
+
 ctxentity: IDENTIFIER {
 		driver.getReactionSystem()->ctxAutPushNamedContextEntity(*$1);
 		free($1);
@@ -236,157 +274,199 @@ ctxentity: IDENTIFIER {
 	;
 
 /* formulae */
-	
-bool_contexts: IDENTIFIER {
-        $$ = new BoolContexts(*$1);
+
+state_constr: IDENTIFIER DOT IDENTIFIER {
+        $$ = new StateConstr(*$1, *$3);
         free($1);
+        free($3);
     }
-    | NOT bool_contexts {
-        $$ = new BoolContexts(BCTX_NOT, $2);
+    | NOT state_constr {
+        $$ = new StateConstr(STC_NOT, $2);
     }
-    | LRB bool_contexts RRB {
+    | LRB state_constr RRB {
         $$ = $2;
     }
-    | bool_contexts AND bool_contexts {
-        $$ = new BoolContexts(BCTX_AND, $1, $3);
+    | state_constr AND state_constr {
+        $$ = new StateConstr(STC_AND, $1, $3);
     }
-    | bool_contexts OR bool_contexts {
-        $$ = new BoolContexts(BCTX_OR, $1, $3);
+    | state_constr OR state_constr {
+        $$ = new StateConstr(STC_OR, $1, $3);
     }
-    | bool_contexts XOR bool_contexts {
-        $$ = new BoolContexts(BCTX_XOR, $1, $3);
+    | state_constr XOR state_constr {
+        $$ = new StateConstr(STC_XOR, $1, $3);
     }
 	;
 
-actions:
-    LCB action RCB {
-        $$ = new ActionsVec_f;
-        $$->push_back(*$2);
-        free($2);
-    }
-    | actions COMMA LCB action RCB {
-        $$ = $1;
-        $$->push_back(*$4);
-        free($4);
-    }
-    ;
+// actions:
+//     LCB action RCB {
+//         $$ = new ActionsVec_f;
+//         $$->push_back(*$2);
+//         free($2);
+//     }
+//     | actions COMMA LCB action RCB {
+//         $$ = $1;
+//         $$->push_back(*$4);
+//         free($4);
+//     }
+//     ;
 
-action:
-    { 
-        $$ = new Action_f;
-    } 
-    | f_entity {
-        $$ = new Action_f;
-        $$->insert(*$1);
-        free($1);
+// action:
+//     {
+//         $$ = new Action_f;
+//     }
+//     | f_entity {
+//         $$ = new Action_f;
+//         $$->insert(*$1);
+//         free($1);
+//     }
+//     | action COMMA f_entity {
+//         $$ = $1;
+//         $$->insert(*$3);
+//         free($3);
+//     }
+//     ;
+
+// f_entity: IDENTIFIER {
+//         $$ = new Entity_f(*$1);
+//         free($1);
+//     }
+//     ;
+
+agents:
+    IDENTIFIER {
+      Agents_f *ag = new Agents_f;
+      ag->insert(*$1);
+      free($1);
+      $$ = ag;
     }
-    | action COMMA f_entity {
-        $$ = $1;        
-        $$->insert(*$3);
+    | agents COMMA IDENTIFIER {
+      $1->insert(*$3);
+      free($3);
+      $$ = $1;
+    }
+
+rsctlk_form:
+    IDENTIFIER DOT IDENTIFIER {
+        $$ = new FormRSCTLK(*$1, *$3);
+        free($1);
         free($3);
     }
-    ;
-
-f_entity: IDENTIFIER {
-        $$ = new Entity_f(*$1);
-        free($1);
+    | NOT rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_NOT, $2);
     }
-    ;
-
-rsctl_form: IDENTIFIER {
-        $$ = new FormRSCTL(*$1);
-        free($1);
-    }
-    | NOT rsctl_form {
-        $$ = new FormRSCTL(RSCTL_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);
     }
-    | E LSB actions RSB X rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
+    | UK LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_UK, *$3, $6);
+        free($3);
     }
-    | E LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
-        $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
+    | NK LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_NK, *$3, $6);
+        free($3);
     }
-    | E LSB actions RSB F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
+    | UE LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_UE, *$3, $6);
+        free($3);
     }
-    | E LSB actions RSB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
+    | NE LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_NE, *$3, $6);
+        free($3);
     }
-    | A LSB actions RSB X rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
+    | UC LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_UC, *$3, $6);
+        free($3);
     }
-    | A LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
-        $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
+    | NC LSB agents RSB LRB rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_NC, *$3, $6);
+        free($3);
     }
-    | A LSB actions RSB F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
+
+    // | E LSB actions RSB X rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
+    // }
+    // | 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 rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
+    // }
+    // | E LSB actions RSB G rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
+    // }
+    // | A LSB actions RSB X rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
+    // }
+    // | 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 rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
+    // }
+    // | A LSB actions RSB G rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
+    // }
+
+	  /* contexts as boolean formulae  */
+    | E LAB state_constr RAB X rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
     }
-    | A LSB actions RSB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
+    | E LAB state_constr RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
     }
-	/* contexts as boolean formulae  */
-    | E LAB bool_contexts RAB X rsctl_form { 
-        $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
+    | E LAB state_constr RAB F rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EF_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 state_constr RAB G rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
+    | A LAB state_constr RAB X rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
+    | A LAB state_constr RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
+        $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
     }
-    | A LAB bool_contexts RAB X rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
+    | A LAB state_constr RAB F rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AF_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 F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
-    }
-    | A LAB bool_contexts RAB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
+    | A LAB state_constr RAB G rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
     }
     ;
 %%
@@ -396,4 +476,3 @@ yy::rsin_parser::error(const yy::rsin_parser::location_type &l, const std::strin
 {
     driver.error(l, m);
 }
-
diff --git a/stateconstr.cc b/stateconstr.cc
new file mode 100644
index 0000000..8bb6f27
--- /dev/null
+++ b/stateconstr.cc
@@ -0,0 +1,118 @@
+/*
+    Copyright (c) 2018
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "stateconstr.hh"
+#include "types.hh"
+#include "cudd.hh"
+#include "bdd_macro.hh"
+#include "symrs.hh"
+
+std::string StateConstr::toStr(void) const
+{
+  if (oper == STC_PV) {
+    return proc_name + "." + entity_name;
+  }
+  else if (oper == STC_TF) {
+    if (tf) {
+      return "true";
+    }
+    else {
+      return "false";
+    }
+  }
+  else if (oper == STC_AND) {
+    return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_OR) {
+    return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_XOR) {
+    return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_NOT) {
+    return "~" + arg[0]->toStr();
+  }
+
+  else {
+    return "??";
+    assert(0);
+  }
+}
+
+BDD StateConstr::getBDDforState(const SymRS *srs) const
+{
+  return getBDD(srs, false);
+}
+
+BDD StateConstr::getBDDforContext(const SymRS *srs) const
+{
+  return getBDD(srs, true);
+}
+
+BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
+{
+  if (oper == STC_PV) {
+    if (encode_context) {
+      return srs->encActStrEntity(proc_name, entity_name);
+    }
+    else {
+      return srs->encEntity(proc_name, entity_name);
+    }
+  }
+  else if (oper == STC_TF) {
+    if (tf) {
+      return srs->getBDDtrue();
+    }
+    else {
+      return srs->getBDDfalse();
+    }
+  }
+  else if (oper == STC_AND) {
+    return arg[0]->getBDD(srs, encode_context) * arg[1]->getBDD(srs, encode_context);
+  }
+  else if (oper == STC_OR) {
+    return arg[0]->getBDD(srs, encode_context) + arg[1]->getBDD(srs, encode_context);
+  }
+  else if (oper == STC_XOR) {
+    return arg[0]->getBDD(srs, encode_context) ^ arg[1]->getBDD(srs, encode_context);
+  }
+  else if (oper == STC_NOT) {
+    return !arg[0]->getBDD(srs, encode_context);
+  }
+  else {
+    assert(0);
+    FERROR("Undefined operator used in Boolean state/context definition. This should not happen.");
+    return srs->getBDDfalse();
+  }
+}
+
+bool StateConstr::isFalse(void) const
+{
+  if (oper == STC_TF && tf == false) {
+    return true;
+  }
+
+  if (oper == STC_NOT && arg[0]->isTrue()) {
+    return true;
+  }
+
+  return false;
+}
+
+bool StateConstr::isTrue(void) const
+{
+  if (oper == STC_TF && tf == true) {
+    return true;
+  }
+
+  if (oper == STC_NOT && arg[0]->isFalse()) {
+    return true;
+  }
+
+  return false;
+}
diff --git a/stateconstr.hh b/stateconstr.hh
new file mode 100644
index 0000000..21b42ae
--- /dev/null
+++ b/stateconstr.hh
@@ -0,0 +1,115 @@
+/*
+    Copyright (c) 2018
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#ifndef STATECONSTR_HH
+#define STATECONSTR_HH
+
+#include "types.hh"
+
+/* For state constraints: */
+#define STC_PV   80
+#define STC_AND  81
+#define STC_OR   82
+#define STC_XOR  83
+#define STC_NOT  84
+#define STC_TF   90
+
+#define STC_COND_1ARG(a) ((a) == STC_NOT)
+#define STC_COND_2ARG(a) ((a) == STC_AND || (a) == STC_OR || (a) == STC_XOR)
+#define STC_IS_VALID(a) (STC_COND_1ARG(a) || STC_COND_2ARG(a) || (a) == STC_PV || (a) == STC_TF)
+
+class SymRS;
+
+class StateConstr
+{
+    Oper oper;
+    StateConstr *arg[2];
+    std::string entity_name;
+    std::string proc_name;
+    bool tf;
+
+  public:
+
+    StateConstr(std::string procName, std::string varName)
+    {
+      oper = STC_PV;
+      entity_name = varName;
+      proc_name = procName;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for true/false.
+     *
+     * @param   val value of the logical constant
+     */
+    StateConstr(bool val)
+    {
+      oper = STC_TF;
+      tf = val;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula.
+     */
+    StateConstr(Oper op, StateConstr *form1)
+    {
+      assert(op == STC_NOT);
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula.
+     */
+    StateConstr(Oper op, StateConstr *form1, StateConstr *form2)
+    {
+      assert(STC_COND_2ARG(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+    }
+
+    ~StateConstr()
+    {
+      delete arg[0];
+      delete arg[1];
+    }
+
+    std::string toStr(void) const;
+
+    BDD getBDD(const SymRS *srs, bool encode_context) const;
+    BDD getBDDforContext(const SymRS *srs) const;
+    BDD getBDDforState(const SymRS *srs) const;
+
+    Oper getOper(void) const
+    {
+      assert(STC_IS_VALID(oper));
+      return oper;
+    }
+    StateConstr *getLeftSF(void) const
+    {
+      assert(arg[0] != nullptr);
+      return arg[0];
+    }
+    StateConstr *getRightSF(void) const
+    {
+      assert(STC_COND_2ARG(oper));
+      assert(arg[1] != nullptr);
+      return arg[1];
+    }
+
+    bool isFalse(void) const;
+    bool isTrue(void) const;
+};
+
+#endif
diff --git a/symrs.cc b/symrs.cc
index 6440e93..c7476c6 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -4,597 +4,972 @@
 */
 
 #include "symrs.hh"
-
+#include "rs.hh"
+#include "stateconstr.hh"
+#include "bdd_macro.hh"
 
 SymRS::SymRS(RctSys *rs, Options *opts)
 {
-    this->rs = rs;
-    this->opts = opts;
-    totalRctSysStateVars = rs->getEntitiesSize();
-    totalReactions = rs->getReactionsSize();
-    totalActions = rs->getActionsSize();
-	
-	totalCtxAutStateVars = getCtxAutStateEncodingSize();
-	
-	totalStateVars = totalRctSysStateVars + totalCtxAutStateVars;
-	
-    partTrans = nullptr;
-    monoTrans = nullptr;
-	
-	pv_ca = nullptr;
-	pv_ca_succ = nullptr;
-	tr_ca = nullptr;
+  this->rs = rs;
+  this->opts = opts;
 
-    encode();	
+  mapProcEntities();
+
+  totalEntities = rs->getEntitiesSize();
+
+  // TODO: remove
+  totalActions = 0;
+
+  totalRctSysStateVars = getTotalProductVariables();
+  totalCtxEntities = getTotalCtxEntitiesVariables();
+
+  totalCtxAutStateVars = getCtxAutStateEncodingSize();
+  totalStateVars = totalRctSysStateVars + totalCtxAutStateVars;
+  numberOfProc = rs->getNumberOfProcesses();
+
+  partTrans = nullptr;
+  monoTrans = nullptr;
+
+  pv_ca = nullptr;
+  pv_ca_succ = nullptr;
+  tr_ca = nullptr;
+
+  encode();
 }
 
-BDD SymRS::encEntity_raw(Entity entity, bool succ) const
+bool SymRS::usingContextAutomaton(void)
 {
-    BDD r;
-
-    if (succ)
-        r = (*pv_succ)[entity];
-    else
-        r = (*pv)[entity];
-
-    return r;
+  return rs->ctx_aut != nullptr;
 }
 
-BDD SymRS::encEntitiesConj_raw(const Entities &entities, bool succ)
+
+BDD SymRS::encEntity(std::string proc_name, std::string entity_name) const
 {
-    BDD r = BDD_TRUE;
-
-    for (const auto &entity : entities)
-    {
-        if (succ) r *= encEntitySucc(entity);
-        else r *= encEntity(entity);
-    }
-
-    return r;
-}
-
-BDD SymRS::encEntitiesDisj_raw(const Entities &entities, bool succ)
-{
-    BDD r = BDD_FALSE;
-
-    for (const auto &entity : entities)
-    {
-        if (succ) r += encEntitySucc(entity);
-        else r += encEntity(entity);
-    }
-
-    return r;
-}
-
-BDD SymRS::encStateActEntitiesConj(const Entities &entities)
-{
-    BDD r = BDD_TRUE;
-
-    for (const auto &entity : entities)
-    {
-        BDD state_act = encEntity(entity);
-        int actEntity;
-		
-		// if entity is also an action entity, we include it in the encoding
-        if ((actEntity = getMappedStateToActID(entity)) >= 0)
-            state_act += encActEntity(actEntity);
-        
-		r *= state_act;
-    }
-
-    return r;
-}
-
-BDD SymRS::encStateActEntitiesDisj(const Entities &entities)
-{
-    BDD r = BDD_FALSE;
-
-    for (const auto &entity : entities)
-    {
-        BDD state_act = encEntity(entity);
-        int actEntity;
-
-		// if entity is also an aciton entity, we include it in the encoding
-        if ((actEntity = getMappedStateToActID(entity)) >= 0)
-            state_act += encActEntity(actEntity);
-		
-        r += state_act;
-    }
-
-    return r;
-}
-
-BDD SymRS::encActEntitiesConj(const Entities &entities)
-{
-    BDD r = BDD_TRUE;
-
-    for (const auto &entity : entities)
-    {
-        Entity actEntity = getMappedStateToActID(entity);
-        r *= encActEntity(actEntity);
-    }
-
-    return r;
-}
-
-BDD SymRS::compState(const BDD &state) const
-{
-    BDD s = state;
-
-    for (unsigned int i = 0; i < totalRctSysStateVars; ++i)
-    {
-        if (!(*pv)[i] * state != cuddMgr->bddZero())
-            s *= !(*pv)[i];
-    }
-
-    return s;
-}
-
-BDD SymRS::compContext(const BDD &context) const
-{
-    BDD c = context;
-
-    for (unsigned int i = 0; i < totalActions; ++i)
-    {
-        if (!(*pv_act)[i] * context != cuddMgr->bddZero())
-            c *= !(*pv_act)[i];
-    }
-
-    return c;
-}
-
-std::string SymRS::decodedRctSysStateToStr(const BDD &state)
-{
-    std::string s = "{ ";
-    for (unsigned int i = 0; i < totalRctSysStateVars; ++i)
-    {
-        if (!(encEntity(i) * state).IsZero())
-        {
-            s += rs->entityToStr(i) + " ";
-        }
-    }
-    s += "}";
-    return s;
-}
-
-void SymRS::printDecodedRctSysStates(const BDD &states)
-{
-    BDD unproc = states;
-    while (!unproc.IsZero())
-    {
-        BDD t = unproc.PickOneMinterm(*pv_rs);
-        cout << decodedRctSysStateToStr(t) << endl;
-        if (opts->verbose > 9) {
-            t.PrintMinterm();
-            cout << endl;
-        }
-        unproc -= t;
-    }
-}
-
-void SymRS::initBDDvars(void)
-{
-	VERB("Initialising CUDD");
-	
-    cuddMgr = new Cudd(0,0);
-
-    VERB("Preparing BDD variables");
-
-	// used for bddVar
-	unsigned int bdd_var_idx = 0;
-	
-	// used for pv, pv_succ
-	unsigned int global_state_idx = 0;
-
-	// Variables for reaction system with CA (if used)
-    pv = new vector<BDD>(totalStateVars);
-    pv_succ = new vector<BDD>(totalStateVars);
-    pv_E = new BDD(BDD_TRUE);
-    pv_succ_E = new BDD(BDD_TRUE);
-	
-	// Reaction system (no actions, no CA)
-    pv_rs = new vector<BDD>(totalRctSysStateVars);
-    pv_rs_succ = new vector<BDD>(totalRctSysStateVars);
-    pv_rs_E = new BDD(BDD_TRUE);
-    pv_rs_succ_E = new BDD(BDD_TRUE);
-
-	for (unsigned int i = 0; i < totalRctSysStateVars; ++i)
-	{
-		(*pv_rs)[i] = cuddMgr->bddVar(bdd_var_idx++);
-        (*pv_rs_succ)[i] = cuddMgr->bddVar(bdd_var_idx++);
-        *pv_rs_E *= (*pv_rs)[i];
-        *pv_rs_succ_E *= (*pv_rs_succ)[i];
-		
-		(*pv)[global_state_idx] = (*pv_rs)[i];
-		(*pv_succ)[global_state_idx] = (*pv_rs_succ)[i];
-		++global_state_idx;
-	}
-
-	// CA
-	if (usingContextAutomaton())
-	{
-		VERB("Context automaton variables");
-
-		pv_ca = new vector<BDD>(totalCtxAutStateVars);
-		pv_ca_succ = new vector<BDD>(totalCtxAutStateVars);
-		pv_ca_E = new BDD(BDD_TRUE);
-		pv_ca_succ_E = new BDD(BDD_TRUE);
-
-		for (unsigned int i = 0; i < totalCtxAutStateVars; ++i)
-		{
-			(*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++);
-	        (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++);
-	        *pv_ca_E *= (*pv_ca)[i];
-	        *pv_ca_succ_E *= (*pv_ca_succ)[i];
-			
-			(*pv)[global_state_idx] = (*pv_ca)[i];
-			(*pv_succ)[global_state_idx] = (*pv_ca_succ)[i];
-			++global_state_idx;	
-		}
-	}
-	
-	// Actions/Contexts
-    pv_act = new vector<BDD>(totalActions);
-    pv_act_E = new BDD(BDD_TRUE);
-    
-	for (unsigned int i = 0; i < totalActions; ++i)
-    {
-        (*pv_act)[i] = cuddMgr->bddVar(bdd_var_idx++);
-        *pv_act_E *= (*pv_act)[i];
-    }
-	
-	// Quantification BDDs
-	
-	*pv_E = *pv_rs_E;
-	*pv_succ_E = *pv_rs_succ_E;
-	
-	if (usingContextAutomaton())
-	{
-		*pv_E *= *pv_ca_E;
-		*pv_succ_E *= *pv_ca_succ_E;
-	}
-
-    VERB("All BDD variables ready");
-}
-
-void SymRS::encodeTransitions(void)
-{
-    DecompReactions dr;
-
-    VERB("Decomposing reactions");
-    for (unsigned int i = 0; i < totalReactions; ++i)
-    {
-        ReactionCond cond;
-        cond.rctt = rs->reactions[i].rctt;
-        cond.inhib = rs->reactions[i].inhib;
-    
-        for (Entities::iterator p = rs->reactions[i].prod.begin();
-                p != rs->reactions[i].prod.end(); ++p)
-        {
-            dr[*p].push_back(cond);
-        }
-    }
-
-    VERB("Encoding reactions");
-
-    if (opts->part_tr_rel)
-    {
-        VERB("Using partitioned transition relation encoding");
-        partTrans = new vector<BDD>(totalRctSysStateVars);
-    }
-    else
-    {
-        VERB("Using monolithic transition relation encoding");
-        monoTrans = new BDD(BDD_TRUE);
-    }
-
-    for (unsigned int p = 0; p < totalRctSysStateVars; ++p)
-    {
-        VERB_L3("Encoding for successor " << p);
-
-        DecompReactions::iterator di;
-
-        if ((di = dr.find(p)) == dr.end())
-        {
-            // there is no reaction producing p:
-            if (opts->part_tr_rel)
-                (*partTrans)[p] = !encEntitySucc(p);
-            else
-            {
-                *monoTrans *= !encEntitySucc(p);
-            }
-        }
-        else
-        {
-            // di - reactions producing p
-            
-            BDD conditions = BDD_FALSE;
-
-            assert(di->second.size() > 0);
-
-            for (unsigned int j = 0; j < di->second.size(); ++j)
-            {
-                conditions += encStateActEntitiesConj(di->second[j].rctt) * !encStateActEntitiesDisj(di->second[j].inhib);
-            }
-
-            if (opts->part_tr_rel)
-            {
-                (*partTrans)[p] = conditions * encEntitySucc(p);
-                (*partTrans)[p] += !conditions * !encEntitySucc(p);
-            }
-            else
-            {
-                *monoTrans *= (conditions * encEntitySucc(p)) + (!conditions * !encEntitySucc(p));
-            }
-        }
-        if (opts->reorder_trans)
-        {
-            VERB_L2("Reordering");
-            Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
-        }
-
-    }
-
-    VERB("Reactions ready");
-	
-	if (usingContextAutomaton())
-	{
-		VERB("Augmenting transition relation encoding with the transition relation for context automaton");
-		if (opts->part_tr_rel)
-		{
-			assert(0);
-		}
-		else
-		{
-			assert(tr_ca != nullptr);
-			*monoTrans *= *tr_ca;
-		}
-	}
-		
-	VERB("Transition relation encoded")
-}
-
-BDD SymRS::getEncState(const Entities &entities)
-{
-    assert(0);
-    //BDD state = compState(encEntitiesConj(rs->initState));
-    //for (RctSys::Entities::iterator at = rs->actionEntities.begin(); at != rs->actionEntities.end(); ++at)
-    //{
-    //    state = state.ExistAbstract(encEntity(*at));
-    //}
-    return BDD_FALSE;
-}
-
-BDD SymRS::encNoContext(void)
-{
-	BDD noContextBDD = BDD_TRUE;
-
-    for (unsigned int i = 0; i < totalActions; ++i)
-    {
-        noContextBDD *= !(*pv_act)[i];
-    }
-
-	return noContextBDD;
-}
-
-void SymRS::encodeInitStates(void)
-{
-	if (usingContextAutomaton())
-	{
-	    VERB("Encoding initial states (using context automaton)");
-		encodeInitStatesForCtxAut();
-	}
-	else
-	{
-	    VERB("Encoding initial states (for the action entities method -- no CA)");
-		encodeInitStatesNoCtxAut();
-	}
-    VERB("Initial states encoded");
-}
-
-void SymRS::encodeInitStatesForCtxAut(void)
-{
-    initStates = new BDD(BDD_TRUE);
-
-    for (unsigned int i = 0; i < totalRctSysStateVars; ++i)
-    {
-    	*initStates *= !(*pv)[i];
-    }
-
-	*initStates *= getEncCtxAutInitState();
-}
-
-void SymRS::encodeInitStatesNoCtxAut(void)
-{
-#ifndef NDEBUG
-    if (opts->part_tr_rel)
-        assert(partTrans != nullptr);
-#endif
-
-    initStates = new BDD(BDD_FALSE);
-		
-    for (auto state = rs->initStates.begin();
-            state != rs->initStates.end();
-            ++state)
-    {
-        VERB("Encoding a single inital state");
-        BDD newInitState = compState(encEntitiesConj(*state)); 
-        BDD q = BDD_TRUE;
-        if (opts->part_tr_rel)
-        {
-            for (unsigned int i = 0; i < partTrans->size(); ++i)
-            {
-                q *= newInitState * (*partTrans)[i] * encNoContext();
-            }
-        }
-        else
-        {
-            q *= newInitState * *monoTrans * encNoContext();
-        }
-		
-        q = (q.ExistAbstract(*pv_E)).SwapVariables(*pv_succ, *pv);
-        q = q.ExistAbstract(*pv_act_E);
-
-        *initStates += q;
-    }
-}
-
-void SymRS::mapStateToAct(void)
-{
-    VERB("Mapping state variables to action variables");
-    unsigned int j = 0;
-    for (unsigned int i = 0; i < totalRctSysStateVars; ++i)
-    {
-        if (rs->isActionEntity(i)) {
-            stateToAct.push_back(j++);
-        }
-        else
-        {
-            stateToAct.push_back(-1);
-        }
-    }
-	const unsigned int verbosity_level = 9;
-    if (opts->verbose > verbosity_level)
-    {
-        for (unsigned int i = 0; i < stateToAct.size(); ++i)
-        {
-            cout << "ii VERBOSE(" << verbosity_level << "): stateToAct[" << i << "] = " << stateToAct[i] << endl;
-        }
-    }
+  return encEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name));
 }
 
 void SymRS::encode(void)
 {
-    VERB("Encoding...");
+  VERB("Encoding...");
 
-    if (opts->measure)
-    {
-        opts->enc_time = cpuTime();
-        opts->enc_mem = memUsed();
-    }
+  if (opts->measure) {
+    opts->enc_time = cpuTime();
+    opts->enc_mem = memUsed();
+  }
 
-    mapStateToAct();
+  initBDDvars();
 
-    initBDDvars();
-	
-	if (usingContextAutomaton())
-	{
-		encodeCtxAutTrans();
-	}
-	else
-	{
-		VERB_LN(3, "Not using context automata, not encoding TR for CA")
-	}
-	
-    encodeTransitions();
-    encodeInitStates();
+  if (usingContextAutomaton()) {
+    encodeCtxAutTrans();
+  }
+  else {
+    VERB_LN(3, "Not using context automata, not encoding TR for CA")
+  }
 
-    if (opts->measure)
-    {
-        opts->enc_time = cpuTime() - opts->enc_time;
-        opts->enc_mem = memUsed() - opts->enc_mem;
-    }
+  encodeTransitions();
+  encodeInitStates();
 
-    VERB("Encoding done");
+  if (opts->measure) {
+    opts->enc_time = cpuTime() - opts->enc_time;
+    opts->enc_mem = memUsed() - opts->enc_mem;
+  }
+
+  VERB("Encoding done");
 }
 
-BDD SymRS::encActStrEntity(std::string name) const 
+LocalIndicesForProcEntities SymRS::buildLocalEntitiesMap(
+  const EntitiesForProc &procEnt)
 {
-    int id = getMappedStateToActID(rs->getEntityID(name));
-	if (id < 0) 
-	{
-		FERROR("Entity \"" << name << "\" not defined as context entity");
-		return BDD_FALSE;
-	} else {
-		return encActEntity(getMappedStateToActID(rs->getEntityID(name)));
-	}
+  LocalIndicesForProcEntities ent_map;
+
+  for (const auto &proc_ent : procEnt) {
+    Process proc_id = proc_ent.first;
+
+    unsigned int cnt = 0;
+
+    for (const auto &e : proc_ent.second) {
+      ent_map[proc_id][e] = cnt++;
+    }
+  }
+
+  return ent_map;
+}
+
+void SymRS::initBDDvars(void)
+{
+  VERB("Initialising CUDD");
+
+  cuddMgr = new Cudd(0, 0);
+
+  VERB("Preparing BDD variables");
+
+  // used for bddVar
+  unsigned int bdd_var_idx = 0;
+
+  // used for pv, pv_succ
+  unsigned int global_state_idx = 0;
+
+  // ----------------------------------------------------------
+  //                        Global state
+  // ----------------------------------------------------------
+  //
+  //  Variables for reaction system with CA (if used)
+  //
+
+  pv = new BDDvec(totalStateVars);
+  pv_succ = new BDDvec(totalStateVars);
+  pv_E = new BDD(BDD_TRUE);
+  pv_succ_E = new BDD(BDD_TRUE);
+
+  // ----------------------------------------------------------
+  //                       Distributed RS
+  // ----------------------------------------------------------
+
+  pv_drs = new vector<BDDvec>(numberOfProc);
+  pv_drs_succ = new vector<BDDvec>(numberOfProc);
+
+  pv_drs_flat = new BDDvec(totalRctSysStateVars);
+  pv_drs_flat_succ = new BDDvec(totalRctSysStateVars);
+
+  pv_drs_E = new BDDvec(numberOfProc);
+
+  pv_drs_flat_E = new BDD(BDD_TRUE);
+  pv_drs_flat_succ_E = new BDD(BDD_TRUE);
+
+  VERB_LN(2, "DRS processing");
+
+  unsigned int drs_flat_index = 0;
+
+  for (const auto &proc_ent : usedProducts) {
+
+    auto proc_id = proc_ent.first;
+    auto entities_count = proc_ent.second.size();
+
+    //
+    // The order of entities and their correspondence to the
+    // correct entities in pv (global) does not matter here.
+    //
+    // The correspondence is established in the methods
+    // returning BDD variables (encoding) of the individual
+    // enties.
+    //
+    // We only need to make sure we have the correct number of
+    // variables that are going to be used in the encoding.
+    //
+    // For efficiency, we do not introduce BDD variables for
+    // entites that are never produced in a given local component.
+    // Instead, we only select those that are. We apply the same
+    // strategy to product entities and context entities.
+    //
+
+    // First, we need to adjust the sizes of all the nested vectors
+    (*pv_drs)[proc_id].resize(entities_count);
+    (*pv_drs_succ)[proc_id].resize(entities_count);
+
+    (*pv_drs_E)[proc_id] = BDD_TRUE;
+
+    for (unsigned int i = 0; i < entities_count; ++i) {
+
+      assert(drs_flat_index < totalRctSysStateVars);
+      assert(global_state_idx < totalStateVars);
+      assert(proc_id < numberOfProc);
+      assert(i < totalEntities);
+
+      // Variables for each individual process/component
+      (*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
+      (*pv_drs_succ)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
+
+      // Quantification (per proc)
+      (*pv_drs_E)[proc_id] *= (*pv_drs)[proc_id][i];
+
+      // The DRS part of the system (flattened): these vars do not include CA
+      (*pv_drs_flat)[drs_flat_index] = (*pv_drs)[proc_id][i];
+      (*pv_drs_flat_succ)[drs_flat_index] = (*pv_drs_succ)[proc_id][i];
+
+      *pv_drs_flat_E *= (*pv_drs_flat)[drs_flat_index];
+      *pv_drs_flat_succ_E *= (*pv_drs_flat_succ)[drs_flat_index];
+
+      // Variables used for the global states
+      (*pv)[global_state_idx] = (*pv_drs)[proc_id][i];
+      (*pv_succ)[global_state_idx] = (*pv_drs_succ)[proc_id][i];
+
+      *pv_E *= (*pv)[global_state_idx];
+      *pv_succ_E *= (*pv_succ)[global_state_idx];
+
+      ++drs_flat_index;
+      ++global_state_idx;
+    }
+  }
+
+  // ----------------------------------------------------------
+  //                      Context Automaton
+  // ----------------------------------------------------------
+
+  if (usingContextAutomaton()) {
+    VERB_LN(2, "Context automaton variables");
+
+    pv_ca = new BDDvec(totalCtxAutStateVars);
+    pv_ca_succ = new BDDvec(totalCtxAutStateVars);
+    pv_ca_E = new BDD(BDD_TRUE);
+    pv_ca_succ_E = new BDD(BDD_TRUE);
+
+    for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) {
+      (*pv_ca)[i] = cuddMgr->bddVar(bdd_var_idx++);
+      (*pv_ca_succ)[i] = cuddMgr->bddVar(bdd_var_idx++);
+      *pv_ca_E *= (*pv_ca)[i];
+      *pv_ca_succ_E *= (*pv_ca_succ)[i];
+
+      (*pv)[global_state_idx] = (*pv_ca)[i];
+      (*pv_succ)[global_state_idx] = (*pv_ca_succ)[i];
+      ++global_state_idx;
+    }
+  }
+
+  // ----------------------------------------------------------
+  //                Enabledness of processes
+  // ----------------------------------------------------------
+  //
+  //  These variables indicate which process is
+  //  allowed to perform action
+  //
+  VERB_LN(2, "Variables for process enabledness/activity");
+
+  pv_proc_enab = new BDDvec(numberOfProc);
+  pv_proc_enab_E = new BDD(BDD_TRUE);
+
+  for (unsigned int i = 0; i < numberOfProc; ++i) {
+    auto bdd_var = cuddMgr->bddVar(bdd_var_idx++);
+    (*pv_proc_enab)[i] = bdd_var;
+    *pv_proc_enab_E *= bdd_var;
+  }
+
+  // ----------------------------------------------------------
+  //                   Context Entities
+  // ----------------------------------------------------------
+
+  VERB_LN(2, "Variables for context entities");
+
+  pv_ctx = new BDDvec(totalCtxEntities);
+  pv_ctx_E = new BDD(BDD_TRUE);
+  pv_proc_ctx = new vector<BDDvec>(numberOfProc);
+  pv_proc_ctx_E = new BDDvec(numberOfProc);
+
+  unsigned int flat_ctx_index = 0;
+
+  for (const auto &proc_ent : usedCtxEntities) {
+
+    auto proc_id = proc_ent.first;
+    auto entities_count = proc_ent.second.size();
+
+    assert(entities_count < totalEntities);
+
+    // adjust the size of the nested vector before we use an index
+    (*pv_proc_ctx)[proc_id].resize(entities_count);
+
+    (*pv_proc_ctx_E)[proc_id] = BDD_TRUE;
+
+    for (unsigned int i = 0; i < entities_count; ++i) {
+
+      assert(flat_ctx_index < totalCtxEntities);
+      assert(proc_id < numberOfProc);
+
+      (*pv_proc_ctx)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
+      (*pv_proc_ctx_E)[proc_id] *= (*pv_proc_ctx)[proc_id][i];
+
+      (*pv_ctx)[flat_ctx_index] = (*pv_proc_ctx)[proc_id][i];
+      *pv_ctx_E *= (*pv_ctx)[flat_ctx_index];
+
+      ++flat_ctx_index;
+    }
+
+  }
+
+  if (usingContextAutomaton()) {
+
+    VERB_LN(2, "Updating quantification BDDs with context automaton")
+
+    *pv_E *= *pv_ca_E;
+    *pv_succ_E *= *pv_ca_succ_E;
+  }
+
+  VERB("All BDD variables ready");
+}
+
+size_t SymRS::getTotalProductVariables(void)
+{
+  size_t total = 0;
+
+  for (const auto &it : usedProducts) {
+    total += it.second.size();
+  }
+
+  return total;
+}
+
+size_t SymRS::getTotalCtxEntitiesVariables(void)
+{
+  size_t total = 0;
+
+  for (const auto &it : usedCtxEntities) {
+    total += it.second.size();
+  }
+
+  return total;
+}
+
+void SymRS::mapProcEntities(void)
+{
+  //
+  // Reactions
+  //
+  for (const auto &proc_rcts : rs->proc_reactions) {
+    Process proc_id = proc_rcts.first;
+
+    for (const auto &rct : proc_rcts.second) {
+
+      // collect entities that can be produced
+      // locally by the process with proc_id
+
+      SET_ADD(usedProducts[proc_id], rct.prod);
+    }
+  }
+
+  prod_ent_local_idx = buildLocalEntitiesMap(usedProducts);
+
+  //
+  // Context automaton
+  //
+  for (const auto &tr : rs->ctx_aut->transitions) {
+    for (const auto &proc_ctx : tr.ctx) {
+      Process proc_id = proc_ctx.first;
+      SET_ADD(usedCtxEntities[proc_id], proc_ctx.second);
+    }
+  }
+
+  ctx_ent_local_idx = buildLocalEntitiesMap(usedCtxEntities);
+
+  if (opts->verbose > 9) {
+    cout << "Used product entities:" << endl;
+    cout << rs->procEntitiesToStr(usedProducts) << endl;
+
+    cout << "Used context entities:" << endl;
+    cout << rs->procEntitiesToStr(usedCtxEntities) << endl;
+  }
+}
+
+unsigned int SymRS::getLocalProductEntityIndex(Process proc_id, Entity entity) const
+{
+  assert(productEntityExists(proc_id, entity));
+  auto idx = prod_ent_local_idx.at(proc_id).at(entity);
+  assert(idx < prod_ent_local_idx.at(proc_id).size());
+  return idx;
+}
+unsigned int SymRS::getLocalCtxEntityIndex(Process proc_id, Entity entity) const
+{
+  assert(ctxEntityExists(proc_id, entity));
+  auto idx = ctx_ent_local_idx.at(proc_id).at(entity);
+  assert(idx < ctx_ent_local_idx.at(proc_id).size());
+  return idx;
+}
+
+BDD SymRS::encEntity_raw(Process proc_id, Entity entity, bool succ) const
+{
+  BDD r;
+
+  assert(proc_id < numberOfProc);
+  assert(productEntityExists(proc_id, entity));
+
+  auto local_entity_id = getLocalProductEntityIndex(proc_id, entity);
+
+  if (succ) {
+    r = (*pv_drs_succ)[proc_id][local_entity_id];
+  }
+  else {
+    r = (*pv_drs)[proc_id][local_entity_id];
+  }
+
+  return r;
+}
+
+BDD SymRS::encCtxEntity(Process proc_id, Entity entity) const
+{
+  assert(entity < totalEntities);
+  assert(proc_id < numberOfProc);
+  assert(ctxEntityExists(proc_id, entity));
+
+  auto local_entity_id = getLocalCtxEntityIndex(proc_id, entity);
+
+  return (*pv_proc_ctx)[proc_id][local_entity_id];
+}
+
+bool SymRS::productEntityExists(Process proc_id, Entity entity) const
+{
+  if (prod_ent_local_idx.count(proc_id) == 0) {
+    return false;
+  }
+  else {
+    if (prod_ent_local_idx.at(proc_id).count(entity) == 1) {
+      return true;
+    }
+  }
+
+  return false;
+}
+
+bool SymRS::ctxEntityExists(Process proc_id, Entity entity) const
+{
+  if (ctx_ent_local_idx.count(proc_id) == 0) {
+    return false;
+  }
+  else {
+    if (ctx_ent_local_idx.at(proc_id).count(entity) == 1) {
+      return true;
+    }
+  }
+
+  return false;
+}
+
+bool SymRS::processUsesEntity(Process proc_id, Entity entity_id) const
+{
+  if (productEntityExists(proc_id, entity_id) || ctxEntityExists(proc_id, entity_id)) {
+    return true;
+  }
+
+  return false;
+}
+
+BDD SymRS::encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ)
+{
+  BDD r = BDD_TRUE;
+
+  for (const auto &entity : entities) {
+    if (succ) {
+      r *= encEntitySucc(proc_id, entity);
+    }
+    else {
+      r *= encEntity(proc_id, entity);
+    }
+  }
+
+  return r;
+}
+
+BDD SymRS::encEntitiesDisj_raw(Process proc_id, const Entities &entities, bool succ)
+{
+  BDD r = BDD_FALSE;
+
+  for (const auto &entity : entities) {
+    if (succ) {
+      r += encEntitySucc(proc_id, entity);
+    }
+    else {
+      r += encEntity(proc_id, entity);
+    }
+  }
+
+  return r;
+}
+
+BDD SymRS::encEntityCondition(Process proc_id, Entity entity_id)
+{
+  //
+  // Here we encode an entity-based condition which uses
+  // the entity appearing as a product or a context entity.
+  //
+  BDD r = BDD_FALSE;
+
+  if (productEntityExists(proc_id, entity_id)) {
+    r += encEntity(proc_id, entity_id);
+  }
+
+  if (ctxEntityExists(proc_id, entity_id)) {
+    r += encCtxEntity(proc_id, entity_id);
+  }
+
+  // pointless call to this function -- we should have prevented it:
+  assert(r != BDD_FALSE);
+
+  return r;
+}
+
+BDD SymRS::encContext(const EntitiesForProc &proc_entities)
+{
+  BDD r = BDD_TRUE;
+
+  for (const auto &pe : proc_entities) {
+    auto proc_id = pe.first;
+    auto entities = pe.second;
+
+    for (const auto &entity : entities) {
+      r *= encCtxEntity(proc_id, entity);
+    }
+
+    r *= encProcEnabled(proc_id);
+  }
+
+  return r;
+}
+
+BDD SymRS::compState(const BDD &state) const
+{
+  assert(0);
+  BDD s = state;
+
+  for (unsigned int i = 0; i < totalRctSysStateVars; ++i) {
+    if (!(*pv)[i] * state != cuddMgr->bddZero()) {
+      s *= !(*pv)[i];
+    }
+  }
+
+  return s;
+}
+
+BDD SymRS::compContext(const BDD &context) const
+{
+  BDD c = context;
+
+  for (const auto &var : *pv_ctx) {
+    if (!var * context != cuddMgr->bddZero()) {
+      c *= !var;
+    }
+  }
+
+  for (const auto &var : *pv_proc_enab) {
+    if (!var * context != cuddMgr->bddZero()) {
+      c *= !var;
+    }
+  }
+
+  return c;
+}
+
+std::string SymRS::decodedRctSysStateToStr(const BDD &state)
+{
+  std::string s = "{ ";
+
+  for (const auto &proc_entities : usedProducts) {
+
+    auto proc_id = proc_entities.first;
+    auto entities = proc_entities.second;
+    s += rs->getProcessName(proc_id) + "={ ";
+
+    for (const auto &entity : entities) {
+      if (!(encEntity(proc_id, entity) * state).IsZero()) {
+        s += rs->entityToStr(entity) + " ";
+      }
+    }
+
+    s += "} ";
+  }
+
+  s += "}";
+  return s;
+}
+
+void SymRS::printDecodedRctSysStates(const BDD &states)
+{
+  BDD unproc = states;
+
+  while (!unproc.IsZero()) {
+    BDD t = unproc.PickOneMinterm(*pv_drs_flat);
+    cout << decodedRctSysStateToStr(t) << endl;
+
+    if (opts->verbose > 9) {
+      BDD_PRINT(t);
+      cout << endl;
+    }
+
+    unproc -= t;
+  }
+}
+
+DecompReactions SymRS::getProductionConditions(Process proc_id)
+{
+  DecompReactions dr;
+
+  for (const auto &rct : rs->proc_reactions[proc_id]) {
+    ReactionCond cond;
+    cond.rctt = rct.rctt;
+    cond.inhib = rct.inhib;
+
+    for (const auto &prod : rct.prod) {
+      dr[prod].push_back(cond);
+    }
+  }
+
+  return dr;
+}
+
+BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
+{
+  assert(prod_conds.size() > prod_proc_id);
+
+  BDD enab = BDD_FALSE;
+
+  auto production_conditions = prod_conds[prod_proc_id][entity_id];
+
+  VERB_LN(5, "| Produce " << rs->getEntityName(entity_id) << " in " << rs->getProcessName(prod_proc_id) << ":");
+
+  // Iterate through production conditions for the entity (entity_id) that
+  // belongs to the process prod_proc_id which contain:
+  //  - reactants
+  //  - inhibitors
+  //
+  // Here we are building an alternative for the enab BDD,
+  // for all the possible production conditions
+  //
+  for (const auto &cond : production_conditions) {
+
+    // Take all the reactants... (conjuntion)
+    BDD reactants = BDD_TRUE;
+
+    for (const auto &reactant : cond.rctt) {
+
+      // Disjunction for all the processes
+      BDD proc_reactants = BDD_FALSE;
+
+      if (ctxEntityExists(prod_proc_id, reactant)) {
+        proc_reactants += encCtxEntity(prod_proc_id, reactant);
+      }
+
+      for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
+        if (productEntityExists(proc_id, reactant)) {
+
+          proc_reactants += encProcEnabled(proc_id) * encEntity(proc_id, reactant);
+
+          VERB_LN(5, "| - if process " << rs->getProcessName(proc_id) << " is enabled and has " << rs->getEntityName(reactant));
+
+        }
+      } // END FOR: prod_id
+
+      reactants *= proc_reactants;
+    } // END FOR: reactant
+
+
+    // Take all the inhibitors... (conjunction)
+    BDD inhibitors = BDD_TRUE;
+
+    for (const auto &inhibitor : cond.inhib) {
+
+      // Conjunction for all the processes
+      BDD proc_inhibitors = BDD_TRUE;
+
+      if (ctxEntityExists(prod_proc_id, inhibitor)) {
+        proc_inhibitors *= !encCtxEntity(prod_proc_id, inhibitor);
+      }
+
+      for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
+        if (productEntityExists(proc_id, inhibitor)) {
+          proc_inhibitors *= !encEntity(proc_id, inhibitor) + !encProcEnabled(proc_id);
+        }
+      }
+
+      inhibitors *= proc_inhibitors;
+
+    }
+
+    enab += reactants * inhibitors;
+
+  } // END FOR: cond
+
+  reorder();
+
+  return enab;
+}
+
+// BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
+// {
+//   assert(prod_conds.size() > prod_proc_id);
+
+//   BDD enab = BDD_FALSE;
+
+//   auto production_conditions = prod_conds[prod_proc_id][entity_id];
+
+//   VERB_LN(5, "| Produce " << rs->getEntityName(entity_id) << " in " << rs->getProcessName(prod_proc_id) << ":");
+
+//   for (const auto &cond : production_conditions) {
+
+//     BDD reactants = BDD_TRUE;
+//     BDD inhibitors = BDD_TRUE;
+
+//     for (const auto &reactant : cond.rctt) {
+//       BDD proc_reactants = BDD_FALSE;
+
+//       for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
+//         if (processUsesEntity(proc_id, reactant)) {
+//           proc_reactants += encProcEnabled(proc_id) * encEntityCondition(proc_id, reactant);
+
+//           VERB_LN(5, "| - if process " << rs->getProcessName(proc_id) << " is enabled and has " << rs->getEntityName(reactant));
+
+//         }
+//       } // END FOR: prod_id
+
+//       reactants *= proc_reactants;
+//     } // END FOR: reactant
+
+//     // For inhibitors, we take all the processes first and then we iterate over the inhibitors
+//     for (unsigned int proc_id = 0; proc_id < numberOfProc; ++proc_id) {
+//       BDD proc_inhibitors = BDD_TRUE;
+
+//       for (const auto &inhibitor : cond.inhib) {
+//         if (processUsesEntity(proc_id, inhibitor)) {
+//           proc_inhibitors *= !encEntityCondition(proc_id, inhibitor);
+//         }
+//       }
+
+//       if (proc_inhibitors != BDD_TRUE) { // just an optimisation
+//         proc_inhibitors += !encProcEnabled(proc_id);
+//         inhibitors *= proc_inhibitors;
+//       }
+//     }
+
+//     enab += reactants * inhibitors;
+
+//   } // END FOR: cond
+
+//   if (opts->reorder_trans) {
+//     VERB_L2("Reordering");
+//     Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+//   }
+
+//   return enab;
+// }
+
+
+BDD SymRS::encEntitySameSuccessor(Process proc_id, Entity entity_id)
+{
+  return BDD_IFF(encEntity(proc_id, entity_id), encEntitySucc(proc_id, entity_id));
+}
+
+BDD SymRS::encEntityProduction(Process proc_id, Entity entity_id)
+{
+  BDD enabled = encEnabledness(proc_id, entity_id);
+
+  BDD when_produced = enabled * encEntitySucc(proc_id, entity_id);
+  BDD when_not_produced = !enabled * !encEntitySucc(proc_id, entity_id);
+
+  BDD proc_enabled = encProcEnabled(proc_id) * (when_produced + when_not_produced);
+  BDD proc_disabled = !encProcEnabled(proc_id) * encEntitySameSuccessor(proc_id, entity_id);
+
+  BDD result = proc_enabled + proc_disabled;
+
+  return result;
+}
+
+void SymRS::encodeTransitions(void)
+{
+  VERB("Decomposing reactions");
+
+  prod_conds.resize(numberOfProc);
+
+  for (auto proc_id = 0; proc_id < numberOfProc; ++proc_id) {
+    prod_conds[proc_id] = getProductionConditions(proc_id);
+  }
+
+  VERB("Encoding reactions");
+
+  if (opts->part_tr_rel) {
+    VERB("Using partitioned transition relation encoding");
+
+    if (usingContextAutomaton()) {
+      partTrans = new BDDvec(numberOfProc + 1);
+    }
+    else {
+      partTrans = new BDDvec(numberOfProc);
+    }
+
+  }
+  else {
+
+    VERB("Using monolithic transition relation encoding");
+    monoTrans = new BDD(BDD_TRUE);
+
+  }
+
+  VERB_LN(3, "Entity production encoding for all the processes and their products");
+
+  if (opts->part_tr_rel) {
+
+    for (const auto &proc_products : usedProducts) {
+      auto proc_id = proc_products.first;
+      auto products = proc_products.second;
+
+      (*partTrans)[proc_id] = BDD_TRUE;
+
+      for (const auto &prod : products) {
+        (*partTrans)[proc_id] *= encEntityProduction(proc_id, prod);
+      }
+    }
+
+
+  }
+  else {
+
+    for (const auto &proc_products : usedProducts) {
+      auto proc_id = proc_products.first;
+      auto products = proc_products.second;
+
+      for (const auto &prod : products) {
+        *monoTrans *= encEntityProduction(proc_id, prod);
+      }
+    }
+
+  }
+
+  VERB("Reactions ready");
+
+  if (usingContextAutomaton()) {
+    VERB("Augmenting transitions with transitions for context automaton");
+
+    if (opts->part_tr_rel) {
+      auto last_index = numberOfProc;
+      (*partTrans)[last_index] = *tr_ca;
+    }
+    else {
+      assert(tr_ca != nullptr);
+      *monoTrans *= *tr_ca;
+      reorder();
+    }
+  }
+}
+
+void SymRS::encodeInitStates(void)
+{
+  if (usingContextAutomaton()) {
+    VERB("Encoding initial states (using context automaton)");
+    encodeInitStatesForCtxAut();
+  }
+  else {
+    FERROR("Context automaton required");
+  }
+
+  VERB("Initial states encoded");
+}
+
+void SymRS::encodeInitStatesForCtxAut(void)
+{
+  initStates = new BDD(BDD_TRUE);
+
+  for (unsigned int i = 0; i < totalRctSysStateVars; ++i) {
+    *initStates *= !(*pv)[i];
+  }
+
+  *initStates *= getEncCtxAutInitState();
+}
+
+BDD SymRS::encActStrEntity(std::string proc_name, std::string entity_name) const
+{
+  auto enc_entity = encCtxEntity(rs->getProcessID(proc_name), rs->getEntityID(entity_name));
+  return enc_entity;
 }
 
 size_t SymRS::getCtxAutStateEncodingSize(void)
 {
-	if (!usingContextAutomaton()) return 0;
-	
-	assert(rs->ctx_aut != nullptr);
-	
-    size_t bitCount = 0;
-    size_t bitCountMaxVal = 1;
-    size_t numStates = rs->ctx_aut->statesCount();
-    while (bitCountMaxVal <= numStates)
-    {
-        bitCount++;
-        bitCountMaxVal *= 2;
-    }
-	
-	VERB_LN(3, "Bits required for CA: " << bitCount);
-    return bitCount;
+  if (!usingContextAutomaton()) {
+    return 0;
+  }
+
+  assert(rs->ctx_aut != nullptr);
+
+  size_t bitCount = 0;
+  size_t bitCountMaxVal = 1;
+  size_t numStates = rs->ctx_aut->statesCount();
+
+  while (bitCountMaxVal < numStates) {
+    bitCount++;
+    bitCountMaxVal *= 2;
+  }
+
+  VERB_LN(3, "Bits required for CA: " << bitCount);
+  return bitCount;
 }
 
 BDD SymRS::encCtxAutState_raw(State state_id, bool succ) const
-{	
-	// select appropriate BDD vector
-	vector<BDD> *enc_vec;
-    if (succ)
-        enc_vec = pv_ca_succ;
-    else
-        enc_vec = pv_ca;
+{
+  // select appropriate BDD vector
+  BDDvec *enc_vec;
 
-	assert(enc_vec != nullptr);
- 
-    BDD r = BDD_TRUE;
-	State val = state_id;
+  if (succ) {
+    enc_vec = pv_ca_succ;
+  }
+  else {
+    enc_vec = pv_ca;
+  }
 
-	for (unsigned int i = 0; i < totalCtxAutStateVars; ++i)
-	{
-		if (val != 0)
-		{
-			if (val % 2 == 1)
-			{
-				r *= (*enc_vec)[i];	
-			}
-			else
-			{
-				r *= !(*enc_vec)[i];	
-			}
-			val /= 2;
-		}
-		else
-			r *= !(*enc_vec)[i];
-	}
+  assert(enc_vec != nullptr);
 
-    return r;
+  BDD r = BDD_TRUE;
+  State val = state_id;
+
+  for (unsigned int i = 0; i < totalCtxAutStateVars; ++i) {
+    if (val != 0) {
+      if (val % 2 == 1) {
+        r *= (*enc_vec)[i];
+      }
+      else {
+        r *= !(*enc_vec)[i];
+      }
+
+      val /= 2;
+    }
+    else {
+      r *= !(*enc_vec)[i];
+    }
+  }
+
+  return r;
 }
 
 BDD SymRS::getEncCtxAutInitState(void)
 {
-	VERB_LN(2, "Encoding context automaton's initial state");
-	
-	State state = rs->ctx_aut->getInitState();
+  VERB_LN(1, "Encoding context automaton's initial state");
 
-	return encCtxAutState(state);
+  State state = rs->ctx_aut->getInitState();
+
+  return encCtxAutState(state);
 }
 
 void SymRS::encodeCtxAutTrans(void)
 {
-	VERB_LN(2, "Encoding context automaton's transition relation");
+  VERB_LN(1, "Encoding context automaton's transition relation");
 
-	if (tr_ca != nullptr)
-	{
-		VERB_LN(1, "Encoding for context automaton already present, not replacing")
-		return;	
-	}
-	
-	tr_ca = new BDD(BDD_FALSE);
+  if (tr_ca != nullptr) {
+    VERB_LN(1, "Encoding for context automaton already present, not replacing")
+    return;
+  }
 
-	for (auto &t : rs->ctx_aut->transitions)
-	{
-		VERB_LN(2, "Encoding CA transition " << rs->ctx_aut->getStateName(t.src_state) 
-			<< " -> " << rs->ctx_aut->getStateName(t.dst_state));
-		BDD enc_src = encCtxAutState(t.src_state);
-		BDD enc_dst = encCtxAutStateSucc(t.dst_state);
-		BDD enc_ctx = compContext(encActEntitiesConj(t.ctx));
-		
-		*tr_ca += enc_src * enc_ctx * enc_dst;
-	}
+  tr_ca = new BDD(BDD_FALSE);
+
+  for (auto &t : rs->ctx_aut->transitions) {
+    VERB_LN(2, "Encoding CA transition " << rs->ctx_aut->getStateName(t.src_state)
+            << " -> " << rs->ctx_aut->getStateName(t.dst_state));
+    BDD enc_src = encCtxAutState(t.src_state);
+    BDD enc_dst = encCtxAutStateSucc(t.dst_state);
+    BDD enc_ctx = compContext(encContext(t.ctx));
+    BDD enc_drs_state = BDD_TRUE;
+
+    if (t.state_constr != nullptr) {
+      enc_drs_state = t.state_constr->getBDDforState(this);
+    }
+
+    BDD new_trans = enc_src * enc_drs_state * enc_ctx * enc_dst;
+
+    *tr_ca += new_trans;
+
+    reorder();
+  }
+}
+
+
+void SymRS::reorder(void)
+{
+  if (opts->reorder_trans) {
+    VERB_L2("Reordering START");
+    // Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+    cuddMgr->ReduceHeap(CUDD_REORDER_GROUP_SIFT);
+    VERB_L2("Reordering DONE");
+  }
 }
 
 /** EOF **/
diff --git a/symrs.hh b/symrs.hh
index 376c559..aa275af 100644
--- a/symrs.hh
+++ b/symrs.hh
@@ -13,11 +13,12 @@
 #include <algorithm>
 #include <map>
 #include <cassert>
+#include <iostream>
 #include "cudd.hh"
 #include "types.hh"
 #include "macro.hh"
 #include "bdd_macro.hh"
-#include "rs.hh"
+// #include "rs.hh"
 #include "options.hh"
 #include "memtime.hh"
 
@@ -27,79 +28,289 @@ using std::endl;
 using std::vector;
 using std::map;
 
+class RctSys;
+
 class SymRS
 {
     friend class ModelChecker;
-    friend class FormRSCTL;
+    friend class FormRSCTLK;
+
+  public:
+    SymRS(RctSys *rs, Options *opts);
+
+    BDDvec *getEncPV(void)
+    {
+      return pv;
+    }
+    BDDvec *getEncPVsucc(void)
+    {
+      return pv_succ;
+    }
+    BDD *getEncPV_E(void)
+    {
+      return pv_E;
+    }
+    BDD *getEncPVsucc_E(void)
+    {
+      return pv_succ_E;
+    }
+    BDD *getEncPVctx_E(void)
+    {
+      return pv_ctx_E;
+    }
+    BDD *getEncPVproc_enab_E(void)
+    {
+      return pv_proc_enab_E;
+    }
+    BDDvec *getEncPVdrs_E(void)
+    {
+      return pv_drs_E;
+    }
+    BDDvec *getEncPartTrans(void)
+    {
+      return partTrans;
+    }
+    BDD *getEncMonoTrans(void)
+    {
+      return monoTrans;
+    }
+    BDD *getEncInitStates(void)
+    {
+      return initStates;
+    }
+    Cudd *getCuddMgr(void)
+    {
+      return cuddMgr;
+    }
+    unsigned int getTotalStateVars(void)
+    {
+      return totalStateVars;
+    }
+    unsigned int getTotalRctSysStateVars(void)
+    {
+      return totalRctSysStateVars;
+    }
+    BDD encEntity(std::string proc_name, std::string entity_name) const;
+    BDD encActStrEntity(std::string proc_name, std::string entity_name) const;
+    BDD getBDDtrue(void) const
+    {
+      return BDD_TRUE;
+    }
+    BDD getBDDfalse(void) const
+    {
+      return BDD_FALSE;
+    }
+
+    /**
+     * @brief Checks if context automaton is used
+     *
+     * @return True if CA is used
+     */
+    bool usingContextAutomaton(void);
+
+    /**
+     * @brief Encodes a context automaton's state
+     *
+     * @return Returns the encoded state
+     */
+    BDD encCtxAutState_raw(State state_id, bool succ) const;
+
+    /**
+     * @brief Encodes a context automaton's state (as predecessor/non-primed)
+     *
+     * @return Returns the encoded state
+     */
+    BDD encCtxAutState(State state_id) const
+    {
+      return encCtxAutState_raw(state_id, false);
+    }
+
+    /**
+     * @brief Encodes a context automaton's state (as successor/primed)
+     *
+     * @return Returns the encoded state
+     */
+    BDD encCtxAutStateSucc(State state_id) const
+    {
+      return encCtxAutState_raw(state_id, true);
+    }
+
+    /**
+     * @brief Encodes the initial state of context automaton
+     *
+     * @return Returns the encoded state(s)
+     */
+    BDD getEncCtxAutInitState(void);
+
+    /**
+     * @brief Getter for context automaton's state variables (predecessor/non-primed)
+     *
+     * @return Returns a vector of BDDs
+     */
+    BDDvec *getEncCtxAutPV(void)
+    {
+      return pv_ca;
+    }
+
+    /**
+     * @brief Getter for context automaton's successor (primed) state variables
+     *
+     * @return Returns a vector of BDDs
+     */
+    BDDvec *getEncCtxAutPVsucc(void)
+    {
+      return pv_ca_succ;
+    }
+
+    /**
+     * @brief Getter for context automaton's quantification BDD (for non-primed vars)
+     *
+     * @return Returns a BDD for quantification
+     */
+    BDD *getEncCtxAutPV_E(void)
+    {
+      return pv_ca_E;
+    }
+
+    /**
+     * @brief Getter for context automaton's quantification BDD (for primed vars)
+     *
+     * @return Returns a BDD for quantification
+     */
+    BDD *getEncCtxAutPVsucc_E(void)
+    {
+      return pv_ca_succ_E;
+    }
+
+    /**
+     * @brief Encodes the monolithic transition relation
+     */
+    void encodeCtxAutTrans(void);
+
+    /**
+     * @brief Getter for context automaton's transition relation
+     *
+     * @return Returns a BDD encoding the transition relation
+     */
+    BDD *getEncCtxAutTrans(void)
+    {
+      return tr_ca;
+    }
+
+  private:
 
     RctSys *rs;
     Cudd *cuddMgr;
     Options *opts;
 
-	// Mapping: entity ID -> action/context entity ID
-    StateEntityToAction stateToAct;
+    BDD *initStates;              /*!< BDD with initial states encoded */
 
-    BDD *initStates;
-	
-    vector<BDD> *pv;
-    vector<BDD> *pv_succ;
+    BDDvec *pv;                   /*!< PVs for the global state (all the variables, flat) */
+    BDDvec *pv_succ;
     BDD *pv_E;
     BDD *pv_succ_E;
 
-    vector<BDD> *pv_rs;
-    vector<BDD> *pv_rs_succ;
-    BDD *pv_rs_E;
-    BDD *pv_rs_succ_E;
+    BDDvec *pv_proc_enab;         /*!< Variables indicating if a process is enabled */
+    BDD *pv_proc_enab_E;
 
-    vector<BDD> *partTrans;
+    vector<BDDvec> *pv_drs;       /*!< PVs for the product part of state
+                                       (per DRS process) */
+    vector<BDDvec> *pv_drs_succ;  /*!< PVs for the product (successor)
+                                       part of state (per DRS process) */
 
+    BDDvec *pv_drs_E;             /*!< Quantification BDDs for each process */
+
+    BDDvec *pv_drs_flat;          /*!< PVs for the DRS product part of state (flat) */
+    BDDvec *pv_drs_flat_succ;     /*!< PVs for the DRS product (successor) part of state (flat) */
+
+    BDD *pv_drs_flat_E;
+    BDD *pv_drs_flat_succ_E;
+
+    vector<DecompReactions> prod_conds; /*!< Production conditions (per process and per entity) */
+
+    BDDvec *partTrans;
     BDD *monoTrans;
 
-	// Context automaton
-	vector<BDD> *pv_ca;
-	vector<BDD> *pv_ca_succ;
-	BDD *pv_ca_E;
-	BDD *pv_ca_succ_E;
-	BDD *tr_ca;
+    // Context automaton
+    BDDvec *pv_ca;
+    BDDvec *pv_ca_succ;
+    BDD *pv_ca_E;
+    BDD *pv_ca_succ_E;
+    BDD *tr_ca;
 
-    vector<BDD> *pv_act;
+    BDDvec *pv_ctx;               /*!< Flat */
+    BDD *pv_ctx_E;
+    vector<BDDvec> *pv_proc_ctx;
+    BDDvec *pv_proc_ctx_E;
+
+    // TODO: remove
+    BDDvec *pv_act;
     BDD *pv_act_E;
 
+    unsigned int totalEntities;
+    unsigned int numberOfProc;         /*!< The number of DRS processes */
     unsigned int totalStateVars;
-    unsigned int totalReactions;
-    unsigned int totalRctSysStateVars;
+    unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */
+    unsigned int totalCtxEntities;     /*!< Total number of different (process,context) entities used */
     unsigned int totalActions;
-	unsigned int totalCtxAutStateVars;
-	
-    BDD encEntity_raw(Entity entity, bool succ) const;
-    BDD encEntity(Entity entity) const {
-        return encEntity_raw(entity, false);
-    }
-    BDD encActEntity(Entity entity) const {
-		assert(entity < pv_act->size());
-        return (*pv_act)[entity];
-    }
-    BDD encEntitySucc(Entity entity) const {
-        return encEntity_raw(entity, true); 
-    }
-    BDD encEntitiesConj_raw(const Entities &entities, bool succ);
-    BDD encEntitiesConj(const Entities &entities) {
-        return encEntitiesConj_raw(entities, false);
-    }
-    BDD encEntitiesConjSucc(const Entities &entities) {
-        return encEntitiesConj_raw(entities, true);
-    }
-    BDD encEntitiesDisj_raw(const Entities &entities, bool succ);
-    BDD encEntitiesDisj(const Entities &entities) {
-        return encEntitiesDisj_raw(entities, false);
-    }
-    BDD encEntitiesDisjSucc(const Entities &entities) {
-        return encEntitiesDisj_raw(entities, true);
-    }
-    BDD encStateActEntitiesConj(const Entities &entities);
-    BDD encStateActEntitiesDisj(const Entities &entities);
+    unsigned int totalCtxAutStateVars;
 
-	BDD encActEntitiesConj(const Entities &entities);
+    EntitiesForProc usedProducts;     /*!< Entities used in products (per process) */
+    EntitiesForProc usedCtxEntities;  /*!< Entities used in context sets (per process) */
+
+    LocalIndicesForProcEntities prod_ent_local_idx; /*!< Local indices for each entity (per process): product entities */
+    LocalIndicesForProcEntities ctx_ent_local_idx;  /*!< Local indices for each entity (per process): context entities */
+
+    size_t getTotalProductVariables(void);
+    size_t getTotalCtxEntitiesVariables(void);
+
+    unsigned int getLocalProductEntityIndex(Process proc_id, Entity entity) const;
+    unsigned int getLocalCtxEntityIndex(Process proc_id, Entity entity) const;
+
+    BDD encEntity_raw(Process proc_id, Entity entity, bool succ) const;
+    BDD encEntity(Process proc_id, Entity entity) const
+    {
+      return encEntity_raw(proc_id, entity, false);
+    }
+    BDD encEntitySucc(Process proc_id, Entity entity) const
+    {
+      return encEntity_raw(proc_id, entity, true);
+    }
+
+    BDD encCtxEntity(Process proc_id, Entity entity) const;
+
+    bool productEntityExists(Process proc_id, Entity entity) const;
+    bool ctxEntityExists(Process proc_id, Entity entity) const;
+    bool processUsesEntity(Process proc_id, Entity entity_id) const;
+
+    BDD encProcEnabled(Process proc_id) const
+    {
+      return (*pv_proc_enab)[proc_id];
+    }
+
+    BDD encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ);
+    BDD encEntitiesConj(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesConj_raw(proc_id, entities, false);
+    }
+    BDD encEntitiesConjSucc(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesConj_raw(proc_id, entities, true);
+    }
+
+    BDD encEntitiesDisj_raw(Process proc_id, const Entities &entities, bool succ);
+    BDD encEntitiesDisj(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesDisj_raw(proc_id, entities, false);
+    }
+    BDD encEntitiesDisjSucc(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesDisj_raw(proc_id, entities, true);
+    }
+
+    BDD encEntityCondition(Process proc_id, Entity entity_id);
+
+    BDD encContext(const EntitiesForProc &proc_entities);
 
     /**
      * @brief Complements an encoding of a given state by negating all the variables that are not set to true
@@ -113,122 +324,25 @@ class SymRS
     std::string decodedRctSysStateToStr(const BDD &state);
     void printDecodedRctSysStates(const BDD &states);
 
-	BDD encNoContext(void);
+    DecompReactions getProductionConditions(Process proc_id);
 
     void initBDDvars(void);
+
+    BDD encEnabledness(Process proc_id, Entity entity_id);
+    BDD encEntitySameSuccessor(Process proc_id, Entity entity_id);
+    BDD encEntityProduction(Process proc_id, Entity entity_id);
+
     void encodeTransitions(void);
-    void encodeTransitions_old(void);
     void encodeInitStates(void);
-	void encodeInitStatesForCtxAut(void);
-	void encodeInitStatesNoCtxAut(void);
-    void mapStateToAct(void);
+    void encodeInitStatesForCtxAut(void);
+    LocalIndicesForProcEntities buildLocalEntitiesMap(const EntitiesForProc &procEnt);
+    void mapProcEntities(void);
     void encode(void);
 
-    int getMappedStateToActID(int stateID) const 
-	{ 
-		assert(stateID < static_cast<int>(totalRctSysStateVars)); 
-		return stateToAct[stateID]; 
-	}
+    size_t getCtxAutStateEncodingSize(void);
 
-	size_t getCtxAutStateEncodingSize(void);
-	
-public:
-    SymRS(RctSys *rs, Options *opts);
-	
-    vector<BDD> *getEncPV(void) { return pv; }
-    vector<BDD> *getEncPVsucc(void) { return pv_succ; }
-    BDD *getEncPV_E(void) { return pv_E; }
-    BDD *getEncPVsucc_E(void) { return pv_succ_E; }
-    BDD *getEncPVact_E(void) { return pv_act_E; }
-    vector<BDD> *getEncPartTrans(void) { return partTrans; }
-    BDD *getEncMonoTrans(void) { return monoTrans; }
-    BDD getEncState(const Entities &entities);
-    BDD *getEncInitStates(void) { return initStates; }
-    Cudd *getCuddMgr(void) { return cuddMgr; }
-    unsigned int getTotalStateVars(void) { return totalStateVars; }
-    unsigned int getTotalRctSysStateVars(void) { return totalRctSysStateVars; }
-    BDD encEntity(std::string name) const {
-        return encEntity(rs->getEntityID(name));
-    }
-	
-    BDD encActStrEntity(std::string name) const;
-    BDD getBDDtrue(void) const { return BDD_TRUE; }
-    BDD getBDDfalse(void) const { return BDD_FALSE; }
-	
-    /**
-     * @brief Checks if context automaton is used
-     *
-     * @return True if CA is used
-     */
-	bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; }
-	
-    /**
-     * @brief Encodes a context automaton's state
-     *
-     * @return Returns the encoded state
-     */
-	BDD encCtxAutState_raw(State state_id, bool succ) const;
+    void reorder(void);
 
-	/**
-     * @brief Encodes a context automaton's state (as predecessor/non-primed)
-     *
-     * @return Returns the encoded state
-     */
-	BDD encCtxAutState(State state_id) const { return encCtxAutState_raw(state_id, false); }
-	
-    /**
-     * @brief Encodes a context automaton's state (as successor/primed)
-     *
-     * @return Returns the encoded state
-     */
-	BDD encCtxAutStateSucc(State state_id) const { return encCtxAutState_raw(state_id, true); }
-	
-    /**
-     * @brief Encodes the initial state of context automaton
-     *
-     * @return Returns the encoded state(s)
-     */
-	BDD getEncCtxAutInitState(void);
-	
-    /**
-     * @brief Getter for context automaton's state variables (predecessor/non-primed)
-     *
-     * @return Returns a vector of BDDs
-     */
-	vector<BDD> *getEncCtxAutPV(void) { return pv_ca; }
-
-    /**
-     * @brief Getter for context automaton's successor (primed) state variables
-     *
-     * @return Returns a vector of BDDs
-     */
-	vector<BDD> *getEncCtxAutPVsucc(void) { return pv_ca_succ; }
-
-    /**
-     * @brief Getter for context automaton's quantification BDD (for non-primed vars)
-     *
-     * @return Returns a BDD for quantification 
-     */
-	BDD *getEncCtxAutPV_E(void) { return pv_ca_E; }
-
-    /**
-     * @brief Getter for context automaton's quantification BDD (for primed vars)
-     *
-     * @return Returns a BDD for quantification 
-     */
-	BDD *getEncCtxAutPVsucc_E(void) { return pv_ca_succ_E; }
-
-    /**
-     * @brief Encodes the monolithic transition relation
-     */	
-	void encodeCtxAutTrans(void);
-	
-    /**
-     * @brief Getter for context automaton's transition relation
-     *
-     * @return Returns a BDD encoding the transition relation
-     */	
-	BDD *getEncCtxAutTrans(void) { return tr_ca; }	
 };
 
 #endif
diff --git a/types.hh b/types.hh
index 23529bf..9d69bf7 100644
--- a/types.hh
+++ b/types.hh
@@ -13,16 +13,29 @@
 #include <map>
 #include <vector>
 #include <string>
+#include "cudd.hh"
+
+typedef unsigned char Oper;
+
+typedef std::vector<BDD> BDDvec;
 
 typedef unsigned int Entity;
 typedef std::set<Entity> Entities;
 struct Reaction {
-    Entities rctt;
-    Entities inhib;
-    Entities prod;
+  Entities rctt;
+  Entities inhib;
+  Entities prod;
 };
+
+typedef unsigned int Process;
+typedef std::vector<std::string> ProcessesById;
+typedef std::map<std::string, Process> ProcessesByName;
+typedef std::set<Process> ProcSet;
+
 typedef std::vector<Reaction> Reactions;
-typedef std::vector<std::string> EntitiesByIds;
+typedef std::map<Process, Reactions> ReactionsForProc;
+
+typedef std::vector<std::string> EntitiesById;
 typedef std::map<std::string, Entity> EntitiesByName;
 typedef std::set<Entities> EntitiesSets;
 
@@ -30,19 +43,26 @@ typedef unsigned int State;
 typedef std::vector<std::string> StatesById;
 typedef std::map<std::string, State> StatesByName;
 
+typedef std::map<Process, Entities> EntitiesForProc;
+
+typedef std::map<Entity, unsigned int> EntiesToLocalIndex;
+typedef std::map<Process, EntiesToLocalIndex> LocalIndicesForProcEntities;
+
 struct ReactionCond {
-    Entities rctt;
-    Entities inhib;
+  Entities rctt;
+  Entities inhib;
 };
 
 typedef std::vector<ReactionCond> ReactionConds;
-typedef std::map<Entity,ReactionConds> DecompReactions;
+typedef std::map<Entity, ReactionConds> DecompReactions;
 typedef std::vector<int> StateEntityToAction;
 
+class StateConstr;
 struct CtxAutTransition {
-	State src_state;
-	Entities ctx;
-	State dst_state;
+  State src_state;
+  EntitiesForProc ctx;
+  StateConstr *state_constr;
+  State dst_state;
 };
 
 typedef std::vector<CtxAutTransition> CtxAutTransitions;