Support for NK

formrsctlk.cc

@@ -151,6 +151,12 @@ std::string FormRSCTLK::toStr(void) const
   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 "UK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
+  }
 
   else {
     return "??";

formrsctlk.hh

@@ -372,6 +372,15 @@ class FormRSCTLK
       }
     }
     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());
+    }
 };
 
 #endif

in/hsr_drs.rs

@@ -44,21 +44,21 @@ context-automaton {
 }
 
 # P1
-rsctl-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 mainA.hsf3:hse)) }
+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
-#rsctl-property { A[{stress},{nostress}]G(~(hse AND hsf3:hse) IMPLIES A[{stress},{nostress}]X(~(hse AND hsf3:hse))) }
+#rsctlk-property { A[{stress},{nostress}]G(~(hse AND hsf3:hse) IMPLIES A[{stress},{nostress}]X(~(hse AND hsf3:hse))) }
 
 # P3
-#rsctl-property { A[{stress},{nostress}]G(prot IMPLIES A[{stress},{nostress}]X(prot)) }
+#rsctlk-property { A[{stress},{nostress}]G(prot IMPLIES A[{stress},{nostress}]X(prot)) }
 
 # P4
-#rsctl-property { A[{stress},{nostress}]G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
-#rsctl-property { A< stress XOR nostress >G(mfp IMPLIES A[{stress},{nostress}]X(mfp OR hsp:mfp)) }
+#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
-#rsctl-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) ) )  }
+#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
-#rsctl-property { A[{nostress}]G(hsp:hsf IMPLIES A[{nostress}]X (hsp:hsf)) }
+#rsctlk-property { A[{nostress}]G(hsp:hsf IMPLIES A[{nostress}]X (hsp:hsf)) }
 

mc.cc

@@ -346,6 +346,10 @@ BDD ModelChecker::getStatesRSCTLK(const FormRSCTLK *form)
     return !statesEGctx(form->getActionsBDD(),
                         !getStatesRSCTLK(form->getLeftSF()) * *reach) * *reach;
   }
+  else if (oper == RSCTLK_NK) {
+    auto proc_id = srs->rs->getProcessID(form->getSingleAgent());
+    return statesNK(getStatesRSCTLK(form->getLeftSF()) * *reach, proc_id) * *reach;
+  }
 
   assert(0); // Should never happen
   return BDD_FALSE;
@@ -430,6 +434,16 @@ BDD ModelChecker::statesEFctx(const BDD *contexts, const BDD &states)
   return x;
 }
 
+BDD ModelChecker::statesNK(const BDD &states, Process proc_id)
+{
+  // bdd = new BDD((arg[0]->satStates(reach) * reach).ExistAbstract(bddOnlyIth(getAgent())) * reach);
+  BDD x = states;
+
+  x = x.ExistAbstract(getIthOnly(proc_id));
+
+  return x;
+}
+
 BDD ModelChecker::getIthOnly(Process proc_id)
 {
   /* if possible, we return the BDD from cache */

mc.hh

@@ -60,6 +60,7 @@ class ModelChecker
     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 getIthOnly(Process proc_id);
 

rsin_parser.ll

@@ -68,6 +68,8 @@ blank [ \t]
 "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;
@@ -83,7 +85,7 @@ blank [ \t]
 "K"                     return token::UK;
 "C"                     return token::UC;
 "D"                     return token::UD;
-"E"                     return token::UE;
+"UE"                    return token::UE;
 "NK"                    return token::NK;
 "NC"                    return token::NC;
 "ND"                    return token::ND;

rsin_parser.yy

@@ -370,6 +370,12 @@ rsctlk_form:
         $$ = new FormRSCTLK(RSCTLK_UK, agents, $6);
         free($3);
     }
+    | NK LSB IDENTIFIER RSB LRB rsctlk_form RRB {
+        Agents_f agents;
+        agents.insert(*$3);
+        $$ = new FormRSCTLK(RSCTLK_NK, agents, $6);
+        free($3);
+    }
 
     // | E LSB actions RSB X rsctlk_form {
     //     $$ = new FormRSCTLK(RSCTLK_EX_ACT, $3, $6);