EM 19 10

This page provides the dataset collected during the 2019/20 edition of the "Specification and Modelling" graduate course at the University of Minho with 17 enrolled students, as reported in the paper "Experiences on Teaching Alloy with an Automated Assessment Platform".

Id	Name	#Chall.	Permalink	Dataset
1	Trash FOL	10	zA2MMSGy6iW8Mihep	Data
2	Classroom FOL	15	Pdvipvrpr5hg7JKbs	Data
3	Trash RL	10	WJdLnDL78m7mM7W4J	Data
4	Classroom RL	15	i5u2pjKJt6Bz227QT	Data
5	Graphs	8	28fwdmjL79X4SQ9EP	Data
6	LTS	7	gqS3qTTn4B62NYmJX	Data
7	Production	4	PKy7chamCieZyCix5	Data
8	CV	4	X72J6js9fA3CKYQWX	Data
9	Trash LTL	20	irRLJn7qbQq3xMFGp	Data

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)
• 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]