1 2/****************************************************************************** 3Simple parser for PSL/Sugar properties 4(based on examples/lexyacc in mosml distribution) 5******************************************************************************/ 6 7%{ 8open Data; 9 10(* Function definitions lifted from <holdir>/src/0/Lib.sml *) 11 12fun mem i = 13 let fun itr [] = false 14 | itr (a::rst) = i=a orelse itr rst 15 in itr end; 16 17fun insert i L = if mem i L then L else i::L 18 19fun union [] S = S 20 | union S [] = S 21 | union (a::rst) S2 = union rst (insert a S2) 22 23%} 24 25%token <int> Number 26%token <string> Name 27%token AT SEMICOLON LBRKTSTAR LBRKTSTARRBRKT LBRKTPLUSRBRKT LBRKTEQ LBRKTLEFTARROW 28%token COMMA COLON BAR BARBAR AMPERSAND AMPERSANDAMPERSAND LEFTARROW LEFTRIGHTARROW 29%token BARLEFTARROW BAREQLEFTARROW BAREQUAL EXCLAIM STAR 30%token LPAR RPAR LBRKT RBRKT LBRACE RBRACE 31%token BEFORE BEFOREX BEFOREXU BEFOREU 32%token WHILENOTXU EVENTUALLYX 33%token NEXTX NEXTA NEXTAX NEXTE NEXTEX NEXTEVENT NEXTEVENTX NEXTEVENTAX NEXTEVENTEX 34%token UNTILX UNTILXU UNTILU 35%token WHILENOTX WHILENOTXU WHILENOTU WITHINX WITHINXU WITHINU XX 36%token A AF AG AX ABORT ALWAYS 37%token BEFORE E EF EG EX FORALL G INF NEVER NEXT U X ABORT UNTIL W WHILENOT WITHIN 38%token EOF 39 40%left AT /* lowest precedence */ 41%left ABORT 42%left BAR BARBAR 43%left AMPERSAND AMPERSANDAMPERSAND 44%left COLON SEMICOLON 45%nonassoc STAR LEFTARROW BARLEFTARROW UNTIL EXCLAIM BAREQUAL 46 /* highest precedence */ 47 48%start MainBoolean 49%start MainSERE 50%start MainFL 51%start MainOBE 52%start MainState 53%start MainPath 54%start MainPathSERE 55%start MainPathFL 56 57%type <Data.bexp> Boolean MainBoolean 58%type <Data.sere> SERE MainSERE 59%type <Data.sere> Sequence Sequence_or_Boolean 60%type <Data.sere * Data.sere -> Data.sere> AndOrOp 61%type <int * (int option)> Count Range 62%type <int> LowBound 63%type <int option> HighBound 64%type <Data.fl> FL MainFL 65%type <Data.obe> OBE MainOBE 66%type <string list> State MainState 67%type <(string list)list> Path MainPath 68%type <(string list)list * Data.sere> PathSERE MainPathSERE 69%type <(string list)list * Data.fl> PathFL MainPathFL 70 71%% 72 73MainBoolean: 74 Boolean EOF { $1 } 75; 76 77MainSERE: 78 SERE EOF { $1 } 79; 80 81MainFL: 82 FL EOF { $1 } 83; 84 85MainOBE: 86 OBE EOF { $1 } 87; 88 89Boolean: 90 Name { B_PROP $1 } 91 | EXCLAIM Boolean { B_NOT $2 } 92 | LPAR Boolean RPAR { $2 } 93 | Boolean AMPERSANDAMPERSAND Boolean { B_AND($1, $3) } 94 | Boolean BARBAR Boolean { B_OR($1, $3) } 95 | Boolean LEFTARROW Boolean { B_IMP($1, $3) } 96 | Boolean LEFTRIGHTARROW Boolean { B_IFF($1, $3) } 97; 98 99SERE: 100 Boolean { S_BOOL $1 } 101 | Sequence { $1 } 102 | SERE AT Boolean { S_CLOCK($1,$3) } 103 | SERE SEMICOLON SERE { S_CAT($1, $3) } 104 | Sequence COLON Sequence { S_FUSION($1, $3) } 105 | Sequence AndOrOp Sequence { $2($1,$3) } 106 | SERE LBRKTSTARRBRKT { S_REPEAT $1 } 107 | SERE LBRKTSTAR Count RBRKT { S_RANGE_REPEAT($1,$3) } 108 | LBRKTSTARRBRKT { S_REPEAT(S_BOOL B_TRUE) } 109 | LBRKTSTAR Count RBRKT { S_RANGE_REPEAT(S_BOOL B_TRUE,$2) } 110 | SERE LBRKTPLUSRBRKT { S_NON_ZERO_REPEAT $1} 111 | LBRKTPLUSRBRKT { S_NON_ZERO_REPEAT(S_BOOL B_TRUE)} 112 | Boolean LBRKTEQ Count RBRKT { S_RANGE_EQ_REPEAT($1,$3) } 113 | Boolean LBRKTLEFTARROW RBRKT { S_RANGE_GOTO_REPEAT($1, (1,NONE)) } 114 | Boolean LBRKTLEFTARROW Count RBRKT { S_RANGE_GOTO_REPEAT($1,$3) } 115; 116 117Sequence: 118 LBRACE SERE RBRACE { $2 } 119; 120 121AndOrOp: 122 AMPERSAND { S_FLEX_AND } 123 | AMPERSANDAMPERSAND { S_AND } 124 | BAR { S_OR } 125; 126 127Count: 128 Number { ($1,NONE) } 129 | Range { $1 } 130; 131 132Range: 133 LowBound COLON HighBound { ($1,$3) } 134; 135 136LowBound: 137 Number { $1 } 138; 139 140HighBound: 141 Number { SOME $1 } 142 | INF { NONE } 143; 144 145Sequence_or_Boolean: 146 Sequence { $1 } 147 | Boolean { S_BOOL $1 } 148 149FL: 150 Name { F_BOOL(B_PROP $1) } 151 | LPAR FL RPAR { $2 } 152 | FL AT Boolean EXCLAIM { F_STRONG_CLOCK($1,$3) } 153 | FL AT Boolean { F_WEAK_CLOCK($1,$3) } 154 | FL ABORT Boolean { F_ABORT($1,$3) } 155 | EXCLAIM FL { F_NOT $2 } 156 | FL AMPERSANDAMPERSAND FL { F_AND($1, $3) } 157 | FL BARBAR FL { F_OR($1, $3) } 158 | FL LEFTARROW FL { F_IMP($1, $3) } 159 | FL LEFTRIGHTARROW FL { F_IFF($1, $3) } 160 | X FL { F_WEAK_X $2 } 161 | XX FL { F_STRONG_X $2 } 162 | F FL { F_F $2 } 163 | G FL { F_G $2 } 164 | LBRKT FL U FL RBRKT { F_U($2,$4) } 165 | LBRKT FL W FL RBRKT { F_W($2,$4) } 166 | ALWAYS FL { F_ALWAYS $2 } 167 | NEVER FL { F_NEVER $2 } 168 | NEXT FL { F_WEAK_NEXT $2 } 169 | NEXTX FL { F_STRONG_NEXT $2 } 170 | EVENTUALLYX FL { F_STRONG_EVENTUALLY $2 } 171 | FL UNTILX FL { F_STRONG_UNTIL($1,$3) } 172 | FL UNTIL FL { F_WEAK_UNTIL($1,$3) } 173 | FL UNTILXU FL { F_STRONG_UNTIL_INC($1,$3) } 174 | FL UNTILU FL { F_WEAK_UNTIL_INC($1,$3) } 175 | FL BEFOREX FL { F_STRONG_BEFORE($1,$3) } 176 | FL BEFORE FL { F_WEAK_BEFORE($1,$3) } 177 | FL BEFOREXU FL { F_STRONG_BEFORE_INC($1,$3) } 178 | FL BEFOREU FL { F_WEAK_BEFORE_INC($1,$3) } 179 | X LBRKT Number RBRKT LPAR FL RPAR { F_NUM_WEAK_X($3,$6) } 180 | XX LBRKT Number RBRKT LPAR FL RPAR { F_NUM_STRONG_X($3,$6) } 181 | NEXT LBRKT Number RBRKT LPAR FL RPAR{ F_NUM_WEAK_NEXT($3,$6) } 182 | NEXTX LBRKT Number RBRKT LPAR FL RPAR 183 { F_NUM_STRONG_NEXT($3,$6) } 184 | NEXTA LBRKT Range RBRKT LPAR FL RPAR 185 { F_NUM_WEAK_NEXT_A($3,$6) } 186 | NEXTAX LBRKT Range RBRKT LPAR FL RPAR 187 { F_NUM_STRONG_NEXT_A($3,$6) } 188 | NEXTE LBRKT Range RBRKT LPAR FL RPAR 189 { F_NUM_WEAK_NEXT_E($3,$6) } 190 | NEXTEX LBRKT Range RBRKT LPAR FL RPAR 191 { F_NUM_STRONG_NEXT_E($3,$6) } 192 | NEXTEVENTX LPAR Boolean RPAR LPAR FL RPAR 193 { F_STRONG_NEXT_EVENT($3,$6) } 194 | NEXTEVENT LPAR Boolean RPAR LPAR FL RPAR 195 { F_WEAK_NEXT_EVENT($3,$6) } 196 | NEXTEVENTX LPAR Boolean RPAR LBRKT Number RBRKT LPAR FL RPAR 197 { F_NUM_STRONG_NEXT_EVENT($3,$6,$9) } 198 | NEXTEVENT LPAR Boolean RPAR LBRKT Number RBRKT LPAR FL RPAR 199 { F_NUM_WEAK_NEXT_EVENT($3,$6,$9) } 200 201 | NEXTEVENTAX LPAR Boolean RPAR LBRKT Range RBRKT LPAR FL RPAR 202 { F_NUM_STRONG_NEXT_EVENT_A($3,$6,$9) } 203 | NEXTEVENTA LPAR Boolean RPAR LBRKT Range RBRKT LPAR FL RPAR 204 { F_NUM_WEAK_NEXT_EVENT_A($3,$6,$9) } 205 206 | Sequence LPAR FL RPAR { F_SUFFIX_IMP($1,$3) } 207 | Sequence BARLEFTARROW Sequence EXCLAIM 208 { F_STRONG_IMP($1,$3) } 209 | Sequence BARLEFTARROW Sequence { F_WEAK_IMP($1,$3) } 210 | Sequence BAREQLEFTARROW Sequence EXCLAIM 211 { F_SKIP_STRONG_IMP($1,$3) } 212 | Sequence BAREQLEFTARROW Sequence { F_SKIP_WEAK_IMP($1,$3) } 213 | ALWAYS Sequence { F_SERE_ALWAYS $2 } 214 | NEVER Sequence { F_SERE_NEVER $2 } 215 | EVENTUALLYX Sequence { F_SERE_STRONG_EVENTUALLY $2 } 216 | WITHINX LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence 217 {F_STRONG_WITHIN($3,$5,$7) } 218 | WITHIN LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence 219 {F_WEAK_WITHIN($3,$5,$7) } 220 | WITHINXU LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence 221 {F_STRONG_WITHIN_INC($3,$5,$7) } 222 | WITHINU LPAR Sequence_or_Boolean COMMA Boolean RPAR Sequence 223 {F_WEAK_WITHIN_INC($3,$5,$7) } 224 | WHILENOTX LPAR Boolean RPAR Sequence 225 {F_STRONG_WHILENOT($3,$5) } 226 | WHILENOT LPAR Boolean RPAR Sequence 227 {F_WEAK_WHILENOT($3,$5) } 228 | WHILENOTXU LPAR Boolean RPAR Sequence 229 {F_STRONG_WHILENOT_INC($3,$5) } 230 | WHILENOTU LPAR Boolean RPAR Sequence 231 {F_WEAK_WHILENOT_INC($3,$5) } 232 233; 234 235OBE: 236 Boolean { O_BOOL $1 } 237 | LPAR OBE RPAR { $2 } 238 | EXCLAIM OBE { O_NOT $2 } 239 | OBE AMPERSAND OBE { O_AND($1, $3) } 240 | EX OBE { O_EX $2 } 241 | E LBRKT OBE UNTIL OBE RBRKT { O_EU($3,$5) } 242 | EG OBE { O_EG $2 } 243; 244 245MainState: 246 State EOF { $1 } 247; 248 249State: 250 /* empty */ { [] } 251 | Name { [$1] } 252 | Name COMMA State { insert $1 $3 } 253; 254 255MainPath: 256 Path EOF { $1 } 257; 258 259Path: 260 /* empty */ { [] } 261 | LBRACE State RBRACE { [$2] } 262 | LBRACE State RBRACE Path { $2 :: $4 } 263; 264 265MainPathSERE: 266 PathSERE EOF { $1 } 267; 268 269PathSERE: 270 Path BAREQUAL SERE { ($1,$3) } 271; 272 273MainPathFL: 274 PathFL EOF { $1 } 275; 276 277PathFL: 278 Path BAREQUAL FL { ($1,$3) } 279; 280