一句话：为 Alloy 扩展语法与后端以支持模型计数，让用户能统计给定公式的解的个数。
Alloy 是成熟的规约与分析工具，提供带传递闭包的一阶关系逻辑用于书写规约，并以基于 SAT 求解器的全自动后端进行分析，已应用于验证、安全与合成等领域。但 SAT 求解器通常只给出公式的一个解，当用户需要知道同一公式有多少个解时便无法胜任。本文为 Alloy 新增模型计数后端：扩展其语法加入模型计数命令，并扩展图形界面以配置该命令；所实现的 AlloyMC 支持两种先进模型计数器——近似计数器 ApproxMC 与精确计数器 ProjMC。AlloyMC 可运行于 Linux、Mac 与 Windows，用户只需下载并运行集成的 JAR，无需安装模型计数器及其依赖库；源码、JAR 与数据集均已公开。
Specifying and analyzing desired properties of software systems can play an important role in the development of more dependable systems. Alloy is a mature tool-set that provides a first-order, rela- tional logic with transitive closure for writing the specifications, and a fully automatic backend based on propositional satisfiability (SAT) solvers for analyzing them. Alloy’s intuitive notation and sup- port for modern solvers make it a particularly effective specification and analysis tool, which has been applied in several domains, including verification, security, and synthesis. This paper introduces a new backend for Alloy, which complements SAT solvers, and provides a new method to assist Alloy users to more effectively use the tool-set, specifically in scenarios where multiple solutions to the same formula are desired. We add to the Alloy backend support for model counting, i.e., computing the number of solutions to the given formula. We extend the Alloy grammar to add a new com- mand for model counting, and extend the Alloy GUI to customize it. Our implementation, called AlloyMC, supports two state-of-the-art model counters: the approximate model counter ApproxMC and the exact model counter ProjMC. AlloyMC runs on Linux, Mac, and Windows. To use AlloyMC, users just download and run its integrated JAR file with no need to install dependencies (e.g., model counters and their dependent libraries). The AlloyMC source code, the JAR file, and the data set are available publicly.
DOI 原文 ·
@inproceedings{paperbot5703,
title = {AlloyMC: Alloy meets model counting},
author = {Jiayi Yang and Wenxi Wang and Darko Marinov and Sarfraz Khurshid},
booktitle = {FSE},
year = {2020},
doi = {10.1145/3368089.3417938}
}