summaryrefslogtreecommitdiff
blob: 3b6011d5a48ca5b2a438de82f06f6d4d700fa8e7 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
lexer grammar PropertyLexer;

fragment SEP: [ \t\r\n]+;

L_PAREN: '(';
R_PAREN: ')';
L_BRAKT: '[';
R_BRAKT: ']';

TAG_EXISTING_KW: '(tag_existing' SEP;

IFF_OPERATOR_KW: '(iff' SEP;
AND_OPERATOR_KW: '(and' SEP;
OR_OPERATOR_KW: '(or' SEP;
NOT_OPERATOR_KW: '(not' SEP ;
IMPLIES_OPERATOR_KW: '(implies' SEP;

EQ_SPECIAL_PREDICATE_KW: '(eq' SEP;
REGEX_SPECIAL_PREDICATE_KW: '(string_matches' 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;

DEPTH_NO_PARENT_OPERATOR_KW: ('(NPB' | '(does_not_reach_parent_before') SEP;
DEPTH_NO_CHANGE_OPERATOR_KW: ('(NDCB' | '(does_not_change_depth_before') SEP;

WS: SEP;

ID: [a-zA-Z0-9_]+;
STRING: '"' ~('\r' | '\n' | '"')* '"';

COMMENT: ';;' .*? '\n' -> channel(HIDDEN);