Alloy 是用于描述结构(structure)的语言,也是探索结构的工具。从发现安全机制的漏洞到设计电话交换网络,它已被广泛用于各种应用中。
Alloy 4 是一个自包含的可执行文件,其中包括 Kodkod 模型查找器和各种 SAT 解算器,以及标准的 Alloy 库和一系列教程示例。可以将相同的 jar 文件合并到其他应用程序中,以将 Alloy 用作 API,并包含源代码。
要求:
Alloy 在使用最新 JVM(Java 6 或更高版本)的所有操作系统上运行。它可以与跨平台 SAT 求解器(Sat4j 和更有效的本机 SAT 求解器(minisat,lingeling/plingeling,glucose)一起作为可运行的 jar 文件使用。
但是请注意,从 macOS High Sierra 开始,必须安装专用的 JVM 才能在 macOS 上运行 Alloy。为此提供了一个 .pkg 文件。