diff --git a/ctx_aut.cc b/ctx_aut.cc
index d806449..edc0f8a 100644
--- a/ctx_aut.cc
+++ b/ctx_aut.cc
@@ -121,9 +121,11 @@ void CtxAut::showTransitions(void)
     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;
   }
 }
@@ -134,16 +136,17 @@ void CtxAut::makeProgressive(void)
   assert(!made_progressive);
 
   std::string special_loc = "T";
-  while (hasState(special_loc))
-  {
+
+  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)
-  {
+
+  for (State s = 0; s < states_ids.size(); ++s) {
     if (s == special_loc_id) {
       continue;
     }
@@ -157,22 +160,23 @@ void CtxAut::makeProgressive(void)
 
   for (const auto &t : transitions) {
     State curr_st = t.src_state;
-    if (t.state_constr != nullptr)
-    {
+
+    if (t.state_constr != nullptr) {
       constrs[curr_st] = new StateConstr(
-      STC_OR, constrs[curr_st], t.state_constr);
+        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);
-      }
+  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;
diff --git a/ctx_aut.hh b/ctx_aut.hh
index f56b92f..164d4c7 100644
--- a/ctx_aut.hh
+++ b/ctx_aut.hh
@@ -35,7 +35,10 @@ class CtxAut
     void setInitState(std::string stateName);
     State getInitState(void);
     State getStateID(std::string name);
-    State getLastStateID(void) { return states_ids.size(); }
+    State getLastStateID(void)
+    {
+      return states_ids.size();
+    }
     std::string getStateName(State state_id);
     void printAutomaton(void);
     void showStates(void);
diff --git a/formrsctlk.cc b/formrsctlk.cc
index a760321..fd56f3a 100644
--- a/formrsctlk.cc
+++ b/formrsctlk.cc
@@ -263,23 +263,28 @@ std::string FormRSCTLK::getAgentsStr(void) const
 {
   std::string r = "";
   bool first = true;
-  for (const auto &a : agents)
-  {
-    if (first)
+
+  for (const auto &a : agents) {
+    if (first) {
       first = false;
-    else
+    }
+    else {
       r += " ";
+    }
+
     r += a;
   }
+
   return r;
 }
 
 ProcSet FormRSCTLK::getAgentsAsProcSet(RctSys *rs) const
 {
   ProcSet processes;
-  for (auto &a : agents)
-  {
+
+  for (auto &a : agents) {
     processes.insert(rs->getProcessID(a));
   }
+
   return processes;
 }
diff --git a/in/scripts/gen_tgc_sc.py b/in/scripts/gen_tgc_sc.py
index 23878f4..d4bfcf0 100755
--- a/in/scripts/gen_tgc_sc.py
+++ b/in/scripts/gen_tgc_sc.py
@@ -3,7 +3,7 @@
 from sys import argv,exit
 
 OPTIONS_STR = """
-options { use-context-automaton; make-progressive; }
+options { use-context-automaton; make-progressive; };
 """
 
 PROC_STR = """
@@ -18,16 +18,16 @@ PROC_STR = """
 
 CA_STR = """
 context-automaton {{
-    states {{ init, green, red }}
-    init-state {{ init }}
+    states {{ init, green, red }};
+    init-state {{ init }};
     transitions {{
 {:s}
-    }}
-}}
+    }};
+}};
 """
 
 PROPERTY_STR = """
-rsctlk-property {{ {:s} : {:s} }}
+rsctlk-property {{ {:s} : {:s} }};
 """
 
 
@@ -47,7 +47,7 @@ out += OPTIONS_STR
 out += "reactions {\n"
 for i in range(n):
     out += PROC_STR.format(i)
-out += "}\n"
+out += "};\n"
 
 transitions = ""
 
diff --git a/mc.cc b/mc.cc
index c4a3173..76f1128 100644
--- a/mc.cc
+++ b/mc.cc
@@ -127,6 +127,7 @@ inline BDD ModelChecker::getPreEctx(const BDD &states, const BDD *contexts)
       q *= x * trans;
       reorder();
     }
+
     q *= *contexts;
   }
   else {
@@ -367,13 +368,11 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
     auto proc_set = form->getAgentsAsProcSet(srs->rs);
     return *reach - (statesNE(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
   }
-  else if (oper == RSCTLK_NC)
-  {
+  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)
-  {
+  else if (oper == RSCTLK_UC) {
     auto proc_set = form->getAgentsAsProcSet(srs->rs);
     return *reach - (statesNC(*reach - getStatesRSCTLK(form->getLeftSF()), proc_set) * *reach);
   }
@@ -475,8 +474,7 @@ BDD ModelChecker::statesNE(const BDD &states, ProcSet processes)
 {
   BDD x = BDD_FALSE;
 
-  for (auto const &proc_id : processes)
-  {
+  for (auto const &proc_id : processes) {
     x += states.ExistAbstract(getIthOnly(proc_id));
   }
 
@@ -488,14 +486,14 @@ BDD ModelChecker::statesNC(const BDD &states, ProcSet processes)
   BDD x = BDD_FALSE;
   BDD x_p = *reach;
 
-  while (x != x_p)
-  {
+  while (x != x_p) {
     x_p = x;
     BDD t = BDD_FALSE;
-    for (auto const &proc_id : processes)
-    {
+
+    for (auto const &proc_id : processes) {
       t += x.ExistAbstract(getIthOnly(proc_id));
     }
+
     x = t;
   }
 
diff --git a/memtime.hh b/memtime.hh
index af6a286..086fd6c 100644
--- a/memtime.hh
+++ b/memtime.hh
@@ -69,16 +69,18 @@ static inline int64 memUsedInt64()
 
 #if defined(__APPLE__)
 
-static inline double memUsed() {
-    malloc_statistics_t t;
-    malloc_zone_statistics(NULL, &t);
-    return (double)t.max_size_in_use / (1024*1024); }
+static inline double memUsed()
+{
+  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);
+  return memUsedInt64() / (1024 * 1024);
 }
 
 #endif
diff --git a/reactics.cc b/reactics.cc
index b4745fc..06aeab4 100644
--- a/reactics.cc
+++ b/reactics.cc
@@ -124,7 +124,7 @@ int main(int argc, char **argv)
   if (optind < argc) {
     inputfile = argv[optind];
   }
-	else if (!dump_help_message) {
+  else if (!dump_help_message) {
     cout << "Missing input file" << endl;
     dump_help_message = true;
   }
@@ -217,10 +217,12 @@ int main(int argc, char **argv)
 
   int ret_val;
 
-  if (result)
+  if (result) {
     ret_val = 0;
-  else
+  }
+  else {
     ret_val = 1;
+  }
 
   return ret_val;
 }
@@ -244,25 +246,25 @@ void print_help(std::string path_str)
 #endif
        << " Usage: " << path_str << " [options] <input file>" << endl << endl
        << " TASKS:" << endl
-       << "  -c   -- perform RSCTLK model checking" << 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 the set of all the reachable states" << endl
-       << "  -t   -- print the set of all the reachable states with their successors"
+       << "  -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 (may use less memory)" <<
+       << "  -b       -- disable bounded model checking (BMC) heuristic" << endl
+       << "  -x       -- use partitioned transition relation" <<
        endl
-       << "  -z   -- use reordering of the BDD variables" << endl
-       << "  -v   -- verbose (can be used more than once to increase verbosity)" <<
+       << "  -z       -- use reordering of the BDD variables" << endl
+       << "  -v       -- verbose (use more than once to increase verbosity)" <<
        endl
-       << "  -p   -- show progress (where possible)" << 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
+       << "  -m       -- measure and display time and memory usage" << endl
+       << "  -B       -- display an easy to parse summary (enables -m)" << endl
        << endl;
 }
 
diff --git a/rs.cc b/rs.cc
index 3b6ef7f..f04c578 100644
--- a/rs.cc
+++ b/rs.cc
@@ -363,8 +363,9 @@ void RctSys::ctxAutSaveCurrentContextSet(std::string processName)
 
 void RctSys::ctxAutFinalise(void)
 {
-  if (gen_ctxaut_progressive_closure)
+  if (gen_ctxaut_progressive_closure) {
     ctx_aut->makeProgressive();
+  }
 }
 
 /** EOF **/
diff --git a/rsin_driver.cc b/rsin_driver.cc
index 374f9b7..0c50b29 100644
--- a/rsin_driver.cc
+++ b/rsin_driver.cc
@@ -110,12 +110,11 @@ void rsin_driver::useContextAutomaton(void)
 void rsin_driver::makeProgressive(void)
 {
   make_progressive = true;
-  if (use_ctx_aut)
-  {
+
+  if (use_ctx_aut) {
     getReactionSystem()->ctxAutEnableProgressiveClosure();
   }
-  else
-  {
+  else {
     FERROR("Context automaton not enabled");
   }
 }
diff --git a/stateconstr.cc b/stateconstr.cc
index 734ddb4..8bb6f27 100644
--- a/stateconstr.cc
+++ b/stateconstr.cc
@@ -57,10 +57,12 @@ BDD StateConstr::getBDDforContext(const SymRS *srs) const
 BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
 {
   if (oper == STC_PV) {
-    if (encode_context)
+    if (encode_context) {
       return srs->encActStrEntity(proc_name, entity_name);
-    else
+    }
+    else {
       return srs->encEntity(proc_name, entity_name);
+    }
   }
   else if (oper == STC_TF) {
     if (tf) {
@@ -91,22 +93,26 @@ BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
 
 bool StateConstr::isFalse(void) const
 {
-  if (oper == STC_TF && tf == false)
+  if (oper == STC_TF && tf == false) {
     return true;
+  }
 
-  if (oper == STC_NOT && arg[0]->isTrue())
+  if (oper == STC_NOT && arg[0]->isTrue()) {
     return true;
+  }
 
   return false;
 }
 
 bool StateConstr::isTrue(void) const
 {
-  if (oper == STC_TF && tf == true)
+  if (oper == STC_TF && tf == true) {
     return true;
+  }
 
-  if (oper == STC_NOT && arg[0]->isFalse())
+  if (oper == STC_NOT && arg[0]->isFalse()) {
     return true;
+  }
 
   return false;
 }
diff --git a/symrs.cc b/symrs.cc
index 53a261a..62f60a6 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -773,7 +773,7 @@ void SymRS::encodeTransitions(void)
     VERB("Using partitioned transition relation encoding");
 
     if (usingContextAutomaton()) {
-      partTrans = new BDDvec(numberOfProc+1);
+      partTrans = new BDDvec(numberOfProc + 1);
     }
     else {
       partTrans = new BDDvec(numberOfProc);
@@ -789,8 +789,7 @@ void SymRS::encodeTransitions(void)
 
   VERB_LN(3, "Entity production encoding for all the processes and their products");
 
-  if (opts->part_tr_rel)
-  {
+  if (opts->part_tr_rel) {
 
     for (const auto &proc_products : usedProducts) {
       auto proc_id = proc_products.first;
@@ -949,9 +948,11 @@ void SymRS::encodeCtxAutTrans(void)
     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;