Alloy4Fun Dataset for 2024/25

This dataset contains models submitted by students in the Alloy4Fun platform to solve the challenge models from various editions of formal methods courses in the University of Minho (UM) and the University of Porto (UP) between the fall of 2019 and the spring of 2025, totalling around 185.000 entries. Participants include those enrolled in the optional MSc course "Specification and Modelling" (EM) and the mandatory MSc course "Formal Methods in Software Engineering" (MFES) in UM, and the optional MSc course "Formal Methods for Critical Systems" (MFS) in UP. Note that since the challenges' permalinks are publicly available, the dataset may contain submissions from other participants outside the classroom context. The analysis of the 2021 dataset is reported in the Science of Computer Programming paper "Experiences on Teaching Alloy with an Automated Assessment Platform" (extending the ABZ'20 conference version analysing the 2020 dataset). Name Permalink Courses (Students) Entries Trash FOL sDLK7uBCbgZon3znd EM 19/20 (~20) & 20/21 (~20), MFS 21/22 (~10) & 22/23 (~10) 4333 Classroom FOL YH3ANm7Y5Qe5dSYem EM 19/20 (~20) & 20/21 (~20), MFS 21/22 (~10) & 22/23 (~10) 5106 Trash RL PQAJE67kz8w5NWJuM EM 19/20 (~20) & 20/21 (~20) 4929 Classroom RL zRAn69AocpkmxXZnW EM 19/20 (~20) & 20/21 (~20) 6813 Graphs gAeD3MTGCCv8YNTaK EM 19/20 (~20) & 20/21 (~20) 3382 LTS zoEADeCW2b2suJB2k EM 19/20 (~20) & 20/21 (~20) 3597 Production line jyS8Bmceejj9pLbTW bNCCf9FMRZoxqobfX (v2) aTwuoJgesSd8hXXEP (v3) dyj49tEp7j6aWAQQX (v4) EM 19/20 (~20) & 20/21 (~20) MFES 21/22 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24. (~10) MFES 22/23 (~200) MFES 23/24 (~200) & 24/25 (~200) 2582 6731 3684 13238 CV JC8Tij8o8GZb99gEJ WGdhwKZnCu7aKhXq9 (v2) EM 19/20 (~20) EM 20/21 (~20) 1423 393 Trash LTL 9jPK8KBWzjFmBx4Hb EM 19/20 (~20) & 20/21 (~20) 5910 Train Station FwCGymHmbqcziisH5 QxGnrFQnXPGh2Lh8C (v2) cXPP9QBPTYgTX6WJ6 (v3) EM 20/21 (~20) MFES 21/22 (~200) & 22/23 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24 (~10) MFES 23/24 (~200) & 24/25 (~200) 1285 9383 8805 Courses PSqwzYAfW9dFAa9im JDKw8yJZF5fiP3jv3 (v2) iP5JL36afv5KbDKP6 (v3) MFES 21/22 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24 (~10) MFES 22/23 (~200) MFES 23/24 (~200) & 24/25 (~200) 17515 8533 25722 Social network dkZH6HJNQNLLDX6Aj x3JXgWhJ3uti5Dzxz (v2) MFES 21/22 (~200) & 22/23 (~200), MFS 21/22 (~10) & 22/23 (~10) & 23/24 (~10) MFES 23/24 (~200) & 24/25 (~200) 24688 27302 Each entry of the dataset registers either an execution (which may have returned a result or an error) or the creation of a permalink for sharing, and contains: _id: the id of the interaction time: the timestamp of its creation derivationOf: the parent entry original: the first ancestor with secrets (always the same within an exercise) code: the complete code of the model (excluding the secrets defined in the original entry) (with student comments removed) sat: whether the command was satisfiable (counter-example found for checks), or -1 when error thrown [only for executions] cmd_i: the index of the executed command [only for executions] cmd_n: the name of the executed command [only for successful executions, i.e. no error thrown] cmd_c: whether the command was a check [only for successful executions, i.e. no error thrown] msg: the error or warning message [only for successful executions with warnings or when error thrown] theme: the visualisation theme [only for sharing entries] User comments were removed from the code to guarantee anonymization.本数据集收录了2019年秋季至2025年春季期间，葡萄牙米尼奥大学（University of Minho, UM）与波尔图大学（University of Porto, UP）各类形式化方法课程的挑战模型求解作业，由学生在Alloy4Fun平台（Alloy4Fun）提交的模型组成，总计约185,000条数据项。 参与本数据集的学生涵盖米尼奥大学的选修硕士课程《规格说明与建模》（Specification and Modelling，缩写EM）、必修硕士课程《软件工程中的形式化方法》（Formal Methods in Software Engineering，缩写MFES），以及波尔图大学的选修硕士课程《关键系统形式化方法》（Formal Methods for Critical Systems，缩写MFS）的注册学生。 请注意，由于各挑战的永久链接（permalink）均为公开可得，本数据集可能包含课堂场景之外的其他参与者提交的作业。 2021年数据集的相关分析已发表于《计算机编程科学》（Science of Computer Programming）期刊论文《基于自动化评测平台的Alloy教学实践》（"Experiences on Teaching Alloy with an Automated Assessment Platform"），该论文拓展了分析2020年数据集的ABZ'20会议版本内容。 本数据集包含以下若干挑战模型集，详情如下： 1. **Trash FOL** - 永久链接：sDLK7uBCbgZon3znd - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人）、波尔图大学MFS 21/22（约10人）及22/23（约10人） - 数据条目数：4333 2. **Classroom FOL** - 永久链接：YH3ANm7Y5Qe5dSYem - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人）、波尔图大学MFS 21/22（约10人）及22/23（约10人） - 数据条目数：5106 3. **Trash RL** - 永久链接：PQAJE67kz8w5NWJuM - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人） - 数据条目数：4929 4. **Classroom RL** - 永久链接：zRAn69AocpkmxXZnW - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人） - 数据条目数：6813 5. **Graphs** - 永久链接：gAeD3MTGCCv8YNTaK - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人） - 数据条目数：3382 6. **LTS** - 永久链接：zoEADeCW2b2suJB2k - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人） - 数据条目数：3597 7. **Production line**（共4个版本） - 版本1：永久链接jyS8Bmceejj9pLbTW，参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人），数据条目数：2582 - 版本2：永久链接bNCCf9FMRZoxqobfX (v2)，参与课程：米尼奥大学MFES 21/22（约200人）、波尔图大学MFS 21/22（约10人）及22/23（约10人）及23/24（约10人），数据条目数：6731 - 版本3：永久链接aTwuoJgesSd8hXXEP (v3)，参与课程：米尼奥大学MFES 22/23（约200人），数据条目数：3684 - 版本4：永久链接dyj49tEp7j6aWAQQX (v4)，参与课程：米尼奥大学MFES 23/24（约200人）及24/25（约200人），数据条目数：13238 8. **CV**（共2个版本） - 版本1：永久链接JC8Tij8o8GZb99gEJ，参与课程：米尼奥大学EM 19/20（约20人），数据条目数：1423 - 版本2：永久链接WGdhwKZnCu7aKhXq9 (v2)，参与课程：米尼奥大学EM 20/21（约20人），数据条目数：393 9. **Trash LTL** - 永久链接：9jPK8KBWzjFmBx4Hb - 参与课程：米尼奥大学EM 19/20（约20人）及20/21（约20人） - 数据条目数：5910 10. **Train Station**（共3个版本） - 版本1：永久链接FwCGymHmbqcziisH5，参与课程：米尼奥大学EM 20/21（约20人），数据条目数：1285 - 版本2：永久链接QxGnrFQnXPGh2Lh8C (v2)，参与课程：米尼奥大学MFES 21/22（约200人）及22/23（约200人）、波尔图大学MFS 21/22（约10人）及22/23（约10人）及23/24（约10人），数据条目数：9383 - 版本3：永久链接cXPP9QBPTYgTX6WJ6 (v3)，参与课程：米尼奥大学MFES 23/24（约200人）及24/25（约200人），数据条目数：8805 11. **Courses**（共3个版本） - 版本1：永久链接PSqwzYAfW9dFAa9im，参与课程：米尼奥大学MFES 21/22（约200人）、波尔图大学MFS 21/22（约10人）及22/23（约10人）及23/24（约10人），数据条目数：17515 - 版本2：永久链接JDKw8yJZF5fiP3jv3 (v2)，参与课程：米尼奥大学MFES 22/23（约200人），数据条目数：8533 - 版本3：永久链接iP5JL36afv5KbDKP6 (v3)，参与课程：米尼奥大学MFES 23/24（约200人）及24/25（约200人），数据条目数：25722 12. **Social network**（共2个版本） - 版本1：永久链接dkZH6HJNQNLLDX6Aj，参与课程：米尼奥大学MFES 21/22（约200人）及22/23（约200人）、波尔图大学MFS 21/22（约10人）及22/23（约10人）及23/24（约10人），数据条目数：24688 - 版本2：永久链接x3JXgWhJ3uti5Dzxz (v2)，参与课程：米尼奥大学MFES 23/24（约200人）及24/25（约200人），数据条目数：27302 本数据集的每条数据项均记录一次交互操作（可能返回结果或报错）或一条用于分享的永久链接创建记录，包含以下字段： - `_id`：交互操作的唯一标识符 - `time`：创建时间戳 - `derivationOf`：父级数据项 - `original`：包含敏感信息的首个祖先项（同一习题内始终保持一致） - `code`：模型完整代码（已移除原项中定义的敏感信息及学生注释） - `sat`：命令是否可满足（若为校验命令则表示是否找到反例）；若抛出错误则取值为-1【仅适用于执行操作】 - `cmd_i`：已执行命令的索引【仅适用于执行操作】 - `cmd_n`：已执行命令的名称【仅适用于无报错的成功执行操作】 - `cmd_c`：该命令是否为校验命令【仅适用于无报错的成功执行操作】 - `msg`：错误或警告信息【仅适用于带警告的成功执行操作或报错场景】 - `theme`：可视化主题【仅适用于分享类记录】 为保障匿名性，代码中已移除学生注释。