Alloy is a declarative modeling language that is well suited for verifying system designs. Alloy models are automatically analyzed using the Analyzer, a toolset that helps the user understand their system by displaying the consequences of their properties, helping identify any missing or incorrect properties, and exploring the impact of modifications to those properties. To achieve this, the Analyzer invokes off-the-shelf SAT solvers to search for scenarios, which are assignments to the sets and relations of the model such that all executed formulas hold. To help write more accurate software models, Alloy has a unit testing framework, AUnit, which allows users to outline specific scenarios and check if those scenarios are correctly generated or prevented by their model. Unfortunately, AUnit currently only supports textual specifications of scenarios. This paper introduces Crucible, which allows users to graphically create AUnit test cases. In addition, Crucible provides automated guidance to users to ensure they are creating well structured, valuable test cases. As a result, Crucible eases the burden of adopting AUnit and brings AUnit test case creation more in line with how Alloy scenarios are commonly interacted with, which is graphically.

翻译：中文摘要：Alloy是一种适用于验证系统设计的声明式建模语言。借助分析工具集，Alloy模型可自动执行分析，通过展示其属性的衍生结果来帮助用户理解系统，识别缺失或错误的属性，并探索属性修改带来的影响。分析工具通过调用现成的SAT求解器搜索场景（即模型中集合与关系的赋值，使得所有已执行公式成立）来实现这一目标。为帮助编写更精确的软件模型，Alloy配备了单元测试框架AUnit，允许用户描述特定场景并检测这些场景是否被模型正确生成或抑制。遗憾的是，AUnit当前仅支持场景的文本规格说明。本文推出Crucible，它允许用户通过图形方式创建AUnit测试用例。此外，Crucible还提供自动化引导，确保用户创建结构合理、有价值的测试用例。由此，Crucible减轻了采用AUnit的负担，使AUnit测试用例的创建更符合用户与Alloy场景的常见交互方式，即图形化交互。