DOI: 10.5281/zenodo.17392203
title: Alloy4Fun Semantic Entries

description: 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