Alloy 介绍
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 文件。