MCPcopy Index your code
hub / github.com/AlloyTools/org.alloytools.alloy

github.com/AlloyTools/org.alloytools.alloy @v6.3.0-begin

Chat with this repo
repository ↗ · DeepWiki ↗ · release v6.3.0-begin ↗ · + Follow
8,438 symbols 38,194 edges 563 files 5,056 documented · 60%
What it actually does AI analysis from the code graph — generated when you open this
loading…
README

Logo Release build Snapshot build

Alloy

Alloy 6 is a self-contained executable, which includes an extended version of the Kodkod model finder and a variety of SAT solvers, as well as the standard Alloy library and a collection of tutorial examples. The same jar file can be incorporated into other applications to use Alloy as an API, and includes the source code. See the release notes for details of new features.

Alloy 6 is a major new release More documentation can be found at: http://alloytools.org/documentation.html.

Requirements

Alloy runs on all operating systems with a recent JVM (Java 6 or later). It is made available as a runnable jar file with both a cross-platform SAT solver (Sat4j and more efficient native SAT solvers (minisat, lingeling/plingeling, glucose).

Note however that starting with macOS High Sierra, it is necessary to install a dedicated JVM to run Alloy on macOS. A .pkg file is provided for that purpose.

TL;DR

Checkout the project and type ./gradlew build. You find the executable JAR in org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar after the build has finished.

 $ java -version           # requires 1.8 (and NOT 1.9, gradle does not run on 1.9)
 java version "1.8.0_144"
 Java(TM) SE Runtime Environment (build 1.8.0_144-b01)
 Java HotSpot(TM) 64-Bit Server VM (build 25.144-b01, mixed model
 $ git clone --recursive https://github.com/AlloyTools/org.alloytools.alloy.git
 $ cd org.alloytools.alloy
 $ ./gradlew build
 $ java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar
 # opens GUI

Note: if you are behind a proxy, the call to gradlew is likely to fail, unless you pass it further options about the http and https proxies (and possibly your login and password on this proxy). There are several ways to pass these options, a simple one is to type (replace the XXXXX's by the adequate settings):

 $ ./gradlew -Dhttps.proxyHost=XXXXX -Dhttp.proxyHost=XXXXX -Dhttp.proxyPort=XXXXX \
      -Dhttps.proxyPort=XXXXX -Dhttp.proxyUser=XXXXX -Dhttp.proxyPassword=XXXXX \
      -Dhttps.proxyUser=XXXXX -Dhttps.proxyPassword=XXXXX \
      build

Building Alloy

The Alloy build is using a bnd workspace setup using a maven layout. This means it can be build with Gradle and the Eclipse IDE for interactive development. Projects are setup to continuously deliver the executable.

Projects

The workspace is divided into a number of projects:

Relevant Project files

This workspace uses bnd. This means that the following have special meaning:

  • cnf/build.xml – Settings shared between projects
  • ./bnd.bnd – Settings for a project. This file will drag in code in a JAR.
  • cnf/central.xml – Dependencies from maven central

Eclipse

The workspace is setup for interactive development in Eclipse with the Bndtools plugin. Download Eclipse and install it. You can then Import existing projects from the Git workspace. You should be asked to install Bndtools from the market place. You can also install Bndtools directly from the Eclipse Market place (see Help/Marketplace and search for Bndtools).

Bndtools will continuously create the final executable. The projects are setup to automatically update when a downstream project changes.

IntelliJ IDEA (Ultimate Edition only)

Ensure you have the Osmorc plugin is enabled, as this plugin is needed for Bndtools support. It should be enabled by default.

  1. Choose Import project from existing Sources by using Ctrl + Shift + a.
  2. Select the root folder (default folder name is org.alloytools.alloy).
  3. Choose "Import project from external model: Bnd/Bndtools" and click "Next"
  4. For "Select Bnd/Bndtools project to import", all projects should be checked by default, click "Next"
  5. For project SDK, Choose "1.8", Click Finish
  6. Select folder org/alloytools/kodkod/nativesat/jni as Resource Folder by selecting module org.alloytools.kodkod.nativesat, selecting folder jni -> right click -> Mark Directory As -> Resource Root.

Note: do not link the Gradle project, as this will prevent you from running Alloy within IDEA.

To run the Alloy GUI within IDEA, navigate to org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI and run the SimpleGUI class.

Gradle

In the root of this workspace type ./gradlew. This is a script that will download the correct version of gradle and run the build scripts. For settings look at [gradle.properties] and [settings.gradle].

Continuous Integration

The workspace is setup to build after every commit using Travis.

It releases snapshots to https://oss.sonatype.org/content/repositories/snapshots/org/alloytools/ for every CI build on Travis.

Building the DMG file for OSX systems

Currently only the executable jar in org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar is build. In the org.alloytools.alloy.dist project, run ../gradlew macos. This will leave the PKG file in target/bundle.

CONTRIBUTIONS

Please read the CONTRIBUTING to understand how you can contribute.

Extension points exported contracts — how you extend this code

UnboundedSolver (Interface)
An interface for unbounded relational constraint solvers. Pardinus bounds PardinusBounds are expected, as these [25 implementers]
org.alloytools.pardinus.core/src/main/java/kodkod/engine/UnboundedSolver.java
Clause (Interface)
Unfortunately not all objects are Expr. However, from the UI we want to be able to locate the clauses in the text file a [14 …
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Clause.java
AlloyContext (Interface)
(no doc) [1 implementers]
org.alloytools.api/src/main/java/org/alloytools/alloy/context/api/AlloyContext.java
Func0 (Interface)
(no doc) [1 implementers]
org.alloytools.alloy.lsp/src/main/java/org/alloytools/alloy/lsp/provider/AlloyAppUtil.java
Explorer (Interface)
An iterator implementing more advanced iteration strategies for temporal solutions. @author Nuno Macedo // [HASLab] tem [6 …
org.alloytools.pardinus.core/src/main/java/kodkod/engine/Explorer.java
WorkerTask (Interface)
This defines an interface for performing tasks in a subprocess. [19 implementers]
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/WorkerEngine.java
AlloyLanguageClient (Interface)
(no doc)
org.alloytools.alloy.lsp/src/main/java/org/alloytools/alloy/lsp/provider/AlloyLanguageClient.java
TemporalSolver (Interface)
The interface that should be implemented by model finders that expect to solve temporal problems, i.e., formulas with {@ [25 …
org.alloytools.pardinus.core/src/main/java/kodkod/engine/TemporalSolver.java

Core symbols most depended-on inside this repo

tuple
called by 8473
org.alloytools.pardinus.core/src/main/java/kodkod/instance/TupleFactory.java
product
called by 4112
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java
add
called by 2667
org.alloytools.pardinus.core/src/main/java/kodkod/instance/TupleSet.java
join
called by 2298
org.alloytools.pardinus.core/src/main/java/kodkod/ast/Expression.java
add
called by 1124
org.alloytools.pardinus.core/src/main/java/kodkod/util/ints/IntSet.java
get
called by 1007
org.alloytools.pardinus.core/src/main/java/kodkod/util/ints/IntVector.java
oneOf
called by 1002
org.alloytools.pardinus.core/src/main/java/kodkod/ast/Variable.java
and
called by 908
org.alloytools.pardinus.core/src/main/java/kodkod/ast/Decls.java

Shape

Method 7,547
Class 722
Enum 80
Interface 70
Function 19

Languages

Java87%
C++13%

Modules by API surface

org.alloytools.pardinus.native/native-code/jni/darwin/arm64/jni.h262 symbols
org.alloytools.pardinus.native/native-code/jni/windows/amd64/jni.h261 symbols
org.alloytools.pardinus.native/native-code/jni/linux/amd64/jni.h261 symbols
org.alloytools.pardinus.native/native-code/jni/darwin/amd64/jni.h260 symbols
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/ast/Expr.java101 symbols
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/parser/CompModule.java95 symbols
org.alloytools.pardinus.core/src/main/java/kodkod/util/ints/Ints.java91 symbols
org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/SimpleGUI.java78 symbols
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/translator/A4Solution.java75 symbols
org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4viz/VizGUI.java75 symbols
org.alloytools.alloy.core/src/main/java/edu/mit/csail/sdg/alloy4/A4Preferences.java71 symbols
org.alloytools.alloy.application/src/main/java/edu/mit/csail/sdg/alloy4whole/PreferencesDialog.java69 symbols

For agents

$ claude mcp add org.alloytools.alloy \
  -- python -m otcore.mcp_server <graph>

⬇ download graph artifact

Ask about this repo answers extend the page