User-driven diverse scenario exploration in model finders

Abstract

Model finders can build instances of declarative specifications that satisfy a set of correctness constraints. Some model finders ensure some degree of diversity among the instances they compute. Nevertheless, each model finder uses its own definition of diversity, that may or may not match designer intent. In this paper, we propose a procedure that enables designers to capture the desired notion of diversity they are looking for. Using a simple domain-specific language, they can specify what elements in the specification are relevant when comparing the differences between two instances. This information can then be used to make any model finder diversity-aware while using it as a black box. As a proof of concept, this approach has been implemented on top of the Alloy Analyzer.