This dataset contains the models submitted to the shared models in the Alloy4Fun platform during the 2019/20 and 2020/21 editions of the "Specification and Modelling" graduate course at the University of Minho, totalling with 42 enrolled students, as reported in the Science of Computer Programming paper "Experiences on Teaching Alloy with an Automated Assessment Platform" (extending the ABZ'20 conference version). Trash FOL, sDLK7uBCbgZon3znd Classroom FOL, YH3ANm7Y5Qe5dSYem Trash RL, PQAJE67kz8w5NWJuM Classroom RL, zRAn69AocpkmxXZnW Graphs, gAeD3MTGCCv8YNTaK LTS, zoEADeCW2b2suJB2k Production, jyS8Bmceejj9pLbTW CV, JC8Tij8o8GZb99gEJ, WGdhwKZnCu7aKhXq9 (v2) Trash LTL, 9jPK8KBWzjFmBx4Hb Train, FwCGymHmbqcziisH5 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]