Expistemic operators, quantification

mc.cc

@@ -18,6 +18,7 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
   pv_succ_E = srs->getEncPVsucc_E();
   pv_ctx_E = srs->getEncPVctx_E();
   pv_proc_enab_E = srs->getEncPVproc_enab_E();
+  pv_drs_E = srs->getEncPVdrs_E();
 
   assert(pv != nullptr);
   assert(pv_succ != nullptr);
@@ -25,6 +26,7 @@ ModelChecker::ModelChecker(SymRS *srs, Options *opts)
   assert(pv_succ_E != nullptr);
   assert(pv_ctx_E != nullptr);
   assert(pv_proc_enab_E != nullptr);
+  assert(pv_drs_E != nullptr);
 
   //
   // Transition relations

mc.hh

@@ -26,6 +26,7 @@ class ModelChecker
     BDD *pv_E;
     BDD *pv_succ_E;
     BDD *pv_ctx_E;
+    BDDvec *pv_drs_E;
     BDD *reach;
     vector<BDD> *trp;
     BDD *trm;

rsin_parser.ll

@@ -82,6 +82,14 @@ blank [ \t]
 "U"                     return token::U;
 "F"                     return token::F;
 "G"                     return token::G;
+"UK"                    return token::UK;
+"UC"                    return token::UC;
+"UD"                    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;
 "#".*                   ;
 

rsin_parser.yy

@@ -49,14 +49,14 @@ class rsin_driver;
 %token CONTEXTAUTOMATON STATES INITSTATE TRANSITIONS
 %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
 

symrs.cc

@@ -166,6 +166,7 @@ void SymRS::initBDDvars(void)
       (*pv_drs)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
       (*pv_drs_succ)[proc_id][i] = cuddMgr->bddVar(bdd_var_idx++);
 
+      // Quantification (per proc)
       (*pv_drs_E)[proc_id] *= (*pv_drs)[proc_id][i];
 
       // The DRS part of the system (flattened): these vars do not include CA

symrs.hh

@@ -59,6 +59,10 @@ class SymRS
     {
       return pv_proc_enab_E;
     }
+    BDDvec *getEncPVdrs_E(void)
+    {
+      return pv_drs_E;
+    }
     BDDvec *getEncPartTrans(void)
     {
       return partTrans;
@@ -216,7 +220,7 @@ class SymRS
                                        (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) */