summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-18 10:24:37 +0200
committerNathanael Sensfelder <SpamShield0@MultiAgentSystems.org>2017-07-18 10:24:37 +0200
commitbe20292006bd783b4589b69b5379aae9429f3b3b (patch)
tree0c22bd2fd60b7bd4837252e93771d11a1cc6018c /instr-to-kodkod/parser/PropertyLexer.g4
parent31e1948a7f3bf1f7902cd5a0d6d49cef277e73ae (diff)
First shot at a grammar for the properties.
Diffstat (limited to 'instr-to-kodkod/parser/PropertyLexer.g4')
-rw-r--r--instr-to-kodkod/parser/PropertyLexer.g434
1 files changed, 26 insertions, 8 deletions
diff --git a/instr-to-kodkod/parser/PropertyLexer.g4 b/instr-to-kodkod/parser/PropertyLexer.g4
index 27f1bca..159dec1 100644
--- a/instr-to-kodkod/parser/PropertyLexer.g4
+++ b/instr-to-kodkod/parser/PropertyLexer.g4
@@ -1,13 +1,31 @@
lexer grammar PropertyLexer;
-TAG_EXISTING_KW: '(tag_existing';
-AND_OPERATOR_KW: '(and';
-OR_OPERATOR_KW: '(or';
-NOT_OPERATOR_KW: '(not';
-EXISTS_OPERATOR_KW: '(exists';
-FORALL_OPERATOR_KW: '(forall';
-ID: [a-zA-Z0-9_]+;
+fragment SEP: [ \t\r\n]+;
+
L_PAREN : '(';
R_PAREN : ')';
-WS: [ \t\r\n]+ -> skip;
+TAG_EXISTING_KW: '(tag_existing' SEP;
+
+AND_OPERATOR_KW: '(and' SEP;
+OR_OPERATOR_KW: '(or' SEP;
+NOT_OPERATOR_KW: '(not' SEP ;
+IMPLIES_OPERATOR_KW: '(implies' SEP ;
+
+EXISTS_OPERATOR_KW: '(exists' SEP;
+FORALL_OPERATOR_KW: '(forall' SEP;
+
+CTL_VERIFIES_OPERATOR_KW: '(CTL_verifies' SEP;
+
+AX_OPERATOR_KW: '(AX' SEP;
+EX_OPERATOR_KW: '(EX' SEP;
+AG_OPERATOR_KW: '(AG' SEP;
+EG_OPERATOR_KW: '(EG' SEP;
+AF_OPERATOR_KW: '(AF' SEP;
+EF_OPERATOR_KW: '(EF' SEP;
+AU_OPERATOR_KW: '(AU' SEP;
+EU_OPERATOR_KW: '(EU' SEP;
+
+WS: SEP;
+
+ID: [a-zA-Z0-9_]+;