1 /* spec-compiler.jj Grammer definition for the specification */
6 Each construct should be embraced by /DOUBLE_STAR ... STAR/ annotation.
7 Within there, any line beginning with a "#" is a comment of the annotation.
8 Each constrcut should begin with @Begin and end with @End. Otherwise, the
9 annotation would be considered as normal comments of the source.
21 b) Interface construct
26 @Condition: ... (Optional)
27 @ID: ... (Optional, use default ID)
32 @Post_action: (Optional)
33 @Post_check: (Optional)
36 c) Potential commit construct
38 @Potential_commit_point_define: ...
42 d) Commit point define construct
44 @Commit_point_define_check: ...
51 @Commit_point_define: ...
52 @Potential_commit_point_label: ...
61 JAVA_UNICODE_ESCAPE = true;
64 PARSER_BEGIN(SpecParser)
65 package edu.uci.eecs.specCompiler.grammerParser;
68 public static void main(String[] argvs)
69 throws ParseException, TokenMgrError {
70 SpecParser parser = new SpecParser(System.in);
72 System.out.println("Parsing finished!");
75 PARSER_END(SpecParser)
87 // "#" comment for the specification
88 <"#" (~["\n", "\r"])* (["\n", "\r"])>
90 // "//" comment for the specification
91 <"//" (~["\n", "\r"])* (["\n", "\r"])>
104 <GLOBAL_DEFINE: "@Global_define:">
106 <INTERFACE_CLUSTER: "@Interface_cluster:">
108 <HAPPENS_BEFORE: "@Happens_before:">
110 <INTERFACE: "@Interface:">
112 <COMMIT_POINT_SET: "@Commit_point_set:">
114 <CONDITION: "@Condition:">
116 <HB_CONDITIONS: "@HB_condition:">
124 <POST_ACTION: "@Post_action:">
126 <POST_CHECK: "@Post_check:">
128 <POTENTIAL_COMMIT_POINT_DEFINE: "@Potential_commit_point_define:">
132 <COMMIT_POINT_DEFINE_CHECK: "@Commit_point_define_check:">
134 <COMMIT_POINT_DEFINE: "@Commit_point_define:">
136 <POTENTIAL_COMMIT_POINT_LABEL: "@Potential_commit_point_label:">
140 <#NONZERO_DIGIT: ["1"-"9"]>
142 <#LETTER: ["a"-"z", "A"-"Z"]>
144 <#NUM: <NONZERO_DIGIT> <DIGIT>>
146 <IDENTIFIER: <LETTER> (<LETTER> | <DIGIT> | "_")>
152 Global_construct() <EOF>
155 void Global_construct() :
160 Global_define() (Interface_cluster())? (Happens_before())?
171 void Global_define() :
174 <GLOBAL_DEFINE> C_CPP_CODE()
177 void Conditional_interface() :
180 <IDENTIFIER> (<"(" <IDENTIFIER> ")"> | "")
183 void Interface_cluster() :
186 <IDENTIFIER> "=" "{" Conditional_interface() (",," Conditional_interface())* "}"
189 void Interface_clusters() :
192 <INTERFACE_CLUSTER> (Interface_cluster())+
195 void Happens_before() :
198 <HAPPENS_BEFORE> (Conditional_interface() "->" Conditional_interface())+
206 <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")" "->" <IDENTIFIER>
211 void Potential_commit_point_define() :
216 <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")" "->" <IDENTIFIER>
222 void Commit_point_define() :
227 <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")" "->" <IDENTIFIER>
233 void Commit_point_define_check() :
238 <HAPPENS_BEFORE> <IDENTIFIER> "(" <IDENTIFIER> ")" "->" <IDENTIFIER>