From dec62f944a075de10fe8158381995fd62609543c Mon Sep 17 00:00:00 2001
From: Thomas Haas <tomy.haas@t-online.de>
Date: Thu, 12 Sep 2024 14:31:28 +0200
Subject: [PATCH] Updated CAT grammar to correctly parse LKMM. Commented out
 includes in LKMM because the included file contains unsupported features.

---
 cat/linux-kernel.cat             |  2 +-
 cat/lkmm/lkmm-v00.cat            |  2 +-
 cat/lkmm/lkmm-v01.cat            |  2 +-
 cat/lkmm/lkmm-v02.cat            |  2 +-
 dartagnan/src/main/antlr4/Cat.g4 | 14 ++++----------
 5 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/cat/linux-kernel.cat b/cat/linux-kernel.cat
index ee4da8b4eb..1a3de3e7b2 100644
--- a/cat/linux-kernel.cat
+++ b/cat/linux-kernel.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute matching pairs of nested Srcu-lock and Srcu-unlock *)
 let carry-srcu-data = (data ; [~ Srcu-unlock] ; rf)*
diff --git a/cat/lkmm/lkmm-v00.cat b/cat/lkmm/lkmm-v00.cat
index c954b1ba05..15873da47a 100644
--- a/cat/lkmm/lkmm-v00.cat
+++ b/cat/lkmm/lkmm-v00.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |
diff --git a/cat/lkmm/lkmm-v01.cat b/cat/lkmm/lkmm-v01.cat
index a4d9b983f5..193bae035a 100644
--- a/cat/lkmm/lkmm-v01.cat
+++ b/cat/lkmm/lkmm-v01.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |
diff --git a/cat/lkmm/lkmm-v02.cat b/cat/lkmm/lkmm-v02.cat
index e93320c77c..231317fa60 100644
--- a/cat/lkmm/lkmm-v02.cat
+++ b/cat/lkmm/lkmm-v02.cat
@@ -18,7 +18,7 @@
  * It can be replaced by include "cos.cat" for tests that do not use locks.
  *)
 
-include "lock.cat"
+//include "lock.cat"
 
 (* Compute marked and plain memory accesses *)
 let Marked = (~M) | IW | Once | Release | Acquire | (RMW & R) | (RMW & W) |
diff --git a/dartagnan/src/main/antlr4/Cat.g4 b/dartagnan/src/main/antlr4/Cat.g4
index 95949fe3f2..2c3562f076 100755
--- a/dartagnan/src/main/antlr4/Cat.g4
+++ b/dartagnan/src/main/antlr4/Cat.g4
@@ -5,12 +5,11 @@ import com.dat3m.dartagnan.wmm.axiom.*;
 }
 
 mcm
-    :   (NAME)? definition+ EOF
+    :   (NAME| QUOTED_STRING)? (definition | include)+ EOF
     ;
 
 definition
-    :   include
-    |   axiomDefinition
+    :   axiomDefinition
     |   letDefinition
     |   letRecDefinition
     ;
@@ -91,10 +90,10 @@ NEW         :   'new';
 
 FLAG       :   'flag';
 
-NAME    : [A-Za-z0-9\-_.]+;
-
 QUOTED_STRING : '"' .*? '"';
 
+NAME    : [A-Za-z0-9\-_.]+;
+
 LINE_COMMENT
     :   '//' ~[\n]*
         -> skip
@@ -109,8 +108,3 @@ WS
     :   [ \t\r\n]+
         -> skip
     ;
-
-MODELNAME
-    :   '"' .*? '"'
-        -> skip
-    ;