From 94ae1c602db7781a7030c66fdb2fa18eb7f77914 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Marcin=20Pi=C4=85tkowski?= Date: Wed, 2 Apr 2025 21:20:05 +0200 Subject: [PATCH] Complete rs to ispl translation. --- reactics-bdd/Makefile | 2 +- reactics-bdd/ctx_aut.hh | 1 + reactics-bdd/export.cc | 810 ++++++++++++++++++++++++++++++++++++ reactics-bdd/export.hh | 55 +++ reactics-bdd/formrsctlk.hh | 3 + reactics-bdd/reactics.cc | 20 +- reactics-bdd/reactics.hh | 1 + reactics-bdd/rs.hh | 1 + reactics-bdd/stateconstr.hh | 3 + 9 files changed, 891 insertions(+), 5 deletions(-) create mode 100644 reactics-bdd/export.cc create mode 100644 reactics-bdd/export.hh diff --git a/reactics-bdd/Makefile b/reactics-bdd/Makefile index 4235476..0a6c37e 100644 --- a/reactics-bdd/Makefile +++ b/reactics-bdd/Makefile @@ -11,7 +11,7 @@ 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 formrsctlk.o stateconstr.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 export.o all: reactics diff --git a/reactics-bdd/ctx_aut.hh b/reactics-bdd/ctx_aut.hh index 164d4c7..d446459 100644 --- a/reactics-bdd/ctx_aut.hh +++ b/reactics-bdd/ctx_aut.hh @@ -27,6 +27,7 @@ class StateConstr; class CtxAut { friend class SymRS; + friend class RSExporter; public: CtxAut(Options *opts, RctSys *parent_rctsys); diff --git a/reactics-bdd/export.cc b/reactics-bdd/export.cc new file mode 100644 index 0000000..6682cec --- /dev/null +++ b/reactics-bdd/export.cc @@ -0,0 +1,810 @@ + +#include "export.hh" + + +RSExporter::RSExporter(RctSys *rs, rsin_driver *drv, std::ostream & outStream): + rs(rs), drv(drv), output(outStream) { + + // Store all possible inputs (reactants and inhibitors) and outputs (products) for each process + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const auto & rr : rs->proc_reactions[proc]) { + for (const auto & e : rr.rctt) + procInputs[proc].insert(e); + + for (const auto & e : rr.inhib) + procInputs[proc].insert(e); + + for (const auto & e : rr.prod) + procOutputs[proc].insert(e); + } + } + + // Add possible inputs from context automaton + + for (const auto & trans : rs->ctx_aut->transitions) { + for (const auto & procCtx : trans.ctx) { + for (const auto & e : procCtx.second) { + procInputs[procCtx.first].insert(e); + } + } + } +} + + +void RSExporter::exportToISPL() { + exportEnvironment(); + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) + exportAgent(proc); + + parseFormulas(); + exportEvaluation(); + exportInitStates(); + exportFormulae(); +} + + +void RSExporter::exportEnvironment() { + output << "Agent Environment\n\n"; + + exportEnvironmentVars(); + exportEnvironmentActions(); + exportEnvironmentProtocol(); + exportEnvironmentEvolution(); + + output << "\nend Agent\n" << endl; +} + + +void RSExporter::exportEnvironmentVars() { + output << "Obsvars:\n" + << indent << "mode: {init, clear, select_active_agents, activate_agents,\n" + << indent << indent << "distribute_local, add_context, distribute_global, produce,\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const Entity & e : procOutputs[proc]) { + output << indent << indent << "collect_" << rs->processes_ids[proc] + << "_" << rs->entities_ids[e] << ",\n"; + } + } + + output << indent << indent << "finalize\n" << indent << "};\n\n"; + + output << indent << "-- Boolean variables denoting entities available for each agent --\n\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const Entity & e : procInputs[proc]) { + output << indent << rs->processes_ids[proc] + << "_" << rs->entities_ids[e] << ": 0..1;\n"; + } + + output << "\n"; + } + + output << indent << "-- Boolean variables denoting which agents are active --\n\n"; + + for (const string & procName : rs->processes_ids) + output << indent << "Active_" << procName << ": 0..1;\n"; + + output << "end Obsvars\n\n" + << "Vars:\n\n"; + + output << indent << "-- Context automaton details --\n\n"; + + output << indent << "state: {"; + + for (size_t i=0; ictx_aut->statesCount(); ++i) { + string stName = rs->ctx_aut->getStateName(i); + + // Skip the dummy state used for closure + if (stName == "T") + continue; + + if (i) output << ", "; + + output << stName; + } + + output << "};\n"; + + // Add dummy transition leading to the initial state (no agent is active) + output << indent << "transition: {" + << "\n" << indent << indent << "init_0"; + + int trId {1}; + + for (const CtxAutTransition & trans : rs->ctx_aut->transitions) { + string dstName = rs->ctx_aut->getStateName(trans.dst_state); + + if (dstName == "T") + continue; + + output << ","; + output << "\n" << indent << indent << rs->ctx_aut->getStateName(trans.src_state) + << "_" << dstName << "_" << trId; + ++trId; + } + + output << indent << "\n};\n\n"; + + output << indent << "-- Boolean variables denoting existence of entities in the environment.\n\n"; + + for (const string & entityName : rs->entities_ids) + output << indent << entityName << " : 0..1;\n"; + + output << "end Vars" << endl; +} + + +void RSExporter::exportEnvironmentActions() { + output << "\nActions = {\n" + << indent << "init, clear, select_active_agents, activate_agents,\n" + << indent << "distribute_local, add_context, distribute_global, produce,\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const Entity & e : procOutputs[proc]) { + output << indent << "collect_" << rs->processes_ids[proc] + << "_" << rs->entities_ids[e] << ",\n"; + } + } + + output << indent << "finalize, sleep\n};\n"; +} + + +void RSExporter::exportEnvironmentProtocol() { + output << "\nProtocol:\n" + << indent << "mode=clear : {clear};\n" + << indent << "mode=select_active_agents : {select_active_agents};\n" + << indent << "mode=activate_agents : {activate_agents};\n\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const Entity & e : procOutputs[proc]) { + output << indent << "mode=collect_" << rs->processes_ids[proc] + << "_" << rs->entities_ids[e] + << ": {collect_" << rs->processes_ids[proc] + << "_" << rs->entities_ids[e] << "};\n"; + } + + output << "\n"; + } + + output << indent << "mode=distribute_local : {distribute_local};\n" + << indent << "mode=add_context : {add_context};\n" + << indent << "mode=distribute_global : {distribute_global};\n" + << indent << "mode=produce : {produce};\n" + << indent << "mode=finalize : {finalize};\n\n" + << indent << "Other : {sleep};\n" + << "end Protocol\n"; +} + + +void RSExporter::exportEnvironmentEvolution() { + output << "\nEvolution:\n\n"; + + //-------------------------------------------------------------------------------- + // Reset the environment state after the previous computation step. + // (reset agent activity status, availability of entities, etc.) + //-------------------------------------------------------------------------------- + + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- Reset the environment state after the previous computation step.\n" + << indent <<"-- (reset agent activity status, availability of entities, etc.)\n" + << indent <<"--------------------------------------------------------------------------------\n\n" + << indent; + + for (const string & procName : rs->processes_ids) + output << "Active_" << procName << "=0 and "; + + output << "\n" << indent << indent; + + for (const string & entityName : rs->entities_ids) + output << entityName << "=0 and "; + + output << "\n" << indent << indent << "mode=select_active_agents\n" + << indent << indent << indent << "if mode=clear;\n\n"; + + //-------------------------------------------------------------------------------- + // Active agents are selected based on the current context automaton transition. + //-------------------------------------------------------------------------------- + + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- Active agents are selected based on the current context automaton transition.\n" + << indent <<"--------------------------------------------------------------------------------\n\n" + << indent; + + // For the dummy initial transition leading to the initial state no agent is active + for (Process proc=0; procgetNumberOfProcesses(); ++proc) + output << "Active_" << rs->getProcessName(proc) << "=0 and "; + + output << "mode=activate_agents\n" + << indent << indent << "if mode=select_active_agents and transition=init_0;\n\n" << indent; + + unsigned transNo = 1; + + for (const CtxAutTransition & trans : rs->ctx_aut->transitions) { + vector isActive(rs->getNumberOfProcesses(), false); + + string dstName = rs->ctx_aut->getStateName(trans.dst_state); + + if (dstName == "T") + continue; + + for (const auto & entry : trans.ctx) + isActive[entry.first] = true; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) + output << "Active_" << rs->getProcessName(proc) << "=" + << (isActive[proc] ? "1" : "0") + << " and "; + + output << "mode=activate_agents\n" + << indent << indent << "if mode=select_active_agents and transition=" + << rs->ctx_aut->getStateName(trans.src_state) << "_" + << rs->ctx_aut->getStateName(trans.dst_state) << "_" + << to_string(transNo) << ";\n\n" << indent; + + ++transNo; + } + + //-------------------------------------------------------------------------------- + // Conduct a series of queries to active agents regarding products + // that may have been produced in the last step when they were active. + //-------------------------------------------------------------------------------- + + output << "--------------------------------------------------------------------------------\n" + << indent << "-- Conduct a series of queries to active agents regarding products\n" + << indent << "-- that may have been produced in the last step when they were active.\n" + << indent << "--------------------------------------------------------------------------------\n\n"; + + vector> procProducts; + + for (Process proc=0; proc < rs->getNumberOfProcesses(); ++proc) + for (const Entity & e : procOutputs[proc]) + procProducts.push_back(make_pair(proc, e)); + + output << indent << "mode=collect_" + << rs->getProcessName(procProducts[0].first) << "_" + << rs->getEntityName(procProducts[0].second) << "\n" + << indent << indent << "if mode=activate_agents;\n\n"; + + for (unsigned pairIdx=1; pairIdx < procProducts.size(); ++pairIdx) { + output << indent << rs->getEntityName(procProducts[pairIdx-1].second) + << "=1 and mode=collect_" + << rs->getProcessName(procProducts[pairIdx].first) << "_" + << rs->getEntityName(procProducts[pairIdx].second) << "\n" + << indent << indent << "if mode=collect_" + << rs->getProcessName(procProducts[pairIdx-1].first) << "_" + << rs->getEntityName(procProducts[pairIdx-1].second) + << " and " << rs->getProcessName(procProducts[pairIdx-1].first) + << ".Action=produce_" + << rs->getEntityName(procProducts[pairIdx-1].second) + << ";\n"; + + output << indent << "mode=collect_" + << rs->getProcessName(procProducts[pairIdx].first) << "_" + << rs->getEntityName(procProducts[pairIdx].second) << "\n" + << indent << indent << "if mode=collect_" + << rs->getProcessName(procProducts[pairIdx-1].first) << "_" + << rs->getEntityName(procProducts[pairIdx-1].second) + << " and (" << rs->getProcessName(procProducts[pairIdx-1].first) + << ".Action=not_produce_" + << rs->getEntityName(procProducts[pairIdx-1].second) + << " or " << rs->getProcessName(procProducts[pairIdx-1].first) + << ".Action=sleep);\n\n"; + } + + output << indent << rs->getEntityName(procProducts.rbegin()->second) + << "=1 and mode=distribute_local\n" + << indent << indent << "if mode=collect_" + << rs->getProcessName(procProducts.rbegin()->first) << "_" + << rs->getEntityName(procProducts.rbegin()->second) + << " and " << rs->getProcessName(procProducts.rbegin()->first) + << ".Action=produce_" + << rs->getEntityName(procProducts.rbegin()->second) + << ";\n"; + + output << indent << "mode=distribute_local\n" + << indent << indent << "if mode=collect_" + << rs->getProcessName(procProducts.rbegin()->first) << "_" + << rs->getEntityName(procProducts.rbegin()->second) + << " and (" << rs->getProcessName(procProducts.rbegin()->first) + << ".Action=not_produce_" + << rs->getEntityName(procProducts.rbegin()->second) + << " or " << rs->getProcessName(procProducts.rbegin()->first) + << ".Action=sleep);\n\n"; + + //-------------------------------------------------------------------------------- + // The entities available in the environment are distributed between the agents. + //-------------------------------------------------------------------------------- + + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- The entities available in the environment are distributed between the agents. \n" + << indent <<"--------------------------------------------------------------------------------\n\n" + << indent; + + bool first = true; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const Entity & e : procInputs[proc]) { + if (!first) + output << " and "; + else + first = false; + + output << rs->getProcessName(proc) << "_" << rs->getEntityName(e) << "=" << rs->getEntityName(e); + } + + output << "\n" << indent; + } + + output << "and mode=add_context\n" << indent << indent + << "if mode=distribute_local;\n\n"; + + //-------------------------------------------------------------------------------- + // A set of additional entities, if any, is provided for each active agent + // following the context automaton transition description. + //-------------------------------------------------------------------------------- + + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- A set of additional entities, if any, is provided for each active agent\n" + << indent <<"-- following the context automaton transition description.\n" + << indent <<"--------------------------------------------------------------------------------\n\n" + << indent; + + transNo = 1; + vector> noCtxTrans; + + for (const CtxAutTransition & trans : rs->ctx_aut->transitions) { + if (rs->ctx_aut->getStateName(trans.dst_state) == "T") + continue; + + string ctxStr {""}; + string separator {""}; + first = true; + + for (const auto & procCtx : trans.ctx) { + for (auto ent : procCtx.second) { + if (first) { + first = false; + separator = ""; + } + else + separator = "and "; + + ctxStr += separator + rs->getProcessName(procCtx.first) + "_" + rs->getEntityName(ent) + "=1 "; + } + } + + if (ctxStr.length() > 0) + output << indent << ctxStr + << "and mode=distribute_global\n" << indent << indent + << "if mode=add_context and transition=" + << rs->ctx_aut->getStateName(trans.src_state) << "_" << rs->ctx_aut->getStateName(trans.dst_state) << "_" << transNo + << ";\n\n"; + else + noCtxTrans.push_back({trans.src_state, trans.dst_state, transNo}); + + ++transNo; + } + + //-------------------------------------------------------------------------------- + // Mode change for transitions having no additional entities in the context + //-------------------------------------------------------------------------------- + + if (noCtxTrans.size() > 0) { + output << indent << "mode=distribute_global if mode=add_context and\n" + << indent << indent << " (transition=init_0"; + + for (const auto & trans : noCtxTrans) { + output << " or transition=" << rs->ctx_aut->getStateName(get<0>(trans)) + << "_" << rs->ctx_aut->getStateName(get<1>(trans)) + << "_" << get<2>(trans); + } + + output << ");\n\n"; + } + + //-------------------------------------------------------------------------------- + // Notify active agents to execute all possible reactions. + //-------------------------------------------------------------------------------- + + output << indent << "--------------------------------------------------------------------------------\n" + << indent <<"-- Notify active agents to execute all possible reactions.\n" + << indent <<"--------------------------------------------------------------------------------\n\n" + << indent; + + output << "mode=produce if mode=distribute_global;\n\n"; + + output << indent << "mode=finalize\n" + << indent << indent << "if mode=produce;\n\n"; + + //-------------------------------------------------------------------------------- + // Select next computation step (choose context automaton transition). + //-------------------------------------------------------------------------------- + + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- Select next computation step (choose context automaton transition).\n" + << indent <<"--------------------------------------------------------------------------------\n\n" + << indent; + + transNo = 1; + + for (const CtxAutTransition & trans : rs->ctx_aut->transitions) { + if (rs->ctx_aut->getStateName(trans.dst_state) == "T") + continue; + + output << indent << "mode=clear and state=" + << rs->ctx_aut->getStateName(trans.dst_state) + << " and transition=" + << rs->ctx_aut->getStateName(trans.src_state) << "_" + << rs->ctx_aut->getStateName(trans.dst_state) << "_" + << transNo << "\n" << indent << indent; + + output << "\n" << indent << indent << "if mode=finalize and state=" + << rs->ctx_aut->getStateName(trans.src_state); + + if (trans.state_constr) + output << " and " << stateConstrToStr(trans.state_constr); + + output << ";\n\n"; + + ++transNo; + } + + output << "end Evolution\n"; +} + + +void RSExporter::exportEnvironmentInitState() { + output << indent << "Environment.mode=clear\n\n"; + + for (const string & procName : rs->processes_ids) + output << indent << indent << "and Environment.Active_" << procName << "=0\n"; + + output << "\n"; + + for (const string & entName : rs->entities_ids) + output << indent << indent << "and Environment." << entName << "=0\n"; + + output << "\n"; + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) { + for (const Entity & e : procInputs[proc]) + output << indent << indent << "and Environment." << rs->getProcessName(proc) << "_" + << rs->entities_ids[e] << "=0\n"; + + output << "\n"; + } + + State initState = rs->ctx_aut->getInitState(); + output << indent << indent + << "and Environment.state=" + << rs->ctx_aut->getStateName(initState) << "\n" + << indent << indent << "and Environment.transition=init_0"; +} + + +void RSExporter::exportAgent(const Process & proc) { + output << "\nAgent " << rs->processes_ids[proc] << "\n\n"; + + exportAgentVars(proc); + exportAgentProtocol(proc); + exportAgentEvolution(proc); + + output << "end Agent\n" << endl; +} + + +void RSExporter::exportAgentVars(const Process & proc) { + output << "Vars:\n" + << indent << "isActive: 0..1;\n"; + + for (const Entity & e : procInputs[proc]) { + output << indent << rs->entities_ids[e] << "_in: 0..1;\n"; + } + + for (const Entity & e : procOutputs[proc]) { + output << indent << rs->entities_ids[e] << "_out: 0..1;\n"; + } + + output << "end Vars\n\n"; + + output << "Actions = {\n"; + + for (const Entity & e : procOutputs[proc]) { + output << indent << "produce_" << rs->entities_ids[e] + << ", not_produce_" << rs->entities_ids[e] << ",\n"; + } + + output << indent << "sleep\n};\n\n"; +} + + +void RSExporter::exportAgentProtocol(const Process & proc) { + string procName = rs->processes_ids[proc]; + + output << "Protocol:\n"; + + for (const Entity & e : procOutputs[proc]) { + string entityName = rs->entities_ids[e]; + + output << indent << entityName << "_out=1 and (Environment.mode=collect_" << procName << "_" << entityName + << " and isActive=1): {produce_" << entityName << "};\n" + << indent << entityName << "_out=0 and (Environment.mode=collect_" << procName << "_" << entityName + << " and isActive=1): {not_produce_" << entityName << "};\n\n"; + } + + output << indent << "Other: {sleep};\n" + << "end Protocol\n\n"; +} + + +void RSExporter::exportAgentEvolution(const Process & proc) { + string procName = rs->processes_ids[proc]; + + output << "Evolution:\n\n"; + + //-------------------------------------------------------------------------------- + // Set the agent's activity status. + //-------------------------------------------------------------------------------- + + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- Set the agent's activity status.\n" + << indent <<"--------------------------------------------------------------------------------\n\n"; + + output << indent << "isActive=Environment.Active_" << procName << " "; + + for (const Entity & e : procInputs[proc]) + output << "and " << rs->entities_ids[e] << "_in=0 "; + + output << "\n" << indent << indent << "if Environment.Action=activate_agents;\n\n"; + + bool first {true}; + + //-------------------------------------------------------------------------------- + // Synchronise with the environment state. + //-------------------------------------------------------------------------------- + + output << indent << "--------------------------------------------------------------------------------\n" + << indent <<"-- Synchronise with the environment state.\n" + << indent <<"--------------------------------------------------------------------------------\n\n"; + + for (const Entity & e : procInputs[proc]) { + string entityName = rs->entities_ids[e]; + + if (first) { + first = false; + output << indent; + } + else { + output << "and "; + } + + output << entityName << "_in=Environment." << procName << "_" << entityName << " "; + } + + output << "\n" << indent << indent << "if isActive=1 and Environment.Action=distribute_global;\n\n"; + + exportAgentReactions(proc); + + output << "end Evolution\n\n"; +} + + +void RSExporter::exportAgentReactions(const Process & proc) { + output << indent <<"--------------------------------------------------------------------------------\n" + << indent <<"-- Agent's reactions.\n" + << indent <<"--------------------------------------------------------------------------------\n\n"; + + // For each entity produced accumulate all the ways it may be produced + + map sources; + + for (const auto & reaction : rs->proc_reactions[proc]) { + string rctCond = reactionCondToStr(reaction); + + for (const Entity & e : reaction.prod) { + string rctProduct = rs->getEntityName(e); + + if (sources.count(rctProduct)) + sources[rctProduct] = appendCondition(sources[rctProduct], rctCond); + else + sources[rctProduct] = rctCond; + } + } + + // Output a single formula combining all the agent's reactions + + bool moreReactions {false}; + + for (const auto & entry : sources) { + if (moreReactions) + output << indent << indent << "and\n"; + else + moreReactions = true; + + output << indent << entry.first << "_out = " << entry.second << "\n"; + } + + output << indent << indent << "if isActive=1 and Environment.Action=produce;\n\n"; +} + + +void RSExporter::exportAgentInitState(const Process & proc) { + string procName = rs->processes_ids[proc]; + + output << "\n\n" << indent << indent << "and " << procName << ".isActive=0"; + + for (const Entity & e : procInputs[proc]) { + output << "\n" << indent << indent << "and " << procName << "." << rs->entities_ids[e] << "_in=0"; + } + + for (const Entity & e : procOutputs[proc]) { + output << "\n" << indent << indent << "and " << procName << "." << rs->entities_ids[e] << "_out=0"; + } +} + + +void RSExporter::parseFormulas() { + for (const auto & prop : drv->properties) { + formulas.push_back(formulaToStr(prop.second)); + } +} + + +void RSExporter::exportEvaluation() { + output << "\nEvaluation\n"; + + for (const auto & a : atoms) + output << indent << a.second << " if " << a.first << ";\n"; + + output << "end Evaluation" << endl; +} + + +void RSExporter::exportInitStates() { + output << "\nInitStates\n"; + + exportEnvironmentInitState(); + + for (Process proc=0; procgetNumberOfProcesses(); ++proc) + exportAgentInitState(proc); + + output << ";\n" + << "end InitStates" << endl; +} + + +void RSExporter::exportFormulae() { + output << "\nFormulae\n"; + + for (const string & fStr : formulas) + output << indent << fStr << ";\n"; + + output << "end Formulae" << endl; +} + + +/* State constraints are required to be in conjunctive normal form. */ +string RSExporter::stateConstrToStr(const StateConstr * guard) { + string expr; + + switch (guard->oper) { + case STC_PV: + return guard->proc_name + "_" + guard->entity_name + "=1"; + + case STC_TF: + return guard->tf ? "true" : "false"; + + case STC_AND: + return "(" + stateConstrToStr(guard->arg[0]) + " and " + stateConstrToStr(guard->arg[1]) + ")"; + + case STC_OR: + return "(" + stateConstrToStr(guard->arg[0]) + " or " + stateConstrToStr(guard->arg[1]) + ")"; + + case STC_NOT: + expr = stateConstrToStr(guard->arg[0]); + return expr.substr(0, expr.length()-1) + "0"; + + default: + return "??"; + assert(0); + } +} + + +string RSExporter::reactionCondToStr(const Reaction & reaction) { + string cond; + + bool moreRctts {false}; + + for (const Entity & e : reaction.rctt) { + if (moreRctts) + cond += "*"; + else + moreRctts = true; + + cond += rs->getEntityName(e) + "_in"; + } + + for (const Entity & e : reaction.inhib) + cond += "*(1-" + rs->getEntityName(e) + "_in)"; + + return cond; +} + + +string RSExporter::appendCondition(string & oldCond, string & newCond) { + return "(" + oldCond + ") + " + newCond + " - (" + oldCond + ") * " + newCond; +} + + +string RSExporter::formulaToStr(const FormRSCTLK * form) { + string varStr; + string labelStr; + + switch (form->oper) { + + case RSCTLK_PV: // propositional variable + varStr = form->proc_name + "." + form->entity_name + "_out=1"; + + if (atoms.find(varStr) == atoms.end()) { + labelStr = "atomic_" + to_string(atoms.size()); + atoms[varStr] = labelStr; + } + else { + labelStr = atoms[varStr]; + } + + return labelStr; + + case RSCTLK_AND: + return "(" + formulaToStr(form->arg[0]) + " and " + formulaToStr(form->arg[1]) + ")"; + + case RSCTLK_OR: + return "(" + formulaToStr(form->arg[0]) + " or " + formulaToStr(form->arg[1]) + ")"; + + case RSCTLK_XOR: + return "((" + formulaToStr(form->arg[0]) + " or " + formulaToStr(form->arg[1]) + ") and !(" + + formulaToStr(form->arg[0]) + " and " + formulaToStr(form->arg[1]) + "))"; + + case RSCTLK_NOT: + return "!(" + formulaToStr(form->arg[0]) +")"; + + case RSCTLK_IMPL: + return "(" + formulaToStr(form->arg[0]) + " -> " + formulaToStr(form->arg[1]) + ")"; + + case RSCTLK_EG: // Existential... + return "EG(" + formulaToStr(form->arg[0]) + ")"; + + case RSCTLK_EU: + return "E(" + formulaToStr(form->arg[0]) + " U " + formulaToStr(form->arg[1]) + ")"; + + case RSCTLK_EX: + return "EX(" + formulaToStr(form->arg[0]) + ")"; + + case RSCTLK_EF: + return "EF(" + formulaToStr(form->arg[0]) + ")"; + + case RSCTLK_AG: // Universal... + return "AG(" + formulaToStr(form->arg[0]) + ")"; + + case RSCTLK_AU: + return "A(" + formulaToStr(form->arg[0]) + " U " + formulaToStr(form->arg[1]) + ")"; + + case RSCTLK_AX: + return "AX(" + formulaToStr(form->arg[0]) + ")"; + + case RSCTLK_AF: + return "AF(" + formulaToStr(form->arg[0]) + ")"; + + case RSCTLK_UK: // Epistemic operators + return "K(" + form->getSingleAgent() + ", " + formulaToStr(form->arg[0]) + ")"; + + default: + assert(0); + return "??"; + } +} diff --git a/reactics-bdd/export.hh b/reactics-bdd/export.hh new file mode 100644 index 0000000..b8b0714 --- /dev/null +++ b/reactics-bdd/export.hh @@ -0,0 +1,55 @@ + +#ifndef EXPORT_HH +#define EXPORT_HH + +#include +#include "types.hh" +#include "mc.hh" +#include "rs.hh" +#include "rsin_driver.hh" + + +class RSExporter { +public: + RSExporter(RctSys *rs, rsin_driver *drv, std::ostream & outStream = std::cout); + + void exportToISPL(); +private: + RctSys *rs; + rsin_driver *drv; + string indent {" "}; + std::ostream &output; + + void exportEnvironment(); + void exportAgent(const Process & proc); + + void exportEnvironmentVars(); + void exportEnvironmentActions(); + void exportEnvironmentProtocol(); + void exportEnvironmentEvolution(); + void exportEnvironmentInitState(); + + void exportAgentVars(const Process & proc); + void exportAgentProtocol(const Process & proc); + void exportAgentEvolution(const Process & proc); + void exportAgentReactions(const Process & proc); + void exportAgentInitState(const Process & proc); + + void parseFormulas(); + void exportEvaluation(); + void exportInitStates(); + void exportFormulae(); + + std::string stateConstrToStr(const StateConstr * guard); + std::string reactionCondToStr(const Reaction & reaction); + std::string appendCondition(std::string & oldCond, std::string & newCond); + std::string formulaToStr(const FormRSCTLK * form); + + EntitiesForProc procInputs; + EntitiesForProc procOutputs; + + std::map atoms; + std::vector formulas; +}; + +#endif \ No newline at end of file diff --git a/reactics-bdd/formrsctlk.hh b/reactics-bdd/formrsctlk.hh index 2eae014..b9091fd 100644 --- a/reactics-bdd/formrsctlk.hh +++ b/reactics-bdd/formrsctlk.hh @@ -62,9 +62,12 @@ using std::endl; typedef std::set Agents_f; class StateConstr; +class RSExporter; class FormRSCTLK { + friend class RSExporter; + Oper oper; FormRSCTLK *arg[2]; std::string entity_name; diff --git a/reactics-bdd/reactics.cc b/reactics-bdd/reactics.cc index 6b1a3bd..fddd010 100644 --- a/reactics-bdd/reactics.cc +++ b/reactics-bdd/reactics.cc @@ -16,6 +16,7 @@ int main(int argc, char **argv) bool rstl_model_checking = false; bool reach_states = false; bool reach_states_succ = false; + bool export_to_ispl = false; bool bmc = true; bool benchmarking = false; bool dump_help_message = false; @@ -31,7 +32,7 @@ int main(int argc, char **argv) int c; int option_index = 0; - while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzXh", long_options, + while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzXhe", long_options, &option_index)) != -1) { switch (c) { case 0: @@ -52,6 +53,10 @@ int main(int argc, char **argv) break; + case 'e': + export_to_ispl = true; + break; + //case 'b': // printf("-b with %s\n", optarg); // break; @@ -136,8 +141,8 @@ int main(int argc, char **argv) } 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"); + || show_reactions || print_parsed_sys || export_to_ispl)) { + FERROR("No task specified: -c, -P, -r, -s, or -e needs to be used"); } if (opts->verbose > 0) { @@ -171,7 +176,7 @@ int main(int argc, char **argv) rs.printSystem(); } - if (reach_states || reach_states_succ || rstl_model_checking) { + if (reach_states || reach_states_succ || rstl_model_checking || export_to_ispl) { SymRS srs(&rs, opts); ModelChecker mc(&srs, opts); @@ -184,6 +189,11 @@ int main(int argc, char **argv) mc.printReachWithSucc(); } + if (export_to_ispl) { + RSExporter exp(&rs, &driver); + exp.exportToISPL(); + } + if (rstl_model_checking) { if (bmc) { cout << "Using BDD-based Bounded Model Checking" << endl; @@ -268,6 +278,8 @@ void print_help(std::string path_str) << " Benchmarking options:" << endl << " -m -- measure and display time and memory usage" << endl << " -B -- display an easy to parse summary (enables -m)" << endl + << " -e -- exports to ISPL (MCMAS input format)" << endl + << endl; } diff --git a/reactics-bdd/reactics.hh b/reactics-bdd/reactics.hh index c1e0d7c..59a1455 100644 --- a/reactics-bdd/reactics.hh +++ b/reactics-bdd/reactics.hh @@ -18,6 +18,7 @@ #include "rsin_driver.hh" #include "options.hh" #include "memtime.hh" +#include "export.hh" #define VERSION "2.0" //#define AUTHOR "Artur Meski " diff --git a/reactics-bdd/rs.hh b/reactics-bdd/rs.hh index 45dd971..27ace9b 100644 --- a/reactics-bdd/rs.hh +++ b/reactics-bdd/rs.hh @@ -28,6 +28,7 @@ class RctSys { friend class SymRS; friend class SymRSstate; + friend class RSExporter; public: RctSys(void); diff --git a/reactics-bdd/stateconstr.hh b/reactics-bdd/stateconstr.hh index 31a038b..c6542ad 100644 --- a/reactics-bdd/stateconstr.hh +++ b/reactics-bdd/stateconstr.hh @@ -23,9 +23,12 @@ #define STC_IS_VALID(a) (STC_COND_1ARG(a) || STC_COND_2ARG(a) || (a) == STC_PV || (a) == STC_TF) class SymRS; +class RSExporter; class StateConstr { + friend class RSExporter; + Oper oper; StateConstr *arg[2]; std::string entity_name;