REACH: Refining Alloy Scenarios by Scope

TL;DR

Reach enhances Alloy's Analyzer by enabling size-based scenario exploration, improving performance and scenario ordering, especially when incrementally adjusting scope, thus aiding systematic verification.

Contribution

Reach extends Alloy's Analyzer to allow size-based scenario exploration, improving performance and maintaining scenario order, with benefits for incremental scope adjustments.

Findings

Performance improves with Reach's enumeration.

Scenario ordering is semi-sorted, aiding user exploration.

Incremental scope changes are more efficient with Reach.

Abstract

Writing declarative models has numerous benefits, ranging from automated reasoning and correction of design-level properties be-fore systems are built, to automated testing and debugging of their implementations after they are built. Alloy is a declarative modeling language that is well suited for verifying system designs. A key strength of Alloy is its scenario-finding toolset, the Analyzer, which allows users to explore all valid scenarios that adhere to the model's constraints up to a user-provided scope. In Alloy, it is common for users to desire to first validate smaller scenarios, then once confident, move onto validating larger scenarios. However, the Analyzer only presents scenarios in the order they are discovered by the SAT solver. This paper presents Reach, an extension to the Analyzer which allows users to explore scenarios by size. Experimental results reveal Reach's enumeration improves performance while having the added benefit of maintaining a semi-sorted ordering of scenarios for the user. Moreover, we highlight Reach's ability to improve the performance of Alloy's analysis when the user makes incremental changes to the scope of the enumeration.