reactics-bdd/mc.cc

@@ -200,13 +200,13 @@ void ModelChecker::printReachWithSucc(void)
     t = unproc.PickOneMinterm(*pv);
     if (opts->backend_mode)
     {
-        cout << "G " << srs->decodedRctSysStateToStr(t) << endl;
+        cout << "G " << srs->decodedRctSysStateWithCtxAutToStr(t) << endl;
     }
     else
     {
-        cout << "Successors of " << srs->decodedRctSysStateToStr(t) << ":" << endl;
+        cout << "Successors of " << srs->decodedRctSysStateWithCtxAutToStr(t) << ":" << endl;
     }
-    srs->printDecodedRctSysStates(getSucc(t));
+    srs->printDecodedRctSysWithCtxAutStates(getSucc(t));
     unproc -= t;
   }
 

reactics-bdd/symrs.cc

@@ -567,6 +567,21 @@ std::string SymRS::decodedRctSysStateToStr(const BDD &state)
   return s;
 }
 
+std::string SymRS::decodedRctSysStateWithCtxAutToStr(const BDD &state)
+{
+  std::string s = "( ";
+  s += decodedRctSysStateToStr(state) + " ";
+  for (const auto &aut_state : rs->ctx_aut->states_ids) {
+    const auto state_id = rs->ctx_aut->getStateID(aut_state);
+    if (!(encCtxAutState(state_id) * state).IsZero()) {
+      s += aut_state + " ";
+      break;
+    }
+  }
+  s += ")";
+  return s;
+}
+
 void SymRS::printDecodedRctSysStates(const BDD &states)
 {
   BDD unproc = states;
@@ -591,6 +606,31 @@ void SymRS::printDecodedRctSysStates(const BDD &states)
   }
 }
 
+void SymRS::printDecodedRctSysWithCtxAutStates(const BDD &states)
+{
+  BDD unproc = states;
+
+  while (!unproc.IsZero()) {
+    BDD t = unproc.PickOneMinterm(*pv);
+    if (opts->backend_mode)
+    {
+        cout << "s " << decodedRctSysStateWithCtxAutToStr(t) << endl;
+    }
+    else
+    {
+        cout << decodedRctSysStateWithCtxAutToStr(t) << endl;
+    }
+
+    if (opts->verbose > 9) {
+      BDD_PRINT(t);
+      cout << endl;
+    }
+
+    unproc -= t;
+  }
+}
+
+
 DecompReactions SymRS::getProductionConditions(Process proc_id)
 {
   DecompReactions dr;

reactics-bdd/symrs.hh

@@ -319,7 +319,9 @@ class SymRS
     BDD compContext(const BDD &context) const;
 
     std::string decodedRctSysStateToStr(const BDD &state);
+    std::string decodedRctSysStateWithCtxAutToStr(const BDD &state);
     void printDecodedRctSysStates(const BDD &states);
+    void printDecodedRctSysWithCtxAutStates(const BDD &states);
 
     DecompReactions getProductionConditions(Process proc_id);