From f5e0beb5131aa6acb650cc3a2365e94eb26d9d9d Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 15 Apr 2018 20:00:05 +0100
Subject: [PATCH] Parsing of K

---
 formrsctl.hh   | 30 +++++++++++++++++++++++-------
 rsin_parser.ll | 10 ++++------
 rsin_parser.yy | 11 +++++++++--
 3 files changed, 36 insertions(+), 15 deletions(-)

diff --git a/formrsctl.hh b/formrsctl.hh
index 8f64c97..58b2feb 100644
--- a/formrsctl.hh
+++ b/formrsctl.hh
@@ -40,16 +40,19 @@
 #define RSCTL_AF_ACT  44
 #define RSCTL_TF      50 // true/false
 
+#define RSCTL_UK      60 // Epistemic operators
+#define RSCTL_NK      61
+
 /* 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 BCTX_PV   80
+#define BCTX_AND  81
+#define BCTX_OR   82
+#define BCTX_XOR  83
+#define BCTX_NOT  84
+#define BCTX_TF   90
 
 
-#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_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 || (a) == RSCTL_UK || (a) == RSCTL_NK)
 #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)
@@ -68,6 +71,7 @@ typedef unsigned char Oper;
 // 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 BoolContexts
 {
@@ -162,6 +166,7 @@ class FormRSCTL
     // ActionsVec_f *actions;
     BDD *actions_bdd;
     BoolContexts *boolCtx;
+    Agents_f agents;
   public:
     /**
      * @brief Constructor for propositional variable.
@@ -299,6 +304,17 @@ class FormRSCTL
       boolCtx = bctx;
     }
 
+    FormRSCTL(Oper op, Agents_f agents_set, FormRSCTL *form1)
+    {
+      assert(RSCTL_COND_1ARG(op));
+      oper = op;
+      arg[0] = form1;
+      arg[1] = nullptr;
+      bdd = nullptr;
+      actions_bdd = nullptr;
+      agents = agents_set;
+    }
+
     /**
      * @brief Destructor.
      */
diff --git a/rsin_parser.ll b/rsin_parser.ll
index 20dba91..1abe2fc 100644
--- a/rsin_parser.ll
+++ b/rsin_parser.ll
@@ -76,16 +76,14 @@ 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;
-"UK"                    return token::UK;
-"UC"                    return token::UC;
-"UD"                    return token::UD;
-"UE"                    return token::UE;
+"K"                     return token::UK;
+"C"                     return token::UC;
+"D"                     return token::UD;
+"E"                     return token::UE;
 "NK"                    return token::NK;
 "NC"                    return token::NC;
 "ND"                    return token::ND;
diff --git a/rsin_parser.yy b/rsin_parser.yy
index 0600a30..f308f65 100644
--- a/rsin_parser.yy
+++ b/rsin_parser.yy
@@ -316,7 +316,8 @@ bool_contexts: IDENTIFIER DOT IDENTIFIER {
 //     }
 //     ;
 
-rsctl_form: IDENTIFIER DOT IDENTIFIER {
+rsctl_form: 
+    IDENTIFIER DOT IDENTIFIER {
         $$ = new FormRSCTL(*$1, *$3);
         free($1);
         free($3);
@@ -362,6 +363,12 @@ rsctl_form: IDENTIFIER DOT IDENTIFIER {
     }
     | AG rsctl_form {
         $$ = new FormRSCTL(RSCTL_AG, $2);
+    } 
+    | UK LSB IDENTIFIER RSB LRB rsctl_form RRB {
+        Agents_f agents;
+        agents.insert(*$3);
+        $$ = new FormRSCTL(RSCTL_UK, agents, $6);
+        free($3);
     }
 
     // | E LSB actions RSB X rsctl_form {
@@ -389,7 +396,7 @@ rsctl_form: IDENTIFIER DOT IDENTIFIER {
     //     $$ = new FormRSCTL(RSCTL_AG_ACT, $3, $6);
     // }
 
-	/* contexts as boolean formulae  */
+	  /* contexts as boolean formulae  */
     | E LAB bool_contexts RAB X rsctl_form { 
         $$ = new FormRSCTL(RSCTL_EX_ACT, $3, $6);
     }