有限模型发现的实时编程
摘要：活动模型发现器允许用户在数学逻辑中指定系统的属性，然后自动找到满足这些属性的具体示例，称为解决方案。这些解决方案通常被视为模型发现器的一个关键优势，因为它们为开发人员提供了一个探索性的环境。实际上，用户发现这些解决方案的实际效益比预期要少。多年来，研究人员一直认为问题在于产生了太多的解决方案。然而，最近的用户研究发现，用户实际上更喜欢列举一组广泛的解决方案。受Alloy的近期用户研究启发，我们认为问题在于解决方案与生成它们的逻辑约束之间的关联程度不够，无法帮助用户建立对约束本身的理解。在本文中，我们提出了一个关于Alloy模型的实时编程的概念验证，其中模型的编写和解决方案的探索是相互交织的。我们强调这个开发环境如何在开发人员、模型和解决方案之间实现更加高效的反馈循环。
作者：Allison Sullivan
论文ID：2305.17317
分类：Formal Languages and Automata Theory
分类简称：cs.FL
提交时间：2023-05-30