blob: 1b3272249c88f5483ea0760c5cb0cac90785bc3e (
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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
parser grammar PropertyParser;
options { tokenVocab = PropertyLexer; }
prog: tag_existing;
tag_existing
: TAG_EXISTING_KW L_PAREN (tag_item)+ R_PAREN (WS)* sl_formula (WS)* R_PAREN
;
tag_item
: (WS)* L_PAREN (WS)* ID (WS)+ ID (WS)+ ID (WS)* R_PAREN (WS)*
;
predicate: (WS)* L_PAREN ID ((WS)+ ID)* (WS)* R_PAREN;
/******************************************************************************/
/** Structural Level **********************************************************/
/******************************************************************************/
/**** First Order Expressions *************************************************/
sl_and_operator: (WS)* AND_OPERATOR_KW sl_formula (sl_formula)+ (WS)* R_PAREN;
sl_or_operator: (WS)* OR_OPERATOR_KW sl_formula (sl_formula)+ (WS)* R_PAREN;
sl_not_operator: (WS)* NOT_OPERATOR_KW sl_formula (WS)* R_PAREN;
sl_implies_operator: (WS)* IMPLIES_OPERATOR_KW sl_formula sl_formula (WS)* R_PAREN;
/** Quantified Expressions ****************************************************/
sl_exists_operator:
(WS)* EXISTS_OPERATOR_KW ID (WS)+ ID sl_formula (WS*) R_PAREN
;
sl_forall_operator:
(WS)* FORALL_OPERATOR_KW ID (WS)+ ID sl_formula (WS*) R_PAREN
;
/** Special Expressions *******************************************************/
sl_ctl_verifies_operator:
(WS)* CTL_VERIFIES_OPERATOR_KW ID (WS)* bl_formula (WS)* R_PAREN
;
/**** Formula Definition ******************************************************/
sl_formula:
predicate
| sl_and_operator
| sl_or_operator
| sl_not_operator
| sl_implies_operator
| sl_exists_operator
| sl_forall_operator
| sl_ctl_verifies_operator
;
/******************************************************************************/
/** Behavioral Level **********************************************************/
/******************************************************************************/
/**** First Order Expressions *************************************************/
bl_and_operator: (WS)* AND_OPERATOR_KW bl_formula (bl_formula)+ (WS)* R_PAREN;
bl_or_operator: (WS)* OR_OPERATOR_KW bl_formula (bl_formula)+ (WS)* R_PAREN;
bl_not_operator: (WS)* NOT_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_implies_operator: (WS)* IMPLIES_OPERATOR_KW bl_formula bl_formula (WS)* R_PAREN;
/**** Computation Tree Logic Expressions **************************************/
bl_ax_operator: (WS)* AX_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_ex_operator: (WS)* EX_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_ag_operator: (WS)* AG_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_eg_operator: (WS)* EG_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_af_operator: (WS)* AF_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_ef_operator: (WS)* EF_OPERATOR_KW bl_formula (WS)* R_PAREN;
bl_au_operator: (WS)* AU_OPERATOR_KW bl_formula bl_formula (WS)* R_PAREN;
bl_eu_operator: (WS)* EU_OPERATOR_KW bl_formula bl_formula (WS)* R_PAREN;
/**** Formula Definition ******************************************************/
bl_formula:
predicate
| bl_and_operator
| bl_or_operator
| bl_not_operator
| bl_implies_operator
| bl_ax_operator
| bl_ex_operator
| bl_ag_operator
| bl_eg_operator
| bl_af_operator
| bl_ef_operator
| bl_au_operator
| bl_eu_operator
;
|
