使用 Homebrew, apk, zypper, winget 安装 alloy-analyzer

项目链接

• 主页
• 仓库
• 上游文档
• 软件包管理器页面

命令和别名

• alloy

项目历史

The official about page says Alloy was created in the Software Design Group at MIT. It describes Alloy as a language for evolving structures and the Analyzer as a solver-backed tool that explores models, checks properties, and displays structures graphically.

Alloy's design draws from the Z specification language, Tarski's relational calculus, Linear Temporal Logic with Past, and object-modeling notations such as OMT and UML. That background explains why the Analyzer sits between academic formal methods and practical software modeling.

The current AlloyTools GitHub repository begins in public git history on 2017-07-19. Its README describes Alloy 6 as a self-contained executable with Pardinus/Kodkod, SAT solvers, the standard Alloy library, tutorial examples, and Java 17 as the current runtime requirement.

采用历史

The official about page points to uses ranging from finding holes in security mechanisms to designing telephone switching networks. The documentation and download pages present Alloy as a runnable jar and macOS DMG, while Homebrew packages it as alloy-analyzer with an alloy executable.

Alloy 6 broadened the analyzer's modeling surface by adding native behavioral and temporal modeling, moving users away from manually encoding traces in older Alloy models.

使用方式

Users write Alloy models, run commands or assertions, and inspect generated instances or counterexamples in the Analyzer. The official docs describe executing the jar directly with java -jar, and the repository notes the same jar can also be embedded as an API.

Since Alloy 6, temporal model checking can use external tools such as NuSMV or nuXmv when available on PATH, alongside the bundled SAT-based analysis stack.

为什么软件包爱好者会关心

Alloy Analyzer is important in package catalogs because it packages a complete formal-methods workbench as a command-line-launchable Java artifact. It brings SAT-backed modeling, examples, and visualization into a normal developer install flow instead of a bespoke academic setup.

Its dependency story is also interesting: the distribution is self-contained for common use, but its internals include Kodkod/Pardinus and multiple SAT solver paths, and Alloy 6's temporal mode can reach out to model checkers like NuSMV or nuXmv.

时间线

• MIT era: Alloy created in the Software Design Group at MIT.
• 2017: Current AlloyTools GitHub repository public history begins.
• 2019: v5.1.0 tag appears in repository history.
• 2021: v6.0.0 tag appears in repository history.
• 2024: v6.2.0 tag appears in repository history.

Related projects

• Kodkod and Pardinus: model-finding engines included in the Alloy distribution.
• SAT4J, MiniSat, Lingeling/Plingeling, and Glucose: SAT solver families referenced by the README.
• NuSMV and nuXmv: external model checkers used for Alloy 6 temporal model checking.

来源

• Git history from https://github.com/AlloyTools/org.alloytools.alloy.git
• Official Alloy 6 page: https://alloytools.org/alloy6.html
• Official README: https://github.com/AlloyTools/org.alloytools.alloy
• Official about page: https://alloytools.org/about.html
• Official documentation: https://alloytools.org/documentation.html
• Official download page: https://alloytools.org/download.html