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
 

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);

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; proc<rs->getNumberOfProcesses(); ++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; proc<rs->getNumberOfProcesses(); ++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; proc<rs->getNumberOfProcesses(); ++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; proc<rs->getNumberOfProcesses(); ++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; i<rs->ctx_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; proc<rs->getNumberOfProcesses(); ++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; proc<rs->getNumberOfProcesses(); ++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; proc<rs->getNumberOfProcesses(); ++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<bool> 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; proc<rs->getNumberOfProcesses(); ++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<pair<Process, Entity>> 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; proc<rs->getNumberOfProcesses(); ++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<tuple<State, State, unsigned>> 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; proc<rs->getNumberOfProcesses(); ++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<string, string> 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; proc<rs->getNumberOfProcesses(); ++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 "??";
+    }
+}

reactics-bdd/export.hh

@@ -0,0 +1,55 @@
+
+#ifndef EXPORT_HH
+#define EXPORT_HH
+
+#include <iostream>
+#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<std::string, std::string> atoms;
+    std::vector<std::string> formulas;
+};
+
+#endif

reactics-bdd/formrsctlk.hh

@@ -62,9 +62,12 @@ using std::endl;
 typedef std::set<std::string> Agents_f;
 
 class StateConstr;
+class RSExporter;
 
 class FormRSCTLK
 {
+  friend class RSExporter;
+  
     Oper oper;
     FormRSCTLK *arg[2];
     std::string entity_name;

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;
 }
 

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 <artur.meski@gmail.com>"

reactics-bdd/rs.hh

@@ -28,6 +28,7 @@ class RctSys
 {
     friend class SymRS;
     friend class SymRSstate;
+    friend class RSExporter;
 
   public:
     RctSys(void);

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;