Merge pull request #1 from arturme/distrib_rs

Distributed RS

Makefile

@@ -4,21 +4,22 @@ CUDD_INCLUDE=cudd/lib/libcudd.a
 INCLUDES=-Icudd/include
 CPPFLAGS_SILENT = $(INCLUDES)
 CPPFLAGS = -Wall $(CPPFLAGS_SILENT) #-Werror
-#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG 
+#CPPFLAGS = -Wall $(INCLUDES) -DNDEBUG
 CXXFLAGS_SILENT = -O3 -g
 CXXFLAGS = -std=c++14 $(CXXFLAGS_SILENT)
-#CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
+CXXFLAGS = -std=c++14 -O3 -DPUBLIC_RELEASE -DNDEBUG #-g
-LDLIBS = $(CUDD_INCLUDE) 
+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 formrsctl.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
 
-all: main
+all: reactics
 
 cleanly:
 	rm -f *.lex.cc *.lex.o location.hh stack.hh position.hh rsin_parser.cc rsin_parser.hh
 
 clean: cleanly
-	rm -f *.o main *~ makefile.dep tags
+	rm -f *.o reactics *.orig *~ makefile.dep tags
 
 cleanall: clean
 
@@ -27,7 +28,7 @@ makefile.dep: *.cc *.hh
 
 include makefile.dep
 
-main: main.o $(OBJ)
+reactics: reactics.o $(OBJ)
 
 rsin_parser.hh: rsin_parser.cc
 
@@ -43,3 +44,8 @@ rsin_parser.lex.cc: rsin_parser.ll
 	flex rsin_parser.ll
 	mv lex.yy.c rsin_parser.lex.cc
 
+style:
+	astyle --max-code-length=130 --break-closing-brackets --convert-tabs --add-brackets --max-instatement-indent=40 -s2 -C -xG -S -f -p -H -k1 -c --style=kr --align-pointer=name *.cc *.hh
+
+commit: style
+	git commit -a

bdd_macro.hh

@@ -1,11 +1,13 @@
 #ifndef __BDD_MACRO_HH__
 #define __BDD_MACRO_HH__
 
-#define BDD_IFF(p,q)	(!(p+q)+(p*q))
+#include "cudd.hh"
-#define BDD_TRUE		(cuddMgr->bddOne())
-#define BDD_FALSE		(cuddMgr->bddZero())
 
-#define BDD_PRINT(t)	((t).PrintMinterm())
+#define BDD_IFF(p,q)  (!(p+q)+(p*q))
+#define BDD_TRUE    (cuddMgr->bddOne())
+#define BDD_FALSE   (cuddMgr->bddZero())
+
+#define BDD_PRINT(t)  ((t).PrintMinterm())
 
 #endif
 

ctx_aut.cc

@@ -1,108 +1,186 @@
 
 #include "ctx_aut.hh"
+#include "rs.hh"
+#include "macro.hh"
+#include "stateconstr.hh"
 
-CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys) 
+CtxAut::CtxAut(Options *opts, RctSys *parent_rctsys)
-{ 
+{
-	setOptions(opts);
+  setOptions(opts);
-	this->parent_rctsys = parent_rctsys;
+  this->parent_rctsys = parent_rctsys;
+  made_progressive = false;
 }
 
 bool CtxAut::hasState(std::string name)
 {
-    if (states_names.find(name) == states_names.end())
+  if (states_names.find(name) == states_names.end()) {
-        return false;
+    return false;
-    else
+  }
-        return true;
+  else {
+    return true;
+  }
 }
 
 State CtxAut::getStateID(std::string name)
 {
-    if (!hasState(name))
+  if (!hasState(name)) {
-    {
+    FERROR("No such state: " << name);
-        FERROR("No such state: " << name);
+  }
-    }
+
-    return states_names[name];
+  return states_names[name];
 }
 
 std::string CtxAut::getStateName(State state_id)
 {
-	assert(state_id < states_ids.size());
+  assert(state_id < states_ids.size());
-	return states_ids[state_id];
+  return states_ids[state_id];
 }
 
 void CtxAut::addState(std::string name)
 {
-    if (!hasState(name))
+  if (!hasState(name)) {
-    {
+    State new_state_id = states_ids.size();
-        State new_state_id = states_ids.size();
 
-        VERB_L2("Adding state: " << name << " index=" << new_state_id);
+    VERB_L2("Adding state: " << name << " index=" << new_state_id);
 
-        states_ids.push_back(name);
+    states_ids.push_back(name);
-        states_names[name] = new_state_id;
+    states_names[name] = new_state_id;
-		
+
-		if (!init_state_defined)
+    if (!init_state_defined) {
-		{
+      setInitState(name);
-			setInitState(name);
-		}
     }
+  }
 }
 
 void CtxAut::setInitState(std::string name)
 {
-	VERB_L2("Setting initial CA state: " << name);
+  VERB_L2("Setting initial CA state: " << name);
-	State state_id = getStateID(name);
+  State state_id = getStateID(name);
-	VERB_L2("Got initial CA state ID: index=" << state_id);
+  VERB_L2("Got initial CA state ID: index=" << state_id);
-	init_state_id = state_id;
+  init_state_id = state_id;
-	init_state_defined = true;
+  init_state_defined = true;
 }
 
 State CtxAut::getInitState(void)
 {
-	assert(init_state_defined);
+  assert(init_state_defined);
-	return init_state_id;
+  return init_state_id;
 }
 
 void CtxAut::printAutomaton(void)
 {
-	showStates();
+  showStates();
-	showTransitions();
+  showTransitions();
 }
 
 void CtxAut::showStates(void)
 {
-	cout << "# Context Automaton States:" << endl;
+  cout << "# Context Automaton States:" << endl;
-	cout << " = Init state: " << getStateName(init_state_id) << endl;
+  cout << " = Init state: " << getStateName(init_state_id) << endl;
-	for (const auto &s : states_ids)
+
-		cout << " * " << s << endl;
+  for (const auto &s : states_ids) {
+    cout << " * " << s << endl;
+  }
 }
 
-void CtxAut::pushContextEntity(Entity entity_id) 
+void CtxAut::pushContextEntity(Entity entity_id)
 {
-	tmpEntities.insert(entity_id);
+  tmpEntities.insert(entity_id);
 }
 
-void CtxAut::addTransition(std::string srcStateName, std::string dstStateName) 
+void CtxAut::saveCurrentContextSet(Process proc_id)
 {
-    VERB_L3("Saving transition");
+  if (!parent_rctsys->hasProcess(proc_id)) {
-	
+    FERROR("No such process: ID=" << proc_id);
-	CtxAutTransition new_transition;
+  }
-	
+
-	new_transition.src_state = getStateID(srcStateName);
+  tmpProcEntities[proc_id] = tmpEntities;
-	new_transition.ctx = tmpEntities; 
+  tmpEntities.clear();
-	tmpEntities.clear();
+}
-	new_transition.dst_state = getStateID(dstStateName);
+
-	transitions.push_back(new_transition);
+void CtxAut::addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr)
+{
+  VERB_L3("Saving transition");
+
+  CtxAutTransition new_transition;
+
+  new_transition.src_state = getStateID(srcStateName);
+  new_transition.ctx = tmpProcEntities;
+  // tmpEntities.clear();
+  tmpProcEntities.clear();
+  new_transition.state_constr = stateConstr;
+  new_transition.dst_state = getStateID(dstStateName);
+  transitions.push_back(new_transition);
 }
 
 void CtxAut::showTransitions(void)
 {
-	cout << "# Context Automaton Transitions:" << endl;
+  cout << "# Context Automaton Transitions:" << endl;
-	for (const auto &t : transitions)
+
-	{
+  for (const auto &t : transitions) {
-		cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(t.dst_state) 
+    cout << " * [" << getStateName(t.src_state) << " -> " << getStateName(
-			 << "]: {" << parent_rctsys->entitiesToStr(t.ctx) << "}" << endl;
+           t.dst_state)
-	}
+         << "]: { " << parent_rctsys->procEntitiesToStr(t.ctx) << "}";
+
+    if (t.state_constr != nullptr) {
+      cout << " " << t.state_constr->toStr();
+    }
+
+    cout << endl;
+  }
+}
+
+void CtxAut::makeProgressive(void)
+{
+  VERB_LN(2, "Calculating progressive closure of CA");
+  assert(!made_progressive);
+
+  std::string special_loc = "T";
+
+  while (hasState(special_loc)) {
+    special_loc += "T";
+  }
+
+  addState(special_loc);
+  State special_loc_id = getLastStateID();
+
+  std::map<State, StateConstr *> constrs;
+
+  for (State s = 0; s < states_ids.size(); ++s) {
+    if (s == special_loc_id) {
+      continue;
+    }
+
+    if (constrs.count(s) == 0) {
+      constrs[s] = new StateConstr(true);
+    }
+  }
+
+  constrs[special_loc_id] = new StateConstr(true);
+
+  for (const auto &t : transitions) {
+    State curr_st = t.src_state;
+
+    if (t.state_constr != nullptr) {
+      constrs[curr_st] = new StateConstr(
+        STC_OR, constrs[curr_st], t.state_constr);
+    }
+  }
+
+  for (const auto &s : states_ids) {
+    StateConstr *state_constr = nullptr;
+
+    if (!constrs[getStateID(s)]->isTrue()) {
+      state_constr = new StateConstr(STC_NOT, constrs[getStateID(s)]);
+      addTransition(s, special_loc, state_constr);
+    }
+
+  }
+
+  addTransition(special_loc, special_loc, nullptr);
+
+  made_progressive = true;
+
 }
 
 /** EOF **/

ctx_aut.hh

@@ -1,9 +1,6 @@
 /*
     Copyright (c) 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #ifndef RS_CTX_AUT_HH
@@ -15,45 +12,61 @@
 #include <vector>
 #include <string>
 #include <cstdlib>
-#include "rs.hh"
+// #include "rs.hh"
 #include "types.hh"
-#include "macro.hh"
+// #include "options.hh"
-#include "options.hh"
+// #include "stateconstr.hh"
 
 using std::cout;
 using std::endl;
 
 class RctSys;
+class Options;
+class StateConstr;
 
 class CtxAut
 {
     friend class SymRS;
-	
+
-	public:
+  public:
-		CtxAut(Options *opts, RctSys *parent_rctsys);
+    CtxAut(Options *opts, RctSys *parent_rctsys);
-		bool hasState(std::string name);
+    bool hasState(std::string name);
-		void addState(std::string stateName);
+    void addState(std::string stateName);
-		void setInitState(std::string stateName);
+    void setInitState(std::string stateName);
-		State getInitState(void);
+    State getInitState(void);
-		State getStateID(std::string name);
+    State getStateID(std::string name);
-		std::string getStateName(State state_id);
+    State getLastStateID(void)
-		void printAutomaton(void);
+    {
-		void showStates(void);
+      return states_ids.size();
-		void addTransition(std::string srcStateName, std::string dstStateName);
+    }
-		void showTransitions(void);
+    std::string getStateName(State state_id);
-		void pushContextEntity(Entity entity_id);	
+    void printAutomaton(void);
-	    void setOptions(Options *opts) { this->opts = opts; }
+    void showStates(void);
-		size_t statesCount(void) { return states_ids.size(); }
+    void addTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr);
-		
+    void showTransitions(void);
-	private:
+    void makeProgressive(void);
-		RctSys *parent_rctsys;
+    void pushContextEntity(Entity entity_id);
-	    Options *opts;
+    void saveCurrentContextSet(Process proc_id);
-		StatesById states_ids;
+    void setOptions(Options *opts)
-		StatesByName states_names;
+    {
-		State init_state_id;
+      this->opts = opts;
-		bool init_state_defined;
+    }
-		Entities tmpEntities;
+    size_t statesCount(void)
-		CtxAutTransitions transitions;
+    {
+      return states_ids.size();
+    }
+
+  private:
+    RctSys *parent_rctsys;
+    Options *opts;
+    StatesById states_ids;
+    StatesByName states_names;
+    State init_state_id;
+    bool init_state_defined;
+    EntitiesForProc tmpProcEntities;
+    Entities tmpEntities;
+    CtxAutTransitions transitions;
+    bool made_progressive;
 };
 
 #endif /* RS_CTX_AUT_HH */

drs_benchmark.sh

@@ -0,0 +1,70 @@
+#!/bin/sh
+
+TMPINPUT="tmp_$RANDOM$RANDOM.rs"
+
+CMD="./reactics -B"
+
+timelimit="$((30*60))" # 30 minutes
+timelimit="$((5*60))" # 5 minutes
+
+form_tgc_sc="`seq 1 4`"
+form_asm="`seq 1 2`"
+
+for benchmark in "tgc_sc" "asm"; do
+
+    eval formulae=\$form_${benchmark}
+
+    for opt in "z" "zb" "x" "xz" "xzb" "xb" "" "b";do
+
+        for f in $formulae; do
+
+            done=0
+
+            for i in `seq 2 20`;do
+
+                if [[ $done -eq 1 ]];then
+                    echo "Skipping f=$f i=$i for $opt"
+                    continue
+                fi
+
+                echo "[i] n=$i; generating input file (${benchmark})"
+                in/scripts/gen_${benchmark}.py $i > $TMPINPUT
+
+                echo "[i] Testing formula f$f"
+
+                if [[ "$opt" = "" ]];then
+                    opt_str="NoOpt"
+                    CMDOPT=""
+                else
+                    opt_str="$opt"
+                    CMDOPT="-$opt"
+                fi
+
+                TMPCMD="$CMD $CMDOPT -c f$f $TMPINPUT"
+                echo "[i] running reactics: $TMPCMD"
+
+                res=$(timeout $timelimit $TMPCMD | grep STAT)
+                if [[ $? -ne 0 ]];then
+                    done=1
+                    continue
+                fi
+                mem=$(echo $res | cut -d';' -f 5)
+                time=$(echo $res | cut -d';' -f 6)
+
+                echo "[.] Finished. time:$time, mem:$mem"
+
+                echo "$i $time $mem" >> bench_drs_${benchmark}_${opt_str}_f$f.dat
+
+            done
+
+            echo 
+            
+        done
+
+    done
+
+done
+
+rm -f $TMPINPUT
+
+# EOF

formrsctl.cc

@@ -1,323 +0,0 @@
-/*
-    Copyright (c) 2012, 2013
-    Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
-*/
-
-#include "formrsctl.hh"
-
-
-std::string BoolContexts::toStr(void) const
-{
-    if (oper == BCTX_PV)
-    {
-        return name;
-    }
-    else if (oper == BCTX_TF)
-    {
-        if (tf) return "true";
-        else return "false";
-    }
-    else if (oper == BCTX_AND)
-    {
-        return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
-    }
-    else if (oper == BCTX_OR)
-    {
-        return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == BCTX_XOR)
-    {
-        return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == BCTX_NOT)
-    {
-        return "~" + arg[0]->toStr();
-    }
-	
-	else
-    {
-        return "??";
-        assert(0);
-    }
-}
-
-BDD BoolContexts::getBDD(const SymRS *srs) const
-{
-	if (oper == BCTX_PV)
-	{
-		return srs->encActStrEntity(name);
-	}
-	else if (oper == BCTX_TF)
-	{
-		if (tf) return srs->getBDDtrue();
-		else return srs->getBDDfalse();
-	}
-	else if (oper == BCTX_AND)
-	{
-		return arg[0]->getBDD(srs) * arg[1]->getBDD(srs);
-	}
-	else if (oper == BCTX_OR)
-	{
-		return arg[0]->getBDD(srs) + arg[1]->getBDD(srs);
-	}
-	else if (oper == BCTX_XOR)
-	{
-		return arg[0]->getBDD(srs) ^ arg[1]->getBDD(srs);
-	}
-	else if (oper == BCTX_NOT)
-	{
-		return !arg[0]->getBDD(srs);
-	}
-	else
-	{
-		assert(0);
-		FERROR("Undefined operator used in Boolean context definition. This should not happen.");
-		return srs->getBDDfalse();
-	}
-}
-
-std::string FormRSCTL::toStr(void) const
-{
-    if (oper == RSCTL_PV)
-    {
-        return name;
-    }
-    else if (oper == RSCTL_TF)
-    {
-        if (tf) return "true";
-        else return "false";
-    }
-    else if (oper == RSCTL_AND)
-    {
-        return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_OR)
-    {
-        return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_XOR)
-    {
-        return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_IMPL)
-    {
-        return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_NOT)
-    {
-        return "~" + arg[0]->toStr();
-    }
-    else if (oper == RSCTL_EX)
-    {
-        return "EX(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EG)
-    {
-        return "EG(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EU)
-    {
-        return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EF)
-    {
-        return "EF(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AX)
-    {
-        return "AX(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AG)
-    {
-        return "AG(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AU)
-    {
-        return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AF)
-    {
-        return "AF(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EX_ACT)
-    {
-        return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EG_ACT)
-    {
-        return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EU_ACT)
-    {
-        return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_EF_ACT)
-    {
-        return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AX_ACT)
-    {
-        return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AG_ACT)
-    {
-        return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AU_ACT)
-    {
-        return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
-    }
-    else if (oper == RSCTL_AF_ACT)
-    {
-        return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
-    }
-
-    else
-    {
-        return "??";
-        assert(0);
-    }
-}
-
-bool FormRSCTL::hasOper(Oper op) const
-{
-    if (oper == op)
-        return true;
-    else
-    {
-        bool result = false;
-        if (arg[0] != nullptr) result = arg[0]->hasOper(op);
-        if (!result && arg[1] != nullptr) result = arg[1]->hasOper(op);
-        return result;
-    }
-}
-
-void FormRSCTL::encodeEntities(const SymRS *srs)
-{
-    if (RSCTL_COND_1ARG(oper))
-    {
-        arg[0]->encodeEntities(srs);
-    }
-    else if (RSCTL_COND_2ARG(oper))
-    {
-        arg[0]->encodeEntities(srs);
-        arg[1]->encodeEntities(srs);
-    }
-    else if (oper == RSCTL_PV)
-    {
-        bdd = new BDD(srs->encEntity(name));
-    }
-}
-
-bool FormRSCTL::isERSCTL(void) const
-{
-    if (oper == RSCTL_PV)
-    {
-        return true;
-    }
-
-    if (oper == RSCTL_NOT)
-    {
-        if (arg[0]->getOper() == RSCTL_PV || arg[0]->getOper() == RSCTL_TF)
-            return true;
-        else
-            return false;
-    }
-
-    if (RSCTL_COND_IS_UNIVERSAL(oper))
-    {
-        return false;
-    }
-
-    if (RSCTL_COND_1ARG(oper))
-    {
-        return arg[0]->isERSCTL();
-    }
-
-    if (RSCTL_COND_2ARG(oper))
-    {
-        return arg[0]->isERSCTL() && arg[1]->isERSCTL();
-    }
-
-    assert(0);
-
-    return false;
-}
-
-std::string FormRSCTL::getActionsStr(void) const
-{
-	if (actions != nullptr)
-	{
-	    std::string r = "[ ";
-	    bool firstact = true;
-
-	    for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
-	    {
-	        if (!firstact) r += ",";
-	        else firstact = false;
-	        r += "{";
-	        bool firstent = true;
-	        for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent)
-	        {
-	            if (!firstent) r += ",";
-	            else firstent = false;
-	            r += *ent; 
-	        }
-	        r += "}";
-	    }
-		r += " ]";		
-	    return r;
-	}
-	else if (boolCtx != nullptr)
-	{
-		return "< " + boolCtx->toStr() + " >";
-	}
-	else
-	{
-		FERROR("Context not specified. This should not happen.");
-	}
-}
-
-void FormRSCTL::encodeActions(const SymRS *srs)
-{
-    if (RSCTL_COND_ACT(oper))
-    {
-        if (actions_bdd != nullptr) forgetActionsBDD();
-        actions_bdd = new BDD(srs->getBDDfalse());
-        assert(actions != nullptr || boolCtx != nullptr);
-		assert(!(actions != nullptr && boolCtx != nullptr));
-		if (actions != nullptr)
-		{
-	        for (ActionsVec_f::iterator act = actions->begin(); act != actions->end(); ++act)
-	        {
-	            BDD single_action = srs->getBDDtrue();
-	            for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent)
-	            {
-	                single_action *= srs->encActStrEntity(*ent); 
-	            }
-	            single_action = srs->compContext(single_action);
-	            *actions_bdd += single_action;
-	        }
-		}
-		else if (boolCtx != nullptr)
-		{
-			*actions_bdd = boolCtx->getBDD(srs);
-		}
-		else
-			assert(0);
-    }
-
-    if (RSCTL_COND_1ARG(oper))
-    {
-        arg[0]->encodeActions(srs);
-    }
-
-    if (RSCTL_COND_2ARG(oper))
-    {
-        arg[0]->encodeActions(srs);
-        arg[1]->encodeActions(srs);
-    }
-}

formrsctl.hh

@@ -1,332 +0,0 @@
-/*
-    Copyright (c) 2012-2015
-    Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
-*/
-
-#ifndef RS_FORMRSCTL_HH
-#define RS_FORMRSCTL_HH
-
-#include <iostream>
-#include <string>
-#include <cassert>
-#include "rs.hh"
-#include "symrs.hh"
-#include "cudd.hh"
-
-#define RSCTL_PV      0 // propositional variable
-#define RSCTL_AND     1
-#define RSCTL_OR      2
-#define RSCTL_XOR	 3
-#define RSCTL_NOT     4
-#define RSCTL_IMPL    5
-#define RSCTL_EG      11 // Existential...
-#define RSCTL_EU      12
-#define RSCTL_EX      13
-#define RSCTL_EF      14
-#define RSCTL_AG      21 // Universal...
-#define RSCTL_AU      22
-#define RSCTL_AX      23
-#define RSCTL_AF      24
-#define RSCTL_EG_ACT  31 // Existential...
-#define RSCTL_EU_ACT  32
-#define RSCTL_EX_ACT  33
-#define RSCTL_EF_ACT  34
-#define RSCTL_AG_ACT  41 // Universal...
-#define RSCTL_AU_ACT  42
-#define RSCTL_AX_ACT  43
-#define RSCTL_AF_ACT  44
-#define RSCTL_TF      50 // true/false
-
-/* For Boolean contexts: */
-#define BCTX_PV		60
-#define BCTX_AND 	61
-#define BCTX_OR 	62
-#define BCTX_XOR 	63
-#define BCTX_NOT	64
-#define BCTX_TF		70
-
-
-#define RSCTL_COND_1ARG(a) ((a) == RSCTL_NOT || (a) == RSCTL_EG || (a) == RSCTL_EF || (a) == RSCTL_EX || (a) == RSCTL_AG || (a) == RSCTL_AF || (a) == RSCTL_AX || (a) == RSCTL_EG_ACT || (a) == RSCTL_EF_ACT || (a) == RSCTL_EX_ACT || (a) == RSCTL_AG_ACT || (a) == RSCTL_AF_ACT || (a) == RSCTL_AX_ACT)
-#define RSCTL_COND_2ARG(a) ((a) == RSCTL_AND || (a) == RSCTL_OR || (a) == RSCTL_XOR || (a) == RSCTL_IMPL || (a) == RSCTL_EU || (a) == RSCTL_AU || (a) == RSCTL_EU_ACT || (a) == RSCTL_AU_ACT)
-#define RSCTL_COND_ACT(a) ((a) > 30 && (a) < 45)
-#define RSCTL_IS_VALID(a) (RSCTL_COND_1ARG(a) || RSCTL_COND_2ARG(a) || (a) == RSCTL_PV || (a) == RSCTL_TF)
-
-#define RSCTL_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45))
-
-#define BCTX_COND_1ARG(a) ((a) == BCTX_NOT)
-#define BCTX_COND_2ARG(a) ((a) == BCTX_AND || (a) == BCTX_OR || (a) == BCTX_XOR)
-#define BCTX_IS_VALID(a) (BCTX_COND_1ARG(a) || BCTX_COND_2ARG(a) || (a) == BCTX_PV || (a) == BCTX_TF)
-
-using std::cout;
-using std::endl;
-
-typedef unsigned char Oper;
-
-typedef std::string Entity_f;
-typedef std::set<Entity_f> Action_f;
-typedef vector<Action_f> ActionsVec_f;
-
-class BoolContexts
-{
-	Oper oper;
-	BoolContexts *arg[2];
-	std::string name;
-	bool tf;
-	
-public:
-		
-	BoolContexts(std::string varName)
-	{
-		oper = BCTX_PV;
-		name = varName;
-        arg[0] = nullptr;
-        arg[1] = nullptr;
-	}
-	
-   /**
-    * @brief Constructor for true/false.
-    *
-    * @param   val value of the logical constant
-    */
-   BoolContexts(bool val) {
-       oper = BCTX_TF;
-       tf = val;
-       arg[0] = nullptr;
-       arg[1] = nullptr;
-   }
-
-   /**
-    * @brief Constructor for one-argument formula.
-    */
-   BoolContexts(Oper op, BoolContexts *form1) {
-       assert(op == BCTX_NOT);
-       oper = op;
-       arg[0] = form1;
-       arg[1] = nullptr;
-   }
-
-   /**
-    * @brief Constructor for two-argument formula.
-    */
-   BoolContexts(Oper op, BoolContexts *form1, BoolContexts *form2) {
-       assert(BCTX_COND_2ARG(op));
-       oper = op;
-       arg[0] = form1;
-       arg[1] = form2;
-   }
-   
-   ~BoolContexts() {
-       delete arg[0];
-       delete arg[1];
-   }
-   
-   std::string toStr(void) const;
-   
-   BDD getBDD(const SymRS *srs) const;
-   
-   Oper getOper(void) const {
-       assert(BCTX_IS_VALID(oper));
-       return oper;
-   }
-   BoolContexts *getLeftSF(void) const {
-       assert(arg[0] != nullptr);
-       return arg[0];
-   }
-   BoolContexts *getRightSF(void) const {
-       assert(BCTX_COND_2ARG(oper));
-       assert(arg[1] != nullptr);
-       return arg[1];
-   }
-};
-
-class FormRSCTL
-{
-    Oper oper;
-    FormRSCTL *arg[2];
-    std::string name;
-    bool tf;
-    BDD *bdd;
-    ActionsVec_f *actions;
-    BDD *actions_bdd;
-	BoolContexts *boolCtx;
-public:
-    /**
-     * @brief Constructor for propositional variable.
-     *
-     * @param   varName variable name used mostly for printing the variable.
-     * @param   varBDD  the BDD describing the set where the variable holds.
-     */
-    FormRSCTL(std::string varName) {
-        oper = RSCTL_PV;
-        name = varName;
-        arg[0] = nullptr;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for true/false.
-     *
-     * @param   val value of the logical constant
-     */
-    FormRSCTL(bool val) {
-        oper = RSCTL_TF;
-        tf = val;
-        arg[0] = nullptr;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for two-argument formula.
-     */
-    FormRSCTL(Oper op, FormRSCTL *form1, FormRSCTL *form2) {
-        assert(RSCTL_COND_2ARG(op));
-        assert(!RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = form2;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for two-argument formula with action restrictions.
-     */
-    FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1, FormRSCTL *form2) {
-        assert(acts != nullptr);
-        assert(RSCTL_COND_2ARG(op));
-        assert(RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = form2;
-        bdd = nullptr;
-        actions = acts;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-   /**
-    * @brief Constructor for two-argument formula with Boolean context restrictions.
-    */
-   FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1, FormRSCTL *form2) {
-       assert(bctx != nullptr);
-       assert(RSCTL_COND_2ARG(op));
-       assert(RSCTL_COND_ACT(op));
-       oper = op;
-       arg[0] = form1;
-       arg[1] = form2;
-       bdd = nullptr;
-       actions = nullptr;
-       actions_bdd = nullptr;
-	   boolCtx = bctx;
-   }
-
-    /**
-     * @brief Constructor for one-argument formula.
-     */
-    FormRSCTL(Oper op, FormRSCTL *form1) {
-        assert(RSCTL_COND_1ARG(op));
-        assert(!RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = nullptr;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-    /**
-     * @brief Constructor for one-argument formula with action restrictions.
-     */
-    FormRSCTL(Oper op, ActionsVec_f *acts, FormRSCTL *form1) {
-        assert(acts != nullptr);
-        assert(RSCTL_COND_1ARG(op));
-        assert(RSCTL_COND_ACT(op));
-        oper = op;
-        arg[0] = form1;
-        arg[1] = nullptr;
-        bdd = nullptr;
-        actions = acts;
-        actions_bdd = nullptr;
-		boolCtx = nullptr;
-    }
-
-   /**
-    * @brief Constructor for one-argument formula with Boolean context restrictions.
-    */
-   FormRSCTL(Oper op, BoolContexts *bctx, FormRSCTL *form1) {
-       assert(bctx != nullptr);
-       assert(RSCTL_COND_1ARG(op));
-       assert(RSCTL_COND_ACT(op));
-       oper = op;
-       arg[0] = form1;
-       arg[1] = nullptr;
-       bdd = nullptr;
-       actions = nullptr;
-       actions_bdd = nullptr;
-	   boolCtx = bctx;
-	}
-
-    /**
-     * @brief Destructor.
-     */
-    ~FormRSCTL() {
-        delete arg[0];
-        delete arg[1];
-        delete bdd;
-        delete actions;
-        delete actions_bdd;
-		delete boolCtx;
-    }
-    std::string toStr(void) const;
-    bool hasOper(Oper op) const;
-    const BDD *getBDD(void) const {
-        assert(oper == RSCTL_PV);
-        assert(bdd != nullptr);
-        return bdd;
-    }
-    const BDD *getActionsBDD(void) const {
-        assert(RSCTL_COND_ACT(oper));
-        assert(actions_bdd != nullptr);
-        return actions_bdd;
-    }
-    Oper getOper(void) const {
-        assert(RSCTL_IS_VALID(oper));
-        return oper;
-    }
-    FormRSCTL *getLeftSF(void) const {
-        assert(arg[0] != nullptr);
-        return arg[0];
-    }
-    FormRSCTL *getRightSF(void) const {
-        assert(RSCTL_COND_2ARG(oper));
-        assert(arg[1] != nullptr);
-        return arg[1];
-    }
-    std::string getActionsStr(void) const;
-    bool getTF(void) const {
-        assert(oper == RSCTL_TF);
-        return tf;
-    }
-    void encodeEntities(const SymRS *srs);
-    void encodeActions(const SymRS *srs);
-    void forgetActionsBDD(void) {
-        if (actions_bdd != nullptr) delete actions_bdd;
-    }
-    bool isERSCTL(void) const;
-};
-
-#endif

formrsctlk.cc

@@ -0,0 +1,290 @@
+/*
+    Copyright (c) 2012, 2013
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "formrsctlk.hh"
+#include "rs.hh"
+
+std::string FormRSCTLK::toStr(void) const
+{
+  if (oper == RSCTLK_PV) {
+    return proc_name + "." + entity_name;
+  }
+  else if (oper == RSCTLK_TF) {
+    if (tf) {
+      return "true";
+    }
+    else {
+      return "false";
+    }
+  }
+  else if (oper == RSCTLK_AND) {
+    return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_OR) {
+    return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_XOR) {
+    return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_IMPL) {
+    return "(" + arg[0]->toStr() + " IMPLIES " + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_NOT) {
+    return "~" + arg[0]->toStr();
+  }
+  else if (oper == RSCTLK_EX) {
+    return "EX(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EG) {
+    return "EG(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EU) {
+    return "EU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EF) {
+    return "EF(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AX) {
+    return "AX(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AG) {
+    return "AG(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AU) {
+    return "AU(" + arg[0]->toStr() + "," + arg[1]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AF) {
+    return "AF(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EX_ACT) {
+    return "E" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EG_ACT) {
+    return "E" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_EU_ACT) {
+    return "E" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
+           + ")";
+  }
+  else if (oper == RSCTLK_EF_ACT) {
+    return "E" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AX_ACT) {
+    return "A" + getActionsStr() + "X(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AG_ACT) {
+    return "A" + getActionsStr() + "G(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_AU_ACT) {
+    return "A" + getActionsStr() + "U(" + arg[0]->toStr() + "," + arg[1]->toStr()
+           + ")";
+  }
+  else if (oper == RSCTLK_AF_ACT) {
+    return "A" + getActionsStr() + "F(" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_NK) {
+    return "NK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_UK) {
+    return "K[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_NC) {
+    return "NC[" + getAgentsStr() + "](" + arg[0]->toStr() + ")";
+  }
+  else if (oper == RSCTLK_UC) {
+    return "C[" + getAgentsStr() + "](" + arg[0]->toStr() + ")";
+  }
+
+
+  else {
+    return "??";
+    assert(0);
+  }
+}
+
+bool FormRSCTLK::hasOper(Oper op) const
+{
+  if (oper == op) {
+    return true;
+  }
+  else {
+    bool result = false;
+
+    if (arg[0] != nullptr) {
+      result = arg[0]->hasOper(op);
+    }
+
+    if (!result && arg[1] != nullptr) {
+      result = arg[1]->hasOper(op);
+    }
+
+    return result;
+  }
+}
+
+void FormRSCTLK::encodeEntities(const SymRS *srs)
+{
+  if (RSCTLK_COND_1ARG(oper)) {
+    arg[0]->encodeEntities(srs);
+  }
+  else if (RSCTLK_COND_2ARG(oper)) {
+    arg[0]->encodeEntities(srs);
+    arg[1]->encodeEntities(srs);
+  }
+  else if (oper == RSCTLK_PV) {
+    bdd = new BDD(srs->encEntity(proc_name, entity_name));
+  }
+}
+
+bool FormRSCTLK::isERSCTLK(void) const
+{
+  if (oper == RSCTLK_PV) {
+    return true;
+  }
+
+  if (oper == RSCTLK_NOT) {
+    if (arg[0]->getOper() == RSCTLK_PV || arg[0]->getOper() == RSCTLK_TF) {
+      return true;
+    }
+    else {
+      return false;
+    }
+  }
+
+  if (RSCTLK_COND_IS_UNIVERSAL(oper)) {
+    return false;
+  }
+
+  if (RSCTLK_COND_1ARG(oper)) {
+    return arg[0]->isERSCTLK();
+  }
+
+  if (RSCTLK_COND_2ARG(oper)) {
+    return arg[0]->isERSCTLK() && arg[1]->isERSCTLK();
+  }
+
+  assert(0);
+
+  return false;
+}
+
+std::string FormRSCTLK::getActionsStr(void) const
+{
+  // if (actions != nullptr) {
+  //   std::string r = "[ ";
+  //   bool firstact = true;
+  //
+  //   for (ActionsVec_f::iterator act = actions->begin(); act != actions->end();
+  //        ++act) {
+  //     if (!firstact) {
+  //       r += ",";
+  //     }
+  //     else {
+  //       firstact = false;
+  //     }
+  //
+  //     r += "{";
+  //     bool firstent = true;
+  //
+  //     for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) {
+  //       if (!firstent) {
+  //         r += ",";
+  //       }
+  //       else {
+  //         firstent = false;
+  //       }
+  //
+  //       r += *ent;
+  //     }
+  //
+  //     r += "}";
+  //   }
+  //
+  //   r += " ]";
+  //   return r;
+  // }
+  if (boolCtx != nullptr) {
+    return "< " + boolCtx->toStr() + " >";
+  }
+  else {
+    FERROR("Context not specified. This should not happen.");
+  }
+}
+
+void FormRSCTLK::encodeActions(const SymRS *srs)
+{
+  if (RSCTLK_COND_ACT(oper)) {
+    if (actions_bdd != nullptr) {
+      forgetActionsBDD();
+    }
+
+    actions_bdd = new BDD(srs->getBDDfalse());
+    assert(boolCtx != nullptr);
+    // assert(actions != nullptr || boolCtx != nullptr);
+    // assert(!(actions != nullptr && boolCtx != nullptr));
+
+    // if (actions != nullptr) {
+    //   for (ActionsVec_f::iterator act = actions->begin(); act != actions->end();
+    //        ++act) {
+    //     BDD single_action = srs->getBDDtrue();
+    //
+    //     for (Action_f::iterator ent = act->begin(); ent != act->end(); ++ent) {
+    //       single_action *= srs->encActStrEntity(*ent);
+    //     }
+    //
+    //     single_action = srs->compContext(single_action);
+    //     *actions_bdd += single_action;
+    //   }
+    // }
+    if (boolCtx != nullptr) {
+      *actions_bdd = boolCtx->getBDDforContext(srs);
+    }
+    else {
+      assert(0);
+    }
+  }
+
+  if (RSCTLK_COND_1ARG(oper)) {
+    arg[0]->encodeActions(srs);
+  }
+
+  if (RSCTLK_COND_2ARG(oper)) {
+    arg[0]->encodeActions(srs);
+    arg[1]->encodeActions(srs);
+  }
+}
+
+std::string FormRSCTLK::getAgentsStr(void) const
+{
+  std::string r = "";
+  bool first = true;
+
+  for (const auto &a : agents) {
+    if (first) {
+      first = false;
+    }
+    else {
+      r += " ";
+    }
+
+    r += a;
+  }
+
+  return r;
+}
+
+ProcSet FormRSCTLK::getAgentsAsProcSet(RctSys *rs) const
+{
+  ProcSet processes;
+
+  for (auto &a : agents) {
+    processes.insert(rs->getProcessID(a));
+  }
+
+  return processes;
+}

formrsctlk.hh

@@ -0,0 +1,299 @@
+/*
+    Copyright (c) 2012-2015
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#ifndef RS_FORMRSCTLK_HH
+#define RS_FORMRSCTLK_HH
+
+#include <iostream>
+#include <string>
+#include <cassert>
+// #include "rs.hh"
+#include "symrs.hh"
+#include "cudd.hh"
+#include "types.hh"
+#include "stateconstr.hh"
+
+#define RSCTLK_PV      0 // propositional variable
+#define RSCTLK_AND     1
+#define RSCTLK_OR      2
+#define RSCTLK_XOR  3
+#define RSCTLK_NOT     4
+#define RSCTLK_IMPL    5
+#define RSCTLK_EG      11 // Existential...
+#define RSCTLK_EU      12
+#define RSCTLK_EX      13
+#define RSCTLK_EF      14
+#define RSCTLK_AG      21 // Universal...
+#define RSCTLK_AU      22
+#define RSCTLK_AX      23
+#define RSCTLK_AF      24
+#define RSCTLK_EG_ACT  31 // Existential...
+#define RSCTLK_EU_ACT  32
+#define RSCTLK_EX_ACT  33
+#define RSCTLK_EF_ACT  34
+#define RSCTLK_AG_ACT  41 // Universal...
+#define RSCTLK_AU_ACT  42
+#define RSCTLK_AX_ACT  43
+#define RSCTLK_AF_ACT  44
+#define RSCTLK_TF      50 // true/false
+
+#define RSCTLK_NK      61 // Epistemic operators
+#define RSCTLK_NE      62
+#define RSCTLK_NC      63
+#define RSCTLK_UK      71
+#define RSCTLK_UE      72
+#define RSCTLK_UC      73
+
+#define RSCTLK_COND_1ARG(a) ((a) == RSCTLK_NOT || (a) == RSCTLK_EG || (a) == RSCTLK_EF || (a) == RSCTLK_EX || (a) == RSCTLK_AG || (a) == RSCTLK_AF || (a) == RSCTLK_AX || (a) == RSCTLK_EG_ACT || (a) == RSCTLK_EF_ACT || (a) == RSCTLK_EX_ACT || (a) == RSCTLK_AG_ACT || (a) == RSCTLK_AF_ACT || (a) == RSCTLK_AX_ACT || (a) == RSCTLK_UK || (a) == RSCTLK_NK || (a) == RSCTLK_UE || (a) == RSCTLK_NE || (a) == RSCTLK_UC || (a) == RSCTLK_NC)
+#define RSCTLK_COND_2ARG(a) ((a) == RSCTLK_AND || (a) == RSCTLK_OR || (a) == RSCTLK_XOR || (a) == RSCTLK_IMPL || (a) == RSCTLK_EU || (a) == RSCTLK_AU || (a) == RSCTLK_EU_ACT || (a) == RSCTLK_AU_ACT)
+#define RSCTLK_COND_ACT(a) ((a) > 30 && (a) < 45)
+#define RSCTLK_IS_VALID(a) (RSCTLK_COND_1ARG(a) || RSCTLK_COND_2ARG(a) || (a) == RSCTLK_PV || (a) == RSCTLK_TF)
+
+#define RSCTLK_COND_IS_UNIVERSAL(a) (((a) > 20 && (a) < 25) || ((a) > 40 && (a) < 45) || ((a) > 70 && (a) < 75))
+
+using std::cout;
+using std::endl;
+
+// typedef std::string Entity_f;
+// typedef std::set<Entity_f> Action_f;
+// typedef vector<Action_f> ActionsVec_f;
+typedef std::set<std::string> Agents_f;
+
+class StateConstr;
+
+class FormRSCTLK
+{
+    Oper oper;
+    FormRSCTLK *arg[2];
+    std::string entity_name;
+    std::string proc_name;
+    bool tf;
+    BDD *bdd;
+    // ActionsVec_f *actions;
+    BDD *actions_bdd;
+    StateConstr *boolCtx;
+    Agents_f agents;
+  public:
+    /**
+     * @brief Constructor for propositional variable.
+     *
+     * @param   varName variable name used mostly for printing the variable.
+     * @param   varBDD  the BDD describing the set where the variable holds.
+     */
+    FormRSCTLK(std::string procName, std::string varName)
+    {
+      oper = RSCTLK_PV;
+      proc_name = procName;
+      entity_name = varName;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for true/false.
+     *
+     * @param   val value of the logical constant
+     */
+    FormRSCTLK(bool val)
+    {
+      oper = RSCTLK_TF;
+      tf = val;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula.
+     */
+    FormRSCTLK(Oper op, FormRSCTLK *form1, FormRSCTLK *form2)
+    {
+      assert(RSCTLK_COND_2ARG(op));
+      assert(!RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula with action restrictions.
+     */
+    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1, FormRSCTLK *form2)
+    // {
+    //   assert(acts != nullptr);
+    //   assert(RSCTLK_COND_2ARG(op));
+    //   assert(RSCTLK_COND_ACT(op));
+    //   oper = op;
+    //   arg[0] = form1;
+    //   arg[1] = form2;
+    //   bdd = nullptr;
+    //   actions = acts;
+    //   actions_bdd = nullptr;
+    //   boolCtx = nullptr;
+    // }
+
+    /**
+     * @brief Constructor for two-argument formula with Boolean context restrictions.
+     */
+    FormRSCTLK(Oper op, StateConstr *bctx, FormRSCTLK *form1, FormRSCTLK *form2)
+    {
+      assert(bctx != nullptr);
+      assert(RSCTLK_COND_2ARG(op));
+      assert(RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = bctx;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula.
+     */
+    FormRSCTLK(Oper op, FormRSCTLK *form1)
+    {
+      assert(RSCTLK_COND_1ARG(op));
+      assert(!RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = nullptr;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula with action restrictions.
+     */
+    // FormRSCTLK(Oper op, ActionsVec_f *acts, FormRSCTLK *form1)
+    // {
+    //   assert(acts != nullptr);
+    //   assert(RSCTLK_COND_1ARG(op));
+    //   assert(RSCTLK_COND_ACT(op));
+    //   oper = op;
+    //   arg[0] = form1;
+    //   arg[1] = nullptr;
+    //   bdd = nullptr;
+    //   // actions = acts;
+    //   actions_bdd = nullptr;
+    //   boolCtx = nullptr;
+    // }
+
+    /**
+     * @brief Constructor for one-argument formula with Boolean context restrictions.
+     */
+    FormRSCTLK(Oper op, StateConstr *bctx, FormRSCTLK *form1)
+    {
+      assert(bctx != nullptr);
+      assert(RSCTLK_COND_1ARG(op));
+      assert(RSCTLK_COND_ACT(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      // actions = nullptr;
+      actions_bdd = nullptr;
+      boolCtx = bctx;
+    }
+
+    FormRSCTLK(Oper op, Agents_f agents_set, FormRSCTLK *form1)
+    {
+      assert(RSCTLK_COND_1ARG(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      actions_bdd = nullptr;
+      agents = agents_set;
+    }
+
+    /**
+     * @brief Destructor.
+     */
+    ~FormRSCTLK()
+    {
+      delete arg[0];
+      delete arg[1];
+      delete bdd;
+      // delete actions;
+      delete actions_bdd;
+      delete boolCtx;
+    }
+    std::string toStr(void) const;
+    bool hasOper(Oper op) const;
+    const BDD *getBDD(void) const
+    {
+      assert(oper == RSCTLK_PV);
+      assert(bdd != nullptr);
+      return bdd;
+    }
+    const BDD *getActionsBDD(void) const
+    {
+      assert(RSCTLK_COND_ACT(oper));
+      assert(actions_bdd != nullptr);
+      return actions_bdd;
+    }
+    Oper getOper(void) const
+    {
+      assert(RSCTLK_IS_VALID(oper));
+      return oper;
+    }
+    FormRSCTLK *getLeftSF(void) const
+    {
+      assert(arg[0] != nullptr);
+      return arg[0];
+    }
+    FormRSCTLK *getRightSF(void) const
+    {
+      assert(RSCTLK_COND_2ARG(oper));
+      assert(arg[1] != nullptr);
+      return arg[1];
+    }
+    std::string getActionsStr(void) const;
+    bool getTF(void) const
+    {
+      assert(oper == RSCTLK_TF);
+      return tf;
+    }
+    void encodeEntities(const SymRS *srs);
+    void encodeActions(const SymRS *srs);
+    void forgetActionsBDD(void)
+    {
+      if (actions_bdd != nullptr) {
+        delete actions_bdd;
+      }
+    }
+    bool isERSCTLK(void) const;
+    Agents_f getAgents(void) const
+    {
+      return agents;
+    }
+    std::string getSingleAgent(void) const
+    {
+      assert(oper == RSCTLK_NK || oper == RSCTLK_UK);
+      return *(agents.begin());
+    }
+    std::string getAgentsStr(void) const;
+    ProcSet getAgentsAsProcSet(RctSys *rs) const;
+};
+
+#endif

in/hsr_drs.rs

@@ -0,0 +1,64 @@
+options { use-context-automaton; }
+
+reactions {
+    mainA {
+        {{hsf},{hsp} -> {hsf3}}; #10
+        {{hsf,hsp,mfp},{dI} -> {hsf3}}; #11
+        {{hsf3},{hse,hsp} -> {hsf}}; #12
+        {{hsf3,hsp,mfp},{hse} -> {hsf}}; #13
+        {{hsf3,hse},{hsp} -> {hsf3:hse}}; #14
+        {{hsf3,hse,hsp,mfp},{dI} -> {hsf3:hse}}; #15
+        {{hse},{hsf3} -> {hse}}; #16
+        {{hse,hsf3,hsp},{mfp} -> {hse}}; #17
+        {{hsf3:hse},{hsp} -> {hsf3:hse,hsp}}; #18
+        {{hsf3:hse,hsp,mfp},{dI} -> {hsf3:hse,hsp}}; #19
+        {{hsp,hsf},{mfp} -> {hsp:hsf}}; #20
+        {{hsp:hsf,stress},{nostress} -> {hsp,hsf}}; #21
+        {{hsp:hsf,nostress},{stress} -> {hsp:hsf}}; #22
+        {{hsp,hsf3},{mfp} -> {hsp:hsf}}; #23
+        {{hsp,hsf3:hse},{mfp} -> {hsp:hsf,hse}}; 
+        {{prot,stress},{nostress} -> {prot,mfp}};
+        {{prot,nostress},{stress} -> {prot}};
+        {{hsp,mfp},{dI} -> {hsp:mfp}};
+        {{mfp},{hsp} -> {mfp}};
+        {{hsp:mfp},{dI} -> {hsp,prot}};
+    };
+
+    dummy {
+        {{mfp},{hsp} -> {mfp}};
+    };
+    
+}
+
+context-automaton {
+	states { s0, s1 }
+    init-state { s0 }
+	transitions {
+		{ mainA={hsf,prot,hse,nostress} }: s0 -> s1;
+		{ mainA={hsf,prot,hsp:hsf,stress} }: s0 -> s1;
+		{ mainA={hsp,prot,hsf3:hse,mfp,hsp:mfp,nostress} }: s0 -> s1;
+		{ mainA={stress} }: s1 -> s1;
+		{ mainA={nostress} }: s1 -> s1;
+		{ mainA={stress,nostress} }: s1 -> s1;
+	}
+}
+
+# P1
+rsctlk-property { A<mainA.stress XOR mainA.nostress>G(mainA.hse OR mainA.hsf3:hse IMPLIES A<mainA.stress XOR mainA.nostress>X(mainA.hse OR NK[mainA]( mainA.hsf3:hse ))) }
+
+# P2
+#rsctlk-property { A[{stress},{nostress}]G(~(hse AND hsf3:hse) IMPLIES A[{stress},{nostress}]X(~(hse AND hsf3:hse))) }
+
+# P3
+#rsctlk-property { A[{stress},{nostress}]G(prot IMPLIES A[{stress},{nostress}]X(prot)) }
+
+# P4
+#rsctlk-property { A[{stress},{nostress}]G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
+#rsctlk-property { A< stress XOR nostress >G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
+
+# P5
+#rsctlk-property { A[{stress},{nostress}]G( ((hsf XOR hsf3 XOR hsf3:hse XOR hsp:hsf) OR ~(hsf OR hsf3 OR hsf3:hse OR hsp:hsf)) IMPLIES A[{stress},{nostress}]X( (hsf XOR hsf3 XOR hsf3:hse XOR hsp:hsf) OR ~(hsf OR hsf3 OR hsf3:hse OR hsp:hsf) ) )  }
+
+# P6
+#rsctlk-property { A[{nostress}]G(hsp:hsf IMPLIES A[{nostress}]X (hsp:hsf)) }
+

in/scripts/gen_asm.py

@@ -0,0 +1,93 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; make-progressive; }
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{a}}, {{s}} -> {{y}}}};
+        {{{{y}}, {{s}} -> {{y}}}};
+        {{{{a}}, {{s}} -> {{b}}}};
+        {{{{b}}, {{s}} -> {{c}}}};
+        {{{{c}}, {{s}} -> {{d}}}};
+        {{{{d,y}}, {{s}} -> {{dy}}}};
+    }};
+"""
+
+FINAL_PROC = """
+    procFinal {
+        {{done}, {s} -> {done}};
+    };
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ init, act }}
+    init-state {{ init }}
+    transitions {{
+{:s}
+    }}
+}}
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }}
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+for i in range(1, n+1):
+    out += PROC_STR.format(i)
+
+out += FINAL_PROC
+out += "}\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ proc1={a} }: init -> act;\n"
+transitions += init_trans
+
+for i in range(1, n+1):
+    transitions += "{:s}{{ proc{:d}={{}} }}: act -> act : ~proc{:d}.dy;\n".format(8*" ", i, i, i)
+
+for i in range(2, n+1):
+    transitions += "{:s}{{ proc{:d}={{a}} }}: act -> act : proc{:d}.dy;\n".format(8*" ", i, i-1)
+
+final_cond = "proc1.dy"
+for i in range(2, n+1):
+     final_cond += " AND proc{:d}.dy".format(i)
+
+transitions += "{:s}{{ procFinal={{done}} }}: act -> act : {:s};\n".format(8*" ", final_cond)
+
+out += CA_STR.format(transitions)
+
+# f1
+formula = "EF( procFinal.done )"
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+formula = "AG( proc{:d}.d IMPLIES K[proc{:d}]( proc{:d}.y ) )".format(n, n, n-1)
+out += PROPERTY_STR.format("f2",formula)
+
+# x1
+formula = "EF( ~procFinal.done )"
+out += PROPERTY_STR.format("x1",formula)
+
+print(out)
+

in/scripts/gen_drs_mutex.py

@@ -0,0 +1,89 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; }
+"""
+CONTROLLER_STR = """
+    ct {
+        {{lock},{leave} -> {lock}};
+        {{req},{} -> {lock}};
+    };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{req}}, {{lock}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ s0, s1 }}
+    init-state {{ s0 }}
+    transitions {{
+{:s}
+    }}
+}}
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }}
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+out += CONTROLLER_STR
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "}\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ ct={} "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+
+init_trans += "}: s0 -> s1;\n"
+
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
+
+out += CA_STR.format(transitions)
+
+# f1
+formula = "EF( proc0.in )"
+for i in range(1, n):
+    formula += " AND EF( proc{:d}.in )".format(i)
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+
+out += PROPERTY_STR.format("f2",formula)
+
+print(out)
+

in/scripts/gen_tgc_sc.py

@@ -0,0 +1,117 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; make-progressive; };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out}}, {{}} -> {{approach}}}};
+        {{{{approach}}, {{req}} -> {{req}}}};
+        {{{{allowed}}, {{}} -> {{in}}}};
+        {{{{in}}, {{}} -> {{out,leave}}}};
+        {{{{req}}, {{in}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ init, green, red }};
+    init-state {{ init }};
+    transitions {{
+{:s}
+    }};
+}};
+"""
+
+PROPERTY_STR = """
+rsctlk-property {{ {:s} : {:s} }};
+"""
+
+
+#################################################################
+
+if len(argv) < 1:
+    print("Usage: {:s} <number of processes>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+assert n > 1, "number of proc must be > 1"
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "};\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+init_trans += "}: init -> green;\n"
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{allowed}} }}: green -> red : proc{:d}.req;\n".format(8*" ", i, i)
+
+no_req_cond = "~proc0.req"
+for i in range(1, n):
+     no_req_cond += " AND ~proc{:d}.req".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: green -> green : {:s};\n".format(8*" ", i, no_req_cond)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> green : proc{:d}.leave;\n".format(8*" ", i, i)
+
+no_leave_cond = "~proc0.leave"
+for i in range(1, n):
+     no_leave_cond += " AND ~proc{:d}.leave".format(i)
+
+for i in range(n):
+    transitions += "{:s}{{ proc{:d}={{}} }}: red -> red : {:s};\n".format(8*" ", i, no_leave_cond)
+
+out += CA_STR.format(transitions)
+
+## f1
+#formula = "EF( proc0.in )"
+#out += PROPERTY_STR.format("f1",formula)
+
+# f1
+formula = "EF( E<proc0.allowed>X( proc0.in ) )"
+for i in range(1, n):
+    formula += " AND EF( E<proc{:d}.allowed>X( proc{:d}.in ) )".format(i, i)
+out += PROPERTY_STR.format("f1",formula)
+
+# f2
+formula = "EF( proc0.approach"
+for i in range(1, n):
+    formula += " AND proc{:d}.approach".format(i)
+formula += " )"
+out += PROPERTY_STR.format("f2",formula)
+
+# f3
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+out += PROPERTY_STR.format("f3",formula)
+
+# f4
+subf = "~proc1.in"
+for i in range(2, n):
+    subf += " AND ~proc{:d}.in".format(i)
+all_agents = "proc0"
+for i in range(1, n):
+    all_agents += ",proc{:d}".format(i)
+formula = "AG( proc0.in IMPLIES C[{:s}]({:s}) )".format(all_agents,subf)
+out += PROPERTY_STR.format("f4",formula)
+
+print(out)
+

in/tgc.rs

@@ -0,0 +1,48 @@
+
+options { use-context-automaton; }
+reactions {
+
+    proc0 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc1 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+
+    proc2 {
+        {{out}, {} -> {approach}};
+        {{approach}, {req} -> {req}};
+        {{allowed}, {} -> {in}};
+        {{in}, {} -> {out,leave}};
+        {{req}, {in} -> {req}};
+    };
+}
+
+context-automaton {
+    states { init, green, red }
+    init-state { init }
+    transitions {
+        { proc0={out} proc1={out} proc2={out} }: init -> green;
+        { proc0={} proc1={} proc2={} }: green -> green : ~proc0.req AND ~proc1.req AND ~proc2.req;
+        { proc0={allowed} }: green -> red : proc0.req;
+        { proc1={allowed} }: green -> red : proc1.req;
+        { proc2={allowed} }: green -> red : proc2.req;
+        { proc0={} }: red -> green : proc0.leave;
+        { proc1={} }: red -> green : proc1.leave;
+        { proc2={} }: red -> green : proc2.leave;
+        { proc0={} proc1={} proc2={} } : red -> red : ~proc0.leave AND ~proc1.leave AND ~proc2.leave;
+    }
+}
+
+rsctlk-property { f1 : EF( proc0.in ) AND EF( proc1.in ) AND EF( proc2.in ) }
+
+rsctlk-property { f2 : AG( proc0.in IMPLIES K[proc0](~proc1.in AND ~proc2.in) ) }

macro.hh

@@ -2,13 +2,15 @@
 #define __MY_MACROS__
 
 #include <cassert>
+#include <iostream>
+
 
 #define LINENUM std::cout << __FILE__ <<  " (function " << __func__ << "), line " << __LINE__ << std::endl;
 /* Fatal error */
 #define FERROR(s) \
 { \
-	std::cerr << "EE: " << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << ": " << s << std::endl; \
+  std::cerr << "EE: " << __FILE__ << " (function " << __func__ << "), line " << __LINE__ << ": " << s << std::endl; \
-	exit(1); \
+  exit(1); \
 }
 #define WARNING(s) \
 { \
@@ -18,25 +20,28 @@
 #define VERB(s) \
 assert(opts != nullptr); \
 if (opts->verbose > 0) { \
-	std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(1): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
 #define VERB_L2(s) \
 assert(opts != nullptr); \
 if (opts->verbose > 1) { \
-	std::cerr << "ii VERBOSE(2): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(2): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
 #define VERB_L3(s) \
 assert(opts != nullptr); \
 if (opts->verbose > 2) { \
-	std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(3): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
 #define VERB_LN(n,s) \
 assert(opts != nullptr); \
 if (opts->verbose >= (n)) { \
-	std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;		\
+  std::cerr << "ii VERBOSE(" << (n) << "): " << __FILE__ << " (" << __func__ << ":" << __LINE__ << "): " << s << std::endl;   \
 }
 
+
+#define SET_ADD(set1, set2) (set1).insert((set2).begin(), (set2).end())
+
 #endif

main.cc

@@ -1,236 +0,0 @@
-/*
-    Copyright (c) 2012-2014
-    Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
-*/
-
-#include "main.hh"
-
-int main(int argc, char **argv)
-{
-    rsin_driver driver;
-
-    Options *opts = new Options;
-	driver.setOptions(opts);
-
-    bool show_reactions = false;
-    bool rstl_model_checking = false;
-    bool reach_states = false;
-    bool reach_states_succ = false;
-    bool bmc = true;
-    bool benchmarking = false;
-    bool usage_error = false;
-    bool print_parsed_sys = false;
-
-    static struct option long_options[] = 
-    {
-        {"trace-parsing",   no_argument,    0, 0   },
-        {"trace-scanning",  no_argument,    0, 0   },
-        {0,                 0,              0, 0   }
-    };
-
-    int c;
-    int option_index = 0;
-
-    while ((c = getopt_long(argc, argv, "cbBmpPrsStTvxz", long_options, &option_index)) != -1)
-    {
-        switch (c) {
-            case 0:
-                printf("option %s", long_options[option_index].name);
-                if (optarg)
-                    printf(" with arg %s", optarg);
-                printf("\n");
-
-                if (strcmp(long_options[option_index].name, "trace-parsing"))
-                    driver.trace_parsing = true;
-                else if (strcmp(long_options[option_index].name, "trace-scanning"))
-                    driver.trace_scanning = true;
-
-                break;
-            //case 'b':
-            //    printf("-b with %s\n", optarg);
-            //    break;
-            case 'b':
-                bmc = false;
-                break;
-            case 'p':
-                opts->show_progress = true;
-                break;
-            case 'P':
-                print_parsed_sys = true;
-                break;
-            case 'r':
-                show_reactions = true;
-                break;
-            case 'c':
-                rstl_model_checking = true;
-                break;
-            case 'm':
-                opts->measure = true;
-                break;
-            case 'B':
-                benchmarking = true;
-                opts->measure = true;
-                break;
-            case 's':
-                reach_states = true;
-                break;
-            case 't':
-                reach_states_succ = true;
-                break;
-            case 'v':
-                opts->verbose++;
-                break;
-            case 'x':
-                opts->part_tr_rel = true;
-                break;
-            case 'z':
-                opts->reorder_reach = true;
-                opts->reorder_trans = true;
-                break;
-            default:
-                usage_error = true;
-        }
-    }	
-	
-    std::string inputfile;
-    if (optind < argc)
-    {
-        inputfile = argv[optind];
-    }
-    else
-    {
-        cout << "Missing input file" << endl;
-        usage_error = true;
-    }
-
-    if (usage_error)
-    {
-        cout << endl
-             << " ------------------------------------" << endl
-             << " -- Reaction Systems Model Checker --" << endl
-             << " ------------------------------------" << endl
-             << endl
-             << "   Version:   " << VERSION << endl
-             << "   Contact:   " << AUTHOR << endl
-             << endl
-#ifndef PUBLIC_RELEASE
-             << " ###################################" << endl
-             << "  THIS IS A PRIVATE VERSION OF RSMC " << endl
-             << "     PLEASE, DO NOT DISTRIBUTE      " << endl
-             << " ###################################" << endl
-             << endl
-#endif
-             << " Usage: " << argv[0] << " [options] <inputfile>" << endl << endl
-			 << " TASKS:" << endl	 
-             << "  -c   -- perform RSCTL model checking" << endl
-             //<< " -f K -- generate SMT input for the depth K" << endl
-             << "  -P   -- print parsed system" << endl
-             << "  -r   -- print reactions" << endl
-             << "  -s   -- print the set of all the reachable states" << endl
-             << "  -t   -- print the set of all the reachable states with their successors" << endl
-			 << endl << " OTHER:" << endl 
-	         << "  -b   -- disable bounded model checking (BMC) heuristic" << endl
-             << "  -x   -- use partitioned transition relation (may use less memory)" << endl
-             << "  -z   -- use reordering of the BDD variables" << endl
-             << "  -v   -- verbose (can be used more than once to increase verbosity)" << endl
-             << "  -p   -- show progress (where possible)" << endl
-             << endl
-             << " Benchmarking options:" << endl
-             << "  -m   -- measure and display time and memory usage" << endl
-             << "  -B   -- display an easy to parse summary (enables -m)" << endl
-             << endl;
-        return 100;
-    }
-
-    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");
-    }
-
-    if (opts->verbose > 0) 
-    {
-        cout << "Verbose level: " << opts->verbose << endl;
-    }
-
-    VERB("Parsing " << inputfile);
-
-    if (driver.parse(inputfile))
-    {
-        FERROR("Parse error");
-    }
-	
-	//
-	// Here we retrieve the reaction system from the parser
-	//
-	// We decide which RS will be used at the parser level.
-	// This decision depends on whether we use concentrations,
-	// context automaton, etc.
-	//
-	auto rs = *driver.getReactionSystem();
-	
-    rs.setOptions(opts); // these need to be passed to the driver
-
-    if (show_reactions)
-        rs.showReactions();
-
-    if (print_parsed_sys)
-        rs.printSystem();
-
-    if (reach_states || reach_states_succ || rstl_model_checking)
-    {
-        SymRS srs(&rs, opts);
-
-        ModelChecker mc(&srs, opts);
-
-        if (reach_states)
-		{
-			mc.printReach();
-		}
-        if (reach_states_succ)
-		{
-			mc.printReachWithSucc();	
-		}
-
-        if (rstl_model_checking)
-        {
-            if (bmc)
-			{
-				cout << "Using BDD-based Bounded Model Checking" << endl;
-				mc.checkRSCTL(driver.getFormRSCTL());	
-			}
-            else 
-			{
-				mc.checkRSCTLfull(driver.getFormRSCTL());	
-			}
-        }
-    }
-
-    if (opts->measure) 
-    {
-        cout << endl << std::setprecision(4)
-             << "Encoding time: " << opts->enc_time << " sec" << endl
-             << "Verification time: " << opts->ver_time << " sec" << endl
-             << "Encoding memory: " << opts->enc_mem << " MB" << endl
-             << "Memory (total): " << opts->ver_mem << " MB" << endl
-             << "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl;
-        if (benchmarking)
-        {
-            cout << std::setprecision(4)
-                << "STAT; " << opts->enc_time
-                << " ; " << opts->ver_time 
-                << " ; " << opts->enc_mem
-                << " ; " << opts->ver_mem
-                << " ; " << opts->enc_time+opts->ver_time << endl;
-
-        }
-    }
-
-    delete opts;
-
-    return 0;
-}
-
-/** EOF **/

mc.hh

@@ -4,7 +4,7 @@
 #include "cudd.hh"
 #include "rs.hh"
 #include "symrs.hh"
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
 #include "macro.hh"
 #include "bdd_macro.hh"
 #include "options.hh"
@@ -20,52 +20,65 @@ class ModelChecker
     SymRS *srs;
     Options *opts;
     Cudd *cuddMgr;
-    BDD *initStates; 
+    BDD *initStates;
     vector<BDD> *pv;
     vector<BDD> *pv_succ;
     BDD *pv_E;
     BDD *pv_succ_E;
-    BDD *pv_act_E;
+    BDD *pv_ctx_E;
+    BDDvec *pv_drs_E;
     BDD *reach;
     vector<BDD> *trp;
     BDD *trm;
-	
+
-	// Context Automaton
+    std::map<Process, BDD> ith_only_E;
-	bool using_ctx_aut;
+
-	vector<BDD> *pv_ca;
+    // Context Automaton
-	vector<BDD> *pv_ca_succ;
+    bool using_ctx_aut;
-	BDD *pv_ca_E;	
+    vector<BDD> *pv_ca;
-	BDD *pv_ca_succ_E;
+    vector<BDD> *pv_ca_succ;
-		
+    BDD *pv_ca_E;
+    BDD *pv_ca_succ_E;
+
+    BDD *pv_proc_enab_E;
+
     unsigned int trp_size;
     unsigned int totalStateVars;
-	
+
     /**
      * @brief Abstracts away (in-place!) the context automaton states
      */
-	void dropCtxAutStatePart(BDD &states);
+    void dropCtxAutStatePart(BDD &states);
 
     BDD getSucc(const BDD &states);
     BDD getPreE(const BDD &states);
     BDD getPreEctx(const BDD &states, const BDD *contexts);
-    BDD getStatesRSCTL(const FormRSCTL *form);
+    BDD getStatesRSCTLK(const FormRSCTLK *form);
     BDD statesEG(const BDD &states);
     BDD statesEU(const BDD &statesA, const BDD &statesB);
     BDD statesEF(const BDD &states);
     BDD statesEGctx(const BDD *contexts, const BDD &states);
     BDD statesEUctx(const BDD *contexts, const BDD &statesA, const BDD &statesB);
     BDD statesEFctx(const BDD *contexts, const BDD &states);
+    BDD statesNK(const BDD &states, Process proc_id);
+    BDD statesNE(const BDD &states, ProcSet processes);
+    BDD statesNC(const BDD &states, ProcSet processes);
+
+    BDD getIthOnly(Process proc_id);
+
     void cleanup(void);
 
-public:
+    void reorder(void);
+
+  public:
     ModelChecker(SymRS *srs, Options *opts);
 
     void printReach(void);
     void printReachWithSucc(void);
     bool checkReach(const Entities testState);
-    bool checkRSCTL(FormRSCTL *form);
+    bool checkRSCTLK(FormRSCTLK *form);
-    bool checkRSCTLfull(FormRSCTL *form);
+    bool checkRSCTLKfull(FormRSCTLK *form);
-    bool checkRSCTLbmc(FormRSCTL *form);
+    bool checkRSCTLKbmc(FormRSCTLK *form);
 };
 
 #endif

memtime.hh

@@ -21,47 +21,69 @@
 
 #include <sys/time.h>
 #include <sys/resource.h>
+#if defined(__APPLE__)
+#include <malloc/malloc.h>
+#endif
 #include <stdio.h>
 #include <unistd.h>
 #include "macro.hh"
 
+using namespace std;
+
 typedef long long int64;
 
 static inline double cpuTime(void)
 {
-    struct rusage ru;
+  struct rusage ru;
-    getrusage(RUSAGE_SELF, &ru);
+  getrusage(RUSAGE_SELF, &ru);
-    return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
+  return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000;
 }
 
 static inline int memReadStat(void)
 {
-    char name[256];
+  char name[256];
-    pid_t pid = getpid();
+  pid_t pid = getpid();
-    sprintf(name, "/proc/%d/statm", pid);
+  sprintf(name, "/proc/%d/statm", pid);
-    FILE* in = fopen(name, "rb");
+  FILE *in = fopen(name, "rb");
-    if (in == nullptr)
+
-    {
+  if (in == nullptr) {
-        return 0;
+    return 0;
+  }
+
+  int value;
+
+  for (int field = 0; field >= 0; --field) {
+    if (fscanf(in, "%d", &value) == EOF) {
+      FERROR("EOF")
     }
-    int value;
+  }
-    for (int field = 0; field >= 0; --field)
+
-    {
+  fclose(in);
-        if (fscanf(in, "%d", &value) == EOF)
+  return value;
-            FERROR("EOF");
-    }
-    fclose(in);
-    return value;
 }
 
 static inline int64 memUsedInt64()
 {
-    return (int64)memReadStat() * (int64)getpagesize();
+  return (int64)memReadStat() * (int64)getpagesize();
 }
 
+#if defined(__APPLE__)
+
 static inline double memUsed()
 {
-    return memUsedInt64() / 1048576.0;
+  malloc_statistics_t t;
+  malloc_zone_statistics(NULL, &t);
+  return (double)t.max_size_in_use / (1024 * 1024);
+}
+
+#else
+
+static inline double memUsed()
+{
+  return memUsedInt64() / (1024 * 1024);
 }
 
 #endif
+
+#endif
+

options.hh

@@ -1,9 +1,10 @@
 #ifndef RS_OPTIONS_HH
 #define RS_OPTIONS_HH
 
-class Options {
+class Options
+{
 
-public:
+  public:
     unsigned int verbose;
     bool show_progress;
     bool measure;
@@ -18,19 +19,19 @@ public:
 
     Options(void)
     {
-        verbose = 0;
+      verbose = 0;
-        show_progress = false;
+      show_progress = false;
-        measure = false;
+      measure = false;
 
-        part_tr_rel = false;
+      part_tr_rel = false;
 
-        reorder_reach = false; 
+      reorder_reach = false;
-        reorder_trans = false;
+      reorder_trans = false;
 
-        enc_time = 0;
+      enc_time = 0;
-        enc_mem = 0;
+      enc_mem = 0;
-        ver_time = 0;
+      ver_time = 0;
-        ver_mem = 0;
+      ver_mem = 0;
     }
 };
 

reactics.cc

@@ -0,0 +1,271 @@
+/*
+    Copyright (c) 2012-2014
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "reactics.hh"
+
+int main(int argc, char **argv)
+{
+  rsin_driver driver;
+
+  Options *opts = new Options;
+  driver.setOptions(opts);
+
+  bool show_reactions = false;
+  bool rstl_model_checking = false;
+  bool reach_states = false;
+  bool reach_states_succ = false;
+  bool bmc = true;
+  bool benchmarking = false;
+  bool dump_help_message = false;
+  bool print_parsed_sys = false;
+  std::string property_name = "default";
+
+  static struct option long_options[] = {
+    {"trace-parsing",   no_argument,    0, 0   },
+    {"trace-scanning",  no_argument,    0, 0   },
+    {0,                 0,              0, 0   }
+  };
+
+  int c;
+  int option_index = 0;
+
+  while ((c = getopt_long(argc, argv, "c:bBmpPrsStTvxzh", long_options,
+                          &option_index)) != -1) {
+    switch (c) {
+      case 0:
+        printf("option %s", long_options[option_index].name);
+
+        if (optarg) {
+          printf(" with arg %s", optarg);
+        }
+
+        printf("\n");
+
+        if (strcmp(long_options[option_index].name, "trace-parsing")) {
+          driver.trace_parsing = true;
+        }
+        else if (strcmp(long_options[option_index].name, "trace-scanning")) {
+          driver.trace_scanning = true;
+        }
+
+        break;
+
+      //case 'b':
+      //    printf("-b with %s\n", optarg);
+      //    break;
+      case 'b':
+        bmc = false;
+        break;
+
+      case 'p':
+        opts->show_progress = true;
+        break;
+
+      case 'P':
+        print_parsed_sys = true;
+        break;
+
+      case 'r':
+        show_reactions = true;
+        break;
+
+      case 'c':
+        rstl_model_checking = true;
+        property_name = optarg;
+        break;
+
+      case 'm':
+        opts->measure = true;
+        break;
+
+      case 'B':
+        benchmarking = true;
+        opts->measure = true;
+        break;
+
+      case 's':
+        reach_states = true;
+        break;
+
+      case 't':
+        reach_states_succ = true;
+        break;
+
+      case 'v':
+        opts->verbose++;
+        break;
+
+      case 'x':
+        opts->part_tr_rel = true;
+        break;
+
+      case 'z':
+        opts->reorder_reach = true;
+        opts->reorder_trans = true;
+        break;
+
+      case 'h':
+        dump_help_message = true;
+        break;
+
+      default:
+        dump_help_message = true;
+        break;
+    }
+  }
+
+  std::string inputfile;
+
+  if (optind < argc) {
+    inputfile = argv[optind];
+  }
+  else if (!dump_help_message) {
+    cout << "Missing input file" << endl;
+    dump_help_message = true;
+  }
+
+  if (dump_help_message) {
+    print_help(std::string(argv[0]));
+    return 100;
+  }
+
+  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");
+  }
+
+  if (opts->verbose > 0) {
+    cout << "Verbose level: " << opts->verbose << endl;
+  }
+
+  VERB("Parsing " << inputfile);
+
+  if (driver.parse(inputfile)) {
+    FERROR("Parse error");
+  }
+
+  //
+  // Here we retrieve the reaction system from the parser
+  //
+  // We decide which RS will be used at the parser level.
+  // This decision depends on whether we use concentrations,
+  // context automaton, etc.
+  //
+  auto rs = *driver.getReactionSystem();
+
+  bool result = true;
+
+  rs.setOptions(opts); // these need to be passed to the driver
+
+  if (show_reactions) {
+    rs.showReactions();
+  }
+
+  if (print_parsed_sys) {
+    rs.printSystem();
+  }
+
+  if (reach_states || reach_states_succ || rstl_model_checking) {
+    SymRS srs(&rs, opts);
+
+    ModelChecker mc(&srs, opts);
+
+    if (reach_states) {
+      mc.printReach();
+    }
+
+    if (reach_states_succ) {
+      mc.printReachWithSucc();
+    }
+
+    if (rstl_model_checking) {
+      if (bmc) {
+        cout << "Using BDD-based Bounded Model Checking" << endl;
+        result = mc.checkRSCTLK(driver.getFormRSCTLK(property_name));
+      }
+      else {
+        result = mc.checkRSCTLKfull(driver.getFormRSCTLK(property_name));
+      }
+    }
+  }
+
+  if (opts->measure) {
+    cout << endl << std::setprecision(4)
+         << "Encoding time: " << opts->enc_time << " sec" << endl
+         << "Verification time: " << opts->ver_time << " sec" << endl
+         << "Encoding memory: " << opts->enc_mem << " MB" << endl
+         << "Memory (total): " << opts->ver_mem << " MB" << endl
+         << "TOTAL time: " << opts->enc_time + opts->ver_time << " sec" << endl;
+
+    if (benchmarking) {
+      cout << std::setprecision(4)
+           << "STAT; " << opts->enc_time
+           << " ; " << opts->ver_time
+           << " ; " << opts->enc_mem
+           << " ; " << opts->ver_mem
+           << " ; " << opts->enc_time + opts->ver_time << endl;
+
+    }
+  }
+
+  delete opts;
+
+  int ret_val;
+
+  if (result) {
+    ret_val = 0;
+  }
+  else {
+    ret_val = 1;
+  }
+
+  return ret_val;
+}
+
+void print_help(std::string path_str)
+{
+  cout << endl
+       << " ------------------------------------------------" << endl
+       << " -- ReactICS -- Reaction Systems Model Checker --" << endl
+       << " ------------------------------------------------" << endl
+       << endl
+       << "   Version:   " << VERSION << endl
+       << "   Contact:   " << AUTHOR << endl
+       << endl
+#ifndef PUBLIC_RELEASE
+       << " ###################################" << endl
+       << "  THIS IS A PRIVATE VERSION OF RSMC " << endl
+       << "     PLEASE, DO NOT DISTRIBUTE      " << endl
+       << " ###################################" << endl
+       << endl
+#endif
+       << " Usage: " << path_str << " [options] <input file>" << endl << endl
+       << " TASKS:" << endl
+       << "  -c form  -- perform RSCTLK model checking (form: formula identifier)" << endl
+       //<< " -f K -- generate SMT input for the depth K" << endl
+       << "  -P       -- print parsed system" << endl
+       << "  -r       -- print reactions" << endl
+       << "  -s       -- print all the reachable states" << endl
+       << "  -t       -- print all the reachable states with their successors"
+       << endl
+       << endl << " OTHER:" << endl
+       << "  -b       -- disable bounded model checking (BMC) heuristic" << endl
+       << "  -x       -- use partitioned transition relation" <<
+       endl
+       << "  -z       -- use reordering of the BDD variables" << endl
+       << "  -v       -- verbose (use more than once to increase verbosity)" <<
+       endl
+       << "  -p       -- show progress (where possible)" << endl
+       << endl
+       << " Benchmarking options:" << endl
+       << "  -m       -- measure and display time and memory usage" << endl
+       << "  -B       -- display an easy to parse summary (enables -m)" << endl
+       << endl;
+}
+
+/** EOF **/

reactics.hh

@@ -1,13 +1,10 @@
 /*
-    Copyright (c) 2012, 2013
+    Copyright (c) 2012, 2013, 2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
-#ifndef RS_MAIN_HH
+#ifndef REACTICS_HH
-#define RS_MAIN_HH
+#define REACTICS_HH
 
 #include <iostream>
 #include <string>
@@ -22,9 +19,12 @@
 #include "options.hh"
 #include "memtime.hh"
 
-#define VERSION     "1.0alpha"
+#define VERSION     "2.0"
-#define AUTHOR      "Artur Męski <meski@ipipan.waw.pl>"
+//#define AUTHOR      "Artur Meski <artur.meski@gmail.com>"
+#define AUTHOR      "Artur Meski <meski@ipipan.waw.pl>"
 using std::cout;
 using std::endl;
 
+void print_help(std::string path_str);
+
 #endif

rs.cc

@@ -1,233 +1,371 @@
 /*
-    Copyright (c) 2012-2014
+    Copyright (c) 2012-2018
     Artur Meski <meski@ipipan.waw.pl>
-
-    Reuse of the code or its part for any purpose
-    without the author's permission is strictly prohibited.
 */
 
 #include "rs.hh"
 
 RctSys::RctSys(void)
+  : current_process_defined(false)
 {
-	ctx_aut = nullptr;
+  ctx_aut = nullptr;
+  gen_ctxaut_progressive_closure = false;
 }
 
 bool RctSys::hasEntity(std::string name)
 {
-    if (entities_names.find(name) == entities_names.end())
+  if (entities_names.find(name) == entities_names.end()) {
-        return false;
+    return false;
-    else
+  }
-        return true;
+  else {
+    return true;
+  }
 }
 
 void RctSys::addEntity(std::string name)
 {
-    if (!hasEntity(name))
+  if (!hasEntity(name)) {
-    {
+    Entity new_entity_id = entities_ids.size();
-        Entity new_entity_id = entities_ids.size();
 
-        VERB_L2("Adding entity: " << name << " index=" << new_entity_id);
+    VERB_L2("Adding entity: " << name << " index=" << new_entity_id);
 
-        entities_ids.push_back(name);		
+    entities_ids.push_back(name);
-        entities_names[name] = new_entity_id;
+    entities_names[name] = new_entity_id;
-    }
+  }
 }
 
 std::string RctSys::getEntityName(Entity entityID)
 {
-    if (entityID < entities_ids.size())
+  if (entityID < entities_ids.size()) {
-        return entities_ids[entityID];
+    return entities_ids[entityID];
-    else
+  }
-    {
+  else {
-        FERROR("No such entity ID: " << entityID);
+    FERROR("No such entity ID: " << entityID);
-        return "??";
+    return "??";
-    }
+  }
 }
 
 Entity RctSys::getEntityID(std::string name)
 {
-    if (!hasEntity(name))
+  if (!hasEntity(name)) {
-    {
+    FERROR("No such entity: " << name);
-        FERROR("No such entity: " << name);
+  }
-    }
+
-    return entities_names[name];
+  return entities_names[name];
+}
+
+void RctSys::setCurrentProcess(std::string processName)
+{
+  VERB_LN(2, "Current Process: " << processName);
+
+  if (!hasProcess(processName)) {
+    addProcess(processName);
+  }
+
+  current_proc_id = getProcessID(processName);
+  current_process_defined = true;
+}
+
+void RctSys::addProcess(std::string processName)
+{
+  if (!hasProcess(processName)) {
+    Process new_proc_id = processes_ids.size();
+
+    VERB_L2("Adding process: " << processName << " index=" << new_proc_id);
+
+    processes_ids.push_back(processName);
+    processes_names[processName] = new_proc_id;
+
+    // reactions for the new process
+    proc_reactions[new_proc_id] = Reactions();
+    assert(proc_reactions.size() == new_proc_id + 1);
+  }
+}
+
+bool RctSys::hasProcess(std::string processName)
+{
+  if (processes_names.find(processName) == processes_names.end()) {
+    return false;
+  }
+  else {
+    return true;
+  }
+}
+
+bool RctSys::hasProcess(Process processID)
+{
+  if (processID >= processes_ids.size()) {
+    return false;
+  }
+
+  return true;
+}
+
+Process RctSys::getProcessID(std::string processName)
+{
+  if (!hasProcess(processName)) {
+    FERROR("No such process: " << processName);
+  }
+
+  return processes_names[processName];
+}
+
+std::string RctSys::getProcessName(Process processID)
+{
+  if (hasProcess(processID)) {
+    return processes_ids[processID];
+  }
+  else {
+    FERROR("No such process ID: " << processID);
+  }
 }
 
 void RctSys::pushReactant(std::string entityName)
 {
-    if (!hasEntity(entityName))
+  if (!hasEntity(entityName)) {
-        addEntity(entityName);
+    addEntity(entityName);
-    tmpReactants.insert(getEntityID(entityName));
+  }
+
+  tmpReactants.insert(getEntityID(entityName));
 }
 void RctSys::pushInhibitor(std::string entityName)
 {
-    if (!hasEntity(entityName))
+  if (!hasEntity(entityName)) {
-        addEntity(entityName);
+    addEntity(entityName);
-    tmpInhibitors.insert(getEntityID(entityName));
+  }
+
+  tmpInhibitors.insert(getEntityID(entityName));
 }
 void RctSys::pushProduct(std::string entityName)
 {
-    if (!hasEntity(entityName))
+  if (!hasEntity(entityName)) {
-        addEntity(entityName);
+    addEntity(entityName);
-    tmpProducts.insert(getEntityID(entityName));
+  }
+
+  tmpProducts.insert(getEntityID(entityName));
+}
+
+void RctSys::addReactionForCurrentProcess(Reaction reaction)
+{
+  if (!current_process_defined) {
+    FERROR("Internal error. Current process is not set!");
+  }
+
+  proc_reactions[current_proc_id].push_back(reaction);
 }
 
 void RctSys::commitReaction(void)
 {
-    VERB_L3("Saving reaction");
+  VERB_L3("Saving reaction");
 
-    Reaction r;
+  Reaction r;
 
-    r.rctt = tmpReactants;
+  r.rctt = tmpReactants;
-    r.inhib = tmpInhibitors;
+  r.inhib = tmpInhibitors;
-    r.prod = tmpProducts;
+  r.prod = tmpProducts;
 
-    reactions.push_back(r);
+  addReactionForCurrentProcess(r);
 
-    tmpReactants.clear();
+  tmpReactants.clear();
-    tmpInhibitors.clear();
+  tmpInhibitors.clear();
-    tmpProducts.clear();
+  tmpProducts.clear();
 }
 
 std::string RctSys::entitiesToStr(const Entities &entities)
 {
-    std::string s = " ";
+  std::string s = " ";
-    for (auto a = entities.begin(); a != entities.end(); ++a)
+
-    {
+  for (auto a = entities.begin(); a != entities.end(); ++a) {
-        s += entityToStr(*a) + " ";
+    s += entityToStr(*a) + " ";
-    }
+  }
-    return s;
+
+  return s;
+}
+
+std::string RctSys::procEntitiesToStr(const EntitiesForProc &procEntities)
+{
+  std::string s = "";
+
+  for (auto const &p : procEntities) {
+    s += getProcessName(p.first) + "={" + entitiesToStr(p.second) + "} ";
+  }
+
+  return s;
 }
 
 void RctSys::showReactions(void)
 {
-    cout << "# Reactions:" << endl;
+  cout << "# Reactions:" << endl;
-    for (auto r = reactions.begin(); r != reactions.end(); ++r)
+
-    {
+  for (unsigned int proc_id = 0; proc_id < processes_ids.size(); ++proc_id) {
-        cout << " * (R={" << entitiesToStr(r->rctt) << "},"
+    cout << endl;
-             << "I={" << entitiesToStr(r->inhib) << "}," 
+    cout << "  . proc = \"" << getProcessName(proc_id) << "\":" << endl;
-             << "P={" << entitiesToStr(r->prod) << "})" << endl;
+
-    } 
+    for (const auto &r : proc_reactions[proc_id]) {
+      cout << "     * (R={" << entitiesToStr(r.rctt) << "},"
+           << "I={" << entitiesToStr(r.inhib) << "},"
+           << "P={" << entitiesToStr(r.prod) << "})" << endl;
+    }
+  }
+
+  cout << endl;
 }
 
 void RctSys::pushStateEntity(std::string entityName)
 {
-    if (!hasEntity(entityName))
+  if (!hasEntity(entityName)) {
-    {
+    FERROR("No such entity: " << entityName);
-        FERROR("No such entity: " << entityName);
+  }
-    }
+
-    tmpState.insert(getEntityID(entityName)); 
+  tmpState.insert(getEntityID(entityName));
 }
 
 void RctSys::commitInitState(void)
 {
-	if (ctx_aut != nullptr)
+  if (ctx_aut != nullptr) {
-	{
+    FERROR("Initial RS states must not be used with context automaton");
-		FERROR("Initial RS states must not be used with context automaton");
+  }
-	}
+
-    initStates.insert(tmpState); 
+  initStates.insert(tmpState);
-    tmpState.clear();
+  tmpState.clear();
 }
 
 void RctSys::addActionEntity(std::string entityName)
 {
-    if (!hasEntity(entityName))
+  if (!hasEntity(entityName)) {
-        addEntity(entityName);
+    addEntity(entityName);
-    actionEntities.insert(getEntityID(entityName));
+  }
+
+  actionEntities.insert(getEntityID(entityName));
 }
 
 void RctSys::addActionEntity(Entity entity)
 {
-	if (!isActionEntity(entity))
+  if (!isActionEntity(entity)) {
-	    actionEntities.insert(entity);
+    actionEntities.insert(entity);
+  }
 }
 
 bool RctSys::isActionEntity(Entity entity)
 {
-    if (actionEntities.count(entity) > 0)
+  if (actionEntities.count(entity) > 0) {
-        return true;
+    return true;
-    else
+  }
-        return false;
+  else {
+    return false;
+  }
 }
 
 void RctSys::showActionEntities(void)
 {
-    cout << "# Context entities:";
+  cout << "# Context entities:";
-    for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a)
+
-    {
+  for (auto a = actionEntities.begin(); a != actionEntities.end(); ++a) {
-        cout << " " << getEntityName(*a);
+    cout << " " << getEntityName(*a);
-    }
+  }
-    cout << endl;
+
+  cout << endl;
 }
 
 void RctSys::showInitialStates(void)
 {
-    cout << "# Initial states:" << endl;
+  cout << "# Initial states:" << endl;
-    for (auto s = initStates.begin(); s != initStates.end(); ++s)
+
-    {
+  for (auto s = initStates.begin(); s != initStates.end(); ++s) {
-        cout << " *";
+    cout << " *";
-        for (auto a = s->begin(); a != s->end(); ++a)
+
-        {
+    for (auto a = s->begin(); a != s->end(); ++a) {
-            cout << " " << getEntityName(*a);
+      cout << " " << getEntityName(*a);
-        }
-        cout << endl;
     }
+
+    cout << endl;
+  }
 }
 
 void RctSys::printSystem(void)
 {
-	if (!usingContextAutomaton())
+  if (!usingContextAutomaton()) {
-	    showInitialStates();
+    showInitialStates();
-    showActionEntities();
+  }
-    showReactions();
+
-	
+  showActionEntities();
-	if (ctx_aut != nullptr) ctx_aut->printAutomaton();
+  showReactions();
+
+  if (ctx_aut != nullptr) {
+    ctx_aut->printAutomaton();
+  }
 }
 
 void RctSys::ctxAutEnable(void)
 {
-	assert(ctx_aut == nullptr);
+  assert(ctx_aut == nullptr);
-	if (initStatesDefined())
+
-	{
+  if (initStatesDefined()) {
-		FERROR("Initial states must not be defined if using context automaton");
+    FERROR("Initial states must not be defined if using context automaton");
-	}
+  }
-	ctx_aut = new CtxAut(opts, this);
+
+  ctx_aut = new CtxAut(opts, this);
+}
+
+void RctSys::ctxAutEnableProgressiveClosure(void)
+{
+  gen_ctxaut_progressive_closure = true;
 }
 
 void RctSys::ctxAutAddState(std::string stateName)
 {
-	assert(ctx_aut != nullptr);
+  assert(ctx_aut != nullptr);
-	ctx_aut->addState(stateName);
+  ctx_aut->addState(stateName);
 }
 
 void RctSys::ctxAutSetInitState(std::string stateName)
 {
-	assert(ctx_aut != nullptr);
+  assert(ctx_aut != nullptr);
-	ctx_aut->setInitState(stateName);
+  ctx_aut->setInitState(stateName);
 }
 
-void RctSys::ctxAutAddTransition(std::string srcStateName, std::string dstStateName)
+void RctSys::ctxAutAddTransition(std::string srcStateName,
+                                 std::string dstStateName)
 {
-	assert(ctx_aut != nullptr);
+  assert(ctx_aut != nullptr);
-	ctx_aut->addTransition(srcStateName, dstStateName);
+  ctx_aut->addTransition(srcStateName, dstStateName, nullptr);
+}
+
+void RctSys::ctxAutAddTransition(std::string srcStateName,
+                                 std::string dstStateName, StateConstr *stateConstr)
+{
+  assert(ctx_aut != nullptr);
+  ctx_aut->addTransition(srcStateName, dstStateName, stateConstr);
 }
 
 void RctSys::ctxAutPushNamedContextEntity(std::string entityName)
 {
-	assert(ctx_aut != nullptr);
+  assert(ctx_aut != nullptr);
-	
-	Entity entity_id = getEntityID(entityName);
 
-	//
+  Entity entity_id = getEntityID(entityName);
-	// We mark the entity as an action entity
+
-	//
+  //
-	// 	This step is required to ensure the minimal number of
+  // We mark the entity as an action entity
-	//  BDD variables used in the encoding of the context sets
+  //
-	//
+  //  This step is required to ensure the minimal number of
-	addActionEntity(entity_id);
+  //  BDD variables used in the encoding of the context sets
-	
+  //
-	ctx_aut->pushContextEntity(entity_id);
+  addActionEntity(entity_id);
+
+  ctx_aut->pushContextEntity(entity_id);
+}
+
+void RctSys::ctxAutSaveCurrentContextSet(std::string processName)
+{
+  Process processID = getProcessID(processName);
+  ctx_aut->saveCurrentContextSet(processID);
+}
+
+void RctSys::ctxAutFinalise(void)
+{
+  if (gen_ctxaut_progressive_closure) {
+    ctx_aut->makeProgressive();
+  }
 }
 
 /** EOF **/

rs.hh

@@ -25,83 +25,122 @@ using std::cout;
 using std::endl;
 
 class CtxAut;
+class StateConstr;
 
 class RctSys
 {
-	    friend class SymRS;
+    friend class SymRS;
-	    friend class SymRSstate;
+    friend class SymRSstate;
 
-	public:
+  public:
-		RctSys(void);
+    RctSys(void);
-	    void setOptions(Options *opts)
-	    {
-	        this->opts = opts;
-	    }
-	    bool hasEntity(std::string entityName);
-	    void addEntity(std::string entityName);
-	    std::string getEntityName(Entity entityID);
-	    void pushReactant(std::string entityName);
-	    void pushInhibitor(std::string entityName);
-	    void pushProduct(std::string entityName);
-	    void commitReaction(void);
-	    std::string entityToStr(const Entity entity) {
-	        return entities_ids[entity];
-	    }
-	    std::string entitiesToStr(const Entities &entities);
-	    void showReactions(void);
-	    void pushStateEntity(std::string entityName);
-	    void commitInitState(void);
-	    void addActionEntity(std::string entityName);
-	    void addActionEntity(Entity entity);
-	    bool isActionEntity(Entity entity);
-	    void resetInitStates(void) {
-	        initStates.clear();
-	    }
-	    unsigned int getEntitiesSize(void) {
-	        return entities_ids.size();
-	    }
-	    unsigned int getReactionsSize(void) {
-	        return reactions.size();
-	    }
-	    unsigned int getActionsSize(void) {
-	        return actionEntities.size();
-	    }
-	    void showInitialStates(void);
-	    void showActionEntities(void);
-	    void printSystem(void);
 
-		void ctxAutEnable(void);		
+    void setOptions(Options *opts)
-		void ctxAutAddState(std::string stateName);
+    {
-		void ctxAutSetInitState(std::string stateName);
+      this->opts = opts;
-		void ctxAutAddTransition(std::string srcStateName, std::string dstStateName);
+    }
-		void ctxAutPushNamedContextEntity(std::string entity_name);
+    bool hasEntity(std::string entityName);
-		
+    void addEntity(std::string entityName);
-		bool initStatesDefined(void) { return initStates.size() != 0; }
+    std::string getEntityName(Entity entityID);
-		bool usingContextAutomaton(void) { return ctx_aut != nullptr; }
-		
-	private:
-	    Reactions reactions;
-	    EntitiesSets initStates;
 
-	    Entities actionEntities;
+    void setCurrentProcess(std::string processName);
+    void addProcess(std::string processName);
+    bool hasProcess(Process processID);
+    bool hasProcess(std::string processName);
+    Process getProcessID(std::string processName);
+    std::string getProcessName(Process processID);
 
-		CtxAut *ctx_aut;
+    void addReactionForCurrentProcess(Reaction reaction);
 
-	    EntitiesByIds entities_ids;
+    void pushReactant(std::string entityName);
-	    EntitiesByName entities_names;
+    void pushInhibitor(std::string entityName);
+    void pushProduct(std::string entityName);
+    void commitReaction(void);
+    std::string entityToStr(const Entity entity)
+    {
+      return entities_ids[entity];
+    }
+    std::string entitiesToStr(const Entities &entities);
+    std::string procEntitiesToStr(const EntitiesForProc &procEntities);
+    void showReactions(void);
+    void pushStateEntity(std::string entityName);
+    void commitInitState(void);
+    void addActionEntity(std::string entityName);
+    void addActionEntity(Entity entity);
+    bool isActionEntity(Entity entity);
+    void resetInitStates(void)
+    {
+      initStates.clear();
+    }
+    unsigned int getEntitiesSize(void)
+    {
+      return entities_ids.size();
+    }
+    unsigned int getActionsSize(void)
+    {
+      return actionEntities.size();
+    }
+    void showInitialStates(void);
+    void showActionEntities(void);
+    void printSystem(void);
 
-	    Entities tmpReactants;
+    void ctxAutEnable(void);
-	    Entities tmpInhibitors;
+    void ctxAutEnableProgressiveClosure(void);
-	    Entities tmpProducts;
+    void ctxAutAddState(std::string stateName);
+    void ctxAutSetInitState(std::string stateName);
+    void ctxAutAddTransition(std::string srcStateName, std::string dstStateName);
+    void ctxAutAddTransition(std::string srcStateName, std::string dstStateName, StateConstr *stateConstr);
+    void ctxAutPushNamedContextEntity(std::string entity_name);
+    void ctxAutSaveCurrentContextSet(std::string processName);
+    void ctxAutFinalise(void);
 
-	    Entities tmpState;
+    bool initStatesDefined(void)
+    {
+      return initStates.size() != 0;
+    }
+    bool usingContextAutomaton(void)
+    {
+      return ctx_aut != nullptr;
+    }
 
-	    Options *opts;
+    size_t getNumberOfProcesses(void)
+    {
+      return processes_ids.size();
+    }
 
-	    Entity getEntityID(std::string entityName);
+  private:
+
+    ReactionsForProc proc_reactions;
+
+    EntitiesSets initStates;
+
+    Entities actionEntities;
+
+    CtxAut *ctx_aut;
+
+    bool gen_ctxaut_progressive_closure;
+
+    EntitiesById entities_ids;
+    EntitiesByName entities_names;
+
+    ProcessesById processes_ids;
+    ProcessesByName processes_names;
+
+    Process current_proc_id;
+    bool current_process_defined;
+
+    Entities tmpReactants;
+    Entities tmpInhibitors;
+    Entities tmpProducts;
+
+    Entities tmpState;
+
+    Options *opts;
+
+    Entity getEntityID(std::string entityName);
 
 };
 
 #endif
 
-/** EOF **/
+/** EOF **/

rsin_driver.cc

@@ -1,62 +1,68 @@
 #include "rsin_driver.hh"
 #include "rsin_parser.hh"
 
+#include "rs.hh"
+
 rsin_driver::rsin_driver(void)
-: trace_scanning(false), trace_parsing(false)
+  : trace_scanning(false), trace_parsing(false)
 {
-	initialise();
+  initialise();
 }
 
 rsin_driver::rsin_driver(RctSys *rs)
-: trace_scanning(false), trace_parsing(false)
+  : trace_scanning(false), trace_parsing(false)
 {
-	initialise();
+  initialise();
-	this->rs = rs;
+  this->rs = rs;
 }
 
 void rsin_driver::initialise(void)
 {
-    rs = nullptr;
+  rs = nullptr;
-    rsctlform = nullptr;
+  opts = nullptr;
-	opts = nullptr;
+  use_ctx_aut = false;
-	use_ctx_aut = false;
+  use_concentrations = false;
-	use_concentrations = false;
+  make_progressive = false;
 }
 
 rsin_driver::~rsin_driver ()
 {
-	// placeholder
+  // placeholder
 }
 
 int rsin_driver::parse(const std::string &f)
 {
-    file = f;
+  file = f;
-    scan_begin();
+  scan_begin();
-    yy::rsin_parser parser(*this);
+  yy::rsin_parser parser(*this);
-    parser.set_debug_level(trace_parsing);
+  parser.set_debug_level(trace_parsing);
-    int res = parser.parse();
+  int res = parser.parse();
-    scan_end();
+  scan_end();
-    return res;
+  return res;
 }
 
 void rsin_driver::error(const yy::location &l, const std::string &m)
 {
-    std::cerr << l << ": " << m << std::endl;
+  std::cerr << l << ": " << m << std::endl;
 }
 
 void rsin_driver::error(const std::string &m)
 {
-    std::cerr << m << std::endl;
+  std::cerr << m << std::endl;
 }
 
-FormRSCTL *rsin_driver::getFormRSCTL(void)
+void rsin_driver::addFormRSCTLK(std::string propertyName, FormRSCTLK *f)
 {
-    if (rsctlform == nullptr)
+  properties[propertyName] = f;
-    {
+};
-        FERROR("RSCTL formula was not supplied!");
-    }
 
-    return rsctlform;
+FormRSCTLK *rsin_driver::getFormRSCTLK(std::string propertyName)
+{
+  if (properties.count(propertyName) == 0) {
+    FERROR("Property/formula label does not exist: " << propertyName);
+  }
+
+  return properties[propertyName];
 }
 
 //
@@ -64,40 +70,53 @@ FormRSCTL *rsin_driver::getFormRSCTL(void)
 //
 void rsin_driver::ensureOptionsAllowed(void)
 {
-	if (rs != nullptr)
+  if (rs != nullptr) {
-	{
+    FERROR("Options cannot be set/modified after the reaction system is initialised")
-		FERROR("Options cannot be set/modified after the reaction system is initialised")
+  }
-	}
 }
 
 void rsin_driver::ensureReactionSystemReady(void)
 {
-	if (rs == nullptr)
+  if (rs == nullptr) {
-		setupReactionSystem();
+    setupReactionSystem();
+  }
 }
 
 void rsin_driver::setupReactionSystem(void)
 {
-	assert(rs == nullptr);
+  assert(rs == nullptr);
-	rs = new RctSys;
+  rs = new RctSys;
-	
-	if (use_ctx_aut) VERB("Using RS with CA")
-	else VERB("Using ordinary RS")
 
-	rs->setOptions(opts);
+  if (use_ctx_aut) VERB("Using RS with CA")
+    else VERB("Using ordinary RS")
+
+      rs->setOptions(opts);
 }
 
 RctSys *rsin_driver::getReactionSystem(void)
 {
-	ensureReactionSystemReady();
+  ensureReactionSystemReady();
-	assert(rs != nullptr);
+  assert(rs != nullptr);
-	return rs;
+  return rs;
 }
 
 void rsin_driver::useContextAutomaton(void)
 {
-	ensureOptionsAllowed(); 
+  ensureOptionsAllowed();
-	use_ctx_aut = true; 
+  use_ctx_aut = true;
-	getReactionSystem()->ctxAutEnable();
+  getReactionSystem()->ctxAutEnable();
 }
 
+void rsin_driver::makeProgressive(void)
+{
+  make_progressive = true;
+
+  if (use_ctx_aut) {
+    getReactionSystem()->ctxAutEnableProgressiveClosure();
+  }
+  else {
+    FERROR("Context automaton not enabled");
+  }
+}
+
+// EOF

rsin_driver.hh

@@ -3,8 +3,8 @@
 #include <string>
 #include <map>
 #include "rsin_parser.hh"
-#include "rs.hh"
+// #include "rs.hh"
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
 #include "options.hh"
 
 // Tell Flex the lexer's prototype ...
@@ -16,21 +16,26 @@
 // ... and declare it for the parser's sake.
 YY_DECL;
 
+class RctSys;
+class CtxAut;
+
 // Conducting the whole scanning an parsing of RS
 class rsin_driver
 {
-public:
+  public:
     rsin_driver(void);
     rsin_driver(RctSys *rs);
     virtual ~rsin_driver();
 
     //std::map<std::string, int> variables;
-    FormRSCTL *rsctlform;
     Options *opts;
-	
+
-	// options in configuration file:
+    std::map<std::string, FormRSCTLK *> properties;
-	bool use_ctx_aut;
+
-	bool use_concentrations;
+    // options in configuration file:
+    bool use_ctx_aut;
+    bool use_concentrations;
+    bool make_progressive;
 
     // Handling the scanner
     void scan_begin();
@@ -41,29 +46,36 @@ public:
     std::string file;
     bool trace_parsing;
 
-	void setOptions(Options *opts) 		{ this->opts = opts; };
+    void setOptions(Options *opts)
-    void addFormRSCTL(FormRSCTL *f) 	{ rsctlform = f; };
+    {
-    FormRSCTL *getFormRSCTL(void);
+      this->opts = opts;
+    };
+    void addFormRSCTLK(std::string propertyName, FormRSCTLK *f);
 
-	void ensureOptionsAllowed(void);
+    FormRSCTLK *getFormRSCTLK(std::string propertyName);
-	void useContextAutomaton(void);
+
-	void useConcentrations(void)		{ ensureOptionsAllowed(); use_concentrations = true; };
+    void ensureOptionsAllowed(void);
-	
+    void useContextAutomaton(void);
-	void ensureReactionSystemReady(void);
+    void useConcentrations(void)
-	void setupReactionSystem(void);
+    {
-	
+      ensureOptionsAllowed();
-	RctSys *getReactionSystem(void);
+      use_concentrations = true;
-	CtxAut *getCtxAut(void);
+    };
+    void makeProgressive(void);
+    void ensureReactionSystemReady(void);
+    void setupReactionSystem(void);
+
+    RctSys *getReactionSystem(void);
+    CtxAut *getCtxAut(void);
 
     // Error handling.
     void error(const yy::location &l, const std::string &m);
     void error(const std::string &m);
-	
+
-private:
+  private:
     RctSys *rs;
 
-	void initialise(void);
+    void initialise(void);
 };
 
 #endif
-

rsin_parser.ll

@@ -38,34 +38,39 @@ blank [ \t]
   typedef yy::rsin_parser::token token;
 %}
 
-"options"				return token::OPTIONS;
+"options"				        return token::OPTIONS;
 "use-context-automaton"	return token::USE_CTX_AUT;
-"use-concentrations"	return token::USE_CONCENTRATIONS;
+"use-concentrations"	  return token::USE_CONCENTRATIONS;
+"make-progressive"      return token::MAKE_PROGRESSIVE;
 "reactions"             return token::REACTIONS;
 "initial-contexts"      return token::INITIALCONTEXTS;
 "context-entities"      return token::CONTEXTENTITIES;
-"context-automaton"		return token::CONTEXTAUTOMATON;
+"context-automaton"		  return token::CONTEXTAUTOMATON;
-"transitions"			return token::TRANSITIONS;
+"transitions"			      return token::TRANSITIONS;
-"states"				return token::STATES;
+"states"				        return token::STATES;
-"init-state"			return token::INITSTATE;
+"init-state"			      return token::INITSTATE;
-"rsctl-property"        return token::RSCTLFORM;
+"rsctlk-property"        return token::RSCTLKFORM;
 "{"                     return token::LCB;
 "}"                     return token::RCB;
 "("                     return token::LRB;
 ")"                     return token::RRB;
 "["                     return token::LSB;
 "]"                     return token::RSB;
-"<"						return token::LAB;
+"="						          return token::EQ;
-">"						return token::RAB;
+"<"						          return token::LAB;
-":"						return token::COL;
+">"						          return token::RAB;
+":"						          return token::COL;
 ";"                     return token::SEMICOL;
+"."                     return token::DOT;
 ","                     return token::COMMA;
 "->"                    return token::RARR;
 "AND"                   return token::AND;
 "OR"                    return token::OR;
-"XOR"					return token::XOR;
+"XOR"					          return token::XOR;
 "IMPLIES"               return token::IMPLIES;
 "~"                     return token::NOT;
+"A"                     return token::A;
+"E"                     return token::E;
 "EX"                    return token::EX;
 "EU"                    return token::EU;
 "EF"                    return token::EF;
@@ -74,12 +79,18 @@ blank [ \t]
 "AU"                    return token::AU;
 "AF"                    return token::AF;
 "AG"                    return token::AG;
-"E"                     return token::E;
-"A"                     return token::A;
 "X"                     return token::X;
 "U"                     return token::U;
 "F"                     return token::F;
 "G"                     return token::G;
+"K"                     return token::UK;
+"C"                     return token::UC;
+"D"                     return token::UD;
+"UE"                    return token::UE;
+"NK"                    return token::NK;
+"NC"                    return token::NC;
+"ND"                    return token::ND;
+"NE"                    return token::NE;
 "empty"                 return token::EMPTY;
 "#".*                   ;
 
@@ -118,4 +129,3 @@ rsin_driver::scan_end()
 {
   fclose(yyin);
 }
-

rsin_parser.yy

@@ -6,7 +6,9 @@
 %code requires {
 #include <string>
 #include <set>
-#include "formrsctl.hh"
+#include "formrsctlk.hh"
+#include "rs.hh"
+// #include "stateconstr.hh"
 
 using std::set;
 using std::string;
@@ -33,38 +35,40 @@ class rsin_driver;
 {
     int ival;
     std::string *sval;
-    FormRSCTL *frsctl;
+    FormRSCTLK *frsctlk;
-    Entity_f *ent;
+    // Entity_f *ent;
-    Action_f *act;
+    // Action_f *act;
-    ActionsVec_f *actionsVec;
+    // ActionsVec_f *actionsVec;
-	BoolContexts *fboolctx;
+    StateConstr *fstc;
+    Agents_f *agents;
 };
 
 %code {
 #include "rsin_driver.hh"
 }
 
-%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS
+%token OPTIONS USE_CTX_AUT USE_CONCENTRATIONS MAKE_PROGRESSIVE
-%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLFORM
+%token REACTIONS INITIALCONTEXTS CONTEXTENTITIES RSCTLKFORM
 %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
-%token LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL COMMA RARR
+%token EQ LCB RCB LRB RRB LSB RSB LAB RAB COL SEMICOL DOT COMMA RARR
 %token AND OR XOR IMPLIES NOT
-%token EX EU EF EG AX AU AF AG E A X U F G EMPTY
+%token EX EU EF EG AX AU AF AG E A X U F G UK UC UD UE NK NC ND NE EMPTY
 
 %token        END      0 "end of file"
 %token <sval> IDENTIFIER "identifier"
 %token <ival> NUMBER     "number"
 
 %left AND OR XOR IMPLIES NOT
-%left EX EU EF EG AX AU AF AG E A X U F G
+%left EX EU EF EG AX AU AF AG E A X U F G UK UC UD UE NK NC ND NE
 
 //%right SRB
 
-%type <frsctl> rsctl_form
+%type <frsctlk> rsctlk_form
-%type <ent> f_entity
+// %type <ent> f_entity
-%type <act> action
+// %type <act> action
-%type <actionsVec> actions
+// %type <actionsVec> actions
-%type <fboolctx> bool_contexts
+%type <fstc> state_constr
+%type <agents> agents;
 
 //%printer    { yyoutput << *$$; } "identifier"
 %destructor { delete $$; } "identifier"
@@ -75,35 +79,54 @@ class rsin_driver;
 
 %start system;
 
-system: 
+system:
-	| OPTIONS LCB options RCB system
+	| OPTIONS LCB options RCB SEMICOL system
-    | REACTIONS LCB reactions RCB system
+  | REACTIONS LCB reactionsets RCB SEMICOL system
-    | INITIALCONTEXTS LCB initstates RCB system
+  | INITIALCONTEXTS LCB initstates RCB SEMICOL system
-    | CONTEXTENTITIES LCB actionentities RCB system
+  | CONTEXTENTITIES LCB actionentities RCB SEMICOL system
-	| CONTEXTAUTOMATON LCB ctxaut RCB system
+	| CONTEXTAUTOMATON LCB ctxaut RCB SEMICOL system
-    | RSCTLFORM LCB rsctl_form RCB system {
+  {
-        driver.addFormRSCTL($3);
+    driver.getReactionSystem()->ctxAutFinalise();
-    }
+  }
-    ;
+  | RSCTLKFORM LCB IDENTIFIER COL rsctlk_form RCB SEMICOL system {
+    driver.addFormRSCTLK(*$3, $5);
+    free($3);
+  }
+  ;
 
 options:
 	| options option SEMICOL
 	;
 
 option:
-	| USE_CTX_AUT { 
+	| USE_CTX_AUT {
-		driver.useContextAutomaton(); 
+		driver.useContextAutomaton();
 	}
 	| USE_CONCENTRATIONS {
 		driver.useConcentrations();
 	}
+  | MAKE_PROGRESSIVE {
+    driver.makeProgressive();
+  }
 	;
 
-/* 
+/*
  * -------------------------
- *         REACTIONS 
+ *         REACTIONS
  * -------------------------
  */
+
+reactionsets:
+	| reactionsets process_reactions
+	;
+
+process_reactions: processname LCB reactions RCB SEMICOL
+
+processname: IDENTIFIER {
+		driver.getReactionSystem()->setCurrentProcess(*$1);
+		free($1);
+	}
+
 reactions:
     | reactions reaction SEMICOL
     ;
@@ -131,7 +154,7 @@ reactant: IDENTIFIER {
 
 inhibitors:
     inhibitor
-    | inhibitors COMMA inhibitor 
+    | inhibitors COMMA inhibitor
     ;
 
 inhibitor:
@@ -165,7 +188,7 @@ initstates:
 
 initstate:
     | entity
-    | initstate COMMA entity 
+    | initstate COMMA entity
     ;
 
 entity: IDENTIFIER {
@@ -176,7 +199,7 @@ entity: IDENTIFIER {
 
 /*******************************************/
 
-actionentities: 
+actionentities:
     | actentity
     | actionentities COMMA actentity
     ;
@@ -186,13 +209,13 @@ actentity: IDENTIFIER {
         free($1);
     }
     ;
-	
+
 /*******************************************/
 
 ctxaut:
-	| STATES LCB autstates RCB ctxaut
+	| STATES LCB autstates RCB SEMICOL ctxaut
-	| INITSTATE LCB autinitstate RCB ctxaut
+	| INITSTATE LCB autinitstate RCB SEMICOL ctxaut
-	| TRANSITIONS LCB auttransitions RCB ctxaut
+	| TRANSITIONS LCB auttransitions RCB SEMICOL ctxaut
 	;
 
 autstate: IDENTIFIER {
@@ -211,24 +234,39 @@ autinitstate: IDENTIFIER {
 		free($1);
 	}
 	;
-	
+
 auttransitions:
 	| auttrans
 	| auttrans SEMICOL auttransitions
-	;	
+	;
 
-auttrans: LCB contextset RCB COL IDENTIFIER RARR IDENTIFIER {
+auttrans: LCB proc_ctxsets RCB COL IDENTIFIER RARR IDENTIFIER {
 		driver.getReactionSystem()->ctxAutAddTransition(*$5, *$7);
 		free($5);
 		free($7);
 	}
+    | LCB proc_ctxsets RCB COL IDENTIFIER RARR IDENTIFIER COL state_constr {
+        driver.getReactionSystem()->ctxAutAddTransition(*$5, *$7, $9);
+        free($5);
+        free($7);
+    }
 	;
-	
+
+proc_ctxsets:
+  | proc_ctxsets single_proc_ctxset
+  ;
+
+single_proc_ctxset: IDENTIFIER EQ LCB contextset RCB {
+  driver.getReactionSystem()->ctxAutSaveCurrentContextSet(*$1);
+		free($1);
+	}
+	;
+
 contextset:
-	ctxentity
+	| ctxentity
 	| contextset COMMA ctxentity
 	;
-		
+
 ctxentity: IDENTIFIER {
 		driver.getReactionSystem()->ctxAutPushNamedContextEntity(*$1);
 		free($1);
@@ -236,157 +274,199 @@ ctxentity: IDENTIFIER {
 	;
 
 /* formulae */
-	
+
-bool_contexts: IDENTIFIER {
+state_constr: IDENTIFIER DOT IDENTIFIER {
-        $$ = new BoolContexts(*$1);
+        $$ = new StateConstr(*$1, *$3);
         free($1);
+        free($3);
     }
-    | NOT bool_contexts {
+    | NOT state_constr {
-        $$ = new BoolContexts(BCTX_NOT, $2);
+        $$ = new StateConstr(STC_NOT, $2);
     }
-    | LRB bool_contexts RRB {
+    | LRB state_constr RRB {
         $$ = $2;
     }
-    | bool_contexts AND bool_contexts {
+    | state_constr AND state_constr {
-        $$ = new BoolContexts(BCTX_AND, $1, $3);
+        $$ = new StateConstr(STC_AND, $1, $3);
     }
-    | bool_contexts OR bool_contexts {
+    | state_constr OR state_constr {
-        $$ = new BoolContexts(BCTX_OR, $1, $3);
+        $$ = new StateConstr(STC_OR, $1, $3);
     }
-    | bool_contexts XOR bool_contexts {
+    | state_constr XOR state_constr {
-        $$ = new BoolContexts(BCTX_XOR, $1, $3);
+        $$ = new StateConstr(STC_XOR, $1, $3);
     }
 	;
 
-actions:
+// actions:
-    LCB action RCB {
+//     LCB action RCB {
-        $$ = new ActionsVec_f;
+//         $$ = new ActionsVec_f;
-        $$->push_back(*$2);
+//         $$->push_back(*$2);
-        free($2);
+//         free($2);
-    }
+//     }
-    | actions COMMA LCB action RCB {
+//     | actions COMMA LCB action RCB {
-        $$ = $1;
+//         $$ = $1;
-        $$->push_back(*$4);
+//         $$->push_back(*$4);
-        free($4);
+//         free($4);
-    }
+//     }
-    ;
+//     ;
 
-action:
+// action:
-    { 
+//     {
-        $$ = new Action_f;
+//         $$ = new Action_f;
-    } 
+//     }
-    | f_entity {
+//     | f_entity {
-        $$ = new Action_f;
+//         $$ = new Action_f;
-        $$->insert(*$1);
+//         $$->insert(*$1);
-        free($1);
+//         free($1);
+//     }
+//     | action COMMA f_entity {
+//         $$ = $1;
+//         $$->insert(*$3);
+//         free($3);
+//     }
+//     ;
+
+// f_entity: IDENTIFIER {
+//         $$ = new Entity_f(*$1);
+//         free($1);
+//     }
+//     ;
+
+agents:
+    IDENTIFIER {
+      Agents_f *ag = new Agents_f;
+      ag->insert(*$1);
+      free($1);
+      $$ = ag;
     }
-    | action COMMA f_entity {
+    | agents COMMA IDENTIFIER {
-        $$ = $1;        
+      $1->insert(*$3);
-        $$->insert(*$3);
+      free($3);
+      $$ = $1;
+    }
+
+rsctlk_form:
+    IDENTIFIER DOT IDENTIFIER {
+        $$ = new FormRSCTLK(*$1, *$3);
+        free($1);
         free($3);
     }
-    ;
+    | NOT rsctlk_form {
-
+        $$ = new FormRSCTLK(RSCTLK_NOT, $2);
-f_entity: IDENTIFIER {
-        $$ = new Entity_f(*$1);
-        free($1);
     }
-    ;
+    | LRB rsctlk_form RRB {
-
-rsctl_form: IDENTIFIER {
-        $$ = new FormRSCTL(*$1);
-        free($1);
-    }
-    | NOT rsctl_form {
-        $$ = new FormRSCTL(RSCTL_NOT, $2);
-    }
-    | LRB rsctl_form RRB {
         $$ = $2;
     }
-    | rsctl_form AND rsctl_form {
+    | rsctlk_form AND rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_AND, $1, $3);
+        $$ = new FormRSCTLK(RSCTLK_AND, $1, $3);
     }
-    | rsctl_form OR rsctl_form {
+    | rsctlk_form OR rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_OR, $1, $3);
+        $$ = new FormRSCTLK(RSCTLK_OR, $1, $3);
     }
-    | rsctl_form XOR rsctl_form {
+    | rsctlk_form XOR rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_XOR, $1, $3);
+        $$ = new FormRSCTLK(RSCTLK_XOR, $1, $3);
     }
-    | rsctl_form IMPLIES rsctl_form {
+    | rsctlk_form IMPLIES rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_IMPL, $1, $3);
+        $$ = new FormRSCTLK(RSCTLK_IMPL, $1, $3);
     }
-    | EX rsctl_form {
+    | EX rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_EX, $2);
+        $$ = new FormRSCTLK(RSCTLK_EX, $2);
     }
-    | EU LRB rsctl_form COMMA rsctl_form RRB {
+    | EU LRB rsctlk_form COMMA rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_EU, $3, $5);
+        $$ = new FormRSCTLK(RSCTLK_EU, $3, $5);
     }
-    | EF rsctl_form {
+    | EF rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_EF, $2);
+        $$ = new FormRSCTLK(RSCTLK_EF, $2);
     }
-    | EG rsctl_form {
+    | EG rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_EG, $2);
+        $$ = new FormRSCTLK(RSCTLK_EG, $2);
     }
-    | AX rsctl_form {
+    | AX rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_AX, $2);
+        $$ = new FormRSCTLK(RSCTLK_AX, $2);
     }
-    | AU LRB rsctl_form COMMA rsctl_form RRB {
+    | AU LRB rsctlk_form COMMA rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_AU, $3, $5);
+        $$ = new FormRSCTLK(RSCTLK_AU, $3, $5);
     }
-    | AF rsctl_form {
+    | AF rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_AF, $2);
+        $$ = new FormRSCTLK(RSCTLK_AF, $2);
     }
-    | AG rsctl_form {
+    | AG rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_AG, $2);
+        $$ = new FormRSCTLK(RSCTLK_AG, $2);
     }
-    | E LSB actions RSB X rsctl_form {
+    | UK LSB agents RSB LRB rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_UK, *$3, $6);
+        free($3);
     }
-    | E LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
+    | NK LSB agents RSB LRB rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
+        $$ = new FormRSCTLK(RSCTLK_NK, *$3, $6);
+        free($3);
     }
-    | E LSB actions RSB F rsctl_form {
+    | UE LSB agents RSB LRB rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_UE, *$3, $6);
+        free($3);
     }
-    | E LSB actions RSB G rsctl_form {
+    | NE LSB agents RSB LRB rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_NE, *$3, $6);
+        free($3);
     }
-    | A LSB actions RSB X rsctl_form {
+    | UC LSB agents RSB LRB rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_UC, *$3, $6);
+        free($3);
     }
-    | A LSB actions RSB U LRB rsctl_form COMMA rsctl_form RRB {
+    | NC LSB agents RSB LRB rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
+        $$ = new FormRSCTLK(RSCTLK_NC, *$3, $6);
+        free($3);
     }
-    | A LSB actions RSB F rsctl_form {
+
-        $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
+    // | E LSB actions RSB X rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
+    // }
+    // | E LSB actions RSB U LRB rsctlk_form COMMA rsctlk_form RRB {
+    //     $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
+    // }
+    // | E LSB actions RSB F rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
+    // }
+    // | E LSB actions RSB G rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
+    // }
+    // | A LSB actions RSB X rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
+    // }
+    // | A LSB actions RSB U LRB rsctlk_form COMMA rsctlk_form RRB {
+    //     $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
+    // }
+    // | A LSB actions RSB F rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
+    // }
+    // | A LSB actions RSB G rsctlk_form {
+    //     $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
+    // }
+
+	  /* contexts as boolean formulae  */
+    | E LAB state_constr RAB X rsctlk_form {
+        $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);
     }
-    | A LSB actions RSB G rsctl_form {
+    | E LAB state_constr RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_EU_ACT, $3, $7, $9);
     }
-	/* contexts as boolean formulae  */
+    | E LAB state_constr RAB F rsctlk_form {
-    | E LAB bool_contexts RAB X rsctl_form { 
+        $$ = new FormRSCTLK(RSCTLK_EF_ACT, $3, $6);
-        $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB U LRB rsctl_form COMMA rsctl_form RRB {
+    | E LAB state_constr RAB G rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_EU_ACT, $3, $7, $9);
+        $$ = new FormRSCTLK(RSCTLK_EG_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB F rsctl_form {
+    | A LAB state_constr RAB X rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_EF_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_AX_ACT, $3, $6);
     }
-    | E LAB bool_contexts RAB G rsctl_form {
+    | A LAB state_constr RAB U LRB rsctlk_form COMMA rsctlk_form RRB {
-        $$ = new FormRSCTL(RSCTL_EG_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_AU_ACT, $3, $7, $9);
     }
-    | A LAB bool_contexts RAB X rsctl_form {
+    | A LAB state_constr RAB F rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_AX_ACT, $3, $6);
+        $$ = new FormRSCTLK(RSCTLK_AF_ACT, $3, $6);
     }
-    | A LAB bool_contexts RAB U LRB rsctl_form COMMA rsctl_form RRB {
+    | A LAB state_constr RAB G rsctlk_form {
-        $$ = new FormRSCTL(RSCTL_AU_ACT, $3, $7, $9);
+        $$ = new FormRSCTLK(RSCTLK_AG_ACT, $3, $6);
-    }
-    | A LAB bool_contexts RAB F rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AF_ACT, $3, $6);
-    }
-    | A LAB bool_contexts RAB G rsctl_form {
-        $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
     }
     ;
 %%
@@ -396,4 +476,3 @@ yy::rsin_parser::error(const yy::rsin_parser::location_type &l, const std::strin
 {
     driver.error(l, m);
 }
-

stateconstr.cc

@@ -0,0 +1,118 @@
+/*
+    Copyright (c) 2018
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#include "stateconstr.hh"
+#include "types.hh"
+#include "cudd.hh"
+#include "bdd_macro.hh"
+#include "symrs.hh"
+
+std::string StateConstr::toStr(void) const
+{
+  if (oper == STC_PV) {
+    return proc_name + "." + entity_name;
+  }
+  else if (oper == STC_TF) {
+    if (tf) {
+      return "true";
+    }
+    else {
+      return "false";
+    }
+  }
+  else if (oper == STC_AND) {
+    return "(" + arg[0]->toStr() + " AND " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_OR) {
+    return "(" + arg[0]->toStr() + " OR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_XOR) {
+    return "(" + arg[0]->toStr() + " XOR " + arg[1]->toStr() + ")";
+  }
+  else if (oper == STC_NOT) {
+    return "~" + arg[0]->toStr();
+  }
+
+  else {
+    return "??";
+    assert(0);
+  }
+}
+
+BDD StateConstr::getBDDforState(const SymRS *srs) const
+{
+  return getBDD(srs, false);
+}
+
+BDD StateConstr::getBDDforContext(const SymRS *srs) const
+{
+  return getBDD(srs, true);
+}
+
+BDD StateConstr::getBDD(const SymRS *srs, bool encode_context) const
+{
+  if (oper == STC_PV) {
+    if (encode_context) {
+      return srs->encActStrEntity(proc_name, entity_name);
+    }
+    else {
+      return srs->encEntity(proc_name, entity_name);
+    }
+  }
+  else if (oper == STC_TF) {
+    if (tf) {
+      return srs->getBDDtrue();
+    }
+    else {
+      return srs->getBDDfalse();
+    }
+  }
+  else if (oper == STC_AND) {
+    return arg[0]->getBDD(srs, encode_context) * arg[1]->getBDD(srs, encode_context);
+  }
+  else if (oper == STC_OR) {
+    return arg[0]->getBDD(srs, encode_context) + arg[1]->getBDD(srs, encode_context);
+  }
+  else if (oper == STC_XOR) {
+    return arg[0]->getBDD(srs, encode_context) ^ arg[1]->getBDD(srs, encode_context);
+  }
+  else if (oper == STC_NOT) {
+    return !arg[0]->getBDD(srs, encode_context);
+  }
+  else {
+    assert(0);
+    FERROR("Undefined operator used in Boolean state/context definition. This should not happen.");
+    return srs->getBDDfalse();
+  }
+}
+
+bool StateConstr::isFalse(void) const
+{
+  if (oper == STC_TF && tf == false) {
+    return true;
+  }
+
+  if (oper == STC_NOT && arg[0]->isTrue()) {
+    return true;
+  }
+
+  return false;
+}
+
+bool StateConstr::isTrue(void) const
+{
+  if (oper == STC_TF && tf == true) {
+    return true;
+  }
+
+  if (oper == STC_NOT && arg[0]->isFalse()) {
+    return true;
+  }
+
+  return false;
+}

stateconstr.hh

@@ -0,0 +1,115 @@
+/*
+    Copyright (c) 2018
+    Artur Meski <meski@ipipan.waw.pl>
+
+    Reuse of the code or its part for any purpose
+    without the author's permission is strictly prohibited.
+*/
+
+#ifndef STATECONSTR_HH
+#define STATECONSTR_HH
+
+#include "types.hh"
+
+/* For state constraints: */
+#define STC_PV   80
+#define STC_AND  81
+#define STC_OR   82
+#define STC_XOR  83
+#define STC_NOT  84
+#define STC_TF   90
+
+#define STC_COND_1ARG(a) ((a) == STC_NOT)
+#define STC_COND_2ARG(a) ((a) == STC_AND || (a) == STC_OR || (a) == STC_XOR)
+#define STC_IS_VALID(a) (STC_COND_1ARG(a) || STC_COND_2ARG(a) || (a) == STC_PV || (a) == STC_TF)
+
+class SymRS;
+
+class StateConstr
+{
+    Oper oper;
+    StateConstr *arg[2];
+    std::string entity_name;
+    std::string proc_name;
+    bool tf;
+
+  public:
+
+    StateConstr(std::string procName, std::string varName)
+    {
+      oper = STC_PV;
+      entity_name = varName;
+      proc_name = procName;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for true/false.
+     *
+     * @param   val value of the logical constant
+     */
+    StateConstr(bool val)
+    {
+      oper = STC_TF;
+      tf = val;
+      arg[0] = nullptr;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for one-argument formula.
+     */
+    StateConstr(Oper op, StateConstr *form1)
+    {
+      assert(op == STC_NOT);
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+    }
+
+    /**
+     * @brief Constructor for two-argument formula.
+     */
+    StateConstr(Oper op, StateConstr *form1, StateConstr *form2)
+    {
+      assert(STC_COND_2ARG(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = form2;
+    }
+
+    ~StateConstr()
+    {
+      delete arg[0];
+      delete arg[1];
+    }
+
+    std::string toStr(void) const;
+
+    BDD getBDD(const SymRS *srs, bool encode_context) const;
+    BDD getBDDforContext(const SymRS *srs) const;
+    BDD getBDDforState(const SymRS *srs) const;
+
+    Oper getOper(void) const
+    {
+      assert(STC_IS_VALID(oper));
+      return oper;
+    }
+    StateConstr *getLeftSF(void) const
+    {
+      assert(arg[0] != nullptr);
+      return arg[0];
+    }
+    StateConstr *getRightSF(void) const
+    {
+      assert(STC_COND_2ARG(oper));
+      assert(arg[1] != nullptr);
+      return arg[1];
+    }
+
+    bool isFalse(void) const;
+    bool isTrue(void) const;
+};
+
+#endif

symrs.hh

@@ -13,11 +13,12 @@
 #include <algorithm>
 #include <map>
 #include <cassert>
+#include <iostream>
 #include "cudd.hh"
 #include "types.hh"
 #include "macro.hh"
 #include "bdd_macro.hh"
-#include "rs.hh"
+// #include "rs.hh"
 #include "options.hh"
 #include "memtime.hh"
 
@@ -27,79 +28,289 @@ using std::endl;
 using std::vector;
 using std::map;
 
+class RctSys;
+
 class SymRS
 {
     friend class ModelChecker;
-    friend class FormRSCTL;
+    friend class FormRSCTLK;
+
+  public:
+    SymRS(RctSys *rs, Options *opts);
+
+    BDDvec *getEncPV(void)
+    {
+      return pv;
+    }
+    BDDvec *getEncPVsucc(void)
+    {
+      return pv_succ;
+    }
+    BDD *getEncPV_E(void)
+    {
+      return pv_E;
+    }
+    BDD *getEncPVsucc_E(void)
+    {
+      return pv_succ_E;
+    }
+    BDD *getEncPVctx_E(void)
+    {
+      return pv_ctx_E;
+    }
+    BDD *getEncPVproc_enab_E(void)
+    {
+      return pv_proc_enab_E;
+    }
+    BDDvec *getEncPVdrs_E(void)
+    {
+      return pv_drs_E;
+    }
+    BDDvec *getEncPartTrans(void)
+    {
+      return partTrans;
+    }
+    BDD *getEncMonoTrans(void)
+    {
+      return monoTrans;
+    }
+    BDD *getEncInitStates(void)
+    {
+      return initStates;
+    }
+    Cudd *getCuddMgr(void)
+    {
+      return cuddMgr;
+    }
+    unsigned int getTotalStateVars(void)
+    {
+      return totalStateVars;
+    }
+    unsigned int getTotalRctSysStateVars(void)
+    {
+      return totalRctSysStateVars;
+    }
+    BDD encEntity(std::string proc_name, std::string entity_name) const;
+    BDD encActStrEntity(std::string proc_name, std::string entity_name) const;
+    BDD getBDDtrue(void) const
+    {
+      return BDD_TRUE;
+    }
+    BDD getBDDfalse(void) const
+    {
+      return BDD_FALSE;
+    }
+
+    /**
+     * @brief Checks if context automaton is used
+     *
+     * @return True if CA is used
+     */
+    bool usingContextAutomaton(void);
+
+    /**
+     * @brief Encodes a context automaton's state
+     *
+     * @return Returns the encoded state
+     */
+    BDD encCtxAutState_raw(State state_id, bool succ) const;
+
+    /**
+     * @brief Encodes a context automaton's state (as predecessor/non-primed)
+     *
+     * @return Returns the encoded state
+     */
+    BDD encCtxAutState(State state_id) const
+    {
+      return encCtxAutState_raw(state_id, false);
+    }
+
+    /**
+     * @brief Encodes a context automaton's state (as successor/primed)
+     *
+     * @return Returns the encoded state
+     */
+    BDD encCtxAutStateSucc(State state_id) const
+    {
+      return encCtxAutState_raw(state_id, true);
+    }
+
+    /**
+     * @brief Encodes the initial state of context automaton
+     *
+     * @return Returns the encoded state(s)
+     */
+    BDD getEncCtxAutInitState(void);
+
+    /**
+     * @brief Getter for context automaton's state variables (predecessor/non-primed)
+     *
+     * @return Returns a vector of BDDs
+     */
+    BDDvec *getEncCtxAutPV(void)
+    {
+      return pv_ca;
+    }
+
+    /**
+     * @brief Getter for context automaton's successor (primed) state variables
+     *
+     * @return Returns a vector of BDDs
+     */
+    BDDvec *getEncCtxAutPVsucc(void)
+    {
+      return pv_ca_succ;
+    }
+
+    /**
+     * @brief Getter for context automaton's quantification BDD (for non-primed vars)
+     *
+     * @return Returns a BDD for quantification
+     */
+    BDD *getEncCtxAutPV_E(void)
+    {
+      return pv_ca_E;
+    }
+
+    /**
+     * @brief Getter for context automaton's quantification BDD (for primed vars)
+     *
+     * @return Returns a BDD for quantification
+     */
+    BDD *getEncCtxAutPVsucc_E(void)
+    {
+      return pv_ca_succ_E;
+    }
+
+    /**
+     * @brief Encodes the monolithic transition relation
+     */
+    void encodeCtxAutTrans(void);
+
+    /**
+     * @brief Getter for context automaton's transition relation
+     *
+     * @return Returns a BDD encoding the transition relation
+     */
+    BDD *getEncCtxAutTrans(void)
+    {
+      return tr_ca;
+    }
+
+  private:
 
     RctSys *rs;
     Cudd *cuddMgr;
     Options *opts;
 
-	// Mapping: entity ID -> action/context entity ID
+    BDD *initStates;              /*!< BDD with initial states encoded */
-    StateEntityToAction stateToAct;
 
-    BDD *initStates;
+    BDDvec *pv;                   /*!< PVs for the global state (all the variables, flat) */
-	
+    BDDvec *pv_succ;
-    vector<BDD> *pv;
-    vector<BDD> *pv_succ;
     BDD *pv_E;
     BDD *pv_succ_E;
 
-    vector<BDD> *pv_rs;
+    BDDvec *pv_proc_enab;         /*!< Variables indicating if a process is enabled */
-    vector<BDD> *pv_rs_succ;
+    BDD *pv_proc_enab_E;
-    BDD *pv_rs_E;
-    BDD *pv_rs_succ_E;
 
-    vector<BDD> *partTrans;
+    vector<BDDvec> *pv_drs;       /*!< PVs for the product part of state
+                                       (per DRS process) */
+    vector<BDDvec> *pv_drs_succ;  /*!< PVs for the product (successor)
+                                       part of state (per DRS process) */
 
+    BDDvec *pv_drs_E;             /*!< Quantification BDDs for each process */
+
+    BDDvec *pv_drs_flat;          /*!< PVs for the DRS product part of state (flat) */
+    BDDvec *pv_drs_flat_succ;     /*!< PVs for the DRS product (successor) part of state (flat) */
+
+    BDD *pv_drs_flat_E;
+    BDD *pv_drs_flat_succ_E;
+
+    vector<DecompReactions> prod_conds; /*!< Production conditions (per process and per entity) */
+
+    BDDvec *partTrans;
     BDD *monoTrans;
 
-	// Context automaton
+    // Context automaton
-	vector<BDD> *pv_ca;
+    BDDvec *pv_ca;
-	vector<BDD> *pv_ca_succ;
+    BDDvec *pv_ca_succ;
-	BDD *pv_ca_E;
+    BDD *pv_ca_E;
-	BDD *pv_ca_succ_E;
+    BDD *pv_ca_succ_E;
-	BDD *tr_ca;
+    BDD *tr_ca;
 
-    vector<BDD> *pv_act;
+    BDDvec *pv_ctx;               /*!< Flat */
+    BDD *pv_ctx_E;
+    vector<BDDvec> *pv_proc_ctx;
+    BDDvec *pv_proc_ctx_E;
+
+    // TODO: remove
+    BDDvec *pv_act;
     BDD *pv_act_E;
 
+    unsigned int totalEntities;
+    unsigned int numberOfProc;         /*!< The number of DRS processes */
     unsigned int totalStateVars;
-    unsigned int totalReactions;
+    unsigned int totalRctSysStateVars; /*!< Total number of different entities produced by reactions */
-    unsigned int totalRctSysStateVars;
+    unsigned int totalCtxEntities;     /*!< Total number of different (process,context) entities used */
     unsigned int totalActions;
-	unsigned int totalCtxAutStateVars;
+    unsigned int totalCtxAutStateVars;
-	
-    BDD encEntity_raw(Entity entity, bool succ) const;
-    BDD encEntity(Entity entity) const {
-        return encEntity_raw(entity, false);
-    }
-    BDD encActEntity(Entity entity) const {
-		assert(entity < pv_act->size());
-        return (*pv_act)[entity];
-    }
-    BDD encEntitySucc(Entity entity) const {
-        return encEntity_raw(entity, true); 
-    }
-    BDD encEntitiesConj_raw(const Entities &entities, bool succ);
-    BDD encEntitiesConj(const Entities &entities) {
-        return encEntitiesConj_raw(entities, false);
-    }
-    BDD encEntitiesConjSucc(const Entities &entities) {
-        return encEntitiesConj_raw(entities, true);
-    }
-    BDD encEntitiesDisj_raw(const Entities &entities, bool succ);
-    BDD encEntitiesDisj(const Entities &entities) {
-        return encEntitiesDisj_raw(entities, false);
-    }
-    BDD encEntitiesDisjSucc(const Entities &entities) {
-        return encEntitiesDisj_raw(entities, true);
-    }
-    BDD encStateActEntitiesConj(const Entities &entities);
-    BDD encStateActEntitiesDisj(const Entities &entities);
 
-	BDD encActEntitiesConj(const Entities &entities);
+    EntitiesForProc usedProducts;     /*!< Entities used in products (per process) */
+    EntitiesForProc usedCtxEntities;  /*!< Entities used in context sets (per process) */
+
+    LocalIndicesForProcEntities prod_ent_local_idx; /*!< Local indices for each entity (per process): product entities */
+    LocalIndicesForProcEntities ctx_ent_local_idx;  /*!< Local indices for each entity (per process): context entities */
+
+    size_t getTotalProductVariables(void);
+    size_t getTotalCtxEntitiesVariables(void);
+
+    unsigned int getLocalProductEntityIndex(Process proc_id, Entity entity) const;
+    unsigned int getLocalCtxEntityIndex(Process proc_id, Entity entity) const;
+
+    BDD encEntity_raw(Process proc_id, Entity entity, bool succ) const;
+    BDD encEntity(Process proc_id, Entity entity) const
+    {
+      return encEntity_raw(proc_id, entity, false);
+    }
+    BDD encEntitySucc(Process proc_id, Entity entity) const
+    {
+      return encEntity_raw(proc_id, entity, true);
+    }
+
+    BDD encCtxEntity(Process proc_id, Entity entity) const;
+
+    bool productEntityExists(Process proc_id, Entity entity) const;
+    bool ctxEntityExists(Process proc_id, Entity entity) const;
+    bool processUsesEntity(Process proc_id, Entity entity_id) const;
+
+    BDD encProcEnabled(Process proc_id) const
+    {
+      return (*pv_proc_enab)[proc_id];
+    }
+
+    BDD encEntitiesConj_raw(Process proc_id, const Entities &entities, bool succ);
+    BDD encEntitiesConj(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesConj_raw(proc_id, entities, false);
+    }
+    BDD encEntitiesConjSucc(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesConj_raw(proc_id, entities, true);
+    }
+
+    BDD encEntitiesDisj_raw(Process proc_id, const Entities &entities, bool succ);
+    BDD encEntitiesDisj(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesDisj_raw(proc_id, entities, false);
+    }
+    BDD encEntitiesDisjSucc(Process proc_id, const Entities &entities)
+    {
+      return encEntitiesDisj_raw(proc_id, entities, true);
+    }
+
+    BDD encEntityCondition(Process proc_id, Entity entity_id);
+
+    BDD encContext(const EntitiesForProc &proc_entities);
 
     /**
      * @brief Complements an encoding of a given state by negating all the variables that are not set to true
@@ -113,122 +324,25 @@ class SymRS
     std::string decodedRctSysStateToStr(const BDD &state);
     void printDecodedRctSysStates(const BDD &states);
 
-	BDD encNoContext(void);
+    DecompReactions getProductionConditions(Process proc_id);
 
     void initBDDvars(void);
+
+    BDD encEnabledness(Process proc_id, Entity entity_id);
+    BDD encEntitySameSuccessor(Process proc_id, Entity entity_id);
+    BDD encEntityProduction(Process proc_id, Entity entity_id);
+
     void encodeTransitions(void);
-    void encodeTransitions_old(void);
     void encodeInitStates(void);
-	void encodeInitStatesForCtxAut(void);
+    void encodeInitStatesForCtxAut(void);
-	void encodeInitStatesNoCtxAut(void);
+    LocalIndicesForProcEntities buildLocalEntitiesMap(const EntitiesForProc &procEnt);
-    void mapStateToAct(void);
+    void mapProcEntities(void);
     void encode(void);
 
-    int getMappedStateToActID(int stateID) const 
+    size_t getCtxAutStateEncodingSize(void);
-	{ 
-		assert(stateID < static_cast<int>(totalRctSysStateVars)); 
-		return stateToAct[stateID]; 
-	}
 
-	size_t getCtxAutStateEncodingSize(void);
+    void reorder(void);
-	
-public:
-    SymRS(RctSys *rs, Options *opts);
-	
-    vector<BDD> *getEncPV(void) { return pv; }
-    vector<BDD> *getEncPVsucc(void) { return pv_succ; }
-    BDD *getEncPV_E(void) { return pv_E; }
-    BDD *getEncPVsucc_E(void) { return pv_succ_E; }
-    BDD *getEncPVact_E(void) { return pv_act_E; }
-    vector<BDD> *getEncPartTrans(void) { return partTrans; }
-    BDD *getEncMonoTrans(void) { return monoTrans; }
-    BDD getEncState(const Entities &entities);
-    BDD *getEncInitStates(void) { return initStates; }
-    Cudd *getCuddMgr(void) { return cuddMgr; }
-    unsigned int getTotalStateVars(void) { return totalStateVars; }
-    unsigned int getTotalRctSysStateVars(void) { return totalRctSysStateVars; }
-    BDD encEntity(std::string name) const {
-        return encEntity(rs->getEntityID(name));
-    }
-	
-    BDD encActStrEntity(std::string name) const;
-    BDD getBDDtrue(void) const { return BDD_TRUE; }
-    BDD getBDDfalse(void) const { return BDD_FALSE; }
-	
-    /**
-     * @brief Checks if context automaton is used
-     *
-     * @return True if CA is used
-     */
-	bool usingContextAutomaton(void) { return rs->ctx_aut != nullptr; }
-	
-    /**
-     * @brief Encodes a context automaton's state
-     *
-     * @return Returns the encoded state
-     */
-	BDD encCtxAutState_raw(State state_id, bool succ) const;
 
-	/**
-     * @brief Encodes a context automaton's state (as predecessor/non-primed)
-     *
-     * @return Returns the encoded state
-     */
-	BDD encCtxAutState(State state_id) const { return encCtxAutState_raw(state_id, false); }
-	
-    /**
-     * @brief Encodes a context automaton's state (as successor/primed)
-     *
-     * @return Returns the encoded state
-     */
-	BDD encCtxAutStateSucc(State state_id) const { return encCtxAutState_raw(state_id, true); }
-	
-    /**
-     * @brief Encodes the initial state of context automaton
-     *
-     * @return Returns the encoded state(s)
-     */
-	BDD getEncCtxAutInitState(void);
-	
-    /**
-     * @brief Getter for context automaton's state variables (predecessor/non-primed)
-     *
-     * @return Returns a vector of BDDs
-     */
-	vector<BDD> *getEncCtxAutPV(void) { return pv_ca; }
-
-    /**
-     * @brief Getter for context automaton's successor (primed) state variables
-     *
-     * @return Returns a vector of BDDs
-     */
-	vector<BDD> *getEncCtxAutPVsucc(void) { return pv_ca_succ; }
-
-    /**
-     * @brief Getter for context automaton's quantification BDD (for non-primed vars)
-     *
-     * @return Returns a BDD for quantification 
-     */
-	BDD *getEncCtxAutPV_E(void) { return pv_ca_E; }
-
-    /**
-     * @brief Getter for context automaton's quantification BDD (for primed vars)
-     *
-     * @return Returns a BDD for quantification 
-     */
-	BDD *getEncCtxAutPVsucc_E(void) { return pv_ca_succ_E; }
-
-    /**
-     * @brief Encodes the monolithic transition relation
-     */	
-	void encodeCtxAutTrans(void);
-	
-    /**
-     * @brief Getter for context automaton's transition relation
-     *
-     * @return Returns a BDD encoding the transition relation
-     */	
-	BDD *getEncCtxAutTrans(void) { return tr_ca; }	
 };
 
 #endif

types.hh

@@ -13,16 +13,29 @@
 #include <map>
 #include <vector>
 #include <string>
+#include "cudd.hh"
+
+typedef unsigned char Oper;
+
+typedef std::vector<BDD> BDDvec;
 
 typedef unsigned int Entity;
 typedef std::set<Entity> Entities;
 struct Reaction {
-    Entities rctt;
+  Entities rctt;
-    Entities inhib;
+  Entities inhib;
-    Entities prod;
+  Entities prod;
 };
+
+typedef unsigned int Process;
+typedef std::vector<std::string> ProcessesById;
+typedef std::map<std::string, Process> ProcessesByName;
+typedef std::set<Process> ProcSet;
+
 typedef std::vector<Reaction> Reactions;
-typedef std::vector<std::string> EntitiesByIds;
+typedef std::map<Process, Reactions> ReactionsForProc;
+
+typedef std::vector<std::string> EntitiesById;
 typedef std::map<std::string, Entity> EntitiesByName;
 typedef std::set<Entities> EntitiesSets;
 
@@ -30,19 +43,26 @@ typedef unsigned int State;
 typedef std::vector<std::string> StatesById;
 typedef std::map<std::string, State> StatesByName;
 
+typedef std::map<Process, Entities> EntitiesForProc;
+
+typedef std::map<Entity, unsigned int> EntiesToLocalIndex;
+typedef std::map<Process, EntiesToLocalIndex> LocalIndicesForProcEntities;
+
 struct ReactionCond {
-    Entities rctt;
+  Entities rctt;
-    Entities inhib;
+  Entities inhib;
 };
 
 typedef std::vector<ReactionCond> ReactionConds;
-typedef std::map<Entity,ReactionConds> DecompReactions;
+typedef std::map<Entity, ReactionConds> DecompReactions;
 typedef std::vector<int> StateEntityToAction;
 
+class StateConstr;
 struct CtxAutTransition {
-	State src_state;
+  State src_state;
-	Entities ctx;
+  EntitiesForProc ctx;
-	State dst_state;
+  StateConstr *state_constr;
+  State dst_state;
 };
 
 typedef std::vector<CtxAutTransition> CtxAutTransitions;