From 9aa34aca5143c57f272a0284b980370f07487909 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcin=20Pi=C4=85tkowski?= Date: Mon, 2 Jun 2025 23:08:12 +0200 Subject: [PATCH] Added export to XML (for data sharing with GUI) --- reactics-bdd/export.cc | 103 +++++++++++++++++++++++++++++++++++++++ reactics-bdd/export.hh | 2 + reactics-bdd/reactics.cc | 17 +++++-- 3 files changed, 119 insertions(+), 3 deletions(-) diff --git a/reactics-bdd/export.cc b/reactics-bdd/export.cc index 6682cec..b8fa322 100644 --- a/reactics-bdd/export.cc +++ b/reactics-bdd/export.cc @@ -808,3 +808,106 @@ string RSExporter::formulaToStr(const FormRSCTLK * form) { return "??"; } } + + +void RSExporter::exportToXML() { + output << "\n" + << indent << "\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + output << indent << indent << "processes_ids[proc] << "\">\n"; + + for (const auto & reaction : rs->proc_reactions[proc]) { + output << indent << indent << indent << "\n"; + + for (const Entity & e : reaction.rctt) { + output << indent << indent << indent << indent + << "" << rs->getEntityName(e) << "\n"; + } + + for (const Entity & e : reaction.inhib) { + output << indent << indent << indent << indent + << "" << rs->getEntityName(e) << "\n"; + } + + for (const Entity & e : reaction.prod) { + output << indent << indent << indent << indent + << "" << rs->getEntityName(e) << "\n"; + } + + output << indent << indent << indent << "\n"; + } + + output << indent << indent << "\n"; + } + + output << indent << "\n"; + + output << indent << "\n"; + + for (unsigned stId=0; stIdctx_aut->states_ids.size(); ++stId) { + if (rs->ctx_aut->states_ids[stId] == "T") + continue; + + output << indent << indent << "ctx_aut->states_ids[stId] << "\" x=\"0\" y=\"0\""; + + if (rs->ctx_aut->init_state_defined && stId == rs->ctx_aut->init_state_id) + output << " initial=\"true\""; + + output << "/>\n"; + } + + vector>> edges(rs->ctx_aut->states_ids.size()); + + for (const CtxAutTransition & trans : rs->ctx_aut->transitions) { + if (rs->ctx_aut->states_ids[trans.src_state] == "T" || rs->ctx_aut->states_ids[trans.dst_state] == "T") + continue; + + edges[trans.src_state][trans.dst_state].push_back(trans); + } + + for (unsigned src=0; srcctx_aut->getStateName(src) + << "\" to=\"" << rs->ctx_aut->getStateName(dst.first) << "\">\n"; + + for (const CtxAutTransition &trans : dst.second) { + output << indent << indent << indent << "procEntitiesToStr(trans.ctx) << "\""; + + if (trans.state_constr) + output << " guard=\"" << trans.state_constr->toStr() << "\""; + + output << "/>\n"; + } + + + output << indent << indent << "\n"; + } + } + + output << indent << "\n"; + + output << indent << "\n"; + + for (const auto & prop : drv->properties) { + string fStr = ""; + + for (const char ch : prop.second->toStr()) { + if (ch == '<') + fStr += "<"; + else if (ch =='>') + fStr += ">"; + else + fStr += ch; + } + + output << indent << indent << indent << "" + << fStr << "\n"; + + } + + output << indent << "\n"; + + output << "" << endl; +} diff --git a/reactics-bdd/export.hh b/reactics-bdd/export.hh index b8b0714..bc7d3a7 100644 --- a/reactics-bdd/export.hh +++ b/reactics-bdd/export.hh @@ -14,6 +14,8 @@ public: RSExporter(RctSys *rs, rsin_driver *drv, std::ostream & outStream = std::cout); void exportToISPL(); + void exportToXML(); + private: RctSys *rs; rsin_driver *drv; diff --git a/reactics-bdd/reactics.cc b/reactics-bdd/reactics.cc index c86fec5..90e1298 100644 --- a/reactics-bdd/reactics.cc +++ b/reactics-bdd/reactics.cc @@ -17,6 +17,7 @@ int main(int argc, char **argv) bool reach_states = false; bool reach_states_succ = false; bool export_to_ispl = false; + bool export_to_xml = false; bool bmc = true; bool benchmarking = false; bool dump_help_message = false; @@ -32,7 +33,7 @@ int main(int argc, char **argv) int c; int option_index = 0; - while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheEG", long_options, + while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvXheyEG", long_options, &option_index)) != -1) { switch (c) { case 0: @@ -57,6 +58,10 @@ int main(int argc, char **argv) export_to_ispl = true; break; + case 'y': + export_to_xml = true; + break; + //case 'b': // printf("-b with %s\n", optarg); // break; @@ -141,7 +146,7 @@ int main(int argc, char **argv) } if (!(reach_states || reach_states_succ || rstl_model_checking - || show_reactions || print_parsed_sys || export_to_ispl)) { + || show_reactions || print_parsed_sys || export_to_ispl || export_to_xml)) { FERROR("No task specified: -c, -P, -r, -s, or -e needs to be used"); } @@ -176,7 +181,7 @@ int main(int argc, char **argv) rs.printSystem(); } - if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl) { + if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl || export_to_xml) { SymRS srs(&rs, opts); ModelChecker mc(&srs, opts); @@ -194,6 +199,11 @@ int main(int argc, char **argv) exp.exportToISPL(); } + if (export_to_xml) { + RSExporter exp(&rs, &driver); + exp.exportToXML(); + } + if (rstl_model_checking) { if (bmc) { cout << "Using BDD-based Bounded Model Checking" << endl; @@ -269,6 +279,7 @@ void print_help(std::string path_str) << " -v -- verbose (use more than once to increase verbosity)" << endl << " -p -- show progress (where possible)" << endl << " -X -- backend mode (makes output parsing easier)" << endl + << " -y -- export to XML (for GUI tool)" << endl << endl << " Optimisations:" << endl << " -E -- disable auto-reordering optimisation of BDDs" << endl