# Empirically Exploring How Novices Write Software Models in Alloy

Ana Jovanovic  The University of Texas at ArlingtonArlington, TX, USA
<EMAIL_ADDRESS>and  Allison Sullivan  The University of Texas at
ArlingtonArlington, TX, USA<EMAIL_ADDRESS>
###### Abstract.

Writing declarative models has numerous benefits, ranging from automated
reasoning and correction of design-level properties before systems are built,
to automated testing and debugging of their implementations after they are
built. Alloy is a declarative modeling language that is well-suited for
verifying system designs. A key strength of Alloy is its scenario-finding
toolset, the Analyzer, which allows users to explore all valid scenarios that
adhere to the model’s constraints up to a user-provided scope. However, even
with visualized scenarios, it is difficult to write correct Alloy models. To
address this, a growing body of work explores different techniques for
debugging Alloy models. In order to develop and evaluate these techniques in
an effective manor, this paper presents an empirical study of over 97,000
models written by novice users trying to learn Alloy. We investigate how users
write both correct and incorrect models in order to produce a comprehensive
benchmark for future use as well as a series of observations to guide
debugging and educational efforts for Alloy model development.

##  1\. Introduction

In today’s society, we are becoming increasingly dependent on software
systems. However, we also constantly witness the negative impacts of buggy
software. One way to help develop better software systems is to leverage
software models. When forming requirements, software models can be used to
clearly communicate to all stakeholders both the desired system as well as the
environment it will be deployed in. When creating designs and implementations,
software models can help reason over how well the design and implementation
choices satisfy the requirements. As such, software models can help detect
flaws earlier in development and thus aid in the delivery of more reliable
systems.

Alloy (JacksonAlloyBook2006, ) is a relational modeling language. A key
strength of Alloy is the ability to develop models in the Analyzer, an
automatic analysis engine based on off-the-shelf SAT solvers, which the
Analyzer uses to generate scenarios that highlight how the modeled properties
either hold or are refuted, as desired. The user is able to iterate over these
scenarios one by one, inspecting them for correctness. Alloy has been used to
verify software system designs (Zave15, ; BagheriETAL2018, ;
WickersonETAL2017, ; ChongETAL2018, ), and to perform various forms of
analyses over the corresponding implementation, including deep static checking
(JacksonVaziri00Bugs, ; TACOGaleottiETALTSE2013, ), systematic testing
(MarinovKhurshid01TestEra, ), data structure repair (ZaeemKhurshidECOOP2010,
), automated debugging (GopinathETALTACAS2011, ) and to synthesize security
attacks (websecurity, ; Margrave, ; CheckMateMicro2019, ).

However, to gain the many benefits that come from utilizing software models,
the model itself needs to be correct. Unfortunately, while Alloy offers
succinct formulation of complex properties, Alloy’s support for expressive
operators, such as transitive closure and quantified formulas, can make
writing non-trivial properties challenging, especially for beginner users. In
Alloy, there are two types of faults that can appear in a model: (1)
_underconstrained_ faults in which the model allows scenarios it should
prevent, and (2)  _overconstrained_ faults in which the model prevents
scenarios it should allow. These faults can occur in isolation or combined
together.

To detect an underconstrained fault, during enumeration, the user needs to
observe an unexpected scenario that they did not expect to see. In contrast,
to detect an overconstrained fault, after enumeration, the user needs to
realize that an expected scenario was never present. Since it is common for an
Alloy command to produce hundreds of scenarios, there is a high burden on the
user to realize their Alloy model is incorrect. While observing an over-
constrained fault requires exploring the entire collection of scenarios,
under-constrained faults are still difficult for users to identify and handle.
Moreover, even if the user notices something is wrong, according to a recent
user student, both novice and expert Alloy modelers struggled to refine a
faulty formula given an incorrectly produced scenario (alloyformalise23study,
).

Given these difficulties, there is a growing body of work looking at how to
detect and debug faulty Alloy models. Initially, a unit testing framework
AUnit, was created (AUnitConcept, ; AUnit, ). AUnit enables users to outline a
specific scenario they expect their model to allow or prevent and then check
that this behavior actually occurs, which allows the user to directly check
for under- or over-constrained faults without having to enumerate scenarios.
AUnit has been used for mutation testing (MuAlloyTool, ; MuAlloyTemporal, ),
fault localization (AlloyFL, ), and automated repair (ARepair, ; icebar, ).
Since then, fault localization and repair of Alloy models has become an active
research area (atr, ; flack, ; beafix, ; tar, ).

(a) | (b)
---|---
1\. var sig File { var link : lone File } 2\. var sig Trash in File {} 3\. var sig Protected in File {} 4\. pred ProtectedNeverTrashed { 5\. no Protected & Trash \--incorrect 6\.  \--always no Protected & Trash --correct 7\. } 8\. run  ProtectedNeverTrashed for 3 |  F0F1TrashF2Protectedlink |  F0 F1 Trash, Protected F2Protectedlink
| (State 0) | (State 1)
|  01
Figure 1. Faulty Submission of an Alloy Model of a File System Trash Can

As this field grows, we believe it is important to understand what mistakes
new developers actually make when writing models, so that these techniques can
(1) be effective for the majority of mistakes made, (2) be evaluated with
respect to real faults and not simulated faults and (3) be properly leveraged
to ease the burden of learning to write software models. To achieve these
goals, this paper presents an empirical study to explore the common
development practices of novice Alloy modelers using 97,755 models submitted
through Alloy4Fun, an online educational website for Alloy.

In this paper, we make the following contributions:

Empirical Study: We present a systematic study of both correct and incorrect
models written by novice Alloy users with revision histories. We investigate
what mistakes users commonly make and also how they change the model trying to
correct a mistake.

Practical Impacts: We distill our observations into practical guidelines for
future work in debugging models and building educational material for formal
methods. Based on our results, we present a series of observations and
recommendations to help guide future work for debugging Alloy models.

Benchmarks for Alloy: As part of our efforts to explore the submissions to
Alloy4Fun, we create a collection of real world faulty models broken down by
type of fault.

Open Source: We release our organized datasets at:
https://github.com/NoviceAlloyModels

##  2\. Background

In this section, we describe key concepts of Alloy and the Alloy4Fun
exercises.

###  2.1. Alloy

Figure 1 (a) displays a faulty temporal model of a file system trash can from
the Alloy4Fun benchmark, which is comprised of real-world models from new
Alloy users (alloy4funbenchmark, ). Signature paragraphs introduce named sets
and can define relations, which outline relationships between elements of
sets. Line 1 introduces a named set File and establishes that each File atom
connects to zero or one (lone) File atoms through the link relation. Lines 2
and 3 introduce the named sets Trash and Protected as subsets (in) of File.
Signatures and relations can be declared mutable (var), which means that the
elements of these sets can vary across different states in the same scenario.
In our example, all 3 signatures (File, Trash, and Protected) and the one
relation (link) are mutable.

1\. // a protected file is at no time sent to the trash

2\. pred prop9 {}

3\. //SECRET

4\. pred prop9o { always no Protected & Trash }

5\. check prop9Ok {

6\. (prop9 and not prop9o) implies (prop9o iff prop9)

7\. }

Figure 2. Snipet from the Trash Alloy4Fun Exercise

Predicate paragraphs introduce named first-order, linear temporal logic
formulas that can be invoked elsewhere. The predicate ProtectedNotTrashed uses
empty set (‘no’) and set intersection (‘&’) to incorrectly attempt to
establish that a protected file is never sent to the trash. However, since the
signatures are mutable, the incorrect version is true as long as no protected
files are in the trash for the _first_ state but does not require the
constraint to be true in _every_ state. To correct this, the linear temporal
operator always can be appended to the start of the predicate. Commands
indicate which formulas to invoke and what scope to explore. The scope places
an upper bound on the size of all signature sets and the number of state
transitions. The command on line 8 instructs the Analyzer to search for an
assignment to all sets in the model using up to 3 File atoms and up to 10
state transitions by default. Figure 1 (a) displays the first scenario found
by the Analyzer. This scenario informs the user that their model is incorrect:
in state 1, F1 is both in the trash and protected. At this point, the user can
return to their model, edit their constraints, and re-run the command until
all scenarios enumerated match their expectation.

###  2.2. Alloy4Fun Exercises

Alloy4Fun is an online educational platform for learning Alloy where users can
write and compile Alloy models through an online interface. While anyone can
build and share any model on Alloy4Fun, there are example models users can
explore to get familiar with Alloy. For these models, the base structure – the
signature paragraphs – is given along with a high level description of the
system. In addition, each model contains a varying number of empty predicates
with a corresponding English description of the property. For each of these
empty predicates, the user can attempt to encode the English description into
formal logic.

To check their answer, the user can select properties to check and Alloy4Fun
will compare if their written submission is equivalent to a hidden oracle. If
their submission is not equivalent to the oracle, the user will be presented
with a counterexample: a scenario that depicts a situation where the user’s
formula behaves different than the oracle formula. The user can then continue
to iterate on their formula until it is correct. To illustrate, Figure 2
displays the Trash exercise that generated the model in Figure 1. Lines 1-2
are visible to the user while lines 3-7 are hidden. The check command (lines
5-7) compares if a submission is equivalent to the oracle, which checks for
semantic equivalence and not syntactic equivalence.

Table 1. Overview of Complexity of Models in Study

| #Sig | #Abs | #Ext | #Rel | Arity | #Exe
---|---|---|---|---|---|---
classroom_fol | 5 | 0 | 2 | 3 | 2.33 | 15
classroom_rl | 5 | 0 | 2 | 3 | 2.33 | 15
courses_v1 | 6 | 0 | 2 | 5 | 2.2 | 15
courses_v2 | 6 | 0 | 2 | 5 | 2.2 | 15
cv_v1 | 5 | 1 | 2 | 4 | 2 | 4
cv_v2 | 5 | 1 | 2 | 4 | 2 | 4
graphs | 1 | 0 | 0 | 1 | 2 | 8
lts | 3 | 0 | 1 | 1 | 3 | 6
productionLine_v1 | 5 | 0 | 2 | 3 | 2 | 4
productionLine_v2 | 10 | 1 | 7 | 4 | 2 | 10
productionLine_v3 | 10 | 1 | 7 | 4 | 2 | 10
socialMedia | 5 | 0 | 2 | 5 | 2 | 8
trainstation_fol | 7 | 0 | 5 | 2 | 2 | 10
trainstation_ltl | 6 | 0 | 4 | 3 | 2 | 17
trash_rl | 3 | 0 | 2 | 1 | 2 | 10
trash_ltl | 3 | 0 | 2 | 1 | 2 | 20
trash_fol | 3 | 0 | 2 | 1 | 2 | 10
AVG | 5.18 | 0.24 | 2.71 | 2.94 | 2.12 | 10.65

##  3\. Experiment SetUp

###  3.1. Experimental Data

In our study, we use the publicly released Alloy4Fun dataset, which contains
real world models obtained from student submissions in the academic period of
fall 2019 and spring 2023. In total, there are 97,755 submissions that span 17
different Alloy models and 185 predicates to be filled in (exercises). Of
these, we filtered out 1,742 submissions that change the example model’s
signatures or execute commands other than checking the exercises, leaving us
with 96,013 submissions.

Table 1 gives an overview of the complexity of the models used in our study in
terms of the complexity of the universe of discourse each model creates.
Column #Sig is the total number of signatures in the model, #Abs is the number
of abstract signatures, #Ext is the number of signatures that extend another
signature, #Rel is the number of relations, Arity is the average arity of all
relations in the model (2 indicates a binary relation). Lastly, column #Exe
shows the number of exercises per model. Models with an underscore in their
name represent models that have multiple versions in the dataset. Between
versions, the number of exercise, instructional text for an exercise and/or
the type of logic expected can change.

An exercise falls into one of the following categories: relational logic (RL),
predicate logic (PL), first order logic (FOL), and linear temporal logic
(LTL). Per Alloy4Fun developers (alloy4funbenchmark, ), students were
gradually introduced to the concepts, naturally starting from predicate and
first order logic, then relational logic and finally linear temporal logic.
Table 2 conveys the complexity of the exercise based on type of logic.
Exercises were classified based on the highest operator present with a partial
order of RL$->$PL$->$FOL$->$LTL. The first two columns show the number of
exercises: #Exe is the number of exercises and Rate is the percentage of total
exercises that are the associated type. The last 5 columns demonstrate the
size of the oracle solution broken down by type of logic. Column #AST is the
average number of AST nodes in the oracle, and columns #RL Op, #PL Op, #FOL
Op, and #LTL Op for the associated logic.

Table 2. Number and Size of Exercises by Type

Type | # Exe | Rate | #AST | #RL Op | #PL Op | #FOL Op | #LTL Op
---|---|---|---|---|---|---|---
RL | 50 | 27.62 | 4.18 | 1.84 | 0.00 | 0.00 | 0
PL | 1 | 0.55 | 5.00 | 2.00 | 1.00 | 0.00 | 0
FOL | 95 | 52.49 | 17.47 | 5.88 | 0.31 | 1.07 | 0
LTL | 35 | 19.34 | 16.31 | 4.72 | 0.56 | 0.81 | 2
Total | 181 | 100.00 | 10.74 | 3.61 | 0.47 | 0.47 | 0.50

To illustrate the bounds between the different types of logic, the following
is the subset of Alloy’s grammar that captures all supported relational logic
operators:

unOp::= ~ | * | ^ | ! | not | no | mult | set |binOp::= & | + | - | ++ | <: | :> | .arrowOp::= [mult | set] -> [mult | set]compareOp::= in | = | < | > | =< | >=expr::= decl,+ blockOrBar (comprehension)mult::= lone | some | one

The following is the subset of Alloy’s grammar that captures all supported
predicate logic operators:

binOp::= || | or | && | and | <=> | iff | => | implies

The following is the subset of Alloy’s grammar that captures all supported
first order logic operators:

quant::= all | no | sum | multexpr::= quant decl,+ blockOrBar

The following is the subset of Alloy’s grammar that captures all supported
linear temporal logic operators:

unOp::= always | eventually | after | before | historically | once | ’binOp::= since | triggered | until | releases | ;

###  3.2. Classification of Submissions

Within our dataset, we consider a submission to fall into one of the following
categories: correct, overconstrained (over), underconstrained (under), both
over- and underconstrained (both), type error (type) and syntax error
(syntax). Correct submissions are semantically equivalent to the oracle,
overconstrained submissions prevent valid scenarios from being generated,
underconstrained submissions allow invalid scenarios to be generated, both
submissions allow a combination of over- and underconstrained behaviors, type
errors are formulas that are syntactically valid but fail to typecheck, and
syntax errors are formulas that fail to adhere to the grammar rules as well as
submissions with spelling errors.

To determine which category a submission falls under, we treat the oracle
solution as the ground truth and consider any submission that is semantically
equivalent, even if not syntactically equivalent, as correct. If not correct,
we then user Alloy to check if the submission is overconstrained,
underconstrained or both over- and underconstrained. In addition, if we fail
to compile the model, we use the generated error message to determine if there
was a type error or a syntax error.

(ALL) (RL) (PL) (FOL) (LTL)
---
Figure 3. Breakdown of Submission Results Table 3. Rate of Semantically and Syntactically Unique Submissions RL | PL
---|---
Cx | All | Syn | %Syn | A/Sy | Sem | %Sem | Sy/Se | Cx | All | Syn | %Syn | A/Sy | Sem | %Sem | Sy/Se
Correct | 9814 | 1362 | 13.88 | 7.21 | 50 | 0.51 | 27.24 | Correct | 289 | 39 | 13.49 | 7.41 | 1 | 0.35 | 39.00
Both | 2843 | 1731 | 60.89 | 1.64 | 931 | 32.75 | 1.86 | Both | 239 | 168 | 70.29 | 1.42 | 105 | 43.93 | 1.60
Over | 1637 | 824 | 50.34 | 1.99 | 303 | 18.51 | 2.72 | Over | 93 | 43 | 46.24 | 2.16 | 21 | 22.58 | 2.05
Under | 1248 | 811 | 64.98 | 1.54 | 206 | 16.51 | 3.94 | Under | 57 | 39 | 68.42 | 1.46 | 9 | 15.79 | 4.33
Syntax | 2557 | 2132 | 83.38 | 1.20 |  |  |  | Syntax | 107 | 88 | 82.24 | 1.22 |  |  |
Type | 2396 | 1948 | 81.30 | 1.23 |  |  |  | Type | 104 | 94 | 90.38 | 1.11 |  |  |
Total | 20495 | 8808 | 42.98 | 2.33 | 1490 | 7.27 | 5.91 | Total | 889 | 471 | 52.98 | 1.89 | 136 | 15.30 | 3.46
FOL | LTL
Cx | All | Syn | %Syn | A/Sy | Sem | %Sem | Sy/Se | Cx | All | Syn | %Syn | A/Sy | Sem | %Sem | Sy/Se
Correct | 13906 | 2718 | 19.55 | 5.12 | 92 | 0.66 | 29.54 | Correct | 1499 | 183 | 12.21 | 8.19 | 30 | 2.00 | 6.10
Both | 16802 | 10784 | 64.18 | 1.56 | 5672 | 33.76 | 1.90 | Both | 1783 | 1140 | 63.94 | 1.56 | 726 | 40.72 | 1.57
Over | 5605 | 3375 | 60.21 | 1.66 | 1113 | 19.86 | 3.03 | Over | 744 | 394 | 52.96 | 1.89 | 211 | 28.36 | 1.87
Under | 10468 | 5004 | 47.80 | 2.09 | 858 | 8.20 | 5.83 | Under | 1027 | 518 | 50.44 | 1.98 | 149 | 14.51 | 3.48
Syntax | 8813 | 7589 | 86.11 | 1.16 |  |  |  | Syntax | 650 | 583 | 89.69 | 1.11 |  |  |
Type | 8685 | 7208 | 82.99 | 1.20 |  |  |  | Type | 385 | 302 | 78.44 | 1.27 |  |  |
Total | 64279 | 36678 | 57.06 | 1.75 | 7735 | 12.03 | 4.74 | Total | 6088 | 3120 | 51.25 | 1.95 | 1116 | 18.33 | 2.80

##  4\. Empirical Evaluation

Our research questions are organized by explorations of different
classification of submissions. We first explore general behavior across all
submissions (RQ1 - RQ3) before exploring how users write correct submissions
(RQ4), then we explore how users write incorrect submissions (RQ5 - RQ6).

###  4.1. RQ1: How prevalent are empty submissions?

When solving Alloy4Fun exercises, users are writing properties based on an
English description and a base model comprised of signature paragraphs that
they did not write. By checking an empty submissions, users can be presented
with counterexamples that highlight how the base model should behave, which
can help the user better understand the base structure that they will be
writing constraints within. Therefore, we wanted to determine the rate at
which empty submissions are checked. We discovered that empty submissions
account for 4.44% of all submissions made. We did not find that the models
with the highest rate of empty solutions were correlated with the most complex
base models. For instance, the five highest rate of empty submissions is the
following: trash_rl at 9.04%, productLine_v1 at 7.06%, socialMedia at 6.38%
and trash_fol at 6.37% and cv_v1 at 5.56%. However, there are other models
with more extension signatures, more relations and even higher arity relations
that have lower rates of empty submissions.

While only 4.44% of submissions are empty, this does represent 4,262 times
that a user did want to check what behavior is already supported by the model
before trying to further refine the behavior by writing a predicate. This
represents a chance for tool improvement to better facilitate this behavior. A
recent user study using Alloy highlighted that users better understand pre-
written predicates when shown both allowed and prevented behavior (negpos, ).
This insight can be used to expand the counterexample generation for all
executions, including empty submissions where the user is explicitly asking
for context about the model’s current behavior. Namely, Alloy4Fun can be
extended to (1) label whether the counterexample should be allowed or
prevented behavior and (2) generate multiple counterexamples in which some
should be allowed and some should be prevented by the to-be-written predicate.

For educational tools, developers should consider adding example scenarios to
the exercise description, not just stating the to-be-formulated behavior in
English.

With empty submissions, 17.7% of all the submissions are underconstrained.
However, excluding empty submissions results in only 13.95% of the submissions
being underconstrained. Since empty submissions do not fundamentally
illustrate any effort by the novice user, we removed the empty submissions
from the results presented in the remaining questions to avoid skewing the
results.

###  4.2. RQ2: What classification of submissions do novice users make and at
what rate?

To get a general overview of the submissions made, Figure 3 shows 5 pie charts
depicting the breakdown in classification of submission. In subsequent RQs, we
dive deeper into the submissions within these classifications. The first pie
chart contains information for all submissions made, while the remaining
submissions show the breakdown per type of logic. Across all submissions,
correct submissions account for the largest classification of submissions
(27.8%), but that rate varies based on type of logic. Novice users are the
most effective at writing relational logic properties, which novices express
correctly in 47.88% of the submissions. In contrast, novice users struggle
more with FOL and LTL properties, in which less than a fourth of the
submissions are correct: 21.63% and 24.62% respectively. This decrease in
accuracy for FOL and LTL exercises is expected, as the introduction of
quantified formulas and temporal constraints is non-trivial.

When viewed together, faulty submissions account for 46.38% of all
submissions, with submissions that are both over- and underconstrained
accounting for the largest portion of mistakes at 23.62% followed by
underconstrained at 13.95% and lastly overconstrained at 8.81%. Therefore,
novices are notable more likely to create a model that is more permissive
rather than more restrictive. However, this varies more by type of logic. For
RL and PL exercises, while mistakes that are both over- and underconstrained
remains dominate at 13.87% and 26.88% respectively, both types of logic see
more overconstrained faults (7.99% RL and 10.46% PL) than underconstrained
(6.09% RL and 6.41% PL). This indicates that the addition of quantification
and temporal logic results in novice users writing properties that are often
too permissive in behavior. In RQ6, we dive deeper into common mistakes that
reveals several reasons why both and strictly underconstrained faults are so
prevalent.

Novice users have more difficulty with FOL and LTL properties compared to RL
and PL properties. Novice users are also more likely to write formulas that
are too permissive; therefore, debugging efforts should focus on additive
constraints.

Non-compilable submissions (type and syntax errors) account for 25.83% of all
submissions. These submissions are almost evenly split between syntax errors
(12.48%) and type errors (11.69%). Syntax errors results when the user
produces a formula that is invalid with respect to Alloy’s grammar. Type
errors occur when the user writes a formula that Alloy’s type checking system
detects as malformed. Viewing submissions by the type of logic required to
solve the exercise does not change the general rate of syntax errors. For type
errors, LTL exercises see a notable decrease, where only 6.32% of these
submissions have a type error. One possible explanation for this is that
within the LTL exercises, only some of the signatures and relations are
mutable. As a result, there is a more narrow pool of types for which temporal
properties apply, resulting in novices making less mistakes.

Given the non-nominal rate and which invalid submissions are made, we
investigated Alloy’s current compiler-based error reporting. One nice feature
of Alloy’s compiler is that it uses Alloy’s type system to detect if there is
a type mismatch that will prevent a formula from properly evaluating. As a
result, novices are not left with unsatisfiable or trivial true formulas that
provide no feedback for debugging. However, when exploring some of the
novice’s type errors, we found Alloy’s type checking error reporting to be
limited in feedback and can even be misleading. Consider the following
submission to the classroom_fol inv1 exercise:

no Student in PersonThis must be a set or relation.Instead, it has the
following possible type(s): PrimitiveBoolean

which shows in red the highlighting guidance given by Alloy’s type checking
reporter and the error report. This highlight implies that the issue is that
Student is the wrong type; however, “no Student is itself a valid type checked
formula. The real issue is that “Student in Person” evaluates to a boolean
true/false result and “no” reasons over whether a set is empty, leading to the
type issue. This can mislead the user to try and edit the wrong portion of the
formula, and lead to frustration when the type error persists.

One in four novice submissions are malformed either syntactically or
semantically. Therefore, it is worth the effort to improve Alloy’s error
reporting to better guide users towards what portions of their formula is
invalid.

###  4.3. RQ3: How often do novice users make the same submission?

If users often repeat the same submission, then this represents common
approaches that novices take to modeling, and understanding these common
approach can help guide improvements in tool support and educational material.
Therefore, we investigate how often new users make the same exact submission.

We consider two forms of equivalence: syntactic and semantic. Syntactical
duplicates covey the rate at which novice users literally make the same
mistake, while semantic duplicates allows us to explore the rate at which
users express the same underlying concept, even if they wrote different
formulas. Frequently occurring semantic mistakes can represent a fundamental
misunderstanding that could be happening, which reflects an educational gap
and/or ambiguous wording on the instructions for the exercise. To determine if
two submissions are syntactically equivalent, we used a PrettyStringVisitor to
reprint formulas in a consistent format that eliminates trivial differences in
formatting that arise from different uses of white spaces. We then checked if
the printed Strings are the same using Java’s String equals method. To
determine if two submissions are semantically equivalent, we used the Analyzer
to check for logical equivalence between submissions.

Table 3 shows the rate at which syntactic and semantically equivalent
submissions occur within our dataset broken down by both type of logic and
classification of submission. Column All is the total number of submissions,
column Syn is the number of submissions which are unique syntactically, %Syn
is the percentage of total submissions that are unique syntactically, Sem is
the number of submissions which are unique semantically, %Sem is the
percentage of total submissions that are unique semantically. Column A/Sy
shows the magnitude in reduction between the total number of submissions and
the portion that are syntactically unique. Column Sy/Se shows the magnitude of
reduction between the number of syntactically equivalent submissions compared
to semantically equivalent submissions. Syntax and Type submissions do not
have semantically equivalent values since these submissions do not compile.
For each type of logic, the row Total displays information related to all
submissions made of that type of logic.

In general, around 53.49% of submissions are syntactically unique and 11.42%
are semantically unique, although there are two phenomena that skew this
average. First, there is high redundancy in correct submissions, which is
expected as there are a finite number of ways to express a property correctly.
For correct submissions, the number of unique semantic submissions is
equivalent to the number of exercises that have at least one correct
submission, which is expected as all correct solutions should be semantically
equivalent to one another. Second, there is notably less redundancy in type
and syntax errors, meaning that novice users make a broader range of mistakes
when incorrectly structuring a formula compared to writing a syntactically
valid formula that is logically wrong.

For faulty submissions (both, over and under), the diversity of syntactic
mistakes made by novice users varies slightly depending on the type of logic
needed to solve the exercise. In general, for RL, FOL and LTL exercises, users
repeat submissions by writing the same incorrect formula around half to two
thirds of the time. However, for PL exercises, both over- and under faults as
well as strictly underconstrained faults are repeated less often, with 70.29%
and 68.42% of submissions being unique. However, there is only one PL
exercise; therefore, there is significantly less data behind these results
compared to ther other types of logic. Across all types of logic,
underconstrained faults capture less diversity in the underlying mistake made,
as seen by achieving the largest reduction between syntactically and
semantically unique submissions for all types of logic (column Sy/Se). In
addition, for all types of logic, faults that are both over- and
underconstrained span the widest range of underlying mistakes, with 34.31%
being semantically unique.

Novice users frequently repeat the same submission, even when viewed
syntactically, which indicates that there are common misunderstandings that
occur. Given the high redundancy in underconstrained faults, researchers and
educators can benefit the most by focusing on how to prevent and debug these
types of faults.

Table 4. Location of Oracle in Frequency Ranked Subs

| Top 1 | Rate | Top 5 | Rate | Top 10 | Rate | Not Sub | Rate
---|---|---|---|---|---|---|---|---
RL | 21 | 41.18 | 37 | 72.55 | 44 | 86.27 | 1 | 1.96
PL | 1 | 100.00 | 1 | 100.00 | 1 | 100.00 | 0 | 0.00
FOL | 26 | 27.37 | 53 | 55.79 | 64 | 67.37 | 20 | 21.05
LTL | 12 | 33.33 | 19 | 52.78 | 20 | 55.56 | 13 | 36.11
Total | 60 | 33.15 | 110 | 60.11 | 129 | 70.49 | 34 | 18.58

###  4.4. RQ4: How do novice users’ correct answers differ from the oracle
formula?

While there is an oracle solution formula for all exercise, often times, this
oracle represents one of several ways in which the property could be
expressed, as seen in Table 3 in which the number of syntactically unique
correct solutions is larger than the number of semantically unique correct
solutions. Therefore, we wanted to explore what ways novice users commonly
write correct properties, and to gain insights from ways in which a novice
user’s thinking may differ from the expert written oracles.

First, we explore how frequently the oracle solution appears as a correct
submission. Table 4 displays the location of the oracle submission derived by
ranking all syntactically unique correct submissions in decreasing order from
most to least duplicate submissions. Then, we looked for the location of the
oracle submission within that list. Column type displays the type of logical
exercises under consideration. Column Top 1 shows the number of exercises for
that type in which the oracle is first in the ranked list and associated
Column Rate what percentage the number of Top 1 exercises is out of the total
number of exercises of that type. Table 4 also displays information for
whether the oracle is in the Top 5 and Top 10 locations in the ranked list.

For RL exercises, the oracle is the top submission 41.18% of the times and in
the top 10 86.27% of the time. Rarely (1.96%) the oracle is never submitted.
There is only one PL exercise and it’s oracle is the top submission. As the
complexity of the logic increases, the oracle solutions is less present in the
correct submissions. While the oracle is the top submission for 27.37% of FOL
exercises and 33.33% of LTL exercises, by location 10, the oracle is only
present in 67.37% and 55.56% of the exercises respectively. Moreover, it is
common for the oracle to never be submitted, which happens 21.05% of the time
for FOL exercises and 36.11% of the time for LTL exercises. Overall, FOL and
LTL exercises are both more complex, but also more open ended. For instance,
for FOL exercises, depending on what the user selects as the domain, the
formulas can vary widely. RL exercise use the smallest subset of operators,
and this seems to translate to less diversity in how a property can be
correctly expressed. This is further supported by Table 3, in which 13.88% of
correct RL submissions are syntactically unique but 19.55% of FOL submissions
are syntactically unique. Interestingly, only 12.21% of LTL exercises are
syntactically unique, which indicates that users frequently write the same
correct submissions, but fail to utilize the same structure as the oracle.

Table 5. Differences - Oracle and Hottest Hit Corr. Subs

Difference | # Occ | Rate
---|---|---
Upscaled to quantification | 22 | 12.22
Upscaled to nested quantification | 27 | 15.00
Upscaled to further nested quantification | 6 | 3.33
Downscaled removed nested quantification | 11 | 6.11
Downscaled removed quantification | 8 | 4.44
Different quantification domains | 9 | 5.00
Similar but different order of operands | 7 | 3.89
Similar but formed different sets | 11 | 6.11
Similar but different operator order | 13 | 7.22
Similar but additional trivial operator | 4 | 2.22
Expanded out formula | 2 | 1.11
No Change | 60 | 33.33
Total | 180 | 100.00

Second, to building a better understanding of why LTL exercises often do not
contain the oracle submission, and to further investigate the differences
users make compared to the oracle, we collected the “hottest hit” correct
submission - the correct submission that is submitted the most for a given
exercise. We then manually investigated what differences the user made when
writing their formula compared to the provided oracle. Table 5 displays for
each identified difference the number of hottest hit correct submissions that
have this difference (column # Occ) and the percentage that this accounts for
out of all hottest hit correct submissions (column Rate). The total number
(column # Occ) is 180, which is different than the number of exercises because
10 exercises had no correct submission and 7 exercises had 2 main differences,
bringing the count to 180.

One third of the hottest hit correct submissions are syntactically equivalent
to the oracle. For the remaining two-thirds, there are 35 submissions that are
very similar to the oracle, but involve minor differences, such as using an
interchangeable operator or swapping the order of operands for commutative
operators. These hottest hit submissions give some insight into how novices
approach LTL exercises differently than the oracle, which ultimately results
in the lower rate of occurrence of the oracle across LTL submissions. Of the
13 hottest hit correct submissions that are “similar but different operator
order,” a majority are LTL exercises in which the location of the temporal
operator always varies. In addition, the three of the four “similar but
additional trivial operator” are LTL exercises in which the user appends a
leading always operator.

Novice users prefer leading with temporal operators while the oracle solutions
inserts them close to the subformula of interest. For instance, a novice user
will write “always all a: A” while the oracle will use all a : A $|$ always.

The most prevalent difference is that novice users increase the degree of
quantification in the formula, which is seen in 55 (30.5%) of the hottest hit
correct solutions. In addition, two times the hottest hit correct solution is
an expanded out version of the oracle formula. This indicates that novice
users do not write concise formulas, and often prefer to try and explicitly
outline relationships between atoms or sequences of events. This is further
support by our observations in RQ6, where we see that a common source of
mistakes for novice users is to introduce mistakes when trying to explicitly
outline relationships using quantification instead of relational logic.

Given the preference for quantification, we wanted to follow up on this
observation to see to what degree novice users write less condense formulas.
Table 6 displays the AST difference between the oracle solution and all of the
correct submissions. Column Type conveys the type of logic the row is
displaying results for, with a final Total row that reflects all correct
submission. Column DifTot displays the average difference in total number of
AST nodes between the oracle and all correct submissions. The next four
columns (DifRL, DifPL, DifFOL, DifLTL) displays the average difference in
total number of AST nodes of each type of logic (RL, PL, FOL, and LTL) between
the oracle and all correct submissions. For these columns, a negative number
means the oracle had less AST nodes than the correct submissions. To give
context to how significant the difference in nodes is, column DifMag displays
average magnitude in difference between the oracle solution and correct
submissions.

Overall, Table 6 reinforces the implication from Table 5 that novice users
often write larger formulas. RL and PL exercises see the largest increase in
size, which is expected, as one of the common reasons the formula is larger
based on Table 5 is that the user is adding at least one new quantified
formula to their solution compared to the oracle. Not surprisingly, this
difference in the number of AST nodes translates to the oracle being on
average 0.38$\times$ smaller than the correct submissions for both RL and PL
exercises. However, even FOL exercises, which already have a quantified
formula, also see a large increase in the number of AST nodes, with the oracle
on average being 8.38 nodes smaller. Table 5 includes a breakdown of how the
up-scaling occurs, which highlights that users even up-scaled existing
quantified formulas to have nested or even further nested quantification.
However, for LTL exercises, while the novice correct submissions are still on
average larger, the difference is only 3.7 nodes. However, these 3.7 nodes
results in an oracle that is on average 0.77$\times$ the size of the correct
submission, which is similar to FOL exercises in which the 8.38 nodes means
the oracle is on average 0.78$\times$ the size of the correct submissions.

Table 6. AST Differences Between Oracle and Corr. Subs

| DifTot | DifRL | DifPL | DifFOL | DifLTL | DifMag
---|---|---|---|---|---|---
RL | -11.37 | -2.47 | -0.67 | -1.13 | -0.02 | 0.38
PL | -10.74 | -1.79 | -0.03 | -1.26 | 0 | 0.38
FOL | -8.38 | -1.89 | -0.83 | -0.55 | 0.00 | 0.78
LTL | -3.7 | -0.89 | -0.43 | -0.24 | -0.07 | 0.77
Total | -9.15 | -2.03 | -0.76 | -0.73 | -0.01 | 0.65

When novice modelers write a property correctly, they are likely to increase
the complexity of the formula.

Table 7. Common Mistakes Made by Novices (out of submissions that at least 10 novice users made) | Both | Over | Under | RL | PL | FOL | LTL
---|---|---|---|---|---|---|---
Mistake | Occ | #Sub | Occ | #Sub | Occ | #Sub | Occ | #Sub | Occ | #Sub | Occ | #Sub | Occ | #Sub
More complex quant. domain | 0 | 0 | 0 | 0 | 3 | 54 | 0 | 0 | 0 | 0 | 3 | 54 | 0 | 0
Narrowed quant. domain | 12 | 161 | 0 | 0 | 38 | 765 | 0 | 0 | 0 | 0 | 50 | 926 | 0 | 0
Different quant. domain | 2 | 55 | 0 | 0 | 7 | 186 | 0 | 0 | 0 | 0 | 9 | 241 | 0 | 0
Simplified quant. domain | 2 | 32 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 32 | 0 | 0
Upscaled quant. level trying to state relationship | 49 | 936 | 18 | 409 | 61 | 1124 | 24 | 509 | 0 | 0 | 96 | 1802 | 8 | 158
Downscaled quant. level leading to incorr. expr range | 12 | 186 | 7 | 145 | 11 | 236 | 0 | 0 | 0 | 0 | 27 | 503 | 3 | 64
Downsacled quant. level leading to new subformula | 1 | 10 | 4 | 63 | 0 | 0 | 0 | 0 | 0 | 0 | 5 | 73 | 0 | 0
Tried to inverted concept | 4 | 55 | 4 | 72 | 5 | 137 | 2 | 37 | 0 | 0 | 7 | 158 | 4 | 69
Trying to explicitly outline steps | 1 | 12 | 0 | 0 | 1 | 12 | 0 | 0 | 0 | 0 | 0 | 0 | 2 | 24
Incorrect use of operator | 38 | 711 | 22 | 380 | 25 | 539 | 10 | 175 | 2 | 37 | 63 | 1261 | 10 | 157
Missing operator | 0 | 0 | 8 | 121 | 3 | 62 | 0 | 0 | 0 | 0 | 8 | 125 | 3 | 58
Operator not commutative | 1 | 17 | 7 | 113 | 1 | 81 | 0 | 0 | 0 | 0 | 7 | 173 | 2 | 38
Failed to account for extension signatures | 3 | 49 | 1 | 23 | 0 | 0 | 4 | 72 | 0 | 0 | 0 | 0 | 0 | 0
Subportion of oracle | 1 | 41 | 6 | 141 | 8 | 139 | 2 | 29 | 0 | 0 | 12 | 281 | 1 | 11
Wrong understanding of exercise | 3 | 50 | 1 | 14 | 0 | 0 | 4 | 64 | 0 | 0 | 0 | 0 | 0 | 0
Total | 129 | 2315 | 78 | 1481 | 163 | 3335 | 46 | 886 | 2 | 37 | 289 | 5629 | 33 | 579

###  4.5. RQ5: How often do novice users make the same logical mistake?

As indicated by Table 3, novice users often repeat the same exact mistake and
even more often repeat the same underlying logical mistake. Understanding
these common mistakes can help researchers focusing on fault localization and
repair, as well as educators teaching formal methods. To give further guidance
on this, we explore a subset of “hot hit” submissions in which the same
syntactic submission is made at least 10 times. We manually investigated each
“hot hit” and label it with the classification of mistake(s) present compared
to the oracle solution.

Table 7 displays the common mistakes made broken down by classification of
submission and also type of logic. Columns labeled #S represent the number of
submissions that fit the classification or type of logic. Columns Occ
represent the number of representative “hot hit” submissions of that mistake,
which we view as the rate of occurrence of the mistake in the subset, columns
#Sub represents how many total submissions the “hot hit” submission represents
from the collection of all submissions made.

For our frequently repeated mistakes classification (column Mistake), half of
these classifications relate to novice’s introducing mistakes related to
quantification, which reiterates our observations in RQ2 that FOL exercises
gave novice users problems. Three of the four commonly occurring mistakes are
in relation to quantified formulas. By far, the most commonly occurring
mistake novices make is to upscale the level of quantification in an attempt
to explicitly outline relationships between different elements in the model,
where upscale means the submission inserted quantification or nested
quantification when the oracle solution had none or less nested
quantification. This issue occurred across 128 different hot hit submissions
which together represent 2,469 user submissions. Novice users often introduced
higher levels of quantification in order to attempt to assert different
multiplicity related constraints on the relationship between elements.

As an example, consider the following submission for inv1 for model
socialMedia:

// Every image is posted be one user.s: all x: Photo | some y: User | y->x in postso: all p : Photo | one posts.p

that accounts for 68 (13.28%) of the overconstrained submissions for inv1. To
correct this formula, the user should change the nested quantified to “one” to
prevent more than one user from having the post. Universal (‘all’) and
existential (‘some’) quantification are frequently focused on, but Alloy
supports 5 quantifiers, including no, one, and lone. While these later three
can be expressed using the first two, more prominent focus on their presence
can help mitigate mistakes where users are trying to replicate a relational
logic multiplicity relationship. Mistakes caused when the user upscales the
level of quantification often create underconstrained or both over- and
underconstrained faults and these mistakes frequently occur for both RL and
FOL exercises. As seen in the example above,

Hand in hand with upscaling, downscaling the level of quantification is a
common mistake that often results in correct subexpressions being applied to
the wrong range of elements, often because at some point in the constraint,
the novice user writes a relational join subexpression in which the left hand
side captures too broad of a set. This occurred in 30 different representative
“hot hits” that embodies 567 user submissions. As an example, consider the
submission for inv1 for model lts:

//Each state has at least a transition.s: some State.transo: all s: State | some s.trans

that accounts for 28 (38.89%) of the overconstrained submissions for inv1.
Here, the user effectively rights the same expression [x].trans; however, the
expression is too broadly applied to the set of all State atoms, instead of
checked for each individual State atom. As with upscaling, mistakes caused
when the user downscales the level of quantification often creates
underconstrained or both over- and underconstrained faults, but is almost
entirely a mistake encountered on FOL exercises. This is expected, as our
example highlights how downscaling can result in a multiplicity relationship
between atoms being viewed as “satisfied” because at least one atom of the
same type satisfies the relationship, which would make a model more
permissive.

Besides mistakes changing the level of quantification, the forth most common
overall mistake is for users to make the domain of a quantified formula too
narrow, which frequently produces an underconstrained submission. A narrower
quantification domain almost always occurred on models that had extension
signatures and the novice user used an extension signature for the domain in
place of the base signature. As an example, consider the following submission
for inv6 for model courses_v2:

// Students only work on projects of courses they are enrolled in.s: all s : Student | s.projects in s.enrolled.projectso: all p : Person | p.projects in p.enrolled.projects

which accounts for 68 (28.45%) of the underconstrained submissions for inv6.

Educators should focus on best practices for writing constraints that
establish multiplicity relationships between groups of elements in a model and
emphasize when the use of quantification is appropriate to express the
relationship per atom versus when not using quantification to express the
relationship per type of atom.

Outside of quantification, across all logic types, the second most common
mistake is the incorrect use of an operator. Our dataset on Github includes a
detailed breakdown of which specific operators are incorrectly applied and at
what rates. The most common misapplication is related to the use of the subset
operator and it’s negation. The subset operator is misapplied in 33 “hot hits”
representing 635 submissions and subset exclusion is misapplied in 10 “hot
hits” representing 185 submission. For subset mistakes, novice users often
used subset in place of set equality.

As an example, consider the following submission for inv7 for model graphs:

// Humans and robots cannot work togethers: all n : Node | Node in n.^adjo: all n : Node | Node = n.*adj

which accounts for 26 (26.67%) of the overconstrained submissions for inv7.
This example also highlights another issue that lead to several misapplication
of operators: novice users often make the wrong choice when selecting between
two closely related operators. Besides subset and set quality, as the above
example highlights, novice users also selected transitive closure (‘^’)
instead of reflexive transitive closure (‘*’), relational join (‘.’) instead
of cross product (‘->’), and implication (‘=>’) instead of biconditional
(‘<=>’) in multiple “hot hits” each.

Another common oversight was how the subset operator behaves if the left-hand
side evaluates to an empty set. For example, the following is a submission to
inv6 from the productionLine_v2 model that 20 novice users submitted (19.61%)
of inv7’s underconstrained submissions):

// Components built of dangerous parts are also dangerouss: all c: Component | c.parts in Dangerous => c in Dangerouso: all c: Component | some c.parts & Dangerous => c in Dangerous

In this case, if c.parts is empty, then c.parts in Dangerous evaluates to
true, which prevents any scenario from being generated in which there are
simply no dangerous components at all.

For subset exclusion, novice users often write “a !in B” instead of “no a &
B,” which similarly fails to account for the empty set. As an example, the
following is a submission to inv7 from the trash_fol model that 23 novice
users submitted (22.55% of inv7’s both over- and underconstrained
submissions):

// There is no deleted links: all f:File | f.link not in Trasho: no File.link & Trash

The novice’s constraint will be false if f.link is empty, even thought a file
having no link means that the file’s link cannot be in the trash.

Educators should focus on the difference between similar but different
operators, with a focus on subset and set equality as well as set intersection
and subset exclusion. In addition, educators should illustrate how logical
operators behave in corner case settings, such as when reasoning over the
empty set or extension signatures.

In addition, these common mistakes provide clear blueprints for researchers to
aid in improving debugging-oriented toolsets.

Researchers should consider a small collection of higher order mutants built around interchanging similar but different operators and changing the level of quantification of a formula to improve the suite of debugging tools for Alloy. For instance, for a faulty formula in the form “a !in b,” a possible fix that should be investigated is the second order mutant: “no a & b.” For the later, a faulty formula in the form “all a : A | some a.b,” a possible fix that should be investigated is the second order mutant: “some A.b.”

###  4.6. RQ6: How often are users “one” mistake away?

For incorrect submissions, we were curious to explore how often users were
effectively “one mistake away” from a correct solution. To investigate this,
we applied MuAlloy, a mutation testing tool (MuAlloyTemporal, ), to all
invalid submissions in the both, over and under categories. For each
submission, we generated all first order mutants and then checked if any of
the mutated models were equivalent to the oracle submission. If no
counterexample is found, we classified the submission as fixable and “one
mistake away.”

We were interested in two viewpoints: (1) how often were submissions one
mistake away and (2) what mutants corrected the faulty submissions. For the
first viewpoint, Table 8 depicts the frequency at which mutants correct faulty
submissions broken down by type of logic. Column #Fixes displays the total
number of mutants that fixed a faulty submission, column # Subf shows the
number of submissions that were fixed and column shows what percentage of
submissions for that type of logic # Subf is. The number of fixes is more than
the number of submissions fixed because some submissions could be fixed my
multiple different mutations. Therefore, column # Subm shows the number of
submissions that have multiple possible fixes and column shows what percentage
of submissions for that type of logic # Subm is.

Overall 10.88% of submissions can be correct by first order mutants. The rate
is notable lowest for first order logic exercises, in which mutants can only
correct 8.57%, and the lone PL exercise at 10.4%. However, RL and LTL have
nearly double the fix rate at 18.54% and 19.98% respectively. This trend holds
for submissions with multiple fixes, where the rate at which submissions have
multiple possible one-edit corrections is only 2.8% and 1.87% for PL and FOL
exercises but 5.08% and 5.8% for RL and LTL exercises.

For viewpoint two, Table 9 shows the number of mutants for each classification
of mutant operators (insert, delete, replace and exchange) that fix a faulty
submission broken down by type of logic, with the last rowing representing all
faulty submissions across all four types of logic. A majority of the fixes
come from replacement (46.27%) and insertions (31.07%), indicating that almost
correct faulty submissions often result from missing a constraint or selecting
the wrong operator. The high rate of replacement fixes is supported by
observations from our common mistakes (RQ6), where we found novice users
incorrectly selected between similar but different operators. Similarly, given
the prevalence of underconstrained faults as the second most common fault
type, it is also understandable why inserting an operator is a highly
beneficial mutation action. While deleting an operator occasionally fixes a
submission (15.74%), exchanging the left-hand and right-hand sides of an
operator rarely fixes a mistake (4.0%). While the replacement operator
produces the most fixes for RL, PL and FOL exercises, more LTL exercises are
fixed by insertion. This is caused by two main factors: (1) novices would make
the mistake of leaving out the prime operator when reasoning over the future
state of a mutable expression and (2) a common mistake by novice users is to
leave out a global “always” operator, accidentally producing a formula that is
largely correct but is only required to hold in the first state, as seen in
our example in Section 2.

To take a finer grained look at correcting mutant operators, Table 10 displays
the rate at which individual mutant operators fixed submissions. Column #Fixes
is the number of faulty submissions fixed and Percentage is what percentage of
fixed submissions the preceding #Fixes represents. A majority of the insertion
operators that fix mistakes are unary operator insertions, which accounts for
9.29% of all fixes, followed by binary operator replaces with 6.12% of fixes
and quantified operator replacement with 5.41% of fixes. UOI fixes for LTL
operators often involved inserting always somewhere in the formula, although
sometimes other temporal operators are inserted. This is expected, as we
observed common trends where novice users either omitted temporal operators or
tended to only place them in the beginning of formulas. Transpose insertions
often fixed formulas that used crossproduct expressions. For other types of
logic, a common UOI correction was inserting the transpose and transitive
closure operators. The frequency of BOR fixes is expected and in line with our
common mistakes from RQ6, in which most of the similar but different operators
that get mixed up are binary operators. QOR fixes almost always involve a
correction for a nested quantifier, in which one of the types of
quantification is changed.

Table 8. Frequency of Mutants Correcting Submissions Type | # Fixes | # Subf | % Subf | # Subm | % Subm
---|---|---|---|---|---
RL | 905 | 624 | 18.54 | 171 | 5.08
PL | 35 | 26 | 10.40 | 7 | 2.80
FOL | 2384 | 1642 | 8.57 | 359 | 1.87
LTL | 660 | 410 | 19.98 | 119 | 5.80
Total | 3984 | 2702 | 10.88 | 656 | 2.64
Table 9. Mutant Operator Classifications That Fix Type | Insert | Delete | Replace | Exchange | All
---|---|---|---|---|---
RL | 168 | 216 | 462 | 59 | 905
PL | 4 | 8 | 23 | 0 | 35
FOL | 731 | 330 | 1234 | 89 | 2384
LTL | 372 | 92 | 180 | 16 | 660
Total | 1275 | 646 | 1899 | 164 | 3984
Pct | 31.07 | 15.74 | 46.27 | 4.00 |
Table 10. Breakdown of Mutant Operators That Fixed Subs Mutant Op | # Fixes | Percent
---|---|---
Unary Operator Insertion (UOI) | 1221 | 9.29
Unary Operator Replacement (UOR) | 331 | 2.52
Unary Operator Deletion (UOD) | 159 | 1.21
Binary Operator Replacement (BOR) | 804 | 6.12
Binary Operator Deletion (BOD) | 270 | 2.05
Binary Operator Exchange (BOE) | 164 | 1.25
List Operator Deletion (LOD) | 217 | 1.65
List Operator Replacement (LOR) | 53 | 0.40
Quantifier Operator Replacement (QOR) | 711 | 5.41
Prime Operator Insertion (POI) | 54 | 0.41

First order mutants can fix a small number of mistakes, which is promising,
but second order mutants are likely to fix many more mistakes. To mitigate
scalability issues, second order mutants should focus on combinations that
build more restrictive constraints, such as insertion and replacement, since
novice users, on average, write overly permissive formulas.

##  5\. Threats to Validity

There exists several threats to the validity of our results. First, the
dataset we use does not contain any information related to what novice users
were thinking. Therefore, we are limited in some of the conclusions we can
form. For instance, we can conclude that users give up after 7.5 attempts, but
we cannot assume the user’s thought process, such as if the user gave up
because they were frustrated or they were bored. Second, the novice users are
all master’s students from the University of Minho (UM) and the University of
Porto (UP) between the fall of 2019 and the spring of 2023 semesters. While
there is breadth to the date range of the study, we do not know the details of
the educational performance and background of the master’s students, which may
lack diversity. Third, we discarded 760 submissions. These submissions
executed predicates whose names did not match any of the exercise names.

Besides content in the dataset, we used MuAlloy to explore which submissions
were almost correct. MuAlloy, and the Analyzer itself, does not support higher
order quantification. Occasionally, mutating some of the formulas produced
higher order formulas that could not be solved with the current tools. These
mutants are automatically pruned by MuAlloy during mutant generation. To limit
the impact of this issues, when presenting the number of submissions that can
be fixed by mutations, we include all submissions in this calculation, even if
MuAlloy is unable to produce any valid mutants for a submission. This allows
for our percentage of submissions that can be fixed to most accurately reflect
the possibilities of the current tool support.

##  6\. Related Work

Alloy4Fun. Closely related to our work, the creators of the Alloy4Fun dataset
have published an experience paper outlining the first semester that they used
Alloy4Fun in their classroom (alloy4fun, ). This paper focuses largely on
lessons learned utilizing Alloy4Fun in the classroom, but does contain some
preliminary analysis of the data collected. This data is from an early
benchmark and consists of 9 models and only 5000 executions. While some of our
analysis is similar, the experience report does highlight correct versus
incorrect submissions and commonly reported errors, a majority of our analysis
is more in-depth and spans the significantly larger version of the dataset
that contains over 3 years of information over 17 models and more than 97,000
executions.

User Studies and Empirical Studies Over Alloy. There have been a few user
studies exploring how developers work with Alloy. The most recent study
explored the debugging behavior of novice and expert users and discovered that
users struggle to refine Alloy predicates using only the visual representation
of scenarios (alloyformalise23study, ). Another recent study on novice Alloy
users found that if users are shown a small collection of valid and invalid
scenarios before writing a predicate, then users better understood what
behavior the user should be trying to codify into a constraint (negpos, ). In
addition, there was a user study that explored how users interact with
different enumeration strategies for Alloy (nelsonuserstudy, ). All of these
user studies enrich that same tools and education efforts our study promotes.
while our efforts focus on how to better teach and debug logical constraints,
these user studies collective highlight best practices for how to present and
guide users through the output of these constraints.

Tangent to our work, there is a static profile of 1,652 publicly available
Alloy models pulled from Github that investigates how often users engage with
different parts of Alloy’s grammar and explores the average size and
complexity of Alloy models. This study is not concerned with the accuracy of
the constraints within the model, but does give suggestions for educations
based on frequently used and underutilized features. These recommendations are
complementary to our recommendations.

##  7\. Conclusion

With the expansion of linear temporal logic into Alloy, Alloy is a commonly
used modeling language that is able to represent both static and dynamic
behavior of a system. Moreover, Alloy is packaged in the Analyzer, a scenario
enumeration toolset that presents users with visual representations of
behavior allowed or prevented by their model. As a result, there is a growing
body of work both to debug faulty models and to use the Analyzer in an
educational setting. To help guide future research directions for both of
these avenues, this paper explore a dataset of X submissions made by novice
users. We highlight several key findings, including common patterns in correct
and incorrect novice submissions, how long novice users will attempt an
exercise and the realistic effectiveness of existing mutant operators, which
are often deployed for fault localization and repair. Based on our
observations, we provide a series of recommendations for future researchers.

## References

  * (1) Akhawe, D., Barth, A., Lam, P.E., Mitchell, J., Song, D.: Towards a formal foundation of web security. In: 2010 23rd IEEE Computer Security Foundations Symposium. pp. 290–304 (2010)
  * (2) Alloy4Fun Benchmark: https://zenodo.org/record/4676413 (2022)
  * (3) Bagheri, H., Kang, E., Malek, S., Jackson, D.: A formal approach for detection of security flaws in the Android permission system. Formal Asp. Comput. (2018)
  * (4) Brida, S.G., Regis, G., Zheng, G., Bagheri, H., Nguyen, T., Aguirre, N., Frias, M.F.: Bounded exhaustive search of alloy specification repairs. In: ICSE (2021)
  * (5) Cerqueira, J., Cunha, A., Macedo, N.: Timely specification repair for alloy 6. In: Software Engineering and Formal Methods. pp. 288–303 (2022)
  * (6) Chong, N., Sorensen, T., Wickerson, J.: The semantics of transactions and weak memory in x86, Power, ARM, and C++. SIGPLAN Not. 53(4), 211–225 (2018)
  * (7) Danas, N., Nelson, T., Harrison, L., Krishnamurthi, S., Dougherty, D.J.: User studies of principled model finder output. In: SEFM (2017)
  * (8) Dyer, T., Nelson, T., Fisler, K., Krishnamurthi, S.: Applying cognitive principles to model-finding output: the positive value of negative information. Proceedings of the ACM on Programming Languages 6(OOPSLA1), 1–29 (2022)
  * (9) Galeotti, J.P., Rosner, N., Pombo, C.G.L., Frias, M.F.: TACO: Efficient SAT-based bounded verification using symmetry breaking and tight bounds. TSE (2013)
  * (10) Gopinath, D., Malik, M.Z., Khurshid, S.: Specification-based program repair using SAT. In: TACAS. pp. 173–188 (2011)
  * (11) Gutiérrez Brida, S., Regis, G., Zheng, G., Bagheri, H., Nguyen, T., Aguirre, N., Frias, M.: ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications. Association for Computing Machinery, New York, NY, USA (2023)
  * (12) Jackson, D.: Software Abstractions: Logic, Language, and Analysis. The MIT Press (2006)
  * (13) Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA (Aug 2000)
  * (14) Jovanovic, A., Sullivan, A.: Mutation testing for temporal alloy models. In: 26th ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, MODELS. pp. 228–238 (2023)
  * (15) Macedo, N., Cunha, A., Pereira, J., Carvalho, R., Silva, R., Paiva, A.C.R., Ramalho, M.S., Silva, D.: Experiences on teaching alloy with an automated assessment platform. In: Raschke, A., Méry, D., Houdek, F. (eds.) Rigorous State-Based Methods. pp. 61–77 (2020)
  * (16) Mansoor, N., Bagheri, H., Kang, E., Sharif., B.: An empirical study assessing software modeling in alloy. In: International Conference on Formal Methods in Software Engineering. pp. 44–54 (2023)
  * (17) Marinov, D., Khurshid, S.: TestEra: A novel framework for automated testing of Java programs. In: ASE (2001)
  * (18) Nelson, T., Barratt, C., Dougherty, D.J., Fisler, K., Krishnamurthi, S.: The Margrave tool for firewall analysis. In: LISA (2010)
  * (19) Sullivan, A., Wang, K., Zaeem, R.N., Khurshid, S.: Automated test generation and mutation testing for Alloy. In: ICST (2017)
  * (20) Sullivan, A., Zaeem, R.N., Khurshid, S., Marinov, D.: Towards a test automation framework for Alloy. In: Proceedings of the 2014 SPIN Workshop on Software Model Checking. pp. 113–116 (2014), http://doi.acm.org.ncat.idm.oclc.org/10.1145/2632362.2632369
  * (21) Trippel, C., Lustig, D., Martonosi, M.: Security verification via automatic hardware-aware exploit synthesis: The CheckMate approach. IEEE Micro (2019)
  * (22) Wang, K., Sullivan, A., Khurshid, S.: Automated model repair for Alloy. In: ASE (2018)
  * (23) Wang, K., Sullivan, A., Khurshid, S.: MuAlloy: A Mutation Testing Framework for Alloy. In: Proceedings of the 40th International Conference on Software Engineering (ICSE) Demo Track. pp. 29–32 (2018). https://doi.org/10.1145/3183440.3183488
  * (24) Wang, K., Sullivan, A., Khurshid, S.: Fault localization for declarative models in Alloy. In: ISSRE (2020)
  * (25) Wickerson, J., Batty, M., Sorensen, T., Constantinides, G.A.: Automatically comparing memory consistency models. In: POPL (2017)
  * (26) Zaeem, R.N., Khurshid, S.: Contract-based data structure repair using Alloy. In: ECOOP. pp. 577–598 (2010)
  * (27) Zave, P.: How to make Chord correct (using a stable base). CoRR abs/1502.06461 (2015)
  * (28) Zheng, G., Nguyen, T., Brida, S.G., Regis, G., Aguirre, N., Frias, M.F., Bagheri, H.: Atr: Template-based repair for alloy specifications. In: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis. p. 666–677. ISSTA 2022 (2022)
  * (29) Zheng, G., Nguyen, T., Gutiérrez Brida, S., Regis, G., Frias, M.F., Aguirre, N., Bagheri, H.: Flack: Counterexample-guided fault localization for alloy models. In: 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE). pp. 637–648 (2021)