Alloy4Fun Semantic Entries

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本数据集将Alloy4Fun数据集（Alloy4Fun）中的条目按照语义等价与句法等价进行分组。每一条条目均为学生针对一项需求形式化建模任务（即挑战题）的尝试。每项挑战题均为一条测试指令，用于验证学生所编写的谓词与隐藏基准是否等价。本次分组将约51000条原始条目整合为约7000个语义唯一的规范（以及约17000个句法唯一的规范）。 语义等价性通过Alloy分析器（Alloy Analyzer）进行测试，顶层签名的默认作用域为3。 句法等价性则在经过简单规范化（变量匿名化与运算符交换律处理）后进行验证。 每个名为`original_cmd.json`的文件包含某一Alloy4Fun练习的挑战题相关信息，该练习的模型ID为`original`，其测试指令标注为`cmd`，具体字段说明如下： - `original`：Alloy4Fun数据库中原始模型的ID - `cmd`：挑战题的指令标注 - `pred`：挑战题的谓词标注 - `entry_count`：该挑战题的总条目数 - `semantic_count`：语义唯一的条目数量 - `syntactic_count`：句法唯一的条目数量 - `scope`：用于测试等价性的作用域 - `groups`：实际的语义分组，包含以下子字段： - `entry_count`：该语义分组内的总条目数 - `syntactic_count`：该分组内句法唯一的条目数量 - `correct`：该挑战题是否存在正确解 - `elems`：实际的句法分组，包含以下子字段： - `entry_count`：该句法分组内的总条目数 - `code`：具有代表性的代码提交样例 本次纳入考量的Alloy4Fun练习如下： | 名称 | 永久链接 | 挑战题 | 条目数 | 语义分组数 | 句法分组数 | | ---- | ---- | ---- | ---- | ---- | ---- | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv1 | 3054 | 119 | 377 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv2 | 1599 | 45 | 171 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv3 | 3936 | 858 | 1797 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv4 | 1957 | 150 | 583 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv5 | 2544 | 168 | 524 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv6 | 1223 | 71 | 306 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv7 | 3138 | 528 | 1281 | | 社交网络 | x3JXgWhJ3uti5Dzxz | inv8 | 1254 | 268 | 528 | | 课程系统 | iP5JL36afv5KbDKP6 | inv1 | 1903 | 163 | 482 | | 课程系统 | iP5JL36afv5KbDKP6 | inv2 | 791 | 35 | 105 | | 课程系统 | iP5JL36afv5KbDKP6 | inv3 | 1075 | 86 | 222 | | 课程系统 | iP5JL36afv5KbDKP6 | inv4 | 1167 | 88 | 258 | | 课程系统 | iP5JL36afv5KbDKP6 | inv5 | 1883 | 253 | 721 | | 课程系统 | iP5JL36afv5KbDKP6 | inv6 | 1150 | 177 | 404 | | 课程系统 | iP5JL36afv5KbDKP6 | inv7 | 1163 | 187 | 407 | | 课程系统 | iP5JL36afv5KbDKP6 | inv8 | 928 | 85 | 235 | | 课程系统 | iP5JL36afv5KbDKP6 | inv9 | 1941 | 324 | 1032 | | 课程系统 | iP5JL36afv5KbDKP6 | inv10 | 882 | 82 | 292 | | 课程系统 | iP5JL36afv5KbDKP6 | inv11 | 790 | 91 | 279 | | 课程系统 | iP5JL36afv5KbDKP6 | inv12 | 751 | 92 | 222 | | 课程系统 | iP5JL36afv5KbDKP6 | inv13 | 934 | 302 | 458 | | 课程系统 | iP5JL36afv5KbDKP6 | inv14 | 577 | 54 | 205 | | 课程系统 | iP5JL36afv5KbDKP6 | inv15 | 466 | 133 | 247 | | 生产线 | dyj49tEp7j6aWAQQX | inv1 | 792 | 45 | 122 | | 生产线 | dyj49tEp7j6aWAQQX | inv2 | 1330 | 94 | 514 | | 生产线 | dyj49tEp7j6aWAQQX | inv3 | 539 | 29 | 78 | | 生产线 | dyj49tEp7j6aWAQQX | inv4 | 769 | 80 | 244 | | 生产线 | dyj49tEp7j6aWAQQX | inv5 | 856 | 128 | 372 | | 生产线 | dyj49tEp7j6aWAQQX | inv6 | 1056 | 61 | 203 | | 生产线 | dyj49tEp7j6aWAQQX | inv7 | 908 | 113 | 219 | | 生产线 | dyj49tEp7j6aWAQQX | inv8 | 601 | 108 | 250 | | 生产线 | dyj49tEp7j6aWAQQX | inv9 | 2148 | 588 | 1555 | | 生产线 | dyj49tEp7j6aWAQQX | inv10 | 834 | 288 | 472 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv1 | 792 | 127 | 245 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv2 | 606 | 56 | 153 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv3 | 1473 | 145 | 384 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv4 | 685 | 111 | 272 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv5 | 836 | 166 | 392 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv6 | 461 | 70 | 133 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv7 | 337 | 38 | 78 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv8 | 508 | 53 | 120 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv9 | 768 | 206 | 357 | | 火车站 | cXPP9QBPTYgTX6WJ6 | inv10 | 425 | 90 | 156 |