### Alloy Fact with Skolemization Example

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/skolem.html

This fact demonstrates a quantified formula that can be reduced using skolemization. The analysis will search for the existence of the skolem relation '_x_'.

```alloy
sig A {
    r: lone B
}
sig B {}

fact {
    some x: A | no x.r
}
```

```alloy
x' in A && no x'.r
```

--------------------------------

### Check Java Version

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/README.md

Verify that the installed Java version is 17 or later, which is a requirement for running Alloy.

```bash
java -version           # requires Java 17
openjdk version "17.0.9" 2023-10-17 LTS
OpenJDK Runtime Environment (build 17.0.9+11-LTS)
OpenJDK 64-Bit Server VM (build 17.0.9+11-LTS, mixed mode, sharing)
```

--------------------------------

### CMake Minimum Version and Project Setup

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Sets the minimum required CMake version and defines the project name. Ensure your CMake version meets this requirement.

```cmake
cmake_minimum_required(VERSION 3.0.0 FATAL_ERROR)

project(lingeling)
```

--------------------------------

### Module Import Example

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/a4.html

Demonstrates how Alloy infers module paths based on the 'module' declaration. If the 'module' line is present, paths are relative to the current module's directory. If omitted, paths are relative to the project root.

```Alloy
module MyProject/main
open MyProject/additional/helper
...
```

```Alloy
module MyProject/main
open MyProject/library/helper
...
```

--------------------------------

### Module Path Resolution Example

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/path.html

Demonstrates how Alloy infers module locations based on the current model's path and the module name. Modules in the same directory are resolved directly, while those in subdirectories are found within those subdirectories.

```alloy
model filesystem/main

open filesystem/debug as DEBUG
open filesystem/library/dirmodel as DIR
open filesystem/library/filemodel as FILE
```

--------------------------------

### Example Evaluator Output (Unreadable)

Source: https://github.com/alloytools/org.alloytools.alloy/wiki/5.0.0-Change-List

Illustrates the default, unformatted output from the Alloy evaluator, which can be difficult to read due to lack of newlines and dense atom formatting.

```text
{Foo$1->A$0->-1, Foo$1->A$0->-2, Foo$1->A$0->-3, Foo$1->A$0->-4, 
Foo$1->A$0->0, Foo$1->A$0->1, Foo$1->A$0->2, Foo$1->A$0->3, 
Foo$1->B$0->-2, Foo$1->B$0->-3, Foo$1->B$0->-4, Foo$1->B$0->2,
Foo$2->B$0->-1, Foo$2->B$0->0, Foo$2->B$0->1}
```

--------------------------------

### Commit Message Format

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/CONTRIBUTING.md

Commit messages should start with a short, imperative summary (max 50 chars), followed by an optional detailed explanation separated by an empty line.

```git
[visual] Fix position bug in visualizer

The position of nodes in a trace differ, this bug keeps the 
same node on the same place.
```

--------------------------------

### Set Minimum CMake Version

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Specifies the minimum required version of CMake for the project. Ensure your CMake installation meets this requirement.

```cmake
cmake_minimum_required(VERSION 3.20)
```

--------------------------------

### Run Alloy in Debug Mode

Source: https://github.com/alloytools/org.alloytools.alloy/wiki/5.0.0-Change-List

To resolve crashes when not in debug mode, start Alloy with the debug flag enabled. This is a temporary workaround for a known issue.

```bash
$ jar -Ddebug=yes -jar alloy.jar
```

--------------------------------

### Get First Element of Sequence

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.first' operator returns the first element of sequence 's' if the sequence is not empty. Otherwise, it returns the empty set.

```Alloy
s.first
```

--------------------------------

### Extract Subsequence

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.subseq[from, to]' operator returns a subsequence of 's' starting at index 'from' and ending at index 'to', inclusive. Precondition: 0 <= from <= to < #s.

```Alloy
s.subseq [from, to]
```

--------------------------------

### Set Sequence Length Bound

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

Adjust the maximum allowed length for sequences by setting the scope on 'seq'. This example allows sequences of up to 4 elements.

```Alloy
check SomeAssertion for 4 seq
```

--------------------------------

### Function/Predicate Call Syntax in Alloy 4

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/a4.html

Function and predicate calls now use the same operators '[]' and '.' as relational joins. For example, f(a,b) is written as f[a,b] or a.f[b]. If the argument list is empty, '[]' can be omitted.

```alloy
f[a,b]
```

```alloy
f[a][b]
```

```alloy
a.f[b]
```

```alloy
b.(a.f)
```

```alloy
f[a]
```

```alloy
a.f
```

```alloy
f[ ]
```

```alloy
f
```

```alloy
a.add[b].sub[c]
```

```alloy
pred contains[List, e:Element] { ... }
```

```alloy
pred acyclic { ... }
```

```alloy
pred List.contains[e:Element] { ... }
```

--------------------------------

### JAR File Structure for Native Solvers

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/readme.md

Explains the layout of the JAR file generated by bnd, highlighting the placement of native libraries, SATFactory classes, and license information.

```text
* `native/...` – Contains the native directories in `os/arch/lib|exe` format.
* `services/kodkod.engine.satlab.SATFactory` – Contains a list of all the SATFactory classes in this bundle
* `org/alloytools/solvers/natv/...` – The class files for the included SATFactory's
* `LICENSE` – The licenses for the included files
```

--------------------------------

### Get Sequence Length

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The '#s' operator returns the number of elements in a sequence 's'.

```Alloy
#s
```

--------------------------------

### Build Alloy with Proxy Settings

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/README.md

If you are behind a proxy, use this command to pass proxy settings to the Gradle build. Replace XXXXX with your specific proxy details.

```bash
./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
```

--------------------------------

### Get Set of Sequence Elements

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.elems' operator returns the set of all elements contained within sequence 's'.

```Alloy
s.elems
```

--------------------------------

### Run Alloy Analyzer JAR from Console

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/run.html

Execute the Alloy Analyzer by running its JAR file from the command line. Ensure the JAR file is in the current directory or provide the full path.

```shell
java -jar alloy4.jar
```

--------------------------------

### Custom Build Command for Configuration

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Configures the project and generates header files before the build. This command runs './configure' and 'make' in the 'repo' directory.

```cmake
add_custom_command(
    PRE_BUILD
    COMMAND ./configure
    COMMAND make lglcfg.h lglcflags.h
    WORKING_DIRECTORY ${CMAKE_SOURCE_DIR}/repo
    OUTPUT lglcfg.h
)
```

--------------------------------

### Sample Alloy XML Instance

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/xmlview.html

This is a sample XML file representing an Alloy instance. It defines signatures, fields, and their corresponding atoms and tuples.

```xml
<alloy>

<sig name="Name" extends="univ">
  <atom name="Name$0"/>
  <atom name="Name$1"/>
</sig>

<sig name="Date" extends="univ">
  <atom name="Date$0"/>
</sig>

<sig name="BirthdayBook" extends="univ">
  <atom name="BirthdayBook$0"/>
  <atom name="BirthdayBook$1"/>
</sig>

<field name="known">
    <type> <sig name="BirthdayBook"/> <sig name="Name"/> </type>
    <tuple> <atom name="BirthdayBook$1"/> <atom name="Name$1"/> </tuple>
</field>

<field name="date">
    <type> <sig name="BirthdayBook"/> <sig name="Name"/> <sig name="Date"/> </type>
    <tuple> <atom name="BirthdayBook$1"/> <atom name="Name$1"/> <atom name="Date$0"/> </tuple>
</field>

</instance>

</alloy>
```

--------------------------------

### Configure MiniSatProver CMake Project

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/minisatprover/CMakeLists.txt

Sets the minimum CMake version, project name, and MiniSatProver version. Include directories and library sources are defined, and a shared library is created. Target properties like output name and version are set.

```cmake
cmake_minimum_required(VERSION 3.20 FATAL_ERROR)

project(minisatprover)

set(MINISATP_VERSION "1.1.0")


include_directories(
    ${minisatprover_SOURCE_DIR}/repo 
    ${JNI_INCLUDE} 
    ${minisatprover_SOURCE_DIR}/repo/ADTs         
    ${CMAKE_CURRENT_SOURCE_DIR}/../headers
)
set(CMAKE_OSX_ARCHITECTURES ${OSX_ARCH})

set(MINISATP_LIB_SOURCES
    MiniSatProver.cpp
    repo/File.C
    repo/Proof.C
    repo/Solver.C
)

add_library(libminisatprover SHARED ${MINISATP_LIB_SOURCES})
add_definitions(-Wno-deprecated-declarations -Wno-deprecated)
target_link_libraries(libminisatprover ${GMP_LIBRARY})

set_target_properties(libminisatprover
  PROPERTIES
    OUTPUT_NAME "minisatprover" 
    VERSION ${MINISATP_VERSION})

```

--------------------------------

### Configure Minisat Library Build

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/minisat/CMakeLists.txt

This CMake script sets up the build for the Minisat library. It defines the project, version, includes necessary headers, specifies source files, and links against the ZLIB library.

```cmake
cmake_minimum_required(VERSION 3.0.0 FATAL_ERROR)

project(minisat)

set(MINISAT_VERSION "2.1.0")

set(CMAKE_OSX_ARCHITECTURES ${OSX_ARCH})
find_package(ZLIB)
include_directories(
    ${minisat_SOURCE_DIR}/repo 
    ${CMAKE_CURRENT_SOURCE_DIR}/../headers
    ${JNI_INCLUDE} )

add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS)

set(MINISAT_LIB_SOURCES
    MiniSat.cc
    repo/minisat/utils/Options.cc
    repo/minisat/utils/System.cc
    repo/minisat/core/Solver.cc
    repo/minisat/simp/SimpSolver.cc)

add_library(minisat-lib SHARED ${MINISAT_LIB_SOURCES})

target_link_libraries(minisat-lib ${ZLIB_LIBRARY})


set_target_properties(minisat-lib
  PROPERTIES
    OUTPUT_NAME "minisat")
```

--------------------------------

### Get Last Element of Sequence

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.last' operator returns the last element of sequence 's' if the sequence is not empty. Otherwise, it returns the empty set.

```Alloy
s.last
```

--------------------------------

### Build and Test AlloyTools with Gradle

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/CONTRIBUTING.md

Use this command to assemble and test the AlloyTools projects. It leverages Gradle, which is managed by the gradlew script included in the repository.

```bash
./gradlew build
```

--------------------------------

### Get Last Index of Sequence

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.lastIdx' operator returns the index of the last element in sequence 's', which is (#s)-1. Returns an empty set if 's' is empty.

```Alloy
s.lastIdx
```

--------------------------------

### Run Alloy Executable

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/README.md

Execute the Alloy application by running the generated JAR file. This command will typically open the Alloy GUI.

```bash
java -jar org.alloytools.alloy.dist/target/org.alloytools.alloy.dist.jar
# opens GUI
```

--------------------------------

### Creating the Executable Target

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Builds the 'plingeling' executable using the specified source files. This command links the executable with threading libraries and the math library.

```cmake
add_executable(plingeling ${LIB_SOURCES} repo/plingeling.c)
target_link_libraries(plingeling PRIVATE ${CMAKE_THREAD_LIBS_INIT}  m)
```

--------------------------------

### Get Indices of Sequence Elements

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.inds' operator returns a set of integers representing the valid indices of sequence 's', from 0 up to (#s)-1. Returns an empty set if 's' is empty.

```Alloy
s.inds
```

--------------------------------

### Clone and Build Alloy Project

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/README.md

Clone the Alloy project repository and build the executable JAR using Gradle. The JAR will be located in the specified directory after a successful build.

```bash
git clone --recursive https://github.com/AlloyTools/org.alloytools.alloy.git
cd org.alloytools.alloy
./gradlew build
```

--------------------------------

### Get Sequence Without Last Element

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.butLast' operator returns a new sequence with the last element of 's' removed. If 's' has one or fewer elements, it returns an empty sequence.

```Alloy
s.butLast
```

--------------------------------

### Clone the Main Alloy Repository

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/CONTRIBUTING.md

Clone the main AlloyTools repository to your local system. This sets up the 'origin' remote pointing to the main repository.

```bash
git clone https://github.com/AlloyTools/org.alloytools.alloy.git
```

--------------------------------

### Get Sequence Without First Element

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.rest' operator returns a new sequence with the first element of 's' removed. If 's' has one or fewer elements, it returns an empty sequence.

```Alloy
s.rest
```

--------------------------------

### Get Index After Last Element

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 's.afterLastIdx' operator returns the index immediately following the last element of 's' (#s), provided this index is less than the maximum allowed sequence length. Otherwise, it returns an empty set.

```Alloy
s.afterLastIdx
```

--------------------------------

### Configure Git Push Default (Simple)

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/CONTRIBUTING.md

Configure Git's push.default to 'simple'. This is recommended for clarity unless you are using Git 2.0 or later, where it is the default behavior.

```bash
git config push.default simple
```

--------------------------------

### Include Directories Configuration

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Specifies directories to be searched for header files during compilation. Includes JNI, project-specific, and ZLIB headers.

```cmake
include_directories(
        ${JNI_INCLUDE}
        ${CMAKE_CURRENT_SOURCE_DIR}/repo
        ${CMAKE_CURRENT_SOURCE_DIR}/../headers
        ${ZLIB_INCLUDE_DIR})

```

--------------------------------

### Alloy Literate Programming Syntax

Source: https://github.com/alloytools/org.alloytools.alloy/wiki/5.0.0-Change-List

Demonstrates the basic structure of a literate programming file in Alloy, including the YAML header and the Alloy code block separator. This format is recognized by GitHub for syntax highlighting.

```yaml
---
title: Dining Philosophers
---
```

```alloy
sig Foo {} // this is Alloy syntax
```

--------------------------------

### Setting Project Version and Finding Packages

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Defines the project version and finds the necessary 'Threads' package. The 'Threads' package is required for multi-threading support.

```cmake
set(VERSION "sc2022")
find_package(Threads REQUIRED)
```

--------------------------------

### Defining Library Source Files

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Lists the source files that constitute the project's library. These files are compiled into the main executable.

```cmake
set(LIB_SOURCES
    repo/lglib.c repo/lglbnr.c repo/lgldimacs.c repo/lglopts.c
)
```

--------------------------------

### Including Directories for Headers

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Specifies directories where header files can be found. Ensure all necessary header paths are included here for successful compilation.

```cmake
include_directories(
    ${lingeling_SOURCE_DIR}/repo 
    ${lingeling_SOURCE_DIR}         
    ${CMAKE_CURRENT_SOURCE_DIR}/../headers
    ${JNI_INCLUDE} )
```

--------------------------------

### Configuring Build Type and Architecture

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Sets the build type to 'Debug' and specifies the target architecture for macOS. Adjust 'OSX_ARCH' as needed for your build environment.

```cmake
set(CMAKE_BUILD_TYPE Debug)
set(CMAKE_OSX_ARCHITECTURES ${OSX_ARCH})
```

--------------------------------

### macOS Architecture Setting

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Configures the target architectures for macOS builds. Use the OSX_ARCH variable to specify desired architectures.

```cmake
set(CMAKE_OSX_ARCHITECTURES ${OSX_ARCH})
```

--------------------------------

### Link ZLIB Library

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Links the ZLIB library to the project. This makes ZLIB functions available at link time.

```cmake
link_libraries(${ZLIB_LIBRARY})
```

--------------------------------

### Private Module Import

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/private.html

Illustrates how to use 'private open' to import a module's contents without exposing that module itself to subsequent imports. This is useful for creating layered module dependencies where intermediate modules should not be directly accessible.

```alloy
module moduleA

open moduleB

module moduleB

private open moduleC

open moduleD

sig B { }

module moduleC

sig C { }

module moduleD

sig D { }
```

--------------------------------

### Windows Platform Definitions

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Adds compile definitions for Windows to resolve potential function name conflicts or provide platform-specific implementations.

```cmake
IF(WIN32) 
        add_compile_definitions(putc_unlocked=putc)
        add_compile_definitions(gettimeofday=mingw_gettimeofday)
ENDIF()
```

--------------------------------

### Collect Source Files

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Uses file globbing to find all C++ source files within specified directories. Excludes 'repo/simp/Main.cc' from the list.

```cmake
file(GLOB lib_srcs RELATIVE ${CMAKE_CURRENT_SOURCE_DIR} *.cpp repo/mtl/*.cc repo/core/*.cc repo/simp/*.cc repo/utils/*.cc)
list(REMOVE_ITEM lib_srcs "repo/simp/Main.cc")
```

--------------------------------

### Add Fork Remote for Triangular Workflow

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/CONTRIBUTING.md

Add your forked repository as a remote named 'fork'. Replace 'github-user' with your actual GitHub username. This is part of setting up the Git triangular workflow.

```bash
cd org.alloytools.alloy
git remote add fork git@github.com:github-user/org.alloytools.alloy.git
```

--------------------------------

### Open Statement in Alloy

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/path.html

Use the 'open' statement to include modules from other Alloy files. This is analogous to 'import' in Java or 'include' in C/C++.

```alloy
open util/integer
```

--------------------------------

### Project Name Configuration

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Defines the project name. This is used by CMake for various internal purposes.

```cmake
project(glucose)
```

--------------------------------

### Adding Compiler Definitions

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/lingeling/CMakeLists.txt

Defines preprocessor macros for the compiler. These flags enable various features and optimizations during compilation.

```cmake
add_definitions(-Wall -O3 -DNLGLOG -DNDEBUG -DNCHKSOL -DNLGLDRUPLIG -DNLGLYALSAT -DNLGLFILES -DNLGLDEMA )
```

--------------------------------

### Alloy SAT Solver and Options Definitions

Source: https://github.com/alloytools/org.alloytools.alloy/wiki/Solver-Plugin-Model

Defines the core Alloy language constructs for SAT solvers, including their properties, options, and integration with Kodkod's SATFactory.

```alloy
    enum boolean { true, false }

    -- Core
    abstract sig SatSolver {
       id : String,
       external : String,    -- command line
       options  : seq String -- command line options
    }

    sig A4Options {
        solver : SatSolver,
        -- solver specific options
        skolemDepth : Int,
        unroll      : Int,
        intwidth    : Int
        -- ...
    }

    sig A4Solution {
        Solvers : SatSolver -> SATFactory
        solver  : Solver
    }


    -- Kodkod

    abstract sig SATFactory {
        prover      : boolean,
        incremental : boolean,
        instance    : SATSolver,
        toString    : String -- name of the solver
    }
    abstract sig SATSolver {
          // ...
    }
    abstract sig SATProver extends SATSolver {
          // ...
    }

    sig Solver {
       solver : SATFactory
    }

```

--------------------------------

### Find ZLIB Dependency

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.pardinus.native/native-code/glucose/CMakeLists.txt

Locates and includes the ZLIB compression library, which is required for the project. The REQUIRED keyword ensures the build fails if ZLIB is not found.

```cmake
find_package(ZLIB REQUIRED)
```

--------------------------------

### Sequence in Quantifications

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/seq.html

The 'seq' keyword can be used in quantifications to iterate over sequences.

```Alloy
some s: seq Book | FORMULA
```

--------------------------------

### Private Sig, Field, Function, and Predicate Declaration

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/private.html

Demonstrates the use of the 'private' keyword to declare signatures, fields, functions, and predicates that are not exposed to other modules. Use this to manage module interfaces and prevent unintended access to internal implementation details.

```alloy
module moduleA

open moduleB

module moduleB

sig Person {
    favorite: Book,
    knows: set Person,
    private likes: set Person
}

private sig Book { year: Int }

fun allBook: set Book { Book }

private fun union[a, b: set univ]: set univ { a+b }
```

--------------------------------

### Anonymous Assertions and Predicates

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/a4.html

Allows writing 'check' and 'run' directly with formulas, eliminating the need for separate 'assert' or 'pred' declarations. An optional label can be prepended.

```Alloy
check { A!=B } for 3
```

```Alloy
run { some a:A, b:B | a=b } for 3
```

```Alloy
somelabel: check { A != B } for 3
```

```Alloy
somelabel: run { some a:A, b:B | a=b } for 3
```

--------------------------------

### Integer Operations

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/a4.html

Provides standard arithmetic and bitwise operations for integers. Some operations can be shortened if unambiguous.

```Alloy
a.add[b]
```

```Alloy
a.sub[b]
```

```Alloy
a.mul[b]
```

```Alloy
a.div[b]
```

```Alloy
a.rem[b]
```

```Alloy
- a
```

```Alloy
a = b
```

```Alloy
a != b
```

```Alloy
a < b
```

```Alloy
a > b
```

```Alloy
a <= b
```

```Alloy
a >= b
```

```Alloy
a << b
```

```Alloy
a >> b
```

```Alloy
a >>> b
```

--------------------------------

### Configure Default Push to Fork

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/CONTRIBUTING.md

Set the default remote for push operations to your fork. This ensures that 'git push' commands send commits to your fork repository.

```bash
git config remote.pushdefault fork
```

--------------------------------

### Setting Bitwidth for Integers in Alloy 4

Source: https://github.com/alloytools/org.alloytools.alloy/blob/master/org.alloytools.alloy.extra/extra/help/a4.html

To set the bitwidth for integers, use the 'int' keyword in a 'run' or 'check' command. The scope of Int atoms is now determined by this bitwidth.

```alloy
check MyAssertion for 4 int
```