This dataset groups together entries from the Alloy4Fun dataset according to their semantic and syntactic equivalence. Each entry is a student attempt to formalize a requirement (i.e., a challenge). Each challenge is a command that tests the equivalence of a student predicate against a hidden oracle. This grouping reduces ~51.000 entries into ~7.000 semantically distinct specifications (and ~17.000 syntactically distinct). Semantic equivalence is tested with the Alloy Analyzer (with a default scope of 3 for top-level signatures). Syntactic equivalence is tested after a simple normalization (variable anonymization and operator commutativity). Each file original_cmd.json contains the information regarding a challenge represented by command labeled cmd of an Alloy4Fun exercise whose model has id original, namely: original: the ID of the original model in the Alloy4Fun database cmd: the challenge command label pred: the challenge predicate label entry_count: the total number of entries for the challenge semantic_count: the number of semantically distinct entries syntactic_count: the number of syntactically distinct entries scope: the scope used to test equivalence groups: the actual semantic groups, containing: entry_count: the total number of entries in the semantic group syntactic_count: the number of syntactically distinct entries correct: whether a correct solution to the challenge elems: the actual syntactic groups, containing: entry_count: the total number of entries in the syntactic group code: a representative code submission The following Alloy4Fun exercises where considered: Name Permalink Challenge Entries Semantic groups Syntactic groups Social network x3JXgWhJ3uti5Dzxz inv1 3054 119 377 Social network x3JXgWhJ3uti5Dzxz inv2 1599 45 171 Social network x3JXgWhJ3uti5Dzxz inv3 3936 858 1797 Social network x3JXgWhJ3uti5Dzxz inv4 1957 150 583 Social network x3JXgWhJ3uti5Dzxz inv5 2544 168 524 Social network x3JXgWhJ3uti5Dzxz inv6 1223 71 306 Social network x3JXgWhJ3uti5Dzxz inv7 3138 528 1281 Social network x3JXgWhJ3uti5Dzxz inv8 1254 268 528 Courses iP5JL36afv5KbDKP6 inv1 1903 163 482 Courses iP5JL36afv5KbDKP6 inv2 791 35 105 Courses iP5JL36afv5KbDKP6 inv3 1075 86 222 Courses iP5JL36afv5KbDKP6 inv4 1167 88 258 Courses iP5JL36afv5KbDKP6 inv5 1883 253 721 Courses iP5JL36afv5KbDKP6 inv6 1150 177 404 Courses iP5JL36afv5KbDKP6 inv7 1163 187 407 Courses iP5JL36afv5KbDKP6 inv8 928 85 235 Courses iP5JL36afv5KbDKP6 inv9 1941 324 1032 Courses iP5JL36afv5KbDKP6 inv10 882 82 292 Courses iP5JL36afv5KbDKP6 inv11 790 91 279 Courses iP5JL36afv5KbDKP6 inv12 751 92 222 Courses iP5JL36afv5KbDKP6 inv13 934 302 458 Courses iP5JL36afv5KbDKP6 inv14 577 54 205 Courses iP5JL36afv5KbDKP6 inv15 466 133 247 Production line dyj49tEp7j6aWAQQX inv1 792 45 122 Production line dyj49tEp7j6aWAQQX inv2 1330 94 514 Production line dyj49tEp7j6aWAQQX inv3 539 29 78 Production line dyj49tEp7j6aWAQQX inv4 769 80 244 Production line dyj49tEp7j6aWAQQX inv5 856 128 372 Production line dyj49tEp7j6aWAQQX inv6 1056 61 203 Production line dyj49tEp7j6aWAQQX inv7 908 113 219 Production line dyj49tEp7j6aWAQQX inv8 601 108 250 Production line dyj49tEp7j6aWAQQX inv9 2148 588 1555 Production line dyj49tEp7j6aWAQQX inv10 834 288 472 Train Station cXPP9QBPTYgTX6WJ6 inv1 792 127 245 Train Station cXPP9QBPTYgTX6WJ6 inv2 606 56 153 Train Station cXPP9QBPTYgTX6WJ6 inv3 1473 145 384 Train Station cXPP9QBPTYgTX6WJ6 inv4 685 111 272 Train Station cXPP9QBPTYgTX6WJ6 inv5 836 166 392 Train Station cXPP9QBPTYgTX6WJ6 inv6 461 70 133 Train Station cXPP9QBPTYgTX6WJ6 inv7 337 38 78 Train Station cXPP9QBPTYgTX6WJ6 inv8 508 53 120 Train Station cXPP9QBPTYgTX6WJ6 inv9 768 206 357 Train Station cXPP9QBPTYgTX6WJ6 inv10 425 90 156