artur/reactics
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Context Automaton states in transitions (#2)

Browse Source
This commit was merged in pull request #2.
This commit is contained in:
Artur Meski
2025-04-29 13:13:50 +01:00
committed by GitHub
parent a864329883
commit f86316cdbd
3 changed files with 45 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

6
reactics-bdd/mc.cc
View File

@@ -200,13 +200,13 @@ void ModelChecker::printReachWithSucc(void)
t = unproc.PickOneMinterm(*pv); t = unproc.PickOneMinterm(*pv);
if (opts->backend_mode) if (opts->backend_mode)
{ {
cout << "G " << srs->decodedRctSysStateToStr(t) << endl; cout << "G " << srs->decodedRctSysStateWithCtxAutToStr(t) << endl;
} }
else 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; unproc -= t;
} }

40
reactics-bdd/symrs.cc
View File

@@ -567,6 +567,21 @@ std::string SymRS::decodedRctSysStateToStr(const BDD &state)
return s; 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) void SymRS::printDecodedRctSysStates(const BDD &states)
{ {
BDD unproc = 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 SymRS::getProductionConditions(Process proc_id)
{ {
DecompReactions dr; DecompReactions dr;

2
reactics-bdd/symrs.hh
View File

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