Copyrightby
Allison Sullivan
2017The Dissertation Committee for Allison Sullivan
certifies that this is the approved version of the following dissertation:

Automated Testing and Sketching of Alloy Models

Committee:

Sarfraz Khurshid, Supervisor
Milos Gligoric
Christine Julien
Elizabeth Leonard
Dewayne PerryAutomated Testing and Sketching of Alloy Models

byAllison Sullivan, B.S.; M.S.E.

DISSERTATION
Presented to the Faculty of the Graduate School of
The University of Texas at Austin
in Partial Fulfillmentof the Requirements
for the Degree of
DOCTOR OF PHILOSOPHY

THE UNIVERSITY OF TEXAS AT AUSTIN
May 2017

To my husband, Bahji Ballard, my parents, Lori and Brian Sullivan, and my
grandparents, Arlene Wilding (R.I.P.), Thomas Sullivan (R.I.P) and Eileen
Sullivan, for their unconditional love and support.

Acknowledgments

I would like to thank the multitude of people who have helped me
throughout my journey as a PhD student. First, I would like to sincerely
thank my supervisor, Dr. Sarfraz Khurshid, for his support and guidance over
the years. Sarfraz always goes above and beyond for any of his students. Forme, as family health issues and even my own wedding popped up over the yearsof my PhD studies, Sarfraz never once hesitated to support and accommodate
me as needed. I am thankful to the time he took to help me throughout,from troubleshooting ideas to 6:59 am paper submissions. I would also like toextend my appreciation to my committee members, Dr. Milos Gilgoric, Dr.
Christine Julien, Dr. Elizabeth Leonard, and Dr. Dewayne E. Perry, for theirinvaluable guidance. In particular, I am grateful to Dr. Elizabeth Leonard forher helpful discussions and feedback, as well as her overall support from beinga mentor for me during my internship at the Naval Research Laboratory to
being one of my committee members.
I am thankful to my peers – current and former – in the Software
Verification, Vaildiation and Testing group: Hayes Converse, Nima Dini, Shiyu
Dong, Lisa Hua, Rui Qiu, Srinivasan Raghavendra, Kaiyuan Wang, Cagdas
Yelen, Razieh Nokhbeh-Zaeem, Lingming Zhang, and Mengshi Zhang. Overthe years, everyone in the group has always been welcoming and supportive,v

without hesitation. I’d like to extend a special thanks to Lisa and Hayes fortheir feedback as I prepared for my defense and for their help this past year.
I’d also like to thank Melanie Gulick, the graduate coordinator for Electricaland Computer Engineering department, who is always prepared for anything
and supportive through everything. I never once worried that I would besubmitting the wrong paperwork or missing a deadline.
I’d like to extended my gratitude to my coauthors over the years: Razieh Nokhbeh-Zaeem, Kaiyuan Wang, and Dr. Darko Marinov. I am thankful
to all the helpful discussions with Razieh as I was starting out as a graduate
student and I am thankful to have had someone to help guide by example
during a time period full of change. I am further thankful to fellow graduate
student from the SVVAT group, Kaiyuan Wang, who has helped me flesh out
research ideas (and sat through all my practice talks without complaint). I
am thankful to Darko for his willingness to provide feedback over my research
efforts and his invaluable perspective. Together with Kaiyuan, Darko, andSarfraz, I will have fond memories of late night Skype calls about the trials
and tribulations of sketching Alloy models while juggling 3 time-zones.
Most importantly, I’d like to thank my family and friends for all theirlove and support. To my close friends, Amber Mixon, Traci Overstreet andSamantha Pizzini, thank you for everything over the past few years from being
my bridesmaids to being my support system. Your friendships have neverfailed to lighten up my days. In particular I’d like to thank my best friend,
Traci Overstreet, who as an English teacher with no programming experiencevihas dutifully proofread my papers over the years. She is one in a billion,someone I can draw strength from and I’m thankful for her guidance (read:she is always right), love and support over the past 10 years.
To my husband, Bahji Ballard, thank you for everything from providing
a loving environment to taking on extra tasks when I had a deadline creeping
up to sitting through all of my excited research rambles with a blank but loving
look. To my parents, thank you for every opportunity you provided me withall my life and for every opportunity that you supported me through. To my
grandparents, whom were and are endlessly proud of me, may you rest in peace.
To my extended family, thank you for your unwavering support and eagerness
to hear about my graduate school adventures. Lastly, a specical shout out toMaya Kaul and her car for literally making this submission possible.
This work was funded in part by the Cockrell Foundation through their
bestowment of the Virginia and Ernest Cockrell, Jr. Fellowship and by the
National Science Foundation under Grant Nos.: CCF-0845628, CNS-0958231,
CCF-1319688, CNS-1218232, and CNS-1239498.

vii

Automated Testing and Sketching of Alloy Models

Publication No.
Allison Sullivan, Ph.D.
The University of Texas at Austin, 2017

Supervisor: Sarfraz Khurshid

Models of software systems, e.g., designs, play an important role inthe development of reliable and dependable systems. However, writing correct
designs is hard. What makes formulating desired design properties particularly
hard is the common lack of intuitive and effective techniques for validating
their correctness. Despite significant advances in developing notations andlanguages for writing designs, techniques for validating them are often not as
advanced and pose an undue burden on the users.
Our thesis is that some foundational and widely used techniques insoftware testing – the most common methodology for validating quality ofcode – can provide a basis to develop a familiar and effective new approachfor checking the correctness of designs. We lay a new foundation for testing
designs in the traditional spirit of testing code. Our specific focus is the Alloy
language, which is particularly useful for building models of software systems.

viiiAlloy is a first-order language based on relations and is supported by a SATbased analysis tool, which provides a natural backend for building new analyses
for Alloy. In recent work, we defined a foundation for testing Alloy models
in the spirit of the widely practiced unit testing methodology popularized by
the xUnit family of frameworks, such as JUnit for Java. Specifically, AUnit,
our testing framework for Alloy, defines test cases, test outcomes (pass/fail),and model coverage, and forms a foundation that enables development of new
testing techniques for Alloy.
To provide a more robust validation environment for Alloy, we build on
the AUnit foundation in four primary ways. One, we introduce test generation
algorithms, which automate creation of test inputs, which is traditionally oneof the most costly steps in testing. Two, we introduce synthesis of parts of
Alloy models using sketching by enumeration and constraint checking, where
the user writes a partial Alloy model and outlines the expected behavior using
tests, and our sketching framework completes the Alloy model for the user.
Three, we investigate optimizations to improve the efficacy of our core model
sketching techniques targeting improved scalability. Four, we introduce a second approach for sketching Alloy models that incorporates attributes from ourtest generation efforts as well as our initial sketching framework and uses equivalent formulas to outline expected behavior rather than tests. To evaluate ourtechniques, we use a suite of well-studied Alloy models, including some from
Alloy’s standard distribution, as well as models written by graduate students
as part of their homework.

ix

Table of Contents

Acknowledgmentsv

Abstract

viii

List of Tables

xiii

List of Figures

xiv

Chapter 1. Introduction
1.1 The Need for Testing in Alloy . . . . . . . . . . . . . . . . . .
1.2 Dissertation Overview . . . . . . . . . . . . . . . . . . . . . . .
1.2.1 AUnit Test Generation . . . . . . . . . . . . . . . . . .
1.2.2 Enumeration-Based Sketching of Alloy Models Using Test
Valuations . . . . . . . . . . . . . . . . . . . . . . . . .
1.2.3 Exploring Refinements To Enumeration-Based Sketchingof Alloy Models . . . . . . . . . . . . . . . . . . . . . .
1.2.4 Formula-Based Sketching of Alloy Models . . . . . . . .
1.3 Contributions . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.4 Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . .

7
7
8
10

Chapter 2. Background
2.1 Alloy . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2 AUnit: A Testing Framework for Alloy . . . . . . . . . . . . .
2.2.1 Test Case . . . . . . . . . . . . . . . . . . . . . . . . . .
2.2.2 Test Execution . . . . . . . . . . . . . . . . . . . . . . .
2.2.3 Coverage . . . . . . . . . . . . . . . . . . . . . . . . . .

12
12
14
15
16
18

Chapter 3. Related work
3.1 Automated Test Generation . . . . . . . . . . . . . . . . . . .
3.2 Program Sketching . . . . . . . . . . . . . . . . . . . . . . . .

21
21
23

x

1
3
5
5
6

Chapter 4. AUnit Test Generation
4.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.2 Illustrative Example . . . . . . . . . . . . . . . . . . . . . . . .
4.3 Automated Test Generation Using AUnit . . . . . . . . . . . .
4.3.1 Enumeration-based Input Generation . . . . . . . . . .
4.3.2 Coverage-Directed Input Generation . . . . . . . . . . .
4.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
4.4.1 Model coverage and mutation score . . . . . . . . . . . .
4.4.2 Finding real faults . . . . . . . . . . . . . . . . . . . . .
4.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

26
26
28
32
32
35
40
41
45
48

Chapter 5.
5.1
5.2
5.3

5.4
5.5

Enumeration-Based Sketching of Alloy Models Using Test Valuation
50
Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
50
Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
53
ASketch Framework . . . . . . . . . . . . . . . . . . . . . . . .
57
5.3.1 ASketch Eval : Evaluation-based sketching . . . . . . . . .
60
5.3.1.1 Optimizations . . . . . . . . . . . . . . . . . . .
62
Experimental evaluation . . . . . . . . . . . . . . . . . . . . .
65
5.4.1 ASketch Eval results . . . . . . . . . . . . . . . . . . . . .
68
Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
73

Chapter 6.
6.1
6.2
6.3

6.4

6.5

Exploring Refinements To Enumeration-Based Sketching of Alloy Models
74
Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
74
Subjects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
77
Multi-Threaded ASketch Eval . . . . . . . . . . . . . . . . . . .
78
6.3.1 Approach . . . . . . . . . . . . . . . . . . . . . . . . . .
78
6.3.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . .
81
Exploring Test Order . . . . . . . . . . . . . . . . . . . . . . .
83
6.4.1 Random Test Order Experiment . . . . . . . . . . . . .
84
6.4.2 Guidelines for a Sketching-Based Test Suite . . . . . . .
86
Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
94

xiChapter 7. Formula-Based Sketching Of Alloy Models
7.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.2 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.3 Sketching by Equivalence . . . . . . . . . . . . . . . . . . . . .
7.3.1 Building and Ordering a Test Suite . . . . . . . . . . . .
7.3.2 Completing the Sketch . . . . . . . . . . . . . . . . . . .
7.4 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
7.4.1 Subject Models . . . . . . . . . . . . . . . . . . . . . . .
7.4.2 ASketch Equiv Performance . . . . . . . . . . . . . . . . .
7.5 Summary . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

96
96
98
101
101
104
107
107
108
113

Chapter 8. Future Work115
8.1 Debugging Alloy Models . . . . . . . . . . . . . . . . . . . . . 115
8.2 Advancements for ASketch Eval . . . . . . . . . . . . . . . . . . 118
8.2.1 Exploring the Evaluator . . . . . . . . . . . . . . . . . . 118
8.2.2 Automated Test Ordering . . . . . . . . . . . . . . . . . 118
8.2.3 Iterative Sketching . . . . . . . . . . . . . . . . . . . . . 119
8.3 Bringing Testing to Other Declarative Language(s) . . . . . . . 121
Chapter 9.

Conclusion

124

Appendices125

Appendix A.

Alloy Analyzer with AUnit Toolset

126

Appendix B.

Homework question

132

Appendix C.

Mutation Testing for Alloy134

Appendix D.

Models for Evaluations

137

Bibliography

140

xii

List of Tables

2.1
2.2

Coverage requirements defined by AUnit. . . . . . . . . . . . .
Coverage for Val1 over corrected singly-linked list model. . . .

4.1
4.2

Targeting Constraint Templates. . . . . . . . . . . . . . . . . .
36
Subject Alloy modules. For each subject, lines of code (LOC ),number of predicates (# p), number of basic signatures (# basicsig), number of binary relations (# bin rel ), number of ternary
relations (# ter rel ), number of variables, number of primaryvariables and number of clauses are shown. Pair (a, b) shows
minimum (a) and maximum (b) over all commands in the model. 40
Test suite generation and execution. . . . . . . . . . . . . . . .
42
Mutation Testing. . . . . . . . . . . . . . . . . . . . . . . . . .
44Known Buggy Models – AUnit test generation fault finding ability. 45
Homework submissions – AUnit test generation fault finding
ability. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
45

4.3
4.4
4.5
4.6
5.1
5.2
5.3
5.4

Possible values for non-recursively defined holes. . . . . . . . .
ASketch Gen details . . . . . . . . . . . . . . . . . . . . . . . .
ASketch Eval performance for finding the solution. Times are inseconds. ⊥ indicates a timeout (>15 min). . . . . . . . . . . .
Number of calls to the Evaluator using dynamic pruning expressions and the full test suite. ⊥ indicates a timeout (>15min). . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

19
20

59
68
69
71

6.1
6.2
6.3

Multi-threaded Experiment Results Using ASketch EvalSub . . . .
82
Results for 100 Random Test Order Execution using ASketch EvalSub . 85
Characteristics of the first 5 tests in the best and worst testorders. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
88

7.1

ASketch Equiv performance. Times are in seconds.

. . . . . . .

110

C.1 Mutation Operators . . . . . . . . . . . . . . . . . . . . . . . .

135

xiii

List of Figures

2.1
2.2
4.1
4.2

5.1

5.2
5.3
6.1

7.1
7.2

A faulty Alloy model for a singly-linked list. . . . . . . . . . .
Graphical valuations: (a) (b) (c) and their corresponding textual representations(d) (e) (f). . . . . . . . . . . . . . . . . . .

14

A faulty Alloy model for a singly-linked list. . . . . . . . . . .
(a) Instance: empty list. (b) Non-instance: acyclic list with
1 node. (c) Non-instance: cyclic list with 1 node. (d) Passing test with valuation (a). (e) Failing test with valuation (b).
(f) Passing test with valuation (c). . . . . . . . . . . . . . . .

28

29

Eight valuations shown graphically. Of these, T 0, T 3, and T 4
are valid valuations for the expected acyclicity property, andT 1, T 2, T 5, T 6, and T 7 are invalid. L0 is the list atom. N 0,
N 1, and N 2 are node atoms. . . . . . . . . . . . . . . . . . . .
A partial model of a singly-linked list. . . . . . . . . . . . . . .
Modified Alloy grammar used for holes in ASketch. . . . . . .

53
54
58

First four tests from the best test order (top) and first four testfrom worst order (bottom) for the binary tree variant with 6
holes. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .

87

A singly-linked list model with one specified acyclic predicate
and one sketch predicate. . . . . . . . . . . . . . . . . . . . . .
Two invalid valuations with the same coverage. . . . . . . . .

98
113

xiv

16

Chapter 1
Introduction

Software designs play a key role in the development of reliable and dependable systems. In particular, modeling software designs enable developers
to reason over the system as a whole before development and without focusing on the implementation level details, resulting in earlier detection of highlevel design faults. Recent years have seen much progress in the introduction ofand support for declarative languages, which are well suited for conveying software designs [2, 3, 69]. However, declarative languages often come with steep
learning curves for beginning users, in part because declarative languages are
typically very different in nature from commonly used imperative languages
such as Java and C++. Additionally, even for advanced users, writing correct models in hard, as these languages often lack robust integrated development environments and testing-oriented tool support. For instance, there isno equivalent of Eclipse or Net-Beans for Java in the declarative setting. As a
direct consequence, model validation is ad-hoc, where users over time develop
their own tips and tricks for checking their models, but there is no set testing
infrastructure for end users to leverage. Together, these factors place a burden
on the end-user and limit their ability to write correct models, eroding someof the benefits to these languages, such as the early detection of design faults.
1

Our thesis is that some foundational and widely used techniques insoftware testing – the most common methodology for validating quality ofcode – can provide a basis to develop a familiar and effective new approachfor checking the correctness of designs. We lay a new foundation for testing
designs in the traditional spirit of testing code. Our specific focus is the
Alloy language, which is particularly useful for building models of softwaresystems. Alloy is a first-order language based on relations and is supported
by a SAT-based analysis tool, which provides a natural back-end for building
new analyses for Alloy. In recent work [70, 71], we defined a foundation for
testing Alloy models, AUnit, in the spirit of the widely practiced unit testing
methodology popularized by the xUnit family of frameworks, such as JUnit
for Java. Specifically, AUnit defines test cases, test outcomes (pass/fail), andmodel coverage, and forms a foundation that enables development of new
testing techniques for Alloy.
To further provide a validation environment in Alloy, we build on our
AUnit foundation in four primary ways. One, we introduce test generation
algorithms, which automate creation of test inputs, which is traditionally oneof the most costly steps in testing [71]. Two, we introduce synthesis of partsof Alloy models using sketching based on tests, where the user does not needto try and specify the entirety of the Alloy model. Instead, the user writes
incomplete Alloy models and provides tests that represent “examples” (orcounterexamples) of expected design properties which our sketching approach
uses to produces complete models [75]. Three, we investigate optimizations for2

our sketching technique, focusing on improving scalability. Four, we introduce
a second approach to sketching Alloy models that is formula-based rather
than test-based and utilizes existing ad-hoc validation practices for Alloy. To
evaluate our techniques, we use a suite of well-studied Alloy models, including
some from Alloy’s standard distribution, as well as models written by graduate
students as part of their homework.

1.1

The Need for Testing in Alloy
The Alloy language offers expressive operators, e.g. quantification andtransitive closure, that allow succinct formulation of complex properties. However, the expressiveness and succinctness can make Alloy models look deceptively simple. Formulating them correctly and reasoning their correctness canbe quite challenging, especially for non-experts.
A key strength of Alloy is the Alloy Analyzer [31, 73], an automatic
tool for scope-bounded reasoning where the analysis results hold for the given
scope, i.e., bound on the universe of discourse. Alloy users write commands,
which take two forms: (1) simulation, where the analyzer finds an instance,i.e., a valuation to the relations in the model such that the formula evaluates
to true; and (2) checking, where the analyzer finds a counterexample, i.e., avaluation such that the negation of the formula evaluates to true. Technically,
the underlying analysis for both forms is the same – solving logical constraints.
The analyzer translates the Alloy model to a propositional formula with respect
to the scope, uses off-the-shelf SAT solvers to solve it, and translates SAT
3

solutions to Alloy instances or counterexamples.
Since models written in Alloy are logical constraints, Alloy models have
two basic kinds of faults – underconstraint, where the formula allows valuations that the user wanted to rule out; and overconstraint, where the formula
rules out valuations that the user wanted to allow. Alloy users employ twobasic ad-hoc methods to validate their models. One, they use simulation to
enumerate and inspect valuations to detect if some expected ones are missing
or some invalid ones are present. Two, they use checking to validate expected
properties between different formulas, e.g., checking (bounded) equivalence
between two definitions that they expect are equivalent.
However, there are notable limitations to the existing ad-hoc validation
techniques for Alloy. For simulation, the approach is limited by: (1) the orderin which the Alloy Analyzer enumerates valuations is determined by the SAT
solver, (2) the number of valuations to inspect can be hundreds, thousands oreven hundreds of thousands and (3) despite the challenges of the order and sizeof valuations to inspect, the developer needs to notice either the absence of an
instance or the incorrect structure of instance(s). For checking, the user needs
to ensure that the check itself is not building false confidence in the correctnessof the model. For example, when checking a logical relation, say implication
between formulas f and g, i.e., f ⇒ g, it is standard practice to increase
the scope and re-run the analyzer to increase confidence that the implicationindeed holds; however, if f is overconstrained and simply false, increasing thescope only leads to a false increase in confidence. Similarly, when simulating4

f ∧ g, and finding a solution, the user may inadvertently fail to notice that g
is true but only vacuously.
Furthermore, validating the correctness of an Alloy model is conceptually very different from the widely used practice of testing imperative programs, which is conceptually simple: create some inputs (with respect to somecoverage criterion or otherwise), run the program against them, and check theoutputs. Before providing tool support for testing Alloy models, we first needto define conceptually what a test case and test execution should be within
Alloy’s declarative setting, in which we do not follow a sequential executionof program statements, but rather explore the space of all possible solutions
allowed by the program. To address these challenges, our previous work [72],
introduced basic definitions for unit tests, test execution, and model coveragefor Alloy to lay the foundation of testing Alloy models in the traditional spiritof testing. In Chapter 2, we will outline these concepts in detail through an illustrative example in which we step through building, revealing and correcting
a faulty Alloy model.

1.2

Dissertation Overview

1.2.1

AUnit Test Generation
We introduce two new approaches for automated test generation thatcreate test suites following the spirit of traditional black-box and white-box
testing. The black-box test generation technique, AGenBB , creates suites that
include all instances in the given scope and brings the spirit of bounded exhaus-

5

tive testing for imperative programs [8, 48] to Alloy models. The white-box
test generation technique, AGenW B , brings the spirit of coverage-directed input generation for imperative programs [9, 23, 59] to Alloy models. AGenW B
reduces the problem of directed test generation for Alloy to constraint solving where model coverage requirements (introduced by AUnit) are part of theconstraint. AGenW B iteratively builds a minimal set of (non-isomorphic) tests
to meet the chosen criterion. Both techniques use Alloy’s SAT-based backend for test generation and can be adapted to create suites based on different
solving strategies [45, 52].
1.2.2

Enumeration-Based Sketching of Alloy Models Using Test
Valuations
We introduce the first approach for sketching Alloy models, where theuser does not need to attempt to write complete Alloy models. Our key insightis that valid and invalid valuations enable a user to specify the expected behavior of an Alloy model, providing a foundation for sketching Alloy models.
To sketch an Alloy model, the user writes a partial Alloy model with holes
and provides some valid and invalid valuations for the desired model, and thesketching infrastructure completes the partial model with respect to the given
valuations. Our technique, ASketch Eval , iteratively explores the space of all
possible solutions to the sketch, using constraint checking – rather than constraint solving – and utilizes various optimizations to efficiently search thisspace and report a solution.

6

1.2.3

Exploring Refinements To Enumeration-Based Sketching of
Alloy Models
We introduce two optimizations focused on improving ASketch Eval , ourenumeration-based sketching technique, which has shown to be an effective
technique for sketching Alloy models. First, we outline a multi-threaded implementation of ASketch Eval and evaluate the effectiveness of a parallel approach to exploring the solution space. Second, we perform an exploratory
study of the impact the order of test valuations – one of the key user inputs
to ASketch Eval – has on the run-time. The outcomes of the study are used
to derive insight into both the overall desirable attributes of a sketching test
suite as well as a best practices approach for selectively ordering a test suitefor sketching.
1.2.4

Formula-Based Sketching of Alloy Models
Prior to the introduction of AUnit, Alloy users leverage multiple ad-

hoc methods for validating their models, typically related to leverage existing
Alloy infrastructure such as instance enumeration or assertion checks for the
existence of expected logical relationships between formulas. This latter approach often includes the use of equivalence checks between two formulas theuser expects to be equivalent. For formula-based sketching, we utilize thisexisting validation practice and introduce ASketch Equiv , which instead of requiring a user to provide a suite of test valuations, requires the end user tosupply an equivalent formula. ASketch Equiv combines AGenW B , test ordering

7

observations, and ASketch Eval to provide a second approach to sketching Alloymodels.

1.3

Contributions
We make the following contributions:• Automated test generation for Alloy We introduce the idea of automated test generation for Alloy and techniques to generate tests for
Alloy models in the spirit of traditional black-box and white-box test
generation, titled AGenBB and AGenW B respectively.
• Test Generation Experiments We perform a two-fold evaluation toshow the efficacy of our approach. One, we compute model coverage andmutation score (which is often considered as the strongest test adequacy
criterion in imperative programs) for the generated tests. Two, we show
our approach finds real faults in several subjects, including all 19 faulty
models submitted as solutions to a homework question in a graduate
course in our Department.
• ASketch. We introduce the idea of sketching Alloy models using valuations through the introduction of ASketch Eval , an enumeration-based
technique for sketching Alloy models based on evaluation alone (without
any constraint solving) for completing sketches of Alloy models.
• ASketch Eval Optimizations. We introduce a suite of optimizations
designed for relational expressions and logical formulas to improve the8efficacy of our techniques.
• ASketch Experiments. We present an experimental evaluation withsmall but intricate Alloy formulas to demonstrate that our enumeration
based sketching technique introduces a promising approach for sketching
Alloy models.
• Multi-Threaded ASketch Eval . We present a multi-threaded approachto ASketch Eval , which focuses on exploring the space of potential solutions to a sketch in parallel, and perform an evaluation over our core
set of Alloy sketching models, focusing on the effectiveness of a parallel
search over the solution space.
• Random Test Order Experiments. We investigate the effect of thetest order, one of the main inputs to ASketch Eval , on the overall run-timeof the technique. Based on insights from 100 random test orders over
all models in our ASketch evaluation model suite, we produce a series ofguidelines for producing and ordering tests for sketching.
• Formula-based sketching. We present a second approach to sketching, ASketch Equiv , in which sketching is driven by an equivalent formula
rather than a collection of test valuations. We combine attributes of
AGenW B , ASketch Eval and test ordering observations to facilitate sketching.
• ASketch Equiv Experiments. We present an experimental evaluation
over a small but robust suite of Alloy models, where the focus is on9

models with two distinct formulations of the same property. Our results explore the effectiveness of AGenW B generated test suites over one
formula as a basis for sketching a formula with a different structure.
• Embodiments. For AGenBB and AGenW B , we implement a prototype
that embodies our techniques as well as the theoretical foundations introduced previously by AUnit, specifically to provide test case execution
and code coverage computation in addition to automated test generation. We implement a prototype tool for ASketch that enables our range
of optimizations and focuses primarily on the ASketch Eval portion of theASketch framework. Attributes of both tools are combined together toform a prototype tool-set for ASketch Equiv . Both sketching-based tool
sets focus on finding the first solution to the sketch by default, but can
additionally find some or all of the solutions. All tool-sets were used tofacilitate our experiments across the various techniques.

1.4

Organization
The remainder of this dissertation is outlined as follows. In Chapter

2, we outline the background material for Alloy and AUnit through a guided
example of building and correcting a singly-linked acyclic list model. Chapter
3 highlights the related work for both our test generation and sketching efforts
for Alloy. Chapter 4 presents our two AUnit test generation techniques, as wellas an evaluation comparing and contrasting the two approaches. Chapter 4
through Chapter 6 focus on sketching Alloy models. Chapter 5 introduces our10ASketch framework and details an enumeration-based approach to sketchingthat utilizes our AUnit test cases. Chapter 6 dives into two optimizations
that serve to strictly improve the run-time of ASketch and provide insight into
how to order and structure the input test suite. Chapter 7 presents a second
approach to sketching Alloy models, which combines attributes from Chapters
4, 5 and 6 to develop a formula-based sketching approach. Finally, Chapter
8 outlines some proposed future research directions based on the work in thisdissertation and Chapter 9 provides on overall summary of our work.

11

Chapter 2
Background

2.1

Alloy
An Alloy model consists of five kinds of paragraphs:

1. A signature (sig) declares a set of atoms, which can be viewed asuser defined types. Each signature can declare 0 or more relations. In
Alloy, relations are similar to fields of an object in the Object Oriented
paradigm.
2. A fact (fact) is a formula that must always evaluate to true for any
valid solution to the model. A fact paragraph allows a user to explicitly
declare fact formulas. A fact can also be implicitly added to the model(e.g. multiplicity constraints from signature paragraphs).
3. A predicate (pred) is a named (and optionally parameterized) formulathat can be invoked. A predicate can invoke other predicates, but the
Alloy Analyzer does not support recursive predicates.
4. An assertion (assert) is a formula intended to be checked for validity.
5. A command (run or check) executes a predicate or checks an assertion. A run command directs the analyzer to find an instance to the12corresponding predicate, i.e., a solution to the conjunction of all fact
formulas and the predicate formula. A check command directs the analyzer to find a counterexample to the corresponding assertion, i.e., asolution to the conjunction of all fact formulas and the negation of theassertion formula.
A command may invoke a formula anonymously by providing its body
explicitly; the empty body “{}” represents the formula “true”. Each command(implicitly or explicitly) specifies a scope – a bound on the universe of discourse– and the instances and counterexamples generated are within that scope. A
command may include an expect clause: "expect 0" means no solution is
expected and "expect 1" means some solution is expected.
The Alloy Analyzer executes a command for an Alloy model and reports
the constraint-solving results. If instances or counterexamples are found, theuser can inspect them (e.g., iterate through them) in a variety of different textual and graphical formats. The analyzer adds symmetry-breaking predicatesto remove isomorphic solutions and reduce the total number of solutions [61].
While the analyzer’s default symmetry breaking does not remove all isomorphisms, a number of previous approaches [20, 36] provide non-isomorphic enumeration for Alloy.
To see how these paragraphs piece together to form an Alloy model, we
will step over one possible model for a singly linked list seen in Figure 2.1. The
keyword module names the model, and allows for the model to be imported

13

module list.v.1.0
one sig List { header: lone Node }sig Node { link: lone Node }pred Acyclic { all n : Node | n !in n.^link }Figure 2.1: A faulty Alloy model for a singly-linked list.

into other models. Two signature paragraphs (one sig List and sig Node)are declared, which introduces a singleton set of a list atom – due to the useof the multiplicity constraint one – and a set of node atoms respectively. Bothsignatures declare a binary relation. The relation header maps lists to nodes
while link maps nodes to nodes. Both header and link restrict the mappings
by using the keyword lone, e.g. link maps one Node atom to zero or one Nodeatom. The predicate Acyclic defines acyclicity to constrain that there is no
cycle in the list. The body defines a universally quantified formula that reasons
over the domain of all Node atoms (all n : Node) . Within the quantified
formula, we use negation (!), set inclusion (in), relational composition (.) andtransitive closure (^) to build a formula which states: “n is not in the set ofnodes produced following 1 or more traversals using n’s link relation”, e.g. n
is not reachable from itself.

2.2

AUnit: A Testing Framework for Alloy
The section highlights AUnit, our testing framework for Alloy, and in-troduces the concepts of test case, test execution, and test coverage, which canbe used to validate Alloy models by checking directly for both overconstraint14and underconstraint faults, AUnit is inspired by the series of x-Unit frameworks frequently used to test imperative, object-oriented code. This subsections summarizes the efforts of two publications: “Towards a Test Automation
Framework for Alloy” and “AUnit: A Testing Framework for Alloy.”1
2.2.1

Test CaseA test case is a pair hv, ci where v is a valuation: a (potentially partial)

assignment of values to sets and relations in the model; and c is either theempty command (i.e., c = ) or any valid Alloy command over the model,
including but not limited to predicates and assertions in the model. Thus, atest may specify an assignment without stating any specific Alloy command.
Moreover, a test may have commands other than those already given in themodel. Additionally, the command acts as a label to indicate if the valuationv should be valid or invalid w.r.t. the existing model. Thus, Alloy users
can create tests to directly check for underconstraint (when a given invalid
valuation is allowed by the formula) and overconstraint (when a given valid
valuation is not allowed by the formula).
1“Towards a Test Automation Framework for Alloy” in Proceedings of the 2014 International SPIN Symposium on Model Checking of Software by A. Sullivan, R. Nokhbeh-Zaeem,
S. Khurshid, and D. Marinov. I was the lead student author of this paper and co-designed
this work with S. Khurshid and R. Nokhbeh-Zaeem, with D. Marinov providing valuableguidance on writing the paper. This work is further explored (developed into a toolset andevaluated) in my master’s thesis titled “AUnit: A Testing Framework for Alloy” in which I
am the sole author.

15

List0

header

List0

Node0

header

Node0

List0

Node0

link

link

(a)

(b)

(c)

pred Val1() {some disj List0: List {some disj Node0: Node {pred Val2() {some disj List0: List {some disj Node0: Node {pred Val3() {xsome disj List0: List {some disj Node0: Node {List = List0
Node = Node0
header = List0->Node0no link

List = List0
Node = Node0
header = List0->Node0
link = Node0->Node0}

List = List0
Node = Node0
no headerlink = Node0->Node0

}

}

}

}

(d)

}

(e)

(f)

Figure 2.2: Graphical valuations: (a) (b) (c) and their corresponding textual
representations(d) (e) (f).

2.2.2

Test Execution
A test case t = hv, ci passes if v is a solution to the constraint-solving

problem for the command c. If c = , a test passes if v is a solution to theconstraint-solving problem for the command "run {} for s" where s is thescope required for v. Otherwise, t fails.
To highlight both the motivation for AUnit and how the concepts workin practice, we will step through producing and executing an AUnit test suitefor our singly-linked list in Figure 2.1. Figure 2.2 depicts three valuation for
our linked list model in both a graphical format and a textual format. The
valuation simply states explicitly how to populate the sets and relations of
the model. The keyword disj requires the elements in the associated set to
be distinct, i.e. “some disj Node0, Node1 : Node ” means Node0 and Node1

16

have to be different Node atoms. Using the valuations in figure 2.2(a), we canmake the following commands:
Test1: run { Val1 and Acyclic[] }Test2: run { Val2 and !Acyclic[] }Test3: run { Val3 and Acyclic[] }Two of our tests, Test1 and Test3, expect the valuation to satisfy
Acyclic, while one test, Test2, expects the valuation to violate Acyclic. For
Test3, although Node0 has a self-loop, we expect Val1 to be acyclic because
Node0 is not in the list. However, when we execute Test3, we discover the test

has failed. Our model is overconstrained : we have ruled out a valuation wewant to allow. When defining acylicity, we created a universally quantified formula whose domain is “Node”, meaning our acyclic constraint (n !in n.link)
has to be satisfied by all Node atoms, regardless of if they are in the list or not.
To correct this, we can change our universally quantified formula’s domain toreason over nodes in the list, producing:

module list.v.1.1
one sig List { header: lone Node }sig Node { link: lone Node }pred Acyclic { all n : List.header.*link | n !in n.^link }Our new formula changes the domain of the quantified formula to be
the set of nodes in the list by using reflexive transitive closure (*) to get the17nodes reachable following 0 or more traversals along the header’s link relation.
Note, our use of reflexive transitive closure over transitive closure enables thelist’s header to be included in the domain, allowing for lists of size one to beacyclic.
2.2.3

Coverage
AUnit’s coverage requirements require the tests to exercise various dif-ferent values Alloy expressions and formulas may take as well as the different
ways those values may arise. AUnit introduces coverage requirements for four
Alloy elements: signatures, relations, expressions and formulas. Table 2.1 details these coverage requirements. The requirements outline different “shapes”
for each construct (size and/or value). For signatures, relations and expressions, there are three requirements that each must evaluate to: an empty set,a singleton set, and a non-empty non-singleton set. On the other hand, formulas should evaluate to true and false. Furthermore, quantified formulas mustbe evaluated over an empty domain, a singleton domain, a non-empty nonsingleton domain, and additionally require the formula bodies to also evaluate
to true and false across these different settings.
AUnit formalizes these requirements into 8 coverage metrics. The metrics can be narrow such as predicate coverage, which focuses on the coverage of
all expressions and formulas that appear in predicate paragraphs only, or wider
ranging such as expression coverage, which looks at all expressions, regardlessof their origin in the model. For the coverage reported in this dissertation,

18

Table 2.1: Coverage requirements defined by AUnit.
Alloy
ConstructSignature s

Relation r

Expression e
Formula fCardinality

Coverage
Requirement|s| = 0|s| = 1|s| ≥ 2|r| = 0|r| = 1|r| ≥ 2|e| = 0|e| = 1|e| ≥ 2
f = truef = false|d| = 0|d| = 1, b = True|d| = 1, b = False|d| ≥ 2, b = True|d| ≥ 2, b = True & False|d| ≥ 2, b = False

we will use model coverage: coverage calculated over all signatures, relations,expressions and formulas present anywhere in the model. Model coveragesubsumes all other 7 coverage metrics.
Coverage for a test case t, where t = hv, ci ∈ T , is computed as a set ofmaps hπt , ωt , λt i where: (1) πt maps each Alloy expression invoked by c to theset(s) of tuples it evaluates to for valuation v; (2) ωt maps each Alloy formula
invoked by c to the boolean value(s) it evaluates to for valuation v; and (3)λt maps each signature and relation to the set(s) of tuples it evaluates to forvaluation v. Table 2.2 shows the model coverage for Test1.

19

Table 2.2: Coverage for Val1 over corrected singly-linked list model.
Alloy ConstructSignature s
Relation r
Expression e
Formula f&Cardinality

Model list.v.1.2 Constructs
List
Node
headerlink
List.header.*link
n.^link
n !in n.^link

all n : List.header.*link | n !in n.^link

20

Test1 Coverage|s| = 1|s| = 1|r| = 1|r| = 0|e| = 1|e| = 0f = Truef = Trued = 1, b = True

Chapter 3
Related work

3.1

Automated Test Generation
This section highlights work done in similar spirits to our automatedtesting advancements for Alloy, outlined in Chapter 4. Efforts to introduce
support for testing in its traditional form for Alloy can be found in a numberof previous projects. For example, the Alloy tool-set has built in support forlabeled commands, and allows running all commands; moreover, each command can use the expect clause to indicate whether a solution is expected
or not. Indeed, we leverage this functionality to implement AUnit [72] tests.
Moreover, Montaghami and Rayside’s support for partial instances [50, 51]
takes inspiration in part by the need to bring traditional testing ideas to Alloy. Furthermore, the Alloy analyzer’s support for highlighting unsat cores
helps with debugging faulty unsatisfiable formulas; we conjecture AUnit tests
together with unsat cores provide an effective basis for introducing fault localization [34] and program repair [21] for Alloy. To our knowledge, AUnit is
the only previous project that describes test cases, test execution, and model
coverage (in their traditional spirit) for Alloy.
Symmetry-breaking [20, 37, 60] substantially reduces the number of so-

21

lutions to inspect and plays a key role in traditional analyses using Alloy.
Aluminum [52] limits the instances to minimal solutions to further ease theunderstanding of the models using instance inspection. Our test generation
techniques are orthogonal to and can be applied in synergy with symmetry
breaking, minimal instances, and other scenario exploration techniques [45].
Testing constraint programs in general has been addressed in previous
work. For example, a test framework was built for the constraint language
OPL which focuses on using an oracle model to derive tests that look for
differences in behavior based on conformity properties and provides guidance
for fault localization [42, 43]. Moreover, previous work introduced a reductionof testing UML models to satisfiability checking by encoding the model and aproperty of interest, and using SAT [64]. Other related efforts have focused onleveraging a range of UML diagrams (sequence, class, and activity diagrams)
in conjunction with pre-/post-conditions and invariants in OCL to develop
a few different methodologies for guiding test input generation, stimulating
execution of UML models, and observing their behavior [14, 15, 56].
Numerous efforts have been made to introduce unit testing to thedeclarative language Prolog, and the collection of languages inspired by Prolog. SWI-Prolog is a commonly used Prolog implementation which includes aunit test framework called PLunit [77, 78] and provides tool support for test
coverage and test reporting. For ECLiPSe Prolog, a constraint language basedon Prolog, in addition to a bare bones unit testing framework, work has addressed automated test input generation [58]. Additionally, Mercury, a Prolog
22inspired language with a static type system, has support for unit tests in a
declarative setting [12]. Moreover, in the context of functional programs, e.g.,
in Haskell, automated testing is common practice [10].
Our focus in Chapter 4 is on testing programs written in Alloy, a declarative language. There is a rich history of using declarative specifications totest imperative programs [24] with logical constraints playing an importantrole in systematic testing[8, 11, 22, 25, 27, 29, 39, 48, 53, 57].
While a primary role for tests is in bug finding, a number of recent
projects have leveraged tests for automated debugging [21, 44, 46, 76] and program synthesis [19, 38, 65]. AUnit enables defining such approaches [75] forAlloy.

3.2

Program Sketching
In this section, we will highlight work done in similar fields to sketching

Alloy models, the focus on Chapters 5, 6, and 7. In particular, we introduce
the first approach to sketching Alloy. Program sketching [5, 28, 32, 62, 63, 65–
68] is a form of program synthesis, which is a mature yet active research
topic [7, 17–19, 26, 38, 41, 47, 54, 62]. Researchers have proposed program synthesis techniques for a number of languages, including synthesis of logic programs, e.g., using inductive synthesis based on positive and negative examples, which is a well-studied field [13]. However, prior work has not addressed
the complexity of synthesis in the presence of quantifiers, transitive closure,
relational operators, and more generally, formulas that express structurally
23complex properties, which are the focus of our work.
The Sketch system takes as input a partial program in the Java-like
Sketch language, and uses SAT and inductive synthesis in a counterexampleguided loop [65]. Sketch requires users to provide generators for candidate
expressions for expression holes. The JSketch tool translates Java to Sketch
to allow sketching Java programs [32]. Sketch4J [28] introduces an optimized
backtracking search for completing Java sketches. Some tools focus on specific subclasses of programs to sketch, such as PSketch for concurrent data
structures [67].
Using an enumeration-based approach to synthesize a program has beenused before for Syntax-Guided Synthesis (SyGuS) [6]. EuSolver solves SyGuS
domain problems by enumerating over all expressions enabled by the grammar
until an expression satisfies the specification [6]. While our technique shares
the spirit of optimizing through pruning redundant expressions, it works for adifferent programming paradigm and thus requires different means of generating expression and determining correctness.
Test-Driven Synthesis (TDS) iteratively builds a C# program such thatit satisfies all tests [55]. TDS works over domain-specific languages that havea context-free grammar centered around the .NET framework. Componentbased synthesis builds programs by having a component library used to form
combinations of code within the language of the program being synthesized.
More recent work on component-based synthesis has focused on using oracles
related to I/O for programs that focus on loop-free work over inputs [33].
24

Our approach also shares the spirit of storyboard programming, whichuses user-provided graphical representations of data structures to synthesize
imperative code that performs desired data structure manipulations based on
the insight that it can be easier and more intuitive for a user to draw data
structure manipulations than to write the code [63]. Our test valuations makeuse of a similar insight: an end user can more easily construct valid and invalid
valuations than to write a complete model.
An approach for creating Alloy models using instances was introduced
by aDeryaft [35] in the spirit of the Daikon [16] tool that uses a collection of
known properties to check which of them hold with respect to given inputs.
An approach for translating Alloy formulas to Java checks was introduced by
MintEra [4]. Alchemy [40] defined a translation to database update operations
and integrity constraints. AUnit [71, 72] recently defined the concepts of test
case, test execution, and model coverage for unit testing of Alloy models inthe spirit of popular xUnit frameworks for imperative languages. The test valuations that ASketch uses in the context of synthesis follow AUnit’s definitionof a test case.

25

Chapter 4
AUnit Test Generation

4.1

Overview
While AUnit introduces a testing foundation for Alloy, writing AUnit

tests which reveal faults in a model can be tricky due to the nature of Alloy
itself. As a declarative language, in Alloy, any behavior not ruled out by themodel is valid. Indeed, this attribute is a key strength for using declarative
languages to check software designs, as the language will explore all possible
behavior, potentially revealing unintended restrictions (or lack thereof) of thedesign. However, this means AUnit test suites should be developed with thenotion of exercising any and all assumptions made by the developers. For
instance, in Chapter 2.2, our overconstrained fault was revealed by an AUnit
test case in which a node was disconnected from a list. However, it is possiblethat a developer might assume Alloy will only generate nodes which are within
the list. As a result, the developer would never generate Test3, thus neverrevealing the overconstrained fault.
Accordingly, to address the issue of test generation, this chapter introduces two new approaches for automated testing of Alloy models. Our
approaches are based on creating test suites following the spirit of traditional26

black-box and white-box testing, respectively. The black-box test generation
technique, AGenBB , creates suites that include all (non-isomorphic) instancesin the given scope and brings the spirit of bounded exhaustive testing for imperative programs [8, 48] to Alloy models. The white-box test generation technique, AGenW B , brings the spirit of coverage-directed input generation for imperative programs [9, 23, 59] to Alloy models. AGenW B reduces the problem of
directed test generation for Alloy to constraint solving where model coverage
requirements (introduced by AUnit) are part of the constraint. Thus, any solution (if one exists) covers some previously uncovered requirement(s). AGenW B
iteratively builds a minimal set of (non-isomorphic) tests to meet the chosen
criterion. Both techniques use Alloy’s SAT-based backend for test generationand can be adapted to create suites based on different solving strategies [45, 52].
This chapter is based on a paper titled “Automated Test Generationand Mutation Testing for Alloy” published in ICST 20171 and makes thefollowing contributions:• Automated test generation for declarative models – we introduce automated techniques to generate tests for Alloy models to support
black-box and white-box test generation;
1

A. Sullivan, K. Wang, R. Nokhbeh-Zaeem, and S. Khrushid “Automated Test Generation and Mutation Testing for Alloy” in 10th IEEE International Conference on Software
Testing, Verification and Validation. I was the lead student author for this paper in which I
both designed, developed and evaluated the techniques for automated test generation (presented in this chapter) and designed the overall evaluation of the paper; fellow student Wang
was the lead author for the mutation testing content (not presented in this chapter); withthe remaining co-authors providing valuable guidance and feedback along the way.

27

module list.v.2.1
one sig List { head: lone Node }sig Node { link: lone Node }pred Acyclic {some List.head => { some n: List.head.^link | no n.link }}Figure 4.1: A faulty Alloy model for a singly-linked list.

• Implementation – we implement a prototype that embodies our techniques as well as the theoretical foundations introduced previously byAUnit, specifically to provide test case execution and code coverage computation in addition to automated test generation; and• Experiments – we perform a two-fold evaluation to show the efficacyof our approach. One, we compute model coverage and mutation score(which is often considered as the strongest test adequacy criterion in imperative programs) for the generated tests. Two, we show our approachfinds real faults in several subjects, including all 19 faulty models submitted as solutions to a homework question in a graduate course in our
Department.

4.2

Illustrative Example
This section presents a small but representative example of a faulty Al-

loy model to refresh some key concepts in Alloy and AUnit, which will be used
for our test generation techniques. Figure 4.1 (incorrectly) models an acyclic

28

List0List0

header

List0

Node0

header

Node0

link

(a)
pred Val1() {some disj List0: List {List = List0
no Nodeno headno link(b)(c)

pred Val2() {some disj List0: List {some disj Node0: Node {pred Val3() {some disj List0: List {some disj Node0: Node {List = List0
Node = Node0
head = List0 -> Node0no link

List = List0
Node = Node0
head = List0 -> Node0
link = Node0 -> Node0}}}

T1: run { Val1 and Acyclic }

(d)

}

}

}

T2: run { Val2 and Acyclic }(e)

T2: run { Val3 and !Acyclic }(f)Figure 4.2: (a) Instance: empty list. (b) Non-instance: acyclic list with 1 node.
(c) Non-instance: cyclic list with 1 node. (d) Passing test with valuation (a).
(e) Failing test with valuation (b). (f) Passing test with valuation (c).

singly-linked list. Notice our acyclic constraint is different from section 2.1,
which used universal quantification to expression acyclicity. This time, we use
implication and existential quantification to express the same constraint. The
signature (sig) declaration “sig List” introduces a set of list atoms; similarly “sig Node” introduces a set of node atoms. The keyword “one” declares
List to be a singleton set. Each signature declaration also introduces a binary

relation. The relation header maps lists to nodes. The relation link maps
nodes to nodes. Both header and link are partial functions as declared by the
keyword lone. The predicate (pred) Acyclic defines acyclicity. The predicate
body contains an implication (“=>”) and intends to state that if the list has
some header node, there exists a node reachable from the header with no link,29

i.e., the list is “null-terminated”. The keyword “some” represents existential
quantification. The operator ‘.’ is relational composition and ‘^’ is transitive closure. The expression “List.header.^link” represents the set of nodes
reachable from List’s header following 1+ traversals along link. The formula“some E” for expression E states that E is a non-empty set. Structuring acyclic
as an implication additionally allows for the list to be empty, as without the
implication, the existentially quantified formula requires there to be at least
one Node atom in the List.
The command “run Acyclic” instructs the Alloy analyzer to create
an instance for predicate Acyclic using the default scope – a bound on theuniverse of discourse – of 3. When the command is executed, the analyzer finds
a valuation for List, header, Node and link, which satisfies the constraints in
Acyclic and the facts in the model w.r.t. the given scope, i.e. considering up

to 3 Node atoms, but 1 List atom (one sig List). Figure 4.2(a) graphicallyshows an example instance for “run Acyclic”. Not all valuations are instances.
Figures 4.2(b) and (c) are not instances for “run Acyclic” and thus will not
be generated for this command. While (c) is expected to be a non-instance(since it has a cycle), (b) is a non-instance because of an overconstraint fault
in our model.
To explore this fault, we can look at our AUnit tests. The predicates
Val1, Val2, and Val3 together with their respective labeled run commands
Test1, Test2, and Test3 represent three AUnit tests. Intuitively each predi-

cate represents a test input and each command represents a test oracle. Note30

that Val3 is not acyclic and Test3 passes since the test oracle correctly identifies it (!Acyclic). Test1 and Test3 pass, but Test2 fails and exposes a fault
in the model. The valuation Val2 is expected to be a valid acyclic list but thepredicate Acyclic is overconstrained and erroneously disallows it; the fault
is in the use of transitive closure (‘^’) in List.header.^link. This expression generates the set of Node reachable from 1 or more iterations over List’s
header, but excludes the header itself. Therefore, since this expression ap-

pears inside an existentially quantified formula (some), this requires there to
be at least one Node reachable from List’s header in order for the Acyclic constraint to be satisfied. To correct this, we can use reflexive transitive closure(‘*’) instead, which looks at zero or more iterations. Therefore, our corrected
Acyclic predicate would be:

module list.v.2.2
one sig List { head: lone Node }sig Node { link: lone Node }pred Acyclic {some List.header => { some n: List.header.*link | no n.link }}For the Alloy model in Figure 4.1 and the default scope of 3, ourblack-box generation technique AGenBB creates 157 inputs while our coveragedriven test generation technique AGenW B creates 10 inputs. Both AGenBB
and AGenW B produces all 3 valuations shown in Figure 4.2.
31

4.3

Automated Test Generation Using AUnit
This section presents our automated test generation approach. We

introduce two basic techniques. AGenBB is a black-box technique which uses
constraint solving to enumerate solutions for commands that execute (or check)existing predicates (or assertions) but does not directly utilize the way the
Alloy model is written (Section 4.3.1). AGenW B is a white-box technique,which performs targeted test generation driven by AUnit’s model coverage
requirements (Section 4.3.2).
4.3.1

Enumeration-based Input Generation
Algorithm 1 embodies our enumeration directed approach; conceptu-

ally the algorithm systematically enumerates valuations by running the empty
command (run {}), creates commands based on assertions and predicates (ortheir negations), and creates valuation-command pairs to form tests. The algorithm starts by executing the empty command  over the given model. We
selected the empty command because  can be executed for any model. A naive
approach would be to simply form test cases as follows: henumerated instancei, i. For instance, we could build a test suite for our acyclic singly-linked list
from Figure 4.1 as simply hhFigure 4.2(a), i, hFigure 4.2(b), i, hFigure 4.2(c),ii. However, when a tester manually inspects the generated valuations to see
if their shapes match expectations, the tester can only validate the behaviorof valuations over the facts of the model. As a result, it is possible for the test
suite to contain only valuations that are expected even though the model is32

actually faulty. To produce a more robust, informative test suite, we need to
invoke other paragraphs in the model. Therefore, rather than using  as the
only command for our tests, we use  to get a starting base of valuations.
Specifically, for each instance i enumerated by executing , we add atest case per each predicate and assertion paragraph present in the model,using the negation of the paragraph if the valuation fails the paragraph (thei.eval(P) call is false). Since all these valuations must satisfy the facts of themodel, to reduce the number of overall tests, we do not explicitly generatetests that have  as their command. Taking this into account, our new test
suite for the model in Figure 4.1 is: hhFigure 4.2(a), run Acyclici, hFigure
4.2(b), run Acyclici, hFigure 4.2(c), run !Acyclicii.
While we now have a more robust test suite, all the tests have a common
limitation: we never generate any tests in which the facts of the model are
violated. Therefore, we create a second Alloy model, M 0 , in which all thefacts in the model are replaced with the disjunction of the negation of all thefacts (negateFacts). Any instance satisfying M 0 violates at least one fact
formula. However, the facts of the model limit the possible solution spacesignificantly. If we repeat the process with M 0 (run , enumerate all instances,build up a test suite) we end up with extremely large state spaces, resulting
in an unreasonable number of valuations to consider. Instead, we focus on
enumerating one instance per each size in the scope. If  is satisfiable for the
tailored scope, a test case of the form hfirst instance enumerated, run  expect
0i is added to the test suite. Recall, an expect clause is an Alloy construct used

33

Algorithm 1: AGenBB – Enumeration-based Input Generation.
input : Alloy Model M , Scope S
output: Test Suite Tsuite
Tsuite ← [];Command empty ← new Command(S, run {})A4Solution solSpace ← execute(M, empty)
if solSpace.isSatisfiable thenforeach instance i in solSpace doforeach Alloy paragraph P in M do
if P == PRED or P == ASSERT thenif i.eval(P) thenTsuite .add(new TestCase(i, P ))else
Tsuite .add(new TestCase(i, !P ))AlloyModel M’ = negateFacts(M)for k ← 0 to S do
Command empty ← new Command(k, run {})solSpace ← execute(M’, empty)
if solSpace.isSatisfiable thenTsuite .add(new TestCase(i, run {} expect 0))
return Tsuite
to state whether a command should be satisfiable (expect 1) or not (expect0). By appending expect 0 to the empty command, the tester is informedthat the associated valuations do not adhere to the facts of the model.
The technique can be implemented with any Alloy enumerator (Alloy
Analyzer, Aluminum, TACO). We chose to implement Algorithm 1 to embody
AGenBB using the Alloy Analyzer, which is the enumerator associated withthe standard Alloy distribution. Although the SAT solver needs to be invokedwhen we first execute  and enumerate instances, we can actually build up the34remainder of the test suite without invoking the SAT solver: by using the Kodkod tool’s evaluator API [73]. We invoke the evaluator by passing a test’svaluation and an Alloy formula for a predicate or assertion. The evaluator
returns true if the instance satisfies the formula and false otherwise. Therefore, we can use the Evaluator tp determine the shape of commands for our
generated valuations, i.e. if the call to Acyclic should be negated or not. a
4.3.2

Coverage-Directed Input Generation
Our coverage-directed test generation technique AGenW B utilizes afeedback-loop that ensures each new test generated covers some previously unsatisfied coverage requirement. Specifically, the algorithm iteratively: solves
the current formula to generate a test, obtains its coverage, and adds a logical constraint to update the current formula and capture some uncovered
requirement(s). While these constraints place restrictions based on the coverage obtained for previously generated valuations, the targeting constraints
do not include those valuations in any direct form. Moreover, the targeting
constraints do not directly depend on the size of the previously generated
valuations.
Alloy Analyzer’s enumeration functionality does not guarantee that thenext instance enumerated covers new criteria. Therefore, we introduce targeting constraints to be appended to the base model that will facilitate this ability.
Table 4.1 shows the targeting constraint templates for Alloy constructs basedon AUnit’s coverage requirements. Signature, relation and expression coverage

35

Table 4.1: Targeting Constraint Templates.
Alloy
Construct

Coverage
Targeting
Requirement
Constraint|s| = 0{#s = 0}Signature s|s| = 1{#s = 1}|s| ≥ 2{#s > 1}|r| = 0{#r = 0}Relation r|r| = 1{#r = 1}|r| ≥ 2{#r > 1}|e| = 0{#e = 0}
Expression e|e| = 1{#e = 1}|e| ≥ 2{#e > 1}
f = true{f}
Formula f
f = false{ !f }|d| = 0{#d = 0}|d| = 1, b = True {#d = 1 && b}|d| = 1, b = False {#d = 1 && !b}|d| ≥ 2, b = True {#d > 1 && b}
Cardinality{#d > 1 && b|d| ≥ 2,some e: d | b
b = True & False some e: d | !b}|d| ≥ 2, b = False {#d > 1 && !b}requirements center around the size of the sets for the corresponding Alloy construct, while formula coverage requirements center around truth values. The
cardinality subgroup outlines additional requirements for quantified formulas,where “d” is the domain and “b” is the formula in the body. Further detailsof the coverage requirements can be found elsewhere [70, 72]. To add a targeting constraint to a model, we write the constraint as a fact, guaranteeing its
satisfaction. We call a model with a targeting constraint a targeting model.
There are different ways in which we can include coverage requirementsin the model. One way is unique-targeting: iterate over all requirements and36

target each uncovered requirement by producing an associated targeting model,
executing the empty command, , over the model, and using a satisfying instance, if any, as a valuation for a test case. An issue with unique-targetingis that each uncovered criterion is examined in isolation, and each infeasible criterion is only revealed through a unique invocation of SAT. To address
this issue, we introduce multi-targeting, which explores multiple requirements
together. Specifically, our targeting constraint is a disjunction of all unexplored requirements’ targeting constraints. The multi-targeting template fora targeting constraint is:
For all unexplored requirements c1, ... cn:
c1’s targeting constraint or ... or cn’s targeting constraint

For our running example model, the first multi-targeting constraint
would cover all 35 requirements for the model: (#List = 0) or (#List = 1)or (#List > 1) or ... or (no n.link) or !(no n.link).
Algorithm 2 encapsulates our coverage-driven approach. The algorithm
runs as long as there is some coverage requirement which has not yet been
explored, i.e. is not covered by a previous valuation or marked infeasible. First,
all coverage requirements from the model are collected into a list (criteria),
which will store the coverage landscape of the model as the algorithm runs.
Next, a targeting model is created by appending the targeting constraint,
which will either reflect the next criteria to target under the unique-targeting
guideline or the disjunction of all remaining criteria to explore under the multitargeting guideline (getNextTC). Then,  is executed over the targeting model.
37

Algorithm 2: AGenW B – Coverage-Directed Input Generation.
input : Alloy Model M , Scope S
output: Test Suite Tsuite
List criteria ← M.extractRequirements()
numExplored ← 0AlloyModel targeting ← null
Command empty ← new Command(S, run {})while numExplored != criteria.size() do
TargetingConstraint target ← getNextTC()targeting ← appendTarget(M, target.formula)
A4Solution solSpace ← execute(targeting, empty)
if !solSpace.isSatisfiable() thentargeting ← removeFacts(M)targeting ← appendTarget(targeting, target.formula)
solSpace ← execute(targeting, empty)
if solSpace.isSatisfiable() thenInstance i ← solSpace.getInstance()
foreach uncovered c in criteria do
if i.eval(c.targetingConstraint()) thenc.markCovered()numExplored++
if i.eval(c.getPara()) thenTsuite .add(new TestCase(i, c.getPara())
else
Tsuite .add(new TestCase(i, !c.getPara())
else
foreach criteria c in target doc.markInfeasible()numExplored++
return Tsuite
If the call is unsatisfiable, one of two possibilities hold: the requirements inthe targeting constraint violate the facts of the model or the requirements
are currently infeasible for the given scope. To determine which, we form a38

new targeting model with all facts removed except the targeting constraint(removeFacts) and execute . Should this call also be unsatisfiable, then all
criteria being targeted cannot currently be covered w.r.t. the given scope andare marked infeasible.
However, should we produce a satisfiable solution space from either  invocation, we have successfully targeted at least one new coverage requirement.
We obtain the first instance, i, and analyze i for coverage information. We
mark any requirement c that is covered for the first time as covered, removing
c from the pool of requirements to target in future iterations. A requirement is
known to be covered if the evaluator returns true for c’s targeting constraint.
Then, we generate a test case where the valuation is i and the command iseither the predicate or assertion (or negation of when appropriate) that contains c. If c is located in a fact paragraph, the command is . For example,
if Figure 4.2(a) is the first instance enumerated, the test hFigure 4.2(a), run
Acyclici would be created because the valuation in Figure 4.2(a) covers formulas and expressions in Acyclic, such as #List.head = 0 and some List.head= false).

As with AGenBB , AGenW B uses the evaluator to generate tests without additional invocations of SAT solvers. The evaluator is able to determine
the shape of a test case’s command when passed a requirement’s origin paragraph (c.getPara()). Moreover, the evaluator is able to provide all coverage
information. We can pass a test case’s valuation and an Alloy expression oran Alloy formula depicting the coverage criterion. The call will return the out39

Table 4.2: Subject Alloy modules. For each subject, lines of code (LOC ),number of predicates (# p), number of basic signatures (# basic sig), numberof binary relations (# bin rel ), number of ternary relations (# ter rel ), numberof variables, number of primary variables and number of clauses are shown.
Pair (a, b) shows minimum (a) and maximum (b) over all commands in themodel.
# basic # bin # ter
primaryvars
clauses
sig
rel
rel
vars
1
2
2
0 (195,351) (24,30) (274,521)11
20 (170,289)(21) (249,394)3
1
20 (170,429)(21) (249,1086)
1120 (420,488)(34) (704,926)2
1
20 (1509,2014) (99,105) (3858,5221)22
30 (791,888) (64, 80) (2147,2366)
83
0
2 (296,1103)(57) (374,2066)

ModuleLOC # pLinkedList
BinaryTree
FullTreeHandshake
NQueens
Farmers
Dijkstra

15
20
29
28
26
40
61

come of the expression or formula over the valuation thus indicating whether
or not the criterion is covered.

4.4

Evaluation
This section presents an experimental evaluation of our test genera-tion approaches. Our evaluation is two-fold. First, we use a suite of correct
Alloy subjects to measure two common metrics used to evaluate test suites:(1) model coverage and (2) mutation score. Second, we use a suite of faulty
subjects with real faults, including standard Alloy models and graduate homework submissions, to evaluate fault finding ability (Section 4.4.2) of test suites
generated by our approaches.

40

4.4.1Model coverage and mutation score

Subjects. We use seven correct Alloy models for evaluation. Four of thesemodels, namely LinkedList, BinaryTree, FullTree and NQueens, are written byus, and the rest are from the standard Alloy distribution. These models range
from simple illustrative examples like a singly-linked list to more complex examples like Dijkstra’s mutual exclusion. LinkedList, BinaryTree, and FullTree
capture the constraints of the corresponding data structures. NQueens solves
the problem of how to place N number of queens on a chess board of size
N × N without conflicts. Handshake encapsulates the Halmos handshakelogic problem. Farmers outlines a common logic problem in which a person(the farmer) has to get three objects (fox, chicken, and grain) across a river
without any of the objects eating another object. Lastly, Dijkstra captures
Dijkstra’s mutual exclusion algorithm to prevent deadlocks. Table 4.2 gives
key characteristics of the subjects.
Model coverage results. Table 4.3 shows the details for various attributes
related to generation and execution of the test suites, broken down by technique. Model is the Alloy model under test. #Vals is the number of valuations generated. #SAT is the number of calls made to the backend SAT solver
during test generation. #Tests is the number of test cases generated. The
SAT solver is invoked either when a command in the module is executed or
the constraint to create the next instance is solved. Therefore, for both techniques, this value is the number of valuations plus the number of commands
executed during test generation time. “Tgen [ms]” is the time to generate
41

Table 4.3: Test suite generation and execution.
AGenBB
Model #Vals #SAT #Tests Tgen [ms] Mod Cov Texe [ms] Tcov [ms]LinkedList
1006
1012
4010
1
89.2%
870
9
BinaryTree
1004
1010
3004
1
91.5%
1824
2
FullTree
1004
1010
5004
1
90.5%
3410
4
Handshake
32
38
86
1
88.6%
186
15
NQueens
180
185
1888
3
84.0%
4585
56
Farmers
10
16
927
2
57.7%
205
21
Dijkstra
10
16
2893
2
64.7%
147
15
AGenW B
Model #Vals #SAT #Tests Tgen [ms] Mod Cov Texe [ms] Tcov [ms]LinkedList
8
9
10
467
100.0%
2
2
BinaryTree
8
9
8
162
98.6%
1
2
FullTree
8
9
15
228
95.3%
3
3
Handshake
11
12
11
423
91.4%
5
5
NQueens
7
8
13
181
97.8%
2
3
Farmers
12
13
18
1171
87.37%
25
7
Dijkstra
12
13
14
2337
87.5%
15
7

the tests, starting with the first SAT invocation and ending once writing thetest(s) to a file finishes. “Mod Cov” shows, as a percentage, the model coverage achieved by the tests. Model coverage considers all coverage requirements
produce by all Alloy elements (signatures, relations, expressions and formulas)regardless of their location within the model. Since model coverage subsumes
the other coverage metrics in AUnit [72], we only use model coverage for evaluation. “Texe [ms]” is the time to execute the tests, which is the time to check
whether each valuation is an instance of its paired command. “Tcov [ms]” isthe cumulative time that includes the test execution time and the time tocalculate model coverage.
In all cases, AGenBB produces the largest test suites, and takes thelongest time to both generate and execute test suites. Since this technique42

can produce a very large number of tests, for our evaluation, we capped thenumber of instances that can be enumerated from any single command to1000 for models without parameterized paragraphs, and 10 for models withparameterized paragraphs. As expected, AGenBB makes the most SAT calls.
Furthermore, since Alloy’s default symmetry-breaking does not remove all isomorphisms, some instances generate redundant tests. Naturally, since enumeration is oblivious of model coverage criteria, the resulting suites are notminimal for the level of coverage achieved. However, due to producing many
valuations, AGenBB does, on average, have high model coverage. AGenBB ’s
model coverage is hindered by exploring only a few valuations which violate atleast one fact paragraph. Recall that enumerating all such valuations would
likely create enormous test suites and this choice is a trade off to avoid a hugeincrease in test generation and execution times.
For all subjects, AGenW B produces a relatively small test suite: no morethan 18 for any subject. Test generation, execution, and coverage computation
altogether take less than a seconds for most subjects. In comparison to theother techniques, the coverage-directed generation technique produces tests
that give the highest coverage for all subjects. Indeed, this technique is bydesign constructed to focus on increasing model coverage. While AGenW B ’smodel coverage is not always reported as 100%, AGenW B does achieve thehighest possible model coverage, as infeasible criteria are not currently factored
out of the reported model coverage and the gaps in AGenW B ’s coverage isstrictly due to infeasible criteria. A nice property of the technique is that it

43

Table 4.4: Mutation Testing.
ModuleLinkedList
BinaryTree
FullTreeHandshake
NQueens
Farmers
Dijkstra

AGenBB
AGenW B Mutation% k t[ms] % k t[ms] % k t[ms]27 92.6 120101 85.2
664 100 545
59 59.3 137686 54.2
894 100 972
82 70.7 429942 58.5 2426 100 1997
78 76.9 341575 11.5 3363 100 3072
93 87.1 2297711 69.9 4943 100 4099
99 2.0 233811 2.0 2995 100 2986
187 57.8 5039570 29.9 166154 100 94232# neq-muonly generates non-isomorphic tests – by construction, there are no two tests
that cover the same set of requirements. Note however, coverage-directed
generation does not produce all non-isomorphic tests.
Mutation Testing Results Table 4.4 shows the results of mutation testing.
For each subject, the table gives the number of non-equivalent mutants (#neq-mu), the mutation score (% k) and the time taken for running mutation
testing algorithm (t[ms]) with respect to test suites generated using Alloy
enumeration and coverage-directed generation. Additionally, the last column,
shows the maximum reachable mutation score for each model, which is 100.
In all subjects, the Alloy enumeration technique uniformly gives higher
mutation score compared to the coverage based technique. The exception is
the farmers model, where both techniques only kill 2.0% of the non-equivalentmutants. These poor mutation scores are because most tests generated lead tounsatisfiable formulas in test execution because the Alloy enumeration technique generates predicate invocations with all permutations of parameters.
Most parameter permutations make the tests trivially unsatisfiable for the44

Table 4.5: Known Buggy Models – AUnit test generation fault finding ability.
Model
Farmers
DijkstraFailY
Y

AGenBB#Vals #SAT
41
47
1004
1010

#Tests
9769
287004FailY
Y

AGenW B
#Vals #SAT
13
14
17
18

#Tests15
61

Table 4.6: Homework submissions – AUnit test generation fault finding ability.
Fail
16/19

#Vals
(223,504)

AGenBB#SAT(227,509)#Tests(26296,83753)

Fail
19/19

AGenW B
#Vals #SAT
(13,18) (14,19)#Tests(16,47)

original model and all mutants, which means those tests do not kill any mutant. Another reason is that the farmers problem contains a very limited
number of solutions given our scope of 5, which makes most tests unsatisfiablein the first place. The coverage-based technique kills only 11.5% of the mutants for the handshake model, mainly because the coverage based techniqueonly needs to generate a small number of tests to achieve full coverage due tothe nature of the model, which limits the ability to kill mutants.
4.4.2

Finding real faults

Known buggy models. We consider next two models that are faulty versions of two of our subjects in Section 4.4.1. Faulty Farmers and Dijkstra
models are from Alloy Analyzer v4.1.10 that shipped these buggy versions;the current Alloy release includes the corrected versions after Alloy users discovered and reported the bugs. The faulty Farmers was underconstrained ;the CrossRiver predicate checked the “eating” behavior on only one side of
the river, enabling Objects which should have eaten each other to co-exist
alone. In faulty Dijkstra, when the predicate GrabbedInOrder was invoked45

from GrabOrRelease, the model was overconstrained and only produced a few
trivial instances. We generated test suites for each faulty model using bothtechniques (AGenBB and AGenW B ). If the test generation technique was able
to produce a test which encapsulated the faulty behavior, then the bug is
detected.
Table 4.5 summarizes the results of the two techniques. The column
Fail shows if the technique creates a failing test and finds the fault. Boththe AGenBB and the AGenW B multi-targeting find the faults in both models.
AGenBB continues to create large test suites, which take significant time to
produce and execute. For instance, the Dijkstra model contains no facts;
therefore, the solution space for the empty command is substantially large:
any instance that adheres to the signature declarations is valid. AGenBB isable to enumerate a diverse range of valuations, but each valuation produces
multiple tests. The faulty Farmers model produces 41 valuations, but 9769
tests. AGenW B does not suffer from this limitation, but is still able to detect
the faults.
Homework submissions. We consider next 20 homework submissions for
one question that presented a partial model of a sorted, singly-linked-looplist, where the last list node points to itself. The partial model contained
5 signature declarations, one fact skeleton and 5 predicate skeletons to be
filled in by the students. Appendix B shows the partial model given in the
homework. 19 of the 20 homework solutions were faulty. Using each technique,we produced a test suite over all 20 models. As with the known-buggy models,46

if the test suite produces a test which shows some buggy behavior, then thetest suite has detected fault(s).
Table 4.6 summarizes the results of the two techniques. The column
Fail shows the ratio of faulty models detected with respect to the total numberof faulty models. Both techniques correctly identified the non-faulty student
submission model. Details of the generated test suites are shown in pairs (a,b)
showing the minimum and maximum values across test suites produced overall 19 submissions.
AGenBB detected bugs in a majority of the submissions, but was unable
to detect a fault in 3 out of the 19 buggy models despite producing extremely
large test suites. The loop-list has a number of predicates with parameters,
which means a single valuation does not become a single test per command but
a single test per unique combination of values for the command’s parameter(s).
As a result, for our evaluation, we “timed out” the technique after enumerating
500 instances, generally producing suites of size > 80, 000. AGenBB struggled
to detect faults located in facts, which, as expected, is a limitation of the
AGenBB technique. The solution space for negated facts is typically muchlarger than the valid solution space. AGenBB had greater success at finding
faults in the known-buggy models, whose faults were not in the facts of themodel.
AGenW B was the most effective technique, finding a bug in every faulty
student submission; moreover, it has small test suites, which can reasonably beinspected manually by end users to determine if the actual behavior matches
47the desired behavior. In the end, AGenW B is the only technique to detect abug in every model in our suite of faulty subjects.
Our evaluation of AUnit test generation using homework submissions
made us specifically appreciate AUnit. Aside from this evaluation, we had
manually graded the submissions and some of the bugs found by AUnit werepreviously missed by us. These bugs were usually in relation to non-obvious
compounding formulas, such as the impact a parameter has on the formulas
within the paragraph. In Alloy, parameters are not allowed to be empty (bydefault), which can restrict the domains of the formulas present in the paragraph. Moreover, Alloy’s expressive nature can make it difficult to reason
about a group of formulas together, even if it is easy to understand them separately. Our AGenW B technique is able to automatically produce a test suitethat has been shown to be capable of detecting bugs. While the end user will
typically need to act as an oracle to the test suite (i.e. determining the expect
clause), AGenW B produces representative but small test suites. Furthermore,since AUnit test cases are designed to be visualized, the end user can feasible
step through an AGenW B test suite without much time or resources required.

4.5

Summary
We presented two novel approaches for automated testing of models

written in Alloy – a well-known declarative, first-order language that is supported by a fully automatic SAT-based analysis engine. The two approaches
introduces automated test generation that create test suites in the traditional48

spirit of black-box and separately white-box testing. The two approaches buildon the basis defined previously by our AUnit framework, which introduced
the idea of unit testing for Alloy in the spirit of unit testing for imperative
languages. While test generation is a heavily studied problem with many solutions in the context of imperative languages, the key novelty of our work
is to introduce and address these problems for the declarative programming
paradigm, specifically for the Alloy language. Experimental results using several Alloy subjects, including those with real faults, demonstrate the efficacyof our framework.
We believe our work introduces a novel, yet conceptually familiar, effective way to validate the quality of Alloy models. Indeed, testing remains
the most widely used methodology for validating quality of programs in imperative languages. We hope a well-founded testing methodology for models– written in declarative languages – can be equally useful for finding faults inmodels. We plan to develop our approach for other declarative languages andanalysis tools in future work. We also believe testing in its traditional spirit
has an important role to play in validation of declarative models.

49

Chapter 5
Enumeration-Based Sketching of Alloy Models
Using Test Valuation

5.1

Overview
Declarative languages, such as Alloy, provide a means for specifying thedesign of a system, allowing for earlier validation of the system as a whole. Yet,declarative languages are often limited by their steep learning curves and lackof well-developed tool support. As a consequence, declarative languages often
lack a formal testing framework, leaving users to adopt ad-hoc approaches
to check for correctness. Together, these factors place an increasing burden
on the end user, especially in the face of developing correct models. As aresult, sketching, a form of program synthesis where users provide a partial
program with holes and an outline of expected behavior of the program and a
sketching tool outputs a completed program that meets the expectation(s), is
one approach to improve the usability of declarative languages.
In this chapter, we introduce the first approach for sketching Alloymodels, ASketch, where the user does not need to try and write complete
models. Instead, the user writes a partial model with holes and provides somevalid and invalid valuations that conceptually serve as test cases [72] for the50

desired model. These test valuations allow an end user to specify the expectedbehavior of an Alloy model, thus enabling sketching. ASketch focuses on
sketching constructs of Alloy models, including relational expressions, logicaloperators, quantifiers, etc.
The main focus of this chapter is the introduction of ASketch Eval , ourenumeration-based technique to solve the sketch using constraint checking tosimply evaluate—without any constraint solving—all possible candidate models one by one. Exhaustively considering all combinations of candidates fordifferent holes to complete a sketch would require a prohibitively large numberof calls to the Evaluator, although each call simply reduces to constant propagation; ASketch Eval optimizes sketching using a per valuation reduction oneach set of candidate expressions and subformulas by evaluating (when possible) the candidates separately with respect to one test valuation (at a time)and removing duplicates, i.e., expressions or subformulas that evaluate to thesame value for that valuation.
We perform an experimental evaluation of ASketch using 24 sketches
derived from five core Alloy models. Experimental results show that ASketch
can complete the models for sketches that can simultaneously have up to 3
expression holes and 3 operator holes. To highlight the complexity of theunderlying problem, one formula, BinaryTree with 6 holes, has a state spaceof over 7.8 billion candidate Alloy models (3 operator holes with 4 candidates
each and 3 expression holes with 496 semantically non-equivalent candidateseach). ASketch Eval , with all optimizations, makes 43,154 calls to the evaluator51

to explore 756 million candidate models before it finds a solution (w.r.t. 20
test valuations). Our results show that for all other cases except the binary
tree model with 6 holes (which has the biggest search space), ASketch Evalfinds a solution to the sketch quickly, with most sketches finishing in under 10
seconds.
This chapter is based on a paper titled “Sketching Alloy Models Using
Test Valuations.”1 and makes the following contributions:ASketch: We introduce the idea of sketching Alloy models using test valuations. Our framework highlights the different problems for sketching an Alloymodel: updating the Alloy input language, producing fragments, and solving
the sketch.
ASketch Eval : We introduce a technique based on evaluation alone (without
constraint solving) for completing Alloy sketches.
Optimizations: We introduce a suite of optimizations designed for relational
expressions and logical formulas to improve the efficacy of our techniques.
Experiments: We present an experimental evaluation with small but intricate Alloy formulas; the results show that ASketch introduces a promising
approach for sketching Alloy models.
1“Sketching Alloy Models Using Test Valuations” is submitted for peer-review by A. Sullivan, K. Wang, D. Marinov, and S. Khurshid. This paper presents two sketching techniques:
ASketch Eval (focus of this chapter) and ASketch Solve (not presented in this chapter). I was
the lead student author for ASketch Eval – designing, developing, implementing and evaluating the technique with feedback from the coauthors. I worked closely with S. Khurshid in
the design phase.

52

(T 0)

(T 1)

(T 2)

(T 3)

(T 4)

(T 5)

(T 6)

L0

L0

L0

L0

L0

L0

L0

head
N0

head
N0
link

head
N0
link

head
N0
link

head
N0
link

(T 7)
L0

head
N0

head
N0

link

link

link

link
N1

N1

N1
link

N2

N2

link

N1
link
N2

N1

N1

link

N2

link
N2

link

Figure 5.1: Eight valuations shown graphically. Of these, T 0, T 3, and T 4 arevalid valuations for the expected acyclicity property, and T 1, T 2, T 5, T 6, andT 7 are invalid. L0 is the list atom. N 0, N 1, and N 2 are node atoms.
ASketch brings the spirit of traditional program sketching [5, 28, 32,
62, 63, 65–68]—which is regarded as the breakthrough approach in program
synthesis for imperative and functional programs during the last decade—toa declarative, relational logic. We hope ASketch serves as a sound basis for ahighly effective methodology for synthesizing Alloy models, which ultimately
increases the use of analyzable models and leads to better software.

5.2

ExampleTo illustrate our ASketch approach, consider the following partial Alloymodel for an acyclic singly linked list in Figure 5.2. The Alloy keyword"module" names the model, which can be included in another module. The

signature (sig) declaration introduces a set of atoms and a user-defined type53

Figure 5.2: A partial model of a singly-linked list.

module list v.3.0
one sig List { header: lone Node }sig Node { link: lone Node }pred Acyclic() { \Q\ n: Node | n \CO\ \E\ => n \CO\ \E\ }in the Alloy model. A signature may optionally declare fields, i.e., relations.
The signature List declares a set of list atoms; "one" makes the set singleton,
i.e., have exactly 1 atom, which represents the list we are modeling. The fieldheader declares a binary relation of type List × Node; lone declares header

to be a partial function, i.e., each List atom maps to ≤ 1 Node atom. The
signature Node declares a set of nodes and introduces the field link, which isa partial function of type Node × Node.
The predicate (pred) Acyclic introduces a named formula (which may
have parameters). The body of the predicate is a formula sketch with threedifferent types of holes: one \Q\ hole (quantifier hole), two \CO\ holes (comparison operator hole), two \E\ holes (expression hole). ASketch introduces
these hole kinds to the Alloy grammar. The variable n is introduced by thequantifier (to be sketched) and is of type Node; the operator => denotes logicalimplication.
The goal is to fill in the holes in the Acyclic predicate such that the formula we are sketching states that the nodes in the list form an acyclic structure.
Figure 5.1 graphically illustrates eight test valuations for the model. Three54

of these valuations–T 0, T 3, and T 4, are valid with respect to the expected
acyclicity constraint, i.e., can be generated as instances by executing the command “run Acyclic” for a correct completion of the given predicate Acyclic.
While five of these valuations – T 1, T 2, T 5, T 6, T 7 – are invalid, i.e., cannot
be generated by executing the command “run Acyclic”. Note, valuation T 3
is valid although its node N 2 links to itself. N 2 is not in the list, and theformula we are sketching should constrain only the nodes that are actually inthe list to form an acyclic structure.
The user can provide the test valuations simply as Alloy predicates. For
example, the following predicate represents test valuation T 0 from Figure 5.1:

pred Test0() {some L0: List {List = L0
no headerno Nodeno link
Acyclic[]}}

This predicate uses an existentially quantified (some) formula to assign
a value to the List set. Using the Alloy keyword no, the predicate declares
the rest of the signatures and relations to be the empty set. The predicate
invocation Acyclic[] labels the valuation as valid for the expected completionof the acyclicity constraint.
As another example, the following predicate represents test valuation
T 2 from Figure 5.1:

55

pred Test2() {some L0: List | some disj N0, N1: Node {List = L0
header = L0->N0
Node = N0 + N1
link = N0->N1 + N1->N0!Acyclic[]}}

The keyword disj requires the variables in the declaration to represent disjoint
sets, i.e., unique nodes, the operator -> denotes Cartesian product, the operator + denotes set union, and the predicate invocation !Acyclic[] labels thevaluation as invalid for the expected completion of the acyclicity constraint.
Consider using ASketch to complete all five holes. Alloy allows 5 quantifiers for \Q\ (all, no, some, lone and one) and 4 comparison operators for\CO\ (=, in, != and !in). Two are expression holes \E\, and using the optimized version of an expression generation technique outlined in [75], Alloy
allows for 57 unique, non-equivalent expression candidates. Together, thesesubstitutions produce a total of 259,920 candidate Alloy models. ASketch Eval
searches threw this space to complete the sketch. Here is one solution ASketch Eval finds, with a universally quantified (all) formula:

all n: Node | n in List.header.*link => n !in n.^link
The Alloy keyword in represents the subset, and ! denotes logicalnegation. The operator * denotes reflexive transitive closure, and ^ denotes
transitive closure. The expression List.header.*link represents the set of all56

nodes reachable from the list’s header (following zero or more traversals of the
field link). The expression n.^link represents the set of all node reachable
from n (following one or more traversals of the field link). Thus, this universally quantified formula states that for any node, if the node is in the list, thenode is not reachable from itself, which correctly characterizes our expected
acyclicity constraint.
The user may choose to enumerate more than one solution. For these 5holes and 8 valuations depicted in Figure 5.1, ASketch Eval creates 4 formulas
to complete the sketch:

all n: Node | n in n.^link => n !in List.header.^link
all n: Node | n in n.^link => n !in List.header.*link
all n: Node | n in List.header.^link => n !in n.^link
all n: Node | n in List.header.*link => n !in n.^link
All 4 formulas are equivalent and correctly represent our expected acyclicity
constraint.
To complete the sketch, our optimized ASketch Eval takes only 0.6 seconds and invokes the Alloy evaluator 410 times. Moreover, ASketch Eval enumerates all 4 solutions on average in 0.4 seconds per solution and invokes the
Alloy evaluator 128.5 times per solution.

5.3

ASketch Framework
We first present two aspects of the ASketch framework needed to allow

sketching of Alloy models: updating the ASketch grammar to account for Alloy57

expr ::= unOpE expr | expr binOp expr | expr arrowOp expr | "none" |"iden" | "univ" | "(" expr ")" | name | "\E\"name ::= ("this" | ID) ["/" ID]*
quant ::= "all" | "no" | "some" | "lone" | "one" | "\Q\"
unOp ::= "no" | "some" | "lone" | "one" | "\UO\"
unOpF ::= "!" | "not" | "\UOF\"
logicOp ::= "||" | "or" | "&&" | "and" | "<=>" | "iff" | "=>" | "implies" |"\LO\"
compareOp ::= ["!"|"not"] actualCompareOp | "\CO\"actualCompareOp ::= "=" | "in"unOpE ::= "~" | "*" | "^" | "\UOE\"
binOp ::= "+" | "&" | "-" | "." | "->" | "\BO\"

Figure 5.3: Modified Alloy grammar used for holes in ASketch.
models with holes and the problem of how to generate Alloy fragments to use
as candidates for the holes. Then, we describe how ASketch Eval determines
which fragments complete the sketch to produce an Alloy model that satisfies
all the given test valuations.
The input to ASketch is an Alloy model with holes. Our input language
effectively extends the Alloy grammar with new syntactic constructs that represent holes. The current, full Alloy grammar is available online [49]; we follow
an older exposition of Alloy [30] that also provided the semantics of the kernel
Alloy language. Figure 5.3 shows the portions of the Alloy grammar that wehave introduced holes for. For instance, we extend quant so the quantifier can

58

Table 5.1: Possible values for non-recursively defined holes.
Sketch Kind
Quantifier
Logical Operator
Compare Operator
Unary Operator
Unary Operator Formula
Unary Operator Expression
Binary Operator

Hole
\Q\
\LO\
\CO\
\UO\
\UOF\
\UOE\
\BO\

Candidates
all, no, some, lone, one||, &&, <=>, =>=, in, !=, !inno, some, lone, one!,
˜, *, ˆ&, +, -

be a hole \Q\and comparison operators (compareOp) include all operators from
Alloy and also a hole \CO\. For all the kinds of holes depicted in Figure 5.3
minus \E\, we can use the concrete nature of the Alloy grammar to determine
the substitution for each kind of hole. We will refer to these kinds of holes
as operator holes. Table 5.1 shows the fragment substitutions for all operator
kinds of holes.
Expression holes, \E\, present a unique challenge for generating fragments for substitutions for our sketching problem. Unlike operator holes, forexpression holes, the Alloy grammar does not present a finite list of valid substitutions. However, the Alloy grammar does provide a blueprint for building
expressions bottom up from the Alloy grammar, starting from smaller subexpressions and building larger ones by creating all the combinations of thesubexpressions. While this avoids the need for an end user to provide the expression fragments, in practice, this leads to an exponentially large list of candidate expressions, which would make sketching infeasible. For instance, for our
linked list model, building up expressions using just relational join could lead59

to an infinite generation such as: n.link, n.link.link, n.link.link.link,n.link.link.link.link, ...

, n.link.

...

.link. To even make gener-

ation of expressions feasible, bounds need to be set to determine a reasonabletermination point.
In [75], we address all of these problems through the introduction of
ASketch Gen which uses the following 4 bounds: (1) the max depth of thegenerated expressions, (2) the max arity of all generated expressions, (3) the
intended arity of the expressions (if any), and (4) the max number of operatorsfor each expression and two optimization approaches (static pruning and dynamic pruning) to generate robust but not prohibitively sized expression holefragments. For our example model in Figure 5.2, ASketch Gen finds 1914 expressions, uses static pruning to reduce that to 67, and uses dynamic pruning
to further reduce the static set to 57 candidate expressions. When we refer toASketch Gen in the remainder of this chapter, we are referring to this technique.
5.3.1

ASketch Eval : Evaluation-based sketching
ASketch Eval leverages the evaluator feature of the Alloy Analyzer, specif-

ically the Kodkod tool [73] called Evaluator, to systematically check every possible candidate model (a completed model with all holes filled in) with respect
to the provided test valuations. ASketch Eval takes as input an Alloy modelwith holes, a set of Alloy fragments for each hole generated by ASketch Gen ,and a set of user-provided test valuations (called simply tests in this context).
In the unoptimized version, ASketch Eval iterates over all possible com60

binations of fragments that can be formed to cover all holes, checks whether
each combination satisfies all the provided tests, and if so, outputs the combination as a solution to the sketch. A key feature of ASketch Eval is that it
requires no constraint solving. The main tool leveraged by the technique, theEvaluator, takes as input an Alloy expression/formula and an Alloy instance,and returns the value of the expression/formula with regards to the given instance. By using the Evaluator, which does not use the backend SAT solver,
ASketch Eval only needs the valuation to check if each given test satisfies theconstraints.
Specifically, ASketch Eval checks each candidate for each test by invoking the Evaluator created from the valuation either on the candidate or on
its negation, depending on whether the test is marked valid or not. If the
Evaluator returns false, the candidate does not properly complete the sketch;

ASketch Eval immediately discards the candidate and moves to the next candidate. If a candidate satisfies all tests, ASketch Eval presents that candidate to
the user as a solution. To illustrate, one incorrect candidate for the Acyclic
predicate is:all n : Node | n in List.header.*link => n in n.^link
The candidate satisfies the test in Figure 5.1(T 0); however, it does not satisfy
the test in Figure 5.1(T 1), where it returns false rather than true for thevalid test valuation. This candidate solution is immediately discarded, and
ASketch Eval moves on to exploring the next candidate solution.
61

5.3.1.1

Optimizations

We improve on the unoptimized version with two optimizations that
effectively re-use previous computations. The intuition is to not evaluate eachand every expression in every candidate but to group expressions into equivalence classes (with respect to the provided tests) and to evaluate only one
representative from each class. Multiple expressions often evaluate to thesame value. For example, consider a test that depicts an empty list, i.e.,
no node reachable from l.header; the expressions l.header, l.header.*link,
and l.header.^link all evaluate to the empty set. Therefore, ASketch Eval
conceptually groups them together. In any given candidate where these three
expressions could fill in the same hole, ASketch Eval evaluates only one expression over the empty list test valuation and applies that result across the othertwo expressions. We call this optimization ASketchEvalExp .
Moreover, the equivalence classes need not be formed only at the levelof individual expressions but can consider larger contexts of the parse subtreesthat include expressions. Even if two expressions have different value for sometest, e.g., E1 ≡l.header and E2 ≡l.header.*link have different values for
non-empty lists, they may have the same value for the same test in a larger
context, e.g., in l in \E\, both l in E1 and l in E2 evaluate to true. A
good option in Alloy is to form equivalence classes over subformulas, because
they evaluate to either true or false for each test. We call that optimization
ASketchEvalSub . An additional benefit of ASketch EvalSub is that it can create
equivalence classes that combine multiple expression holes and even operator
62

Algorithm 3: Candidate Checker.
Input: ASketch model (M ), tests (T ), fragments for each hole (D)Output: candidate solution
State: values: (Test,String) 7→ String // caches computed
values ← {} // empty map
cache ← {} // empty map (Test,String) 7→ Boolean
foreach cand in buildCandidates(M, D) do
foreach t in ts do
rep ← ””
if OPT = BASE then rep ← toString(cand)else if OPT = EXPR thenforeach Expr hole h in M do
rep += memoExpression(t, h)foreach non-Expr hole h in M do
rep += cand.getValueForHole(h)else if OPT = SUBF thenforeach subf in subformulas(M) do
rep += memoSubFormula(t, subf)
foreach hole h not in a subformula do
rep += cand.getValueForHole(h)if !cache.containsKey(t, rep) then
if !eval(t, cand) thencache[(t, rep)] = false
breakcache[(t, rep)] = trueelse if !cache[(t, rep)] then break
if last test case then return candholes. To illustrate, for our list example, \Q\ n : Node | n \CO\ \E\ => n\CO\ \E\, ASketch EvalExp forms groups (for equivalence classes) for each \E\

separately, whereas ASketch EvalSub first forms such groups but then also groups
both n \CO\ \E\ subformulas, before looking at the entire formula.
63

Algorithm 3 shows ASketch Eval ; the optimization level OPT is either
BASE, EXPR, or SUBF. Implementation-wise, the algorithm then creates a poolof Kodkod Evaluator objects to avoid recreating them multiple times when
the tests are checked in a nested loop. The algorithm first initializes values, a
map that memoizes values of expressions and formulas (encoded as strings foreasier presentation) for various tests. It also initializes a cache that memoizes
encountered candidates (again, encoded as strings) to be looked up when an
equivalent candidate model is encountered for a test more than once. The
goal of these maps is to save calls to the Kodkod Evaluator, which can get
expensive.
The algorithm builds all candidates by looping over all combinationsof the provided fragments for each hole. For each combination, it produces acomplete Alloy model, cand. For each candidate cand, the algorithm checks
tests. For each test t, the algorithm first builds a representation rep of thecandidate. With no optimization, the representation is the entire candidate(hence no re-use of any results across candidates). With an optimization,
the representation includes the values previously computed and memoized invalues for each expression over t (for ASketch EvalExp ) or for each subformulain the candidate (for ASketch EvalSub ). The values map is populated by thehelper functions memoExpression and memoSubFormula, shown in Algorithm 4.
An interesting aspect is handling free variables in expressions; memoExpression
does that by trying all possible atoms for the domain of the expression, e.g.,
if the expression is n.*link, and n’s domain is Node, then memoExpression will64

compute the value of n.*link for all possible Node atoms in the scope.
The algorithm caches not only expression and formula values but theentire candidates, represented via the values of their expressions and formulas.
If the representation rep is encountered for the first time, the algorithm calls
the Evaluator and stores the result in cache. However, should cache containrep, then the algorithm has already encountered a candidate that is equiva-

lent (w.r.t. to the test), and the previous result from cache is reused. If the
Evaluator returns false or the previous result was false, the candidate failed

a test, and the loop exits without trying other tests. If the candidate does
pass all tests, the candidate is printed as the solution.
In sum, our optimizations specifically target reducing calls to the Evaluator.
Compared to SAT solving, those calls are cheap. However, they are not negligible; to evaluate a candidate, ASketch Eval needs to parse the candidate formulas– which can add to the cost when there are a large number of long, complex
candidate expressions. By breaking the problem up into subproblems, which
are much less expensive to solve for, we reduce the overall cost of the approach.
Additionally, our optimizations are able to identify ways to prevent making –what are in the end – duplicate checks.

5.4

Experimental evaluation
We use 24 subjects derived from five core Alloy models: LinkedList

from Section 5.2, BinaryTree models the acyclicity constraint of a binary tree,
Contains checks whether a list contains an element, Remove models remov-65

Algorithm 4: Helper Functions for Candidate Checker.
Input: test (t), Alloy expression (e) or formula (f )Output: value of e (or f ) for t
Function memoExpression(t, e)
if !values.containsKey(t, toString(e)) then
if !containsVariables(e) thenvalues[(t, toString(e))] = eval(t, e)
else
foreach atom a of e’s domain dovalues[(t, toString(e))] += eval(t, e, a)
return values[(t, toString(e))]
Function memoSubFormula(t, f )k ← ””
foreach Expr e in f.getExprs() do k += memoExpression(e)foreach Non-expression hole h do
k += cand.getValueForHole(h)if !values.containsKey(t, k) thenvalues[(t, k)] = eval(t, f)
return values[(t, k)]ing an element from a list, and Dijkstra models Dijkstra’s mutual exclusion
algorithm.
For each core model, we picked one predicate and created several sketching subjects by increasing the total number of holes (H#) in the body of thepredicate, from left to right. This process enables us to systematically createmodel variants to explore how the number of hole(s) affects our techniques.
For example, for LinkedList, we identified 3 operator holes and 2 expression
holes in the Acyclic predicate and produced these 5 variants:\Q\ n: Node | n in List.header.*link => n !in n.^link\Q\ n: Node | n \CO\ List.header.*link => n !in n.^link66

\Q\ n: Node | n \CO\ \E\ => n !in n.^link\Q\ n: Node | n \CO\ \E\ => n \CO\ n.^link\Q\ n: Node | n \CO\ \E\ => n \CO\ \E\

We will refer to the different sketches produced over a base model asmodel variants. For each core model, we built up a test suite (full ) for themodel variant with the most holes such that the suite has at least 16 tests
and all solutions found using ASketch are equivalent. Both the BinaryTree
and Remove models have 20 tests, rather than 16. For the input fragmentsfor operator holes, we use the Alloy grammar as outlined in Table 5.1. For
expression holes, we use two optimized versions of ASketch Gen – static pruningand dynamic pruning – presented in [75]. Experimental results in [75] show
a trade-off between the two approaches: static pruning finishes in seconds but
produces larger fragments in comparison to dynamic which can take minutes
but produces smaller fragments. For a robust look at ASketch Eval , we will
run experiments over both fragment generation techniques to see the impactof a sketch’s fragment sizes on ASketch Eval ’s runtime. Table 5.2 shows boththe size of the expression fragments produced for each expression hole and thetime taken. The times reflected in the remainder of the evaluation section do
not include ASketch Gen ’s run-time.
Our experiments are performed on a MacBook Pro running OS X El
Capitan with 2.5 GHz Intel Core i7-4870HQ.

67

Table 5.2: ASketch Gen details
Model
LinkedList
BinaryTree
Contains
RemoveDijkstra

5.4.1

Hole
3,5
2,4,6
1,3
1,3,4
2
6

Static
67
617
621
1210
9
21

Dynamic
57
496
227
449
9
21

ASketch Eval results

ASketch Eval Performance. Table 5.3 shows the solving time for various
sketching problems using different fragment generation approaches and test
suite across all three ASketch Eval approaches. The columns AEB , AEE and AES
show the time for the basic ASketch Eval , ASketch EvalExp , and ASketch EvalSub ,respectively. Our experiments use half-size and full-size test suites, where thehalf test suite is the first half of the full test suite. The half-size test suite canprecisely sketch some of the model variants that have a few holes, but, withthe exception of LinkedList, does not fully capture the sketching problem forthe model variants with more holes. For all 24 sketches, using the full test
suite allows only the desired model to be produced. Therefore, to validate
our implementation, we used the Alloy Analyzer to check that every solution
produced by our technique over the full test suite is correct, i.e. equivalent toour desired formula. Additionally, we checked that every solution generated
in the experiments is plausible by checking that each solution passes all the
tests associated with its generation.
As the number of holes increases, both ASketch EvalExp and ASketch EvalSub
68

69

DijkstraRemove Contains

BinaryTree

LinkedList

1H
2H
3H
4H
5H
1H
2H
3H
4H
5H
6H
1H
2H
3H
1H
2H
3H
4H
1H
2H
3H
4H
5H
6H

Model

Static Pruning
Half Test Suite
Full Test Suite
AEB AEE AES
AEB AEE AES
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.4
0.2
0.2
0.4
0.3
0.2
1.3
0.5
0.2
1.5
0.5
0.3
16.2
3.6
0.6
15.9
4.0
0.7
0.0
0.0
0.0
0.0
0.0
0.0
0.5
0.4
0.3
0.5
0.5
0.4
0.6
0.5
0.3
0.5
0.5
0.4
36.2
6.7
1.2 154.3 14.8
2.7
⊥ 50.3 12.2
⊥ 57.2 12.4
678.2 30.7
9.0
⊥
⊥
⊥
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.1
0.3
0.3
0.3
0.3
0.3
0.3
0.3
0.3
0.3
1.8
0.8
0.8
1.8
0.8
0.7
10.2
1.1
1.1
10.6
1.1
1.2
19.4
1.1
0.9
⊥ 76.5 57.3
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.1
0.1
0.0
0.1
0.1
0.0
0.1
0.1
0.0
0.1
0.1
0.0
0.2
0.2
0.1
0.2
0.1
0.1
5.5
4.0
0.6
6.5
4.3
0.6

Dynamic Pruning
Half Test Suite
Full Test Suite
AEB AEE AES
AEB AEE
AES
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.4
0.2
0.2
0.4
0.2
0.2
1.3
0.4
0.2
1.5
0.5
0.3
14.1
3.4
0.5
13.7
3.9
0.6
0.0
0.0
0.0
0.0
0.0
0.0
0.4
0.4
0.3
0.5
0.4
0.3
0.5
0.4
0.3
0.5
0.4
0.3
31.9
6.1
0.9 120.7 13.4
2.0
⊥ 42.27.8⊥ 48.59.3
769.0 41.7
7.4⊥
⊥ 776.4
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.1
0.2
0.2
0.2
0.2
0.2
0.2
0.2
0.1
0.2
0.8
0.4
0.4
0.8
0.4
0.3
4.8
0.6
0.6
4.6
0.6
0.6
6.5
0.5
0.4
⊥ 12.4
9.5
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.0
0.1
0.1
0.1
0.1
0.1
0.0
0.1
0.1
0.0
0.1
0.1
0.0
0.2
0.2
0.1
0.2
0.1
0.1
6.4
3.9
0.6
6.6
4.7
0.8

Table 5.3: ASketch Eval performance for finding the solution. Times are inseconds. ⊥ indicates a timeout (>15 min).

make significant gains over the base algorithm; the base ASketch Eval outperforms the optimizations only for Contains 3H, where the optimizations provide
a minor overhead given how quickly the solution is found. Additionally, table 5.3 shows that ASketch EvalSub outperforms ASketch EvalExp . This behavior
is expected, as a subformula would increase the chance for redundancy compared to an expression. All in all, across both static and dynamic pruning results, ASketch EvalSub ’s performance is relatively fast, with all but two sketches
finishing in under a minute, and almost all finishing in under 10 seconds.
With an on-average fast run time and better performance than the otherASketch Eval algorithms, ASketch EvalSub is a solid initial approach to sketching
Alloy models. There is one notable exception: BinaryTree 6H. For this sketch,
ASketch EvalSub , like the other versions, times out using static pruning, but
is the only version of ASketch Eval to not time out using dynamic pruning.
However, ASketch EvalSub takes 13 minutes to find a solution. This variant
has the largest candidate solution space to explore, totaling over 7.8 billion
for dynamic pruning (3 operator holes each at size 4 and 3 expression holes
each at size 496) and requires the largest number of candidate solutions to
be explored at over 756 million. However, large candidate solutions do notnecessarily hurt ASketch EvalSub ’s performance: for static pruning, Remove 4H
has over 5.3 billion candidates solutions and explores 311 million of them before
finding a solution in 57.3 seconds.
Comparing Optimizations. Comparing the optimized versions of ASketch Evalto the base implementation, ASketch EvalExp and ASketch EvalSub are effective at70

Table 5.4: Number of calls to the Evaluator using dynamic pruning expressions
and the full test suite. ⊥ indicates a timeout (>15 min).
Model Variant
LinkedList 5H
BinaryTree 6H
Contains 3H
Remove 4H
Dijkstra 6H

For Opt.
AEE
AES
273
607
⊥ 36397
412
471
2896
3864
195
537

#Evaluator Calls
Checking Candidates
AEB
AEE
AES
AEB
88473 10839
137
88473
⊥
⊥ 6575
⊥
393
59
0
393
⊥ 11878 2450⊥
137356 51830 1430 137356

Total
AEE
11112
⊥
471
14774
52025

AES
744
42972
471
6314
1967

decreasing the runtime, often significantly. For instance, consider Remove 4H,
in which the base ASketch Eval technique times out while ASketch EvalExp finishes in 12.4 seconds (or 76.5 using static pruning) and ASketch EvalSub finishes
in 9.5 seconds (or 57.3 seconds using static pruning). Digging deeper into theactual work done for the different algorithms, Table 5.4 looks at the numberof calls made to the Evaluator to: (1) perform the optimizations – columns
2 and 3, (2) check if a candidate solution passes a test case – columns 4 - 6
and (3) the sum of the calls made for (1) and (2) – columns 7 - 9. Column 1
indicates which model variant we are considering: for each model, we selected
the largest model variant.
Contains 3H represents an interesting corner case in which ASketch EvalExp

and ASketch EvalSub make the same number of calls to the Evaluator. For
this model variant, the entire sketch is one formula with no subformulas, ASketch EvalExp and ASketch EvalSub will end up doing the same amount of work.
In particular, ASketch EvalSub does not need to use the Evaluator to check any
candidates, as the representation produced by the optimization for a “subfor-

71mula” captures the behavior of the candidate over the test valuation.
The number of Evaluator calls that ASketch Eval makes reduces as moreadvanced optimizations are used. Specifically, the basic algorithm makes thehighest number of Evaluator calls and ASketch EvalSub has the smallest number of calls, with ASketch EvalExp in between. While ASketch EvalExp makes
less calls to the Evaluator to perform the optimization, ASketch EvalExp makes
more overall calls to the Evaluator than ASketch EvalSub , including more of
the expensive calls to check the candidate’s behavior over a test valuation. In
other words, ASketch EvalExp forms less equivalence classes over the candidate
solutions, requiring more overall work to find a solution to the sketch. On theother hand, ASketch EvalSub makes more Evaluator calls to form less equivalence classes, resulting in less work and thus better performance. Overall,while the optimizations do extra work to determine a candidate’s equivalenceclass, the trade-off of grouping candidates together to reduce the number ofcandidates which need to be individually checked across a test valuation is
worth it, as seen by the difference in performance across the techniques inTable 5.3, especially as the complexity of the sketching problem grows.
In the end, as ASketch EvalSub is almost always the fastest, it is currently the best technique for sketching Alloy programs. The main strengthof ASketch EvalSub is the optimization’s ability to avoid checking redundantcandidates, and instead directly applying the previous evaluation result. ASketch EvalSub finds more redundancy than ASketch EvalExp , giving ASketch EvalSub
consistently better performance across our range of models, test suites, and72

fragment generation approaches. Regardless of optimizations, ASketch Eval ’s
run-time is dependent on finding a solution by exploring combinations. The
more combinations there are, the longer the search may take. Future work candetermine if different orderings of the generated expressions, different exploration of the holes, or different ordering of the tests can improve ASketch Eval ’s
performance.

5.5

Summary
We introduced ASketch, the first approach for sketching Alloy mod-els. Given a model with holes and some valid and invalid valuations, ASketch
completes the model with respect to the valuations. The ASketch framework has three key components: extending the Alloy grammar, outlining how
to generate a pool of candidate fragments for each hole, and exploring theresulting space of candidate models to find one that conforms to the valuations. ASketch introduces a suite of optimizations to efficiently explore verylarge spaces of candidate models. An experimental evaluation using a suiteof subject sketches shows that ASketch introduces a promising approach forsketching Alloy models.

73

Chapter 6
Exploring Refinements To Enumeration-Based
Sketching of Alloy Models

6.1

Overview
In Chapter 5, we introduced a sketching framework for Alloy, ASketch,in which the user does not need to focus on developing complete and correct Alloy models, but instead can provide partial Alloy models that ASketch
completes for the end user. ASketch is based on the insight that our AUnit
tests enable a user to outline the expected behavior of a model. To solve thesketch, we introduced ASketch Eval , an enumeration-based approach that uses
constraint checking to explore candidate models. The optimized version, ASketch EvalSub , has proven to be a promising approach to sketching Alloy models(section 5.4, [75]).
A key attribute to make any sketching technique feasible for use isscalability. ASketch EvalSub is able to find solutions to almost all model variants
in under 10 seconds. However, for the model variant with the largest solution
space, BinaryTree 6H, ASketch EvalSub takes about 13 minutes to finish, which issignificantly longer than the next highest runtime at 9.5 seconds for Remove 4H.
Therefore, this chapter focuses on exploring avenues to improve the overall

74

run-time of ASketch Eval , motivated by improving BinaryTree 6H’s runtime.
For BinaryTree 6H, given our dynamic pruning list of fragments and thecurrent order in which we explore the space of candidate models, ASketch Eval
checks 756 million candidates before finding a solution. This highlights themain limitation of any enumeration-based technique: the technique may end
up searching over a large number of candidates. If the order we explore candidates remains the same, while we can optimize the work done for a candidate, we cannot avoid the need to explore 756 million candidates to sketch
BinaryTree 6H. To address this, our first refinement explores a multi-threaded

implementation of ASketch Eval , where we outline how to explore the solution
space in parallel.
Notably, exploring hundreds of millions of candidates does not guarantee a long run time. In comparison to BinaryTree 6H, consider Remove 4H
using static pruning fragments. ASketch EvalSub explores 311 million candidates – 2.4 times less candidates than BinaryTree 6H – but finds a solution in
57.4 seconds – 13.5 times faster than BinaryTree 6H. Why is Remove able toexplore candidates faster than BinaryTree? Upon comparison, Remove 4H has
fewer equivalence classes than BinaryTree 6H thus enabling the ASketch Eval
to explore candidate models faster, as a whole. In section 5.4, we saw thebenefit of fewer equivalence classes in the difference in performance between
ASketch EvalExp and ASketch EvalSub , where our per candidate level optimizations compound to given ASketch EvalSub a markedly better performance.
A series of improvements made at the implementation level of AS75

ketch Eval since its initial embodiment further supports this insight. Over time,
our embodiment of ASketch Eval has improved, as we have found various redundancies in the implementation that could be removed. For instance, one such
improvement is utilizing the fact that when we explore the next test candidate,
not all of the subformulas change. As a result, we can keep a local reference
to the representation of each subformula in the sketch, and only look for a
new representation when some subformula differs from the previous candidate
explored. This reduced the work per candidate solution, and served to reduce
the run time over the BinaryTree 6H using ASketch EvalSub from 1078 seconds
to 776.4 seconds. Accordingly, our second improvement to ASketch Eval focuses on improving the order of the test valuations, one of the main inputs
to ASketch, which impacts the amount of work each candidate solution must
do: the earlier a candidate is eliminated by a test, the less overall work the
candidate does.
In total, this chapter makes the following contributions:ASketch Eval Multi-Threaded: We introduce the idea of breaking the spaceof candidate models to be explored by ASketch Eval into a series of smaller
domains to explore in parallel.
Exploring Test Order: We outline and provide the results of a random testorder experiment, designed to determine the impact of the test order on theoverall run-time of ASketch Eval .
Guidelines for Test Valuations: Based on the random test order study, we76

present a series of guidelines for both the generation of a test suite as well asordering a test suite for sketching purposes.
Experiments: We present an experimental evaluation of our multi-threaded
technique and produce the random test orders runs over a small but intricate
collection of Alloy formulas, previously used to evaluate ASketch Eval .
The remainder of this chapter is organized as follows. Next, we will outline our subject Alloy models which will be used to evaluate both improvements
to ASketch Eval . Then, we will both step over and evaluate our multi-threaded
implementation. Lastly, we will present our random test order experiment andprovide an analysis of the results, culminating in a set guideline for generating
and ordering test suites for sketching.

6.2

Subjects
As we explore different optimizations to ASketch Eval , we will reason

over results from five core models. Two models represent common data structures: LinkedList and BinaryTree capture the acyclic property of a singlylinked list and a well-formed binary tree respectively. Two models reason overa list in which node’s contain an element value: Contains checks if a given
element is in the list and Remove checks if a given element has been removed
from the list. Lastly, Dijkstra captures the deadlock property that is prevented by Dijkstra’s mutex ordering algorithm. All experiments were run fora scope of three. Sketches were formed by abstracting away one predicate fromeach model, iteratively building sketches by removing one valid construct each77

iteration, as we did in our experiments in section 5.4. For our experiments,
we used dynamic pruning output from our ASketch Gen approach outlined in[75]. For the input test suites, we used our full test suite from our prior experiments, which encapsulates our sketching problem. For LinkedList, Contains,and Dijkstra the test suite consists of 16 tests, while BinaryTree and Remove
have 20 tests. All experiments use the same set of subjects and test suites.
The experiments were run on an Intel Core i7-4790K Quad-Core 4.0 GHz on
Windows 7.

6.3

Multi-Threaded ASketch Eval
ASketch Eval is overall an enumeration technique which iterates over all

possible combinations, until a solution is found. As a result, ASketch Eval lends
itself to a multi-threaded algorithm, since the domain – the entire collectionof unique candidate solutions – can be divided across threads and checkedin parallel. In this section, we will outline a multi-threaded implementation
evaluated using ASketch EvalSub .
6.3.1

Approach
To demonstrate how a multi-threaded algorithm would work in thecontext of ASketch Eval , we will first step over how ASketch Eval currently enumerates over the domain of all possible candidate models. Before sketching,for each hole, we determine the rate at which the hole should change the value
it contributes from its fragment list, following the findRateOfChange function78

in algorithm 5. The first hole increment is set to 1, meaning that the candidate presented by “hole 0” will change every time. From there, a hole’s “rateof change” is set to the multiple of all previous holes’ sizes. The results are
stored in an array, rateOfChange, which will be used by the main ASketch Eval
algorithm to facilitate iterating over candidate models.
In detail, ASketch Eval ’s iteration is driven by a combination algorithm.
To start, an outer loop iterates from zero to the total number of combinations,or until a solution is found and the loop is exited. For each iteration, an inner
loop determines if any hole(s) should be incremented to the next candidate
value by checking if the current counter, k, is evenly divisible by the increment
at which a given hole should be changed, rateOfChange[i]. If so, then thathole is incremented to the next value, as outlined in the last loop of algorithm 6.
For a multi-threaded implementation, we will divide one range, [0, totalCombinations], into a series of smaller ranges to be sent to individual threads.
Easily, these ranges can be set up to have no overlap; however, the challenge
is in determining what candidate solution the start of the range depicts. Additionally, we want a simple approach that will not add significantly to thestart up cost of the thread. Our methodology for getting the starting value
is depicted in findStartingValues in algorithm 5. First, we determine thenumber of times the hole has changed the value it contributes, which can be
determined by dividing the starting value by the increment at which the holeis meant to change. This number, numChanges, in theory shows how far into
its iteration a given hole is. However, it is possible that a hole has looped over79

Algorithm 5: Helper Algorithms for Multi-threading
State: holeSize = size of candidates for each hole
numHoles = number of holes
Output: rate of change for each hole stored in rateOf Change
Function findRateOfChange()long prevTotal = 1// find increment at which the hole should switch to a new
candidate value
for i = 0, i < numHoles, i++ do
rateOfChange[i] = prevTotal;
prevTotal *= holeSize[i];Input: starting position of range (start)
Output: population of pos based on start
Function findStartingValues(start)// find the starting candidate the hole contributes
for i = 0, i < numHoles, i++ dolong numChanges = start / rateOfChange[i];pos[i] = numChanges % holeSize[i];its size and is on a second(+) iteration; therefore, the starting contribution fora hole is calculated as the number of changes (numChanges) modulus the sizeof the fragment list for a hole (holeSize[x]). Algorithm 6 outlines the basic
structure each thread follows to complete the sketch. First, findStartValues
is invoked, then all the candidate solutions within the range sent to the thread
are executed. The bottom portion of the algorithm outlines how the candidate
solution is incremented to the next candidate within the range.

80

Algorithm 6: Multi-threading Outline
State: totalCombinations = total number of unique combinations
to solve the sketch
pos 7→ lookup for the candidate contributed by each hole
rateOfChange 7→ lookup for the interval at which each holechanges its contribution
findStartingValues(start)k ← start
while k < totalCombinations docand ← buildCand(pos)// ASketch Eval sketching code here...
k++for i = 0, i < numHoles, i++ do
if k % rateOfChange[i] == 0 thenpos[i] = pos[i] + 1;
if pos[i] == holeSize[i] then pos[i] = 0;

6.3.2

Evaluation
Table 6.1 shows the results for running ASketch EvalSub over our 24

different model variants for 1 thread, 2 threads, 4 threads, and 8 threads
respectively. The first two columns depict which model variant is being evaluated, while columns 3 through 6 show the runtime for the different numberof threads. The runtime does not include the time to generate fragment lists,
the work of ASketch Gen , but does include the time to start up and terminate
all threads.
Overall, our results show that a multi-threaded approach is a promisingavenue for improving ASketch Eval runtime. Of note, we do not expect a direct
decrease in time per thread: two threads will not necessarily speed up the81Table 6.1: Multi-threaded Experiment Results Using ASketch EvalSub .

DijkstraRemove Contains

BinaryTree

LinkedList

Model
1H
2H
3H
4H
5H
1H
2H
3H
4H
5H
6H
1H
2H
3H
1H
2H
3H
4H
1H
2H
3H
4H
5H
6H

Number of Threads
1
2
4
8
0.01
0.03
0.06
0.06
0.01
0.03
0.06
0.07
0.05
0.06
0.06
0.08
0.07
0.07
0.07
0.08
0.14
0.10
0.10
0.11
0.02
0.04
0.09
0.12
0.14
0.14
0.12
0.11
0.13
0.10
0.09
0.08
0.90
0.53
0.42
0.23
6.49
3.77
2.64
1.67
728.66 418.25 267.23 172.77
0.03
0.05
0.11
0.11
0.03
0.05
0.11
0.11
0.08
0.12
0.11
0.10
0.09
0.10
0.14
0.13
0.18
0.18
0.17
0.14
0.27
0.22
0.20
0.19
7.53
4.18
2.74
1.45
0.04
0.07
0.15
0.18
0.04
0.07
0.15
0.17
0.04
0.07
0.15
0.17
0.04
0.07
0.16
0.18
0.05
0.07
0.16
0.18
0.29
0.21
0.26
0.31

runtime by a factor of two. The work of ASketch Eval is to iterate over adomain until a solution is found. Therefore, at a certain point through athread, a solution will be found and all results will terminate. For our models
which finish in less than a second, the multi-threaded approach does add aminor overhead, which can cause the multi-threaded approach to be slower,82

albeit by 100 to 200 milliseconds. This overhead is not large enough to deter
the use of multi-threading. Furthermore, we can see the real benefit to a
multi-threaded implementation when we look at any of the model variants
which take longer than a second to solve: BinaryTree 5H, BinaryTree 6H, andRemove 4H. For BinaryTree 6H, ASketch EvalSub goes from taking 12.1 minutes

to find a solution with one thread to a more reasonable 2.8 minutes with eight
threads.
Multi-threaded approaches are limited by the system that is runningthe program, and this factor should come into play when determining how
many threads to run. However, even generating two threads provides a reduction for BinaryTree 6H from just over 12 minutes to just under 7 minutes.
Since exploring the ranges can be done in parallel without causing thread
conflicts which erode the benefits of a parallel approach, a multi-threaded
implementation of ASketch Eval is recommended.

6.4

Exploring Test Order
There is a simple optimization used by all ASketch Eval techniques thatis irrelevant to the variability of Alloy and the order of candidate exploration:
ASketch Eval explores the candidate solutions by looping over tests, and exits
this loop as soon as a candidate fails a test. As a result, the order in whichtests are explored has some impact on the time to the first solution. Consider
a test order in which the first two tests eliminates 75% of the candidates
compared to a test order in which the first ten tests are needed to eliminate
8375% of the candidates. The first test order would result in less work per
candidate, the main feature separating the base ASketch Eval ’s performancefrom the optimized versions. To explore just how much of an impact the testorder has on ASketch Eval ’s run time, we conducted an experimental evaluationof random test orders to answer the following questions: Does the order of tests
have a noticeable impact of the runtime? If so, what factors define a good testorder? And can these factors form a set of guidelines for test generation for
sketching Alloy models?
6.4.1

Random Test Order Experiment
To gather insight into what makes a test order “good”, we set up a ran-

dom test order experiment across all 24 model variants. Each run permutes thetest order with the only restriction being that the new order does not matchany previous order. Table 6.2 shows the results of exploring 100 random testorders using ASketch EvalSub . Columns 1 and 2 are used to show which model
variant is being considered. Then, column 3 shows the minimum runtime, column 4 shows the maximum runtime and column 5 shows the average runtime
across all 100 runs. All times reported in the table are in seconds.
From these results, it is clear that some test orders are better thanothers, as seen by BinaryTree 6H where the minimum run time is faster thanthe maximum run time by a factor of 4.3, which equates to the minimum
order finishing 37 minutes faster than the maximum order. Across all themodel variants, the minimum run time is anywhere from 2 to 4.5 times faster84

Table 6.2: Results for 100 Random Test Order Execution using ASketch EvalSub .

DijkstraRemove Contains

BinaryTree

LinkedList

Model
1H
2H
3H
4H
5H
1H
2H
3H
4H
5H
6H
1H
2H
3H
1H
2H
3H
4H
1H
2H
3H
4H
5H
6H

Min (s)
0.00
0.00
0.11
0.19
0.39
0.00
0.20
0.19
1.68
7.58
670.73
0.02
0.02
0.07
0.08
0.17
0.25
6.70
0.00
0.01
0.01
0.01
0.03
0.40

Max (s)
0.01
0.01
0.37
0.63
0.76
0.03
0.71
0.75
4.99
28.52
2904.94
0.05
0.04
0.27
0.31
0.96
1.17
13.77
0.00
0.07
0.06
0.07
0.07
0.78

Avg. (s)
0.00
0.00
0.26
0.36
0.56
0.01
0.36
0.35
2.78
13.03
1193.48
0.03
0.03
0.13
0.16
0.40
0.53
8.72
0.00
0.02
0.03
0.03
0.04
0.55

than the maximum run time. The order of tests having such an impact on
the run time is similar as to why the equivalence class optimizations ASketch EvalExp and ASketch EvalSub can make substantial decreases in run time:the more candidates eliminated early, the less overall work needs to be done
at a per candidate level. When exploring potentially billions of candidates,
which BinaryTree 6H and Remove 4H can require, catching a majority of the85candidates early is significant. In detail, for the best test order from the random runs over BinaryTree 6H, the first three tests eliminate 98.5% of all the
candidate solutions. On the other hand, for the worst test order, the first
three tests eliminate just 7.7% of the candidates, and nine tests are required
to eliminate over 98.5% of the candidate solutions, which as we have seen, led
to a difference of 37 minutes in their run times.
6.4.2

Guidelines for a Sketching-Based Test Suite
Since the test order does impact the run-time, we want to extract some

general lessons from stepping over the random test order results, in combination with lessons learned from generating our own test suites for sketching.
To form our initial test suites, we started with a base of two tests. Then,
we used our ASketch EvalSub technique to search for the first incorrect solution
and used the solution to produce a counterexample which we turned into atest. This process was repeated until only valid solutions were found. Throughour analysis of the random test orders, we gained additional insight into why
our initial test generation process produced certain tests and did not produce
other tests. In total, we present three guidelines to follow when generating
and ordering a test suite for sketching purposes.
1. Explore different valid and invalid behaviors first. Our first andmost important guideline is to focus on formula level differences at the beginning of a test order. When looking out our best performing test orders, theinitial tests explore a range of different ways that the formula being sketched

86

T0

root

N0

T0

right

root

N0

N1

N2

right

N1

root

N0

right
N1

T0

right

left

N2

N0

left

N1

left

root

left
left

T0

T0

root

N0

N2

T0

root

N0

T0

root

N0

T0

root

N0

left
left

right

left
N1

N1

left
N1 right

left

N1

right
N2

N2

left

Figure 6.1: First four tests from the best test order (top) and first four testfrom worst order (bottom) for the binary tree variant with 6 holes.

could be true or false. For instance, for our BinaryTree model, there are threebasic criteria for a binary tree to be well-formed: (1) no node in the tree isreachable from itself, (2) any node in the tree has one parent, and (3) no nodein the tree left and right fields point to the same node. Figure 6.1 reflects thefirst 4 tests from the best random order over BinaryTree 6H on top, and first
4 tests from the worst random order on bottom.
As we can see in Figure 6.1, the fastest random test order covers: (1) the
formula being true, (2) the formula being false because a node’s left and right
relations point to the same node, (3) the formula being false because a node has
multiple parents and (4) the formula being false because a node is reachable

87

Table 6.3: Characteristics of the first 5 tests in the best and worst test orders.
B
W

1
60.0
60.4

% Cand Eliminated
2
3
4
5
94.6
96.4
98.6
99.9
61.4
65.5
93.8
96.4

1
13.6
30.3

Formula Coverage
2
3
4
50.0
72.7
77.2
33.3
33.4
54.5

5
90.9
54.5

BinaryTree 6H

B
W

91.1
4.9

94.2
7.0

98.5
7.7

98.9
16.5

99.6
20.1

41.7
41.7

58.3
66.7

79.1
66.7

95.8
66.7

100.0
83.3

Contains 3H

B
W

83.8
17.1

98.1
19.0

98.1
19.0

98.1
20.0

100.0
20.0

40.0
20.0

100.0
20.0

100.0
20.0

100.0
60.0

100.0
60.0

Remove 4H

B
W

84.3
12.5

92.4
19.5

96.2
22.7

99.5
74.6

99.6
98.5

28.6
42.8

42.8
57.1

57.1
57.1

85.7
68.2

85.7
85.7

Dijkstra 6H

B
W

82.2
17.8

91.8
26.4

98.9
26.9

99.9
30.4

99.9
36.3

37.5
25.0

68.7
68.7

75.0
68.7

93.7
75.0

100.0
81.2

Model

Ord

LinkedList 5Hfrom itself. Furthermore, nodes are both reachable from the tree and not.
However, the first 4 tests from the worst order all focus on one main failing
attribute: a node reachable from itself. Additionally, due to a self loop, thefourth test also captures a node having multiple parents and unlike our bestordering, all nodes are in the tree.
To expand on this observation, Table 6.3 dives into the behavior of thefirst 5 tests for the best (B) and worst (W) performing test orders. Column 1
highlights the model variant under consideration: we will look at the largest
model variant for each base model. Column 2 shows which test order is being
explored. Columns 3 through 7 show the percentage of candidate solutions
eliminated by the first x tests in increments, i.e. the first 1 test, the first 2
tests, etc. Columns 8 through 12 show the formula level coverage of the firstx tests in the same increments.
Table 6.3 show the worst test orders have a period of stagnant formula
coverage at the beginning of their test suites. In contrast, the best test orders
are constantly improving their formula coverage. When we compare this to88the percentage of candidates being eliminated, we can see the direct impactthat this stagnant coverage period has on our ability to eliminate candidates.
While all of our tests will eliminate some candidates, having stagnant formula
coverage means each additional test provides the same coverage as some previous test, thus reducing a test’s ability to eliminate unique candidate solutions
compared to the preceding tests. To see this in detail, we can look at theworst order for LinkedList 5H. Test one through three have a period of nearlystagnant coverage, which correlates to minute increases in the percentage ofcandidates being eliminated. However, the jump in coverage with test fourtranslate to a big jump in the percentage of candidates eliminate. Of note,the best test order does not always start with or have the highest formula
coverage, but the best test order is constantly improving the formula coveragein the beginning.
However, an important caveat to this guideline is that we do not wantto ignore the intricacies of how these passing and failing behaviors occur whengenerating a test suite. Below are 3 valid valuations of our BinaryTree modelfrom our full test suite:
T0

root

N0

T0

root

right

N0

T0

left

left

N1

N1

root

N1

N0
right
N2

These 3 tests eliminate unique candidates with respect to each other; therefore,
all three are important when it comes to sketching BinaryTree. However,89there is significant overlap in the candidate solutions these tests eliminate.
Accordingly, we would not want to place these three tests next to each otherin our test order.
Based on Table 6.3 and graphical inspections of good and bad test orders, we can see the importance of focusing on exploring diversity at a formulalevel viewpoint in the beginning of the test order. After which, we can narrowin on the different ways these behaviors can occur, such as one tree being valid
because of the left relation, a different tree being valid because of the right
relation and a different tree being valid because of both the left and right
relation.
2. Note any concrete formulations of your sketch. Any part of the
to-be-sketched formula that is concretely provide can have an impact on thevalue of a test. To form our test suites, we used the largest model variant (themodel variant with the most holes) to produce the test suite. Therefore, someof the tests will reason over concrete portions of our smaller model variants,
which do not have a fully abstracted formula. Consider the partial model forour variant BinaryTree 4H:

one sig BinaryTree { root: lone Node }sig Node { left, right: lone Node }pred IsTree{
all n : Node | n in BinaryTree.root.*(left + right) => {n \CO\ \E\ and \UO\ \E\ and no n.left & n.right}}

For this model variant, two of the properties needed to produce a well-formed90

tree are abstracted away into a sketch, while one property, no node in the tree
has the same left and right relation, is concretely specified. When we look at
the slowest orders for BinaryTree 4H, we find that the following invalid test isin the beginning of test orders:
T0

root

N0

right
N1
right

left
N2

This valuation is in place to help sketch "no n.left & n.right", whichis explicitly specified in BinaryTree 4H. As a result, the test depicted above
eliminates 0 candidates – the concrete portions of the formula ensure that every
candidate solution will correctly evaluate to false for this test valuation.
We can further see this behavior if we look into why the empty tree
is never produced as a test for our BinaryTree model. Typically, the empty
instance is an interesting corner case to consider; however, if we add the empty
tree to our sketching test suite, we will find that the test eliminates 0 candidates across all BinaryTree model variants. If we take a closer look out oursketch for BinaryTree, we can see the sketch is embedded in a universally quantified formula ("all n : Node {...}"). As a result, over the empty tree, allcandidate solutions will simply reduce to the vacuous result of this quantified
formula. In other words, the substitutions we make into the holes has zero
impact on whether a candidate solution will pass this test, resulting in zero91

candidate solutions being eliminated. Therefore, this is an important guideline
to take into account when generating a test suite for sketching, as a test which
eliminates no candidates will only serve to slow down the runtime.
3. Remember, in Alloy, any behavior you have not ruled out isvalid. Our last guideline is really a general reminder that in Alloy unless you
rule out a behavior the Alloy model will allow it, which should factor into thecharacteristics you capture in the valuations for your test suite. Consider thecase of generating tests for our BinaryTree model for sketching. We shouldtake into account our various signature and relation multiplicity constraints.
However, we do not have a “connected constraint” requiring all Node atoms to
be in the binary tree. Therefore, it is valid for nodes not to be in the tree, andthis behavior can have an impact on the validity of the tree itself. Below wedepict 4 different valuations which come from our BinaryTree full test suite,where valuations(a) and (c) are labeled valid and valuations (b) and (d) arelabeled invalid:

92

(a)

(b)

N0

N1
right

left
T0

root

N2

left

N1

T0

(c)

left

root

N0

(d)
left
N0
N0

right
T0

root

left

N1
T0

left
N2

root

N1

left

These test valuations show that (a) it is possible to have invalid disconnected nodes as a parent to a node in a valid tree; (b) valid disconnected nodes
can lead to an invalid valuation; (c) valid disconnected nodes can still lead tovalid valuations; and (d) invalid disconnected nodes can still lead to invalid
valuations. These varying ranges of behaviors all serve to eliminate candidate
solutions and are all based on exploring the impact of nodes disconnected fromthe tree.
Whether the test order was fast or slow, at about the half way markthrough the test order, around 98% of the candidate solutions have been eliminated. The second half of the test suite serves to finalize the sketching behavior. However, there is a notable difference between how quickly the fastertest orders eliminate the first 98% compared to how quickly the slower test93

orders eliminate the first 98% of candidates. Our slower test orders always
contain a period in the beginning in which minimal gains are made to eliminate candidates, thus increasing the amount of work done, on average, to ruleout incorrect candidates. In the end, our first guideline – cover the uniquehigh-level properties at which you envision the to-be-sketched formula to betrue and false – is the most important factor for an efficient test order forsketching. However, adhering to our second and third guidelines remains important when generating the test suites as ignoring these guidelines can resultin tests with poor ability to eliminate candidates on their own.

6.5

Summary
Currently, ASketch EvalSub is the recommended methodology for sketch-ing Alloy models. In addition to an enumeration based technique, [75] presents
ASketch Solve , a solving based approach to sketching Alloy models. ASketch Solve
encodes the model under sketch, the test cases and the candidate fragments
into one aggregate Alloy model, and asks the Alloy Analyzer to solve for asolution to the sketch using its SAT-based backend. The results in [75] showthat the more advanced ASketch Solve technique using a symbolic approach
performs worse than the simpler ASketch Eval technique based on enumeration (when accompanied with good optimizations in ASketch EvalSub ), with thenotable exception of BinaryTree 6H, the case that is the motivation behind
our efforts to improve ASketch Eval . Accordingly, this chapter focuses on two
different avenues to improving ASketch Eval ’s runtime. Due to ASketch Eval ’s

94

enumeration-based approach, a multi-threaded implementation is a well-suitedmethod for improving ASketch Eval ’s runtime, as our results show. In addition,
our random test order experiments reveal that even the order of tests candrastically impact the run-time of a sketch. To reduce the likelihood of a user
supplying a bad test order, we introduce a series of sketching-based test suite
guidelines, directed at both the order of the tests and the generation of thetests.

95

Chapter 7
Formula-Based Sketching Of Alloy Models

7.1

Overview
The work outlined in previous chapters has focused on using traditional

testing paradigms – automated test generation (Chapter 4) and program synthesis through sketching (Chapter 5) – to help develop a stronger validation
environment for Alloy. Prior to the introduction of AUnit as a testing framework, end users of Alloy performed ad-hoc measures to validate their models
within the Alloy Analyzer toolset using two common approaches. One, instance enumeration where users run a command in Alloy and visually inspect
the instances displayed by the Alloy Analyzer for their correctness. Two, assertion checks, where the user looks for the existence of expected logical relationship between formulas, and uses an assertion to check that the relationshipholds.
Our initial approach to sketching Alloy models is rooted in the development of AUnit. Specifically, ASketch is based on the insight that test
valuations enable the user to outline the expected behavior of an Alloy model.
Using this expected behavior, ASketch can iterate over all possible solutions
to a sketch, eliminate candidates which violate that behavior, and report so-96

lution(s) to the user which match the behavior, i.e. pass all the tests. While
test valuations are an important input to ASketch, we can utilize existing
validation practices of Alloy users for ASketch inputs.
In particular, we introduce ASketch Equiv , a formula-based sketching approach which is centered around the logical equivalence between an input formula and the to-be-sketched formula. A common assertion used for validationis checking for the logical equivalence between two formulas. By definition,a formula intended to be equivalent to another formula outlines the expectedbehavior of the second formula. As a result, by taking an equivalent formula
as input, ASketch Equiv does not require a user-provided test suite. Instead,
ASketch Equiv uses AGenW B to produce a test suite based on the equivalent
formula, orders the test suite based coverage information, and lastly utilizes
an ASketch Eval back-end to solve the sketch.
This chapter makes the following contributions:
Formula-based sketching: We introduce ASketch Equiv , a technique to sketch
Alloy models based on a user provided equivalent formula instead of user provided test suite. The technique uses a modified version of AGenW B to generatea test suite and leverage ASketch EvalSub to solve the sketch.
Embodiment: Our implementation for ASketch Equiv is based on both theembodiment of AGenW B and ASketch Eval . Furthermore, our toolset provides
a concrete implementation of the sketching-oriented test suite guidelines fromthe results of our random test order experiment (section 6.4).

97

module list.v.3
one sig List { header: lone Node }sig Node { link: lone Node }pred AcyclicSome {no List.header or some n : List.header.*link | no n.^link}

pred AcyclicOther {\Q\ n : List.header.*link | \E\ \CO\ \E\}check { AcyclicOther <=> AcyclicSome }Figure 7.1: A singly-linked list model with one specified acyclic predicate andone sketch predicate.

Experiments: We perform an evaluation of ASketch Equiv over a suite ofAlloy models that have two different formulations of the same property. Our
experimental results show that despite structural differences in the formulas,
AGenW B test suites in combination with with the embodiment of our testorder guidelines are able to sketch Alloy models effectively.

7.2

ExampleTo explore sketching through equivalence, we will step over a model ofa singly-linked list with two different representations of an acyclic property –one a fully specified predicate and the other a to-be-sketched predicate.
Our model is introduced by the keyword module which names the model,

98and enables the model to be imported into other models. Next, two signatures
paragraphs are declared (sig List and sig Node). Signatures introduce a
set of atoms, e.g. our model has two sets: one named List and a separate
set named Node. Within a signature paragraph, 0 or more relations can be
introduced. Relations can introduce relationships between atoms within thesame set – e.g. link establishes a binary relation relating a Node atom to zeroor one Node atom, or relations can relate atoms over different sets – e.g. header
ensures each list’s header is either the empty set or a Node atom. Signaturesand relations can have multiplicity constraints such as “one sig List” which
requires the List set to be comprised of exactly one List atom.
Next, our model introduces two predicate (pred) paragraphs. The first,
AcyclicSome, uses disjunction (or) and existential quantification (some) todefine acyclic. The domain of the quantified formula is the set of Node atoms
in the list (“List.header.*link”). This is achieved by using set join(“.”) andreflexive transitive closure (“*”) to capture the set of Node atoms reachable
from zero or more traversals down the List’s header’s link relation. Using
reflexive transitive closure instead of transitive closure (“^”) ensures that thisset includes the List’s header. Any Node atom in this domain, n, is evaluatedto see if n has no link relation. In other words, if there is a null-terminatednode in the list, there cannot be a cycle in the list. In order for the existentiallyquantified formula to be true, then at least one element in the domain mustsatisfy this constraint. As a result, an empty list is incorrectly ruled out.
Therefore, we include the disjunction to account for the presence of either an99empty list (no List.header) or some node in the list is null-terminated.
The second predicate, AcyclicOther, is looking for another formulationof acyclic. The intent is to discover a representation that does not need theextra disjunction constraints, and instead can reason over a single quantified
formula. The predicate is primarily comprised of a series of holes: one quantifier hole (\Q\), 2 expression holes (\E\), and one compare operator hole (\CO\).
The only part of the formula given concretely is the declaration of the variablen and its domain List.header.*link, as variable declarations are not currently

supported by sketching.
The last part of our model is a check command, which asserts that our
AcyclicSome predicate should be true if and only if our sketched AcyclicOther

predicate is true. In other words, this check is looking for an equivalence
relationship between our two predicates. If this relationship does not hold,the Alloy Analyzer will produce a counterexample, a valuation in which a
difference in behavior between the two predicates can be seen.
With fragments of size 5, 57, 4, and 57 for \Q\, \E\, \CO\, and \E\respectively, ASketch Equiv searches through a potential state space of 64,980
solutions to find the following sketch for AcyclicOther:

all n : List.header.*link | n.^link in (Node - n)
The solution uses universal quantification (all) to state that for all
nodes in the list, the set of nodes reachable from the list (n.^link) is a subset

100

of all nodes minus itself (Node - n). ASketch Equiv finds this solution in 0.08
seconds, after taking 0.15 seconds to build a starting test suite consisting of 5
tests, and will generate 1 additional test while sketching.

7.3

Sketching by Equivalence
In this section, we present our ASketch Equiv technique, which utilizes

our previous ASketch framework (Chapter 5) and our automated input generation technique AGenW B (section 4.3.2). ASketch Equiv is a formula based
sketching approach, which unlike ASketch Eval , does not require the user toprovide a test suite. Instead, the user provides an Alloy formula which isequivalent to the formula the user wants to sketch. This formula does notneed to have the same structure as the to-be-sketched formula and does notneed to be formally presented within the model as a predicate or assertion.
Given an Alloy model with a sketch and an equivalent formula, ASketch Equiv
proceeds in two steps. First, a test suite is generated and re-ordered based on
the guidelines from section 6.4. Second, the sketch is solved, using a modified
ASketch EvalSub approach.
7.3.1

Building and Ordering a Test Suite
In contrast to our prior sketching approaches ([75]), a test suite is nota user provided input. Recall, for ASketch Eval , the test suite facilitated thesketching process. Specifically, ASketch Eval checks that candidate models pass
all tests and additionally, the tests enable our suite of optimizations shown to101

be effective at reducing the run time (section 5.4). In order to make direct useof ASketch EvalSub , the current recommendation for sketching Alloy models,as the backbone of ASketch Equiv , we need a test suite. Since the user does
provide an equivalent formula, we can leverage prior work which established amethodology for automatically generating test suites in Alloy (Chapter 4).
Generating the test suite:

Specifically, we will use a modified versionof AGenW B , coverage-directed input generation. There are a few notable differences with the approach presented in section 4.3.2. First, we will look togenerate a test suite which achieves maximum coverage of the equivalent predicate. Additionally, there is no need for any human intervention as an oracle ofthe tests because our equivalent predicate will act as a oracle for the generated
test suite. Lastly, when generating tests for coverage only, we are interested incovering criteria that violate the facts of the model, as our intent is to provide
a small, but robust test suite to catch any bugs in the model, including thosein the facts. However, with sketching, the model is taken as is, meaning thefacts and any signature or relation constraints are assumed to be valid formulations. Therefore, we are not interested in generating tests over coverage
requirements which violate the facts of the model.
When it comes to generating the test suite, we can re-use the structureof algorithm 2 presented in section 4.3.2, as our changes to AGenW B are in theperimeter. Specifically the call to M.extractRequirements() will now reflect
the changed scope of coverage criteria we are looking for. Next, we will drop
the first if statement which checks if the instance produced by the targeting102constraint is satisfiable. Instead, we immediately treat the targeted criteria as
infeasible if running the empty command is unsatisfiable. Lastly, our test cases
can be immediately labeled valid and invalid based on their valuation over theequivalent predicate. This is already done by the algorithm, but AGenW B
requires a human oracle to confirm that this invalid or valid distinction is the
expected behavior. In our case, we can assume that the result based on theequivalent predicate is accurate.
Ordering the test suite: In section 6.4, experimental results show that theorder of tests has an impact on the sketching time; therefore, we want to apply
these guidelines to ensure we use an efficient test ordering. While AGenW B
produces test suites with maximum coverage, there is not a guarantee thatthe tests are in an order which achieves maximum coverage at the fastest
rate. Additionally, we are not concerned with overall model coverage, which
would factor in signature, relation, expression and formula coverage as equal
contributions. Instead, we are concerned with exploring a broad range of
passing and failing behavior over our equivalent formula, before narrowing inon specifics, such as the size of expressions when the formula containing theexpression is true. Therefore, our test suites will be rearranged to achievecomplete formula coverage first, then expression coverage, and lastly ordering
based on signature and relation coverage.

1037.3.2Completing the Sketch
With a test suite generated and reordered, we can now use various

aspects of our ASketch framework to complete the sketch. First, we still
have the problem of ASketch Gen , in which we will need to produce a list of
candidates fragments for each hole in the model. Once again, we can use theAlloy grammar to outline the fragments for all operator holes i.e. \UO\, \LO\.
In [75], we propose a methodology for automatically building up fragments
for expression holes, which was used previously to generate the expression
fragments for the evaluations done in Chapter 5 and Chapter 6. ASketch Equiv
will use the dynamic pruning ASketch Gen approach to generate the needed
expression fragments, which makes smaller fragment lists but can take minutes
to run. To solve the sketch, we will use the optimized ASketch EvalSub , whichcurrently outperforms all other Alloy sketching algorithms.
Algorithm 7 outlines the overall framework of ASketch Equiv , combining all of the different parts together to complete the sketch. First, we build
the test suite, using the modified AGenW B technique outlined in the previous section (buildTestSuite). Then, we re-order the test suite, as needed(orderTests). Next, we can start sketching following ASketch EvalSub ’s algorithm in which we use a memoized values map to form equivalence classes
over the candidates based on their expression and subformula evaluations overeach test case. The values map is leveraged to help build a representation fora candidate solution where a second map, cache, is used to determine if thisrepresentation has been encountered before. If this representation is encoun104

Algorithm 7: ASketch Equiv .
Input: ASketch model (M ), equivalent formula (equiv f ), fragments foreach hole (D)Output: candidate solution
State: values: (Test,String) 7→ String // caches computed
values ← {} // empty map
cache ← {} // empty map (Test,String) 7→ BooleanbuildTestSuite(M)orderTests(M, ts, equiv f)
foreach cand in buildCandidates(M, D) do
addTest ← false;
foreach t in ts do
rep ← ””// Perform subformula optimization
foreach subf in subformulas(M) do
rep += memoSubFormula(t, subf)
foreach hole h not in a subformula do
rep += cand.getValueForHole(h)if !cache.containsKey(t, rep) then
if !eval(t, cand) thencache[(t, rep)] = false
breakcache[(t, rep)] = trueelse if !cache[(t, rep)] then break
if last test case thenval ← checkCommand(“cand <=> equiv f”)// if check unsatisfiable, then no counterexample found,formulas are equivalent
if val.unsatisfiable then return candelse addTest ← true
if addTest then// check if instance should be allowed by the formula
if val.eval(equiv f ) thents.add(new Test(val, valid))else
ts.add(new Test(val, invalid))
values.put(ts.last, new String 7→ Boolean)cache.put(ts.last, new String 7→ Boolean)105

tered for the first time, the representation is evaluated across the test case;otherwise, the previous encounter with this representation is re-used.
However, when a candidate solution passes all tests, unlike ASketch Eval ,ASketch Equiv has the ability to know if a candidate solution matches the enduser’s expectation. Specifically, we can ask Alloy if the two formulas are equivalent, using a check command of the form:

check { candidateSolution[] <=> equivalentFormula[] }If this check fails, then we know that we have found an incorrect solution
to the sketch. We can adjust our test suite by taking the counterexample
produced by the sketch and turning it into a new test case. The valuation willbe the instance captured by the counterexample and the command will be valid
if the counterexample is an instance allowed by the equivalent predicate, andlabeled invalid otherwise. With the new test added to the suite, we can resume
sketching – all of our previous eliminated candidates are still incorrect and thecache and values mappings still reflect accurate information to continue re-using as required by the optimizations. Both mappings values and cache
will be extended to start collecting results for the new test case. Once thisequivalence check passes, the result is presented to the end user. This notion
introduces the spirit of iterative sketching, addressing the case where the sketch
remains the same but a test has been added to the suite.
While this is an easily built in functionality, our goal is to reduce theneed to generate any new tests while sketching. Section 6.4 highlights the test106

orders role in ASketch execution time, with the first handful of tests having
the largest impact. Therefore, we want to go into the sketching effort with an
initial set of tests where the first few tests together eliminate a majority of
the incorrect candidate solutions. Should our AGenW B technique not generatesome of the needed tests, we want to keep that to a minimal amount of narrowcorner cases. In particular, we do not want to miss any core features of oursketch such that we end up relying on our tests generated while sketching
to eliminate a significant portion of the candidates, which could significantly
impact the runtime.

7.4

Evaluation

7.4.1

Subject Models
Our evaluation is based on a suite of 7 core Alloy models. First, wehave a series of data structure based models, starting with the LinkedList
from our running example (Figure 7.1). Additionally, we use a model of a
BinaryTree which focuses on the acyclic property of a binary tree, Contains

reasons over whether or not a given element is in a list, and Remove looks
at whether a given item has been removed from a list. Then, we have threealgorithm based models: Dijkstra that reasons over the deadlock property
that Dijkstra’s mutex ordering algorithm should prevent, StronglyConnect
which enforces that a graph is strongly connected, and GphColor that looks tocolor a graph such that no connected nodes are the same color.
Each Alloy model has two versions of a predicate that are intended107to be equivalent. To confirm, we used Alloy to check for equivalence overthe scope used in sketching. Additionally, for every model, the two predicate
versions have different formula structures. For each model, one version of thepredicate is set as the “equivalent” predicate, and the other is turned into asketch, starting one hole at a time. For instance, for our example singly-linked
list model, the to-be-sketch predicate would be formed into a series of sketches
as follows:\Q\ n: List.header.*link | n !in n.^link\Q\ n: List.header.*link | \E\ !in n.^link\Q\ n: List.header.*link | \E\ \CO\ n.^link\Q\ n: List.header.*link | \E\ \CO\ \E\Our expression fragments were produced uses the dynamic pruning
approach to ASketch Gen . The experiments were run on an Intel Core i7-4790K
Quad-Core 4.0 GHz on Windows 7.
7.4.2

ASketch Equiv Performance
Table 7.1 captures various performance metrics for our ASketch Equiv

technique. The first column outlines which model variant of a subject model
is being used. Column 2 reflects the time taken to produce the appropriate
test suites, this includes the time to generate the test suites, as well as thetime to re-order the test suite, if needed. Columns 3 and 4 reflect the size ofthe test suite at the start and end of ASketch Equiv ’s execution: the test suite
may grow in size if the AGenW B produced test suite is not adequate. The lastcolumn captures the sketching time: the time from starting the sketch to the108

time the first solution is found. This time includes the time to generate a new
test, if needed. All solutions were checked for correctness by using Alloy tocheck that the solution formula is equivalent to our intended formula.
The time taken to generate our test suites is small, with most model
variants taking less than a second to produce the test suites. Additionally,
based on the time taken to complete the sketch, our ASketch EvalSub remains
effective at sketching Alloy models. In particular, most of the sketching times
are under a second and almost all are under 10 seconds. Our BinaryTree 6Hmodel variant retained most of the complexity from our prior sketching work,
resulting in the longest run time out of all model variants.
As a whole, the AGenW B based test suites were sufficient to sketch amajority of the sketches. At most, 4 additional tests are generated, as seenin BinaryTree 6H, and occasionally one or two tests were generated for thelarger model variants. For all model, the smaller model variants do not needto generate any additional tests, which is expected due to the smaller solution
space for the sketching problem. An interesting occurrence is the generation of
additional tests for the Remove 4H model variant but not the Remove 5H model
variant. A similar situation occurs with the StronglyConnect, in which an
additional test is produced for model variants 4H and 5H but not 6H. Generally, the model variant with the most holes is the “hardest” model to sketch,meaning that typically the entire formula structure has been abstracted away,
producing the largest state space to reason over. However, due to the expressive nature of Alloy, these large model variants can have multiple equivalent109

Table 7.1: ASketch Equiv performance. Times are in seconds.

StronglyConnect GphColor

DijkstraRemoveContains

BinaryTree

LinkedList

Model
1H
2H
3H
4H
1H
2H
3H
4H
5H
6H
1H
2H
3H
4H
5H
1H
2H
3H
4H
5H
1H
2H
3H
4H
5H
6H
1H
2H
3H
4H
1H
2H
3H
4H
5H
6H

Tcreate
0.17
0.18
0.19
0.15
4.32
4.92
5.08
4.69
4.75
4.77
0.19
0.23
0.16
0.18
0.16
0.82
0.95
0.82
0.73
0.86
0.34
0.37
0.34
0.30
0.35
0.27
0.93
0.89
0.97
0.78
0.70
0.68
0.72
0.69
0.67
0.69

Tsuite Size
Start End
5
5
5
5
5
5
5
6
13
13
13
13
13
13
13
15
13
15
13
17
5
5
5
5
5
5
5
5
5
5
8
8
8
8
8
8
8
10
8
8
6
6
6
6
6
6
6
6
6
6
6
6
4
4
4
4
4
4
4
6
9
9
9
9
9
9
9
10
9
10
9
9

110

Tsketch
0.00
0.00
0.00
0.22
0.00
0.18
0.13
1.67
6.06
704
0.00
0.00
0.01
1.20
0.04
0.00
0.42
0.24
1.55
6.27
0.00
0.00
0.00
0.00
0.00
0.44
0.00
0.00
0.00
1.12
0.00
0.00
0.23
0.20
0.17
0.28

solutions, which increases the likelihood of finding a solution early in the enumeration process. Meanwhile, the model variants with most but not all of theformula abstracted to a sketch have less overall solutions to be found. In thesecases, the solution required looking over a number of expression combinations,which facilitated the need for additional tests. However, while the problem tobe sketched has much narrower criteria to meet, the solution space is smalland sketches are completed quickly regardless.
Some of the equivalent formula pairs are similar in nature to each other,such as BinaryTree and Dijkstra. However, other formulas are markedly
different, such as our linked list example which uses universal quantificationand set-based compare operators for one formula, and disjunction, existential
quantification and unary operators for the other formula. Another modelthat reasons over two markedly different structures is StronglyConnect, whichworks with the following formula pairs:
1. no iden & adj and all n : Node | Node - n in n.adj
2. adj = {Node -> Node} - iden

The first formula first asserts that there is no intersection between theset “iden” and the relation “adj” (iden is a keyword for the set containing theidentity of all atoms in the model i.e. for an atom n its identity value is n->n).
Then, the first formula uses universal quantification to state that every node’s
adj relation should be a map to all nodes except itself, using set inclusion(in). On the other hand, the second equation simply uses set equality (=) tostate that the adj relation should be populated with the Node × Node cross111

product, minus any mapping which is also in iden.
Despite these structural differences in the formulas, across the board,
the AGenW B test suites served as a strong starting base across all the model
variants. Although not always adequate, the number of candidate solutions
eliminated by any newly generated test was minimal, numbering from 0.08%
to 0.68% of the total number of candidates eliminated across all the model
variants.
To see why tests were added during sketching, we can look at ourrunning example, the singly-linked list model. The AGenW B test suite wasadequate for all sketches until the largest model variant LinkedList 4H, where
one test was added. Figure 7.2 shows two invalid valuations that have thesame coverage. The valuation depicted in (a) is generated by AGenW B while
valuation(b) is the test added to the suite during ASketch Equiv ’s execution.
Recall our AcyclicSome equivalent formula is the following:

no List.header or some n : List.header.*link | no n.link
The valuations in Figure 7.2 are both related to the quantified formula criteria “|d| > 1 and b = false for all.” However, these two valuations capture two different ways in which all Node atoms in the list can violate
the body (no n.link): (1) a node in the list has a self loop and (2) a node in
the list points to an earlier node in the list. As a result, AGenW B will produce
one of these two valuations, but not both. While both tests are necessary to

112

link
L0

header

N0

link

N1

L0

header

N0

N1
link

link
(a)

(b)

Figure 7.2: Two invalid valuations with the same coverage.

sketch AcyclicOther correctly, the two tests have significant overlap in the candidates they eliminate. Specifically, the addition of the test in Figure 7.2(b)is used to eliminate just 0.68% of the candidate solutions encountered. Meanwhile, the test in 7.2(a) is the second test in the order, and together the
first two tests eliminate 65.18% of the candidate solutions while the first threeeliminate 85.18% of the candidate solutions. Therefore, while AGenW B cancurrently miss some of the intricate details on how different passing or failingbehaviors can occur, since any added test serves to eliminate minor portionsof the candidate solutions, our AGenW B test suites do not miss any importantfunctionality of the formula being sketched.

7.5

Summary
The ASketch Eval approach to sketching works directly with AUnit, by

requiring a collection of user provided test valuations. On the other hand, ASketch Equiv uses AGenW B to enable the sketching of Alloy models through equiv-

113

alence. Rather than having the end user develop a test suite, ASketch Equiv
makes use of an existing ad-hoc Alloy validation technique: the use of assertions to check for the logical relationship between two formulas. While theequivalent formula can take any form, AGenW B has proven to generate strong
test suites for sketching, typically capturing most, if not all, of the to-besketched problem. AGenW B has already proven effective at finding real world
bugs; however, based on the few additional tests generated during sketching,
AGenW B – and the coverage criteria which drives the technique – can be further strengthened. Overall, ASketch Equiv combines multiple AUnit avenues
together to provide another flavor of sketching Alloy models that is rooted in
one of the original debugging methods for Alloy users, while leveraging theeffectiveness of ASketch EvalSub .

114

Chapter 8
Future Work

We take a look at three general avenues for future work based on theinsights and contributions of this dissertaton.

8.1

Debugging Alloy Models
The motivation behind AUnit is to bring well established imperative

testing paradigms to the declarative world, starting with Alloy. Alloy has its
own tool support through the Alloy Analyzer, which allows for an automatedanalysis of the language. Specifically, AUnit introduces the concepts of test
case, test execution and test coverage for Alloy. Efforts have been made to takethe foundation of AUnit and provide: (1) the ability to automatically generatetests and (2) the ability to sketch Alloy models. However, the building blocks
of AUnit facilitate other imperative testing paradigms, two notable candidates
are fault localization and repair.
Fault Localization: When an AUnit test fails, one of two possibilities holds:(1) the user incorrectly specified a test or (2) the user’s model is incorrect.
In the first case, the Alloy Analyzer can visually display the test’s valuation,
enabling the user to quickly validate or correct the test. However, in the second

115case, the user needs to debug the Alloy model. If the model is over-constrained– rules out an instance meant to be valid – then the Alloy Analyzer does provide
an initial basis for fault localization through the Analyzer’s ability to highlightthe unsat core. The unsat core tool-set highlights the parts of the model
which together lead to an unsatisfiable solution for a particular command.
When a model is over-constrained, at least one test will falsely be unsatisfiable,
enabling the user to leverage the unsat core highlighting to narrow the focus fortheir debugging efforts. However, if the model is under-constrained – allows aninvalid instance to be generated – there is currently no support for localizing
the cause of the fault. The user simply knows there is a bug somewhere in
the formula(s) invoked by a failing test’s command. Additionally, there arelimitations to the unsat core functionality. Given a formula is the form “alld :D | a and b ” if the formula is false because “a” is false, the entire

quantified formula will be highlighted. Therefore, regardless of the type ofbug, fault localization techniques are needed.
There are two different avenues to explore for fault localization. The
first is to inspect the output of the unsat core functionality to see if it is possible to get a narrower slice of the Alloy model. Second, using the valuation’s
coverage information, we can paint a clearer picture for the end user over what
is happening when their valuation is essentially an “input” to the formulas of
the test. In particular, we can explore the AUnit coverage slices of passing
and failing tests, with the goal of narrowing in on the unique coverage characteristics of failing tests. Our coverage requirements look to have valuation116

explore different sizes of expressions and different truth values of formulas.
For instance, looking at the unique coverage provided by a failing test could
give insight into the misuse of transitive closure in place of reflexive transitive
closure.
Repair: Given that a user has confidence in their AUnit test suite, failingtest(s) can be used to repair a faulty model. The problem of repair centersaround automatically correcting a faulty portion of code based on an error
in behavior being detected. Taking inspiration from our ASketch framework,
we can view the repair problem as a tailored and narrowly focused sketchingproblem. First, we can use the unsat core and fault localization strategies toisolate what parts of the Alloy model should be abstracted away into a seriesof sketches. These sketches would start with one hole and build up an arrayof different hole combinations e.g. if we want to repair "some List.header"
we could generate 3 sketches (1) "\UO\ List.header", (2) "some \E\", and(3) "\UO\ \E\". Additionally, we can also build on top of our ASketch Gen problem, directly re-using the set of candidates for all terminal holes (Table 5.1).
For expression holes, \E\, we can generate a series of candidate expressions by
mutating the given expression in the model, starting with minor changes andbuilding up to larger mutations. Then, using these new ASketch Gen guidelines,
we can systematically solve each sketch, stopping when one candidate solution
passes all tests.

117

8.2

Advancements for ASketch Eval

8.2.1

Exploring the Evaluator
ASketch Eval is able to solve sketches quickly, as a whole, because of its

ASketch EvalSub optimization, in which test candidates are grouped together
by their evaluation value over the expressions and subformulas in the sketch.
When a test candidate fails a test case, we know that in combination, the valuesof the subformulas being sketched cause the test to fail. However, we do notknow which parts of the test candidate contributed the the failure. Consider
our BinaryTree formula: all n : Node | n in BinaryTree.root.*(left +right) => n \CO\ \E\ and \UO\ \E\ and \UO\ \E\. If this formula fails a test

because of the test candidate’s values for “ n \CO\ \E\”, then we would liketo be able to skip all test candidates with this combination. This optimization
could enable ASketch Eval to skip chunks of candidate solutions in mass, rather
than taking the effort to build a candidate’s representation in order to eliminate
it. However, we currently have no way of knowing what part of the test
candidate contributed to the failure. Future work can focus on exploring theinner workings of the Evaluator to isolate what specifically causes a false
result, which can also lend itself to the fault localization problem for AUnit.
8.2.2

Automated Test Ordering
Chapter 6 highlights the importance of the test order on the time tosolve the sketch. In Chapter 7, we use this information to order a test suite
based on the coverage of that test suite over a user provided equivalent formula.

118

However, this information is not available to use in our traditional sketching
format for ASketch Eval , in which we rely on a user provided test suite to outline expected behavior rather than an equivalent formula. However, we know
the importance of focusing is on high level differences between valuations in
the beginning of a test order. Our AUnit valuations have a textual representation that we commonly work with; however, all valuations additionallyhave a graphical representation. This representation is depicted in the Alloytoolsets as a graph. Therefore, we can explore the range of graph differencing
metrics and to see which metrics would be applicable to defining a process toautomatically order tests based on their valuations.
8.2.3

Iterative Sketching
Moving forward, as the ASketch framework develops, the framework

will need to adapt to an iterative viewpoint. Previously, we have mostly lookedat sketching as a one off problem where a user would provide a skeleton formulawith holes and a robust test suite, then the ASketch framework would executeand report a solution to the end user. However, in practice, sketching can be,
and often is, iterative in nature. Below, we will highlight two main ways inwhich ASketch can leverage re-use in an iterative environment.
Changing the Test Suite:

An end user may initially provide a test suitethat fails to fully outline the intended behavior of a model-to-be-sketched.
For instance, in Chapter 5, with dynamic pruning, the expression holes for
the BinaryTree model have 433 possible candidates expressions each – all of119which are non-equivalent and together depict a wide range of Alloy semantics
and formulations. It is easy to imagine that a user may initial under describe
the sketching problem, resulting in the user refining the test suite. However,rather than starting a new sketch from scratch since the test suite has changed,
we can isolate what previous work we can re-use. If a user adds a test andthe previously reported solution is no longer correct, we can resume sketchingfrom where we initially stopped. All previously eliminated candidate solutions
are not valid. However, we want to reuse the value mapping, which keeps
track of the previous evaluation of expressions and subformulas over the tests.
These evaluations are still valid and can be leveraged when looking for a new
solution among the remaining candidate solutions. This approach was used
in ASketch Equiv when a candidate solution passed all existing tests, but was
not logically equivalent to the user provided equivalent predicate. If a test isremoved, the reported solution is still valid, and there is no need to sketch
anything. However, if a test has changed, the reported solution is not guaranteed to be correct. Assuming the reported solution is now invalid, we cannot
simply resume sketching, as with the addition of a test. Instead, candidate solutions eliminated by the changed test might now be valid. Therefore; we firstre-check these solutions. Once again, we can re-use the value store; however,
we would first need to clear out the mapping for the changed test, as thoseevaluations may no longer hold.
Suggesting Refinements to the End User: Additionally, with Alloy, we
have the ability to guide the user through refinements to their sketching test

120

suite. In our earlier ASketch work in Chapter 5 and Chapter 7, our algorithms
were focused on solving for the first solution. However, the techniques caneasily be modified to look for the first x solutions or all solutions. With
multiple solutions, we can actually use Alloy to determine if the solutions
are equivalent w.r.t. each other. By definition, all reported solutions areequivalent w.r.t. the test suite used for sketching. However, the test suitemight not be adequate, allowing for unintended solutions to be generated.
Using Alloy, we can use a check command to group all potential solutions
into equivalence classes. If more than one equivalence class is found, we canguide the user through eliminating the incorrect solutions by presenting theuser with the counterexample that captures the difference between any two
equivalence classes. In turn, the end user can label the counterexample “valid”
or “invalid,” producing a new test. This test can then be used to narrow down
the remaining pool of solutions.

8.3

Bringing Testing to Other Declarative Language(s)Declarative languages have commonly been used for a range of activ-

ities from a base to automatically generate imperative code to model based
testing to validation of designs. In other words, traditional roles for declarative languages have often resembled providing validation for the design or
implementation of other programs, often written in imperative code. However,recently, declarative languages have been used as a programming solution to
problems which are defined more by a set of rules that lend themselves to121

declarative solutions easily, most notably through the introduction of software
defined networks (SDNs). As the role of declarative languages increases, theneed for better tools and support for these languages will increase. Declarative
languages can take a wide range of shapes themselves, meaning that masteryof one declarative language may not give a user a head start when learning another declarative language. However, through AUnit, we have shown that it ispossible to bring imperative testing paradigms to declarative languages. Furthermore, AUnit opened the door for a number of further testing advancements
in Alloy from automatically generating tests [71] to mutation testing [74] tomodel synthesis through sketching [75]. Below we outline a user study, which
can be used to derived the benefits of AUnit before moving forward to looking
at other languages, as well as a guideline to the problem of SDNs, in which
corporations are turning towards a split-problem approach mixing imperativeand declarative languages.
User Study:

The motivation behind the creation of AUnit is to ease theburden on the end-user by providing a well defined testing environment forAlloy. Furthermore, one envisioned use of the ASketch framework is to aid
beginning Alloy users as a teaching tool. Indeed, one functionality of ASketch
is the ability to present multiple solutions to a sketch to the user. As a result,a beginning Alloy user can be exposed to different ways in which the expressive
nature of Alloy can solve the sketch. Before applying the lessons learned frombuilding the AUnit infrastructure and ASketch framework to other declarative
languages, we recommend a user study of both toolsets, to ensure the foun-122

dation of both techniques are effective at easing the burden of developing in
Alloy. In particular, the study should focus on our notion that graphical valuations would be easy for beginning Alloy developers to reason over and create
as valuations are the heart of our AUnit and ASketch frameworks. Then,the basis of AUnit in Alloy can be applied forward towards other declarative
languages.
SDN Languages:

Software defined networks, SDNs, is a new paradigm

for programming in the networking field. SDNs were conceived as a “divideand conquer” mentality to the issues plaguing the networking community.
Specifically, the routing protocols have changed drastically since the original
implementation of the Internet. Initially, efforts were focused on an imperative implementation to handle packets. As the rules have changed, more andmore imperative code has been tacked onto the initial effort, making testing
difficult. With the need to re-write the packet routing code base, corporations
have turned towards the use of declarative languages to handle this portion ofa network, which is rule-based. Companies are willing to take on the expenseof switching from an imperative base because their existing imperative code is
too large and adhoc to properly test. However, as we have seen throughout thisdissertation, declarative languages can be complex and hard to reason over correctly. Therefore, as different groups have begun to develop declarative-based
solutions, there is a need to improve the development and test environment ofsuch languages. Otherwise, these companies will find themselves back in thesame position: unable to test their packet handling code.

123Chapter 9
Conclusion

Software models play a key role in reliable systems, but writing models
correctly is challenging. This dissertation addresses the problem of creatingcorrect models of software, specifically in the context of the Alloy tool-set.
We take a four-fold approach, building off of the foundations of AUnit. One,
we develop automated testing techniques for Alloy, which allow users to validate their Alloy models in the traditional spirit of testing. Two, we develop
a technique to synthesize parts of Alloy models based on program sketching
and tests, which allow users to write partial models that are completed byautomated tools. Three, we enhance the efficacy of our core sketching technique through multi-threading and exploration of test orders. Four, we leverage our automated testing techniques and our improved sketching technique
to introduce a second sketching approach that requires the user to specify anequivalent formula in place of specifying a suite of test valuations. We embody
our techniques in prototype tools and use them for experimental evaluation; as
subjects, we use a variety of Alloy models, including some from the standard
Alloy distribution and some written by graduate students.

124Appendices125

Appendix A
Alloy Analyzer with AUnit Toolset

In this appendix section, we will highlight our embodiment of AUnit,
currently deployed within the Alloy Analyzer toolset.
To start, our AUnit functionality is built on top of the Alloy Analyzer,
meaning all of the original Alloy Analyzer toolset is still available. Depicted
below is a screen shot from our toolset in which we have re-created our singlylinked list running example. The left hand side of the toolset is the editable
portion of the tool in which the user can specify an Alloy model. The righthand side of the tool contains various reporting tabs: “Log” displays the current Alloy Analyzer’s logging information, “AUnit Results” displays the test
execution details for the last run AUnit test suite, and “Coverage Results”
displays the model coverage details for the last run AUnit test suite. If wepress the “Execute” button, the normal Alloy Analyzer functionality will takeplace. In this case, the labeled command “Test0” will be executed, as it is thefirst command in the model.

126

Note in this model, we have two AUnit test cases (labeled Alloy command Test0 and Test1) showing the two different ways a valuation and command can be specified for the current toolset. For Test0, the valuation predicate (pred Valuation0) does not contain the command, while Test1’s valu-

127ation predicate (pred Valuation1) does contain the command. The second
format is the required format to generate an AUnit test for a predicate withparameter(s), as the valuation is defined solely within its given predicate.
Next, we can execute our AUnit test suite by clicking the “AUnit” button. This button will execute every AUnit test present in the model, specifically by executing all commands in the model whose label contains “Test.”
The right hand side will automatically switch to the “AUnit Results” tab.
If AUnit’s coverage calculation is turned on, the left hand side of the model
will be highlighted according to the coverage derived from all executed tests.
Green means the Alloy construct (signature, relation, expression or formula)
has been fully covered, yellow means the construct is partially covered (at least
one coverage criteria meet but not all) and red means the Alloy construct has
not been covered at all.
Depicted below is the behavior of executing our current AUnit test
suite:

128

Across the top, the overall summary of the test suite execution is displayed including: number of passing tests, number of failing tests, numberof errors (test that ran out of memory or time), and overall time to executethe whole test suite. Then, we display the execution details associated witheach test case. For a passing test, the execution time is displayed directly, but
the details (the AUnit command and valuation) are initially collapsed. Fora failing test, the AUnit test details start off expanded, allowing the user to129immediately see what the command and valuation is. The “View Valuation”
link graphically displays the valuation in a separate window using the Alloy
Analyzer’s visualization toolset, as seen below:

We can click over to the “Coverage Results” tab to view detailed coverage information. The coverage information is broken down by signatures,
relations, and then predicates and assertions. For any given predicate or assertion, the tool displays all expression and formula constructs. The results
130

start collapsed, but each Alloy construct can be expanded to display all of its
coverage criteria and whether or not that criteria has been covered. Below isa screen shot showing what the expanded coverage information looks like:131

Appendix B
Homework question

The following Alloy code was given as a partial Alloy model to becompleted with respect to the given instructions:module list
sig List {header: set Node}sig Node {link: set Node,elem: set Int}

fact CardinalityConstraints {// each list has at most one header node/* your code goes here */// each node has at most one link/* your code goes here */// each node has exactly one elem/* your code goes here */}pred Loop(This: List) {// <This> is a valid loop-list/* your code goes here */}pred Sorted(This: List) {// <This> has elements in sorted order (`<=')/* your code goes here */}pred RepOk(This: List) { // class invariant for List
Loop[This]
Sorted[This]}132

pred Count(This: List, x: Int, result: Int) {// count correctly returns the number of occurences of <x> in <This>// <result> reprsents the return value of count
RepOk[This] // assume This is a valid list/* your code goes here */}abstract sig Boolean {}one sig True, False extends Boolean {}pred Contains(This: List, x: Int, result: Boolean) {// contains returns true if and only if <x> is in <This>// <result> represents the return value of contains
RepOk[This] // assume This is a valid list/* your code goes here */}133

Appendix C
Mutation Testing for Alloy

This appendix summarizes the µAlloy approach, which we include forease of reference; further details can be found in Wang’s Masters thesis [74].
This section describes µAlloy’s mutation operators, process for generating mutants, and mutation score algorithm. µAlloy generates non-equivalent valid
Alloy models as mutants.
µAlloy operators We follow the spirit of mutation testing for imperative
languages to define the mutation operators for Alloy. Specifically, µAlloy uses
the production rules of the Alloy grammar [1] and defines operators to mutate
different constructs, e.g., signature declarations, formulas, and commands, ofthe Alloy language. Table C.1 defines the mutation operators used by µAlloy.
MOR mutates signature multiplicity (e.g. lone sig to one sig). QOR mutates
quantifiers all, some, no, etc.. UOR and BOR define operator replacement
for respectively unary and binary operators. For example, mutate a.∗b toa.^b, and mutate a=>b to a<=>b. IOBU inserts an operator before an unary
expression (e.g. mutate a.b to a.∼b). OD defines operator deletion (e.g.
mutate a.∗ ∼b to a.∗b). BOE exchanges operands for a binary operator. For
example, mutate a => b to b => a. IEOE is similar to BOE with the exception

134

that it mutates the operands of imply-else expression (e.g. mutate a => belse c to a => c else b). IID mutates integer increment and decrement.
Generating Mutants To generate mutants systematically, we iterate overall Alloy AST nodes. If a location that mutation operators can be applied
to is found, then we mutate the model to create a mutant. The mutant isthen checked to see if it is semantically equivalent to the original model (forthe given scope). If the mutant is found to be equivalent, then the mutant isdiscarded. We use Alloy itself to check for equivalence, as we can write a checkcommand to ask Alloy if the two models are in fact equivalent. [74] contains
further details on how to structure the check command depending on what partof the Alloy model is mutated. Not all equivalence checking can be performed
with Alloy 4.2 because the checking may require higher order solvers to solve.
In such cases, we use Alloy∗ to check the equivalence of the original modeland the mutant. Also, we set the scope of equivalence checking algorithm to
8 universally for all 7 Alloy models for higher confidence in the results.
Mutation testing algorithm Algorithm 8 gives steps to calculate the mutation score for the given AUnit test suite. First, the test suite is run against theTable C.1: Mutation Operators
Mutation
Operator

Description

MOR
QOR
UOR
BOR
IOBU
OD
BOE
IEOE
IID

Multiplicity Operator Replacement
Quantifier Operator Replacement
Unary Operator Replacement
Binary Operator Replacement
Insert Operator Before Unary Expression
Operator Deletion
Binary Operand Exchange
Imply-Else Operand Exchange
Integer Increment and Decrement

135

original model and the test execution outcome (either pass or fail) is recorded.
Next, the suite is run against each mutant, and as soon as a different test
execution outcome is detected, the mutant is marked as killed and the process continues to the next mutant. Finally, the mutation score for the suite iscomputed.

Algorithm 8: Mutation Score Algorithm
Input: Alloy model m, mutants mus and AUnit test suite ts
Output: Mutation score// Run the test suite against the original model and record thetest result. The test result shows which test case is allowed ordisallowed in the model.
mTestResult ← runTestSuite(m, ts)// Initialize the number of killed mutant to 0.
numMutantKilled ← 0// Run the test suite against each mutant and see if the test
result is different.
foreach mu ∈ mus do
muTestResult = runTestSuite(mu, ts)// If the result is different, then the mutant is killed. The test
result is considered different if a test case is allowed in theoriginal model but disallowed in the mutant, or vice versa.
if isDifferent(mTestResult, muTestResult) thennumMutantKilled ++// Compute the percentage of mutants got killed.
return numMutantKilled / mus.size()

136

Appendix D
Models for Evaluations
The following Alloy code shows the different Alloy models used in theevaluation section of Chapter 5 and Chapter 6.
module LinkedList
one sig List { header: lone Node }sig Node { link: lone Node }pred Acyclic() {--all n: Node | n in List.header.*link => n !in n.^link
sll_1: \Q\ n : Node | n in List.header.*link => n !in n.^link
sll_2: \Q\ n : Node | n \CO\ List.header.*link => n !in n.^link
sll_3: \Q\ n : Node | n \CO\ \E\ => n !in n.^link
sll_4: \Q\ n : Node | n \CO\ \E\ => n \CO\ n.^link
sll_5: \Q\ n : Node | n \CO\ \E\ => n \CO\ \E\}module BinaryTree
one sig BinaryTree { root: lone Node }sig Node { left, right: lone Node }pred IsTree() {--all n: Node { n in BinaryTree.root.*(left + right) => {-- n !in n.^(left + right) and no n.left & n.right and lone n.~(left + right) }}bt_1: all n: Node { n in BinaryTree.root.*(left + right) => {n \CO\ n.^(left + right) no n.left & n.right lone n.~(left + right) }bt_2: all n: Node { n in BinaryTree.root.*(left + right) => {n \CO\ \E\ no n.left & n.right lone n.~(left + right) }bt_3: all n: Node { n in BinaryTree.root.*(left + right) => {n \CO\ \E\ \UO\ n.left & n.right lone n.~(left + right) }bt_4: all n: Node { n in BinaryTree.root.*(left + right) => {n \CO\ \E\ \UO\ \E\ lone n.~(left + right) }bt_5: all n: Node { n in BinaryTree.root.*(left + right) => {n \CO\ \E\ \UO\ \E\ \UO\ n.~(left + right) }bt_6: all n: Node { n in BinaryTree.root.*(left + right) => {n \CO\ \E\ \UO\ \E\ \UO\ \E\ }}137module Contains
one sig List { header: lone Node }sig Node {
elem: lone Object,
link: lone Node}sig Object {}pred Contains(l: List, e: Object) {--e in l.header.*link.elem
contains_1: \E\ in l.header.*link.elem
contains_2: \E\ \CO\ l.header.*link.elem
contains_3: \E\ \CO\ \E\}module Remove
one sig List { header, header’: lone Node }sig Node {

elem, elem’: one Object,
link, link’: lone Node}sig Object {}pred Remove(l: List, e: Object) {--l.header.*link.elem - e = l.header'.*link'.elem'
remove_1: \E\ - e = l.header’.*link’.elem’remove_2: \E\ \LO\ e = l.header’.*link’.elem’remove_3: \E\ \LO\ \E\ = l.header’.*link’.elem’remove_4: \E\ \LO\ \E\ = \E\}module Dijkstra
open util/ordering [State] as so
sig Process {}sig Mutex {}sig State {holds, waits: Process -> Mutex}

pred Deadlock() {--some Process--some s: State | all p: Process | some p.(s.waits)
djk_1: \UO\ Processsome s: State | all p: Process | some p.(s.waits)
djk_2: \UO\ \E\some s: State | all p: Process | some p.(s.waits)
djk_3: \UO\ \E\

138

\Q\ s: State | all p: Process | some p.(s.waits)
djk_4: \UO\ \E\\Q\ s: State | \Q\ p: Process | some p.(s.waits)
djk_5: \UO\ \E\\Q\ s: State | \Q\ p: Process | \UO\ p.(s.waits)
djk_6: \UO\ \E\\Q\ s: State | \Q\ p: Process | \UO\ \E\}139

Bibliography[1] Alloy Reference. http://alloy.mit.edu/alloy/documentation/book-chapters/alloylanguage-reference.pdf.
[2] Alloy home page. http://alloy.mit.edu.
[3] Unified modeling language webpage. http://www.uml.org/.
[4] Basel Y Al-Naffouri. MintEra: A testing environment for Java programs.
Masters report. Massachusetts Institute of Technology, 2004.
[5] Rajeev Alur, Rastislav Bodı́k, Garvit Juniwal, Milo M. K. Martin, Mukund
Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama,
Emina Torlak, and Abhishek Udupa. Syntax-guided synthesis. In Formal Methods in Computer-Aided Design (FMCAD), pages 1–8, 2013.
[6] Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa. Scaling enumerative program synthesis via divide and conquer, 2016.
[7] Rastislav Bodı́k and Barbara Jobstmann. Algorithmic program synthesis:
Introduction. STTT, 15(5-6):397–411, 2013.
[8] Chandrasekhar Boyapati, Sarfraz Khurshid, and Darko Marinov. Korat:
Automated testing based on Java predicates. In International Symposium
on Software Testing and Analysis, pages 123–133, 2002.
140

[9] Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted
and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, pages 209–224, 2008.
[10] Koen Claessen and John Hughes.

Quickcheck: A lightweight tool for

random testing of Haskell programs.

In Proc. Fifth ACM SIGPLAN

International Conference on Functional Programming, 2000.
[11] L. A. Clarke. A system to generate test data and symbolically executeprograms. IEEE Transactions on Software Engineering, pages 215–222,
September 1976.
[12] François Degrave, Tom Schrijvers, and Wim Vanhoof. Logic-based program synthesis and transformation.

chapter Automatic Generation of

Test Inputs for Mercury, pages 71–86. Springer-Verlag, 2009.
[13] Yves Deville and Kung-Kiu Lau. Logic program synthesis. The Journalof Logic Programming, 19:321–350, 1994.
[14] T. T. Dinh-trong, S. Ghosh, and R. B. France. A systematic approachto generate inputs to test uml design models. In 2006 17th International
Symposium on Software Reliability Engineering, pages 95–104, Nov 2006.
[15] Trung Dinh-Trong, N. Kawane, S. Ghosh, R. France, and A. A. Andrews.
A tool-supported approach to testing uml design models. In 10th IEEE141

International Conference on Engineering of Complex Computer Systems(ICECCS’05), pages 519–528, June 2005.
[16] Michael D. Ernst. Dynamically Discovering Likely Program Invariants.
PhD thesis, University of Washington Department of Computer Scienceand Engineering, Seattle, Washington, August 2000.
[17] Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W.
Reps.

Component-based synthesis for complex APIs.

In Proceedingsof the 44th ACM SIGPLAN Symposium on Principles of Programming
Languages, pages 599–612, 2017.
[18] John K. Feser, Swarat Chaudhuri, and Isil Dillig.

Synthesizing data

structure transformations from input-output examples. In Proceedings ofthe 36th ACM SIGPLAN Conference on Programming Language Design
and Implementation, PLDI ’15, 2015.
[19] Joel Galenson, Philip Reames, Rastislav Bodik, Björn Hartmann, andKoushik Sen. Codehint: Dynamic and interactive synthesis of code snippets. In Proceedings of the 36th International Conference on Software
Engineering, ICSE 2014, New York, NY, USA, 2014. ACM.
[20] Juan Pablo Galeotti, Nicolas Rosner, Carlos G. Lopez Pombo, and Marcelo F.
Frias.

Taco: Efficient sat-based bounded verification using symmetry

breaking and tight bounds. IEEE Transactions on Software Engineering,39(9):1283–1307, September 2013.

142

[21] Khalid Ghori. Constraint-based program repair. Master’s thesis, Department of Electrical and Computer Engineering, University of Texas atAustin, August 2006.
[22] Milos Gligoric, Tihomir Gvero, Vilas Jagannath, Sarfraz Khurshid, Viktor
Kuncak, and Darko Marinov. Test generation through programming in
UDITA. In Proceedings of the 32nd ACM/IEEE International Conference
on Software Engineering-Volume 1, pages 225–234, Cape Town, South
Africa, 2010.
[23] Patrice Godefroid, Nils Klarlund, and Koushik Sen.

DART: Directed

automated random testing. In Proceedings of the 2005 ACM SIGPLAN
Conference on Programming Language Design and Implementation, PLDI
’05, pages 213–223, 2005.
[24] J. Goodenough and S. Gerhart. Toward a theory of test data selection.
IEEE Transactions on Software Engineering, pages 156–173, June 1975.
[25] Arnaud Gotlieb, Bernard Botella, and Michel Rueher. Automatic test
data generation using constraint solving techniques.

In Proc. Inter-national Symposium on Software Testing and Analysis (ISSTA), pages
53–62, Clearwater Beach, FL, 1998.
[26] Tihomir Gvero, Viktor Kuncak, and Ruzica Piskac. Interactive synthesisof code snippets. In Proceedings of the 23rd International Conference on
Computer Aided Verification, pages 418–423, 2011.

143

[27] Hans-Martin Horcher. Improving software tests using Z specifications.
In Proc. 9th International Conference of Z Users, The Z Formal Specification Notation, pages 152–166, 1995.
[28] Jinru Hua and Sarfraz Khurshid. Sketch4J: Execution-driven sketchingfor Java. Under submission, 2017.
[29] J. C. Huang. An approach to program testing. ACM Computing Surveys,
7(3):113–128, 1975.
[30] Daniel Jackson. Alloy: A lightweight object modelling notation. ACM
Trans. Softw. Eng. Methodol., 11(2):256–290, April 2002.
[31] Daniel Jackson, Ian Schechter, and Ilya Shlyakhter. ALCOA: The Alloy constraint analyzer. In Proc. International Conference on Software
Engineering (ICSE), Limerick, Ireland, June 2000.
[32] Jinseong Jeon, Xiaokang Qiu, Jeffrey S. Foster, and Armando SolarLezama.

JSketch: Sketching for Java.

In Proc. 10th Joint Meetingon Foundations of Software Engineering, ESEC/FSE 2015, New York,NY, USA, 2015. ACM.
[33] Susmit Jha, Sumit Gulwani, Sanjit A. Seshia, and Ashish Tiwari. Oracleguided component-based program synthesis. In Proc. 32nd ACM/IEEEInternational Conference on Software Engineering - Volume 1, ICSE ’10,
New York, NY, USA, 2010. ACM.

144

[34] James A. Jones, Mary Jean Harrold, and John Stasko. Visualization oftest information to assist fault localization. In Proceedings of the 24th
International Conference on Software Engineering (ICSE), pages 467–
477, May 2002.
[35] Sarfraz Khurshid, Muhammad Zubair Malik, and Engin Uzuncaova. An
automated approach for writing Alloy specifications using instances. In
Second International Symposium on Leveraging Applications of Formal
Methods (ISoLA), pages 449–457, 2006.
[36] Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, and Daniel Jackson.
A case for efficient solution enumeration.

In Theory and Applicationsof Satisfiability Testing, 6th International Conference, SAT 2003. Santa
Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, pages
272–286, 2003.
[37] Sarfraz Khurshid, Darko Marinov, Ilya Shlyakhter, and Daniel Jackson.
A case for efficient solution enumeration. In SAT, May 2003.
[38] Etienne Kneuss, Ivan Kuraj, Viktor Kuncak, and Philippe Suter. Synthesis modulo recursive functions. In Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages &#38; Applications, OOPSLA ’13, New York, NY, USA,2013.
[39] Bogdan Korel. Automated test data generation for programs with procedures.

In Proc. International Symposium on Software Testing and145

Analysis (ISSTA), pages 209–215, San Diego, CA, 1996.
[40] Shriram Krishnamurthi, Kathi Fisler, Daniel J. Dougherty, and Daniel
Yoo. Alchemy: Transmuting base Alloy specifications into implementations. In 16th ACM SIGSOFT International Symposium on Foundationsof Software Engineering, pages 158–169, 2008.
[41] Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. Complete functional synthesis. SIGPLAN Not., 45(6):316–329, June 2010.
[42] N. Lazaar, A. Gotlieb, and Y. Lebbah. Fault localization in constraint
programs. In 2010 22nd IEEE International Conference on Tools with
Artificial Intelligence, volume 1, pages 61–67, Oct 2010.
[43] Nadjib Lazaar, Arnaud Gotlieb, and Yahia Lebbah. Principles and Practice of Constraint Programming – CP 2010: 16th International Conference, CP 2010, St. Andrews, Scotland, September 6-10, 2010. Proceedings, chapter On Testing Constraint Programs. 2010.
[44] Fan Long and Martin Rinard.

Staged program repair with condition

synthesis. In ESEC/FSE 2015, 2015.
[45] Nuno Macedo, Alcino Cunha, and Tiago Guimarães. Exploring scenario
exploration. In Proceedings of the 18th International Conference on Fundamental Approaches to Software Engineering, pages 301–315, 2015.

146

[46] Muhammad Zubair Malik, Khalid Ghori, Bassem Elkarablieh, and Sarfraz
Khurshid. A case for automated debugging using data structure repair.
In ASE, 2009.
[47] David Mandelin, Lin Xu, Rastislav Bodı́k, and Doug Kimelman. Jungloid
mining: Helping to navigate the API jungle. SIGPLAN Not., 40(6):48–
61, June 2005.
[48] Darko Marinov and Sarfraz Khurshid. TestEra: A novel framework forautomated testing of Java programs. In Proc. Conference on AutomatedSoftware Engineering (ASE), pages 22–31, San Diego, CA, November
2001.
[49] MIT. Alloy grammar.
[50] Vajih Montaghami and Derek Rayside. Extending alloy with partial instances.

In Abstract State Machines, Alloy, B, VDM, and Z - Third

International Conference, ABZ 2012, Pisa, Italy, June 18-21, 2012. Proceedings, pages 122–135, 2012.
[51] Vajih Montaghami and Derek Rayside. Staged evaluation of partial instances in a relational model finder. In Abstract State Machines, Alloy, B,
TLA, VDM, and Z - 4th International Conference, ABZ 2014, Toulouse,
France, June 2-6, 2014. Proceedings, pages 318–323, 2014.
[52] Tim Nelson, Salman Saghafi, Daniel J Dougherty, Kathi Fisler, and Shriram Krishnamurthi. Aluminum: principled scenario exploration through147

minimality. In International Conference on Software Engineering, pages
232–241, 2013.
[53] Jeff Offutt and Aynur Abdurazik. Generating tests from UML specifications. In Proc. Second International Conference on the Unified Modeling
Language, pages 416–429, October 1999.
[54] Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed
program synthesis. SIGPLAN Not., 50(6):619–630, June 2015.
[55] Daniel Perelman, Sumit Gulwani, Dan Grossman, and Peter Provost.
Test-driven synthesis. SIGPLAN Not., 49(6), June 2014.
[56] Orest Pilskalns, Anneliese Andrews, Andrew Knight, Sudipto Ghosh, andRobert France.

Testing {UML} designs.

Information and Software

Technology, 49(8):892 – 912, 2007.
[57] C. V. Ramamoorthy, Siu-Bun F. Ho, and W. T. Chen.

On the auto-mated generation of program test data. IEEE Transactions on Software
Engineering, 2(4):293–300, 1976.
[58] Jason Schimpf. Eclipse prolog unit test library. http://eclipseclp.
org/doc/bips/lib/test_util/index.html.
[59] Koushik Sen, Darko Marinov, and Gul Agha. CUTE: A concolic unit
testing engine for c. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT Interna-148

tional Symposium on Foundations of Software Engineering, ESEC/FSE13, 2005.
[60] Ilya Shlyakhter. Generating effective symmetry-breaking predicates forsearch problems.

In Proc. Workshop on Theory and Applications ofSatisfiability Testing, June 2001.
[61] Ilya Shlyakhter. Declarative Symbolic Pure Logic Model Checking. PhD
thesis, MIT, February 2005.
[62] Rishabh Singh and Sumit Gulwani. Predicting a Correct Program in Programming by Example, pages 398–414. Springer International Publishing,
Cham, 2015.
[63] Rishabh Singh and Armando Solar-Lezama. Synthesizing data structure
manipulations from storyboards. In Proc. 19th ACM SIGSOFT Symposium and the 13th European Conference on Foundations of Software
Engineering, ESEC/FSE ’11, New York, NY, USA, 2011.
[64] M. Soeken, R. Wille, M. Kuhlmann, M. Gogolla, and R. Drechsler. Verifying uml/ocl models using boolean satisfiability. In 2010 Design, Automation Test in Europe Conference Exhibition (DATE 2010), pages 1341–
1344, March 2010.
[65] Armando Solar-Lezama. Program Synthesis by Sketching. PhD thesis,
University of California, Berkeley, 2008.

149

[66] Armando Solar-Lezama, Gilad Arnold, Liviu Tancau, Rastislav Bodik,
Vijay Saraswat, and Sanjit Seshia. Sketching stencils. SIGPLAN Not.,
42(6):167–178, June 2007.
[67] Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik.
Sketching concurrent data structures.

In Proc. 29th ACM SIGPLAN

Conference on Programming Language Design and Implementation, PLDI
’08, New York, NY, USA, 2008. ACM.
[68] Armando Solar-Lezama, Liviu Tancau, Rastislav Bodik, Sanjit Seshia,
and Vijay Saraswat.

Combinatorial sketching for finite programs.

In

12th International Conference on Architectural Support for Programming
Languages and Operating Systems, 2006.
[69] J. M. Spivey. The Z Notation: A Reference Manual. Prentice-Hall, Inc.,
Upper Saddle River, NJ, USA, 1989.
[70] Allison Sullivan. AUnit – a testing framework for Alloy. Master’s thesis,
University of Texas at Austin, May 2014.
[71] Allison Sullivan, Kaiyuan Wang, Razieh Nokhbeh Zaeem, and Sarfraz
Khurshid. Automated test generation and mutation testing for Alloy. In
ICST, 2017.
[72] Allison Sullivan, Razieh Nokhbeh Zaeem, Sarfraz Khurshid, and Darko
Marinov. Towards a test automation framework for alloy. In Proceed-150

ings of the 2014 International SPIN Symposium on Model Checking ofSoftware, SPIN 2014, pages 113–116, 2014.
[73] Emina Torlak and Daniel Jackson. Kodkod: A relational model finder.
In Conference on Tools and Algorithms for Construction and Analysis of
Systems, pages 632–647, 2007.
[74] Kaiyuan Wang.

muAlloy – an automated mutation system for Alloy.

Master’s thesis, University of Texas at Austin, May 2015.
[75] Kaiyuan Wang, Allison Sullivan, Darko Marinov, and Sarfraz Khurshid.
Sketching Alloy models. Submitted for peer-review.
[76] Westley Weimer, ThanhVu Nguyen, Claire Le Goues, and Stephanie Forrest.

Automatically finding patches using genetic programming.

In

ICSE, pages 364–374, 2009.
[77] Jason Wielemaker. Swi prolog reference manual. http://www.swi-prolog.
org/pldoc/doc_for?object=manual.
[78] Jason Wielemaker.

Swi prolog unit test framework.

swi-prolog.org/pldoc/package/plunit.html.

151

http://www.