### Verify Modelator CLI Installation

Source: https://github.com/informalsystems/modelator/blob/dev/INSTALLATION.md

Command to execute the Modelator command-line interface (CLI) and verify its successful installation. Running this command should display information about the tool, confirming it's operational.

```bash
modelator
```

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

### Install Modelator Python Package

Source: https://github.com/informalsystems/modelator/blob/dev/INSTALLATION.md

Command to install the Modelator library using Python's pip package manager. This step assumes Python and pip are correctly set up and accessible in the system's PATH.

```bash
pip install modelator
```

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

### Sample TLA+ Examples Using Modelator Shell

Source: https://github.com/informalsystems/modelator/blob/dev/Modelator.md

This shell command demonstrates how to use the `modelator.shell` to parse a TLA+ model file (`samples/HourClockTraits.tla`) and then sample all auto-collected examples. The output shows the concrete instances (traces or conditions) generated for `ExThreeHours`, `ExHourDecrease`, and `ExFullRun`, illustrating Modelator's ability to provide satisfying examples.

```sh
python
>>> from modelator.shell import *
>>> m = parse_model("samples/HourClockTraits.tla")
>>> m.sample()
Example for "ExThreeHours": 
  hr = 3
Example for "ExHourDecrease": 
  hr = 12 | hr = 1 
Example for "ExFullRun": 
  hr = 1 | hr = 2 | hr = 3 | hr = 4 | hr = 5 | hr = 6 | hr = 7
  hr = 8 | hr = 9 | hr = 10 | hr = 11 | hr = 12
```

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

### Set Python Version with pyenv

Source: https://github.com/informalsystems/modelator/blob/dev/INSTALLATION.md

Commands to install a specific Python version (e.g., 3.10.6) and set it as the global default using pyenv, a tool for managing multiple Python versions. This ensures the correct Python environment for Modelator.

```bash
pyenv install 3.10.6
pyenv global 3.10.6
```

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

### TLA+ Comments Syntax

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Demonstrates how to write single-line and multi-line comments in TLA+ specifications.

```tla
(* Comments *)

(* This is 
   multiline comment *)
\* This is single line comment
```

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

### TLA+ Module Structure and Declarations

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Explains the basic structure of a TLA+ module, including how to define, extend (import), and declare variables and constants within a module. Modules should reside in files with a matching name.

```tla
(* Module structure *)

---- MODULE <module> ----   \* Starts TLA+ module (should be in file <module>.tla)
====                        \* Ends TLA+ module (everything after that is ignored)

EXTENDS <module>            \* EXTEND (import) another TLA+ module
VARIABLES x, y, ...         \* declares variables x, y, ...
CONSTANTS x, y, ...         \* declares constants x, y, ... (should be defined in configuration)
```

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

### Compile Jekyll Website Locally

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

Instructions for setting up a new branch, navigating to the Jekyll directory, installing Ruby dependencies with Bundler, and serving the Jekyll site locally for development. Includes a note on enabling automatic recompilation upon file changes.

```sh
git checkout -b new_page # to create a new branch
cd jekyll
# make sure `bundle` is installed
bundle install
bundle exec jekyll serve
# add `-w` option to recompile automatically the files are changed
# when you are finished, push the commits to new_page branch
```

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

### Verify Modelator CLI Installation

Source: https://github.com/informalsystems/modelator/blob/dev/README.md

After installation, this command is used to verify that the Modelator command-line interface is correctly installed and accessible in the system's PATH. Executing it should display basic information about the tool, confirming its readiness for use.

```Shell
modelator
```

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

### TLA+ Core Syntax Reference

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Fundamental TLA+ syntax elements for constructing tuples, accessing elements, defining Cartesian products, using quantifiers, representing state changes with primed variables and UNCHANGED, and implementing control structures like LET and IF/THEN/ELSE.

```TLA+
<<a, b, c>>                 \* tuple constructor: a tuple of a,b,c (yes! the <<>> constructor is overloaded)
                            \* - sequence elements should be same type; tuple elements may have different types
t[i]                        \* the ith element of the tuple t (1-indexed!)
S \X T                      \* Cartesian product: set of all tuples <<x, y>>, where x is from S, y is from T

(* Quantifiers *)

\A x \in S: e               \* for all elements x in set S it holds that expression e is true
\E x \in S: e               \* there exists an element x in set S such that expression e is true

(* State changes *)

x', y'                      \* a primed variable (suffixed with ') denotes variable value in the next state 
UNCHANGED <<x,y>>           \* variables x, y are unchanged in the next state (same as x'=x /\ y'=y)

(* Control structures *)

LET x == e1 IN e2           \* introduces a local definition: every occurrence of x in e2 is replaced with e1
IF P THEN e1 ELSE e2        \* if P is true, then e1 should be true; otherwise e2 should be true
```

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

### Create Gantt Diagrams with Mermaid

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

An example of Mermaid syntax for generating a Gantt chart. This snippet demonstrates how to define a diagram title, sections, and individual tasks with their durations and dependencies.

```mermaid
gantt
  title A Gantt Diagram

  section Section
  A task: a1, 2014-01-01, 30d
  Another task: after a1, 20d

  section Another
  Task in sec: 2014-01-12, 12d
  Another task: 24d
```

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

### Start Modelator Shell in Python Interactive Mode

Source: https://github.com/informalsystems/modelator/blob/dev/ModelatorShell.md

This snippet demonstrates the command-line instruction to launch the Modelator Shell in an interactive Python environment. Running this command initiates a Python interpreter session with the ModelatorShell module loaded, allowing direct interaction with its functionalities.

```Python
python -i modelator_shell.py
```

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

### TLA+ Function Definitions and Operations

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Covers function construction, application, domain retrieval, and the `EXCEPT` operator for updating function values at specific keys. Also shows how to define a set of all functions mapping keys from one set to values from another.

```tla
(* Functions *) 

[x \in S |-> e]             \* function constructor: maps all keys x from set S to expression e (may refer to x) 
f[x]                        \* function application: the value of function f at key x
DOMAIN f                    \* function domain: the set of keys of function f
[f EXCEPT ![x] = e]         \* function f with key x remapped to expression e (may reference @, the original f[x])
[f EXCEPT ![x] = e1,        \* function f with multiple keys remapped: 
          ![y] = e2, ...]   \*   x to e1 (@ in e1 will be equal to f[x]), y to e2 (@ in e2 will be equal to f[y])
[S -> T]                    \* function set constructor: set of all functions with keys from S and values from T
```

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

### Set Up Modelator Development Environment

Source: https://github.com/informalsystems/modelator/blob/dev/README.md

These commands outline the steps to set up a local development environment for contributing to Modelator. It involves cloning the repository from GitHub, navigating into the project directory, installing project dependencies using Poetry, and activating the Poetry shell for development.

```Shell
git clone git@github.com/informalsystems/modelator
cd modelator
poetry install
poetry shell
```

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

### Install Modelator via pip

Source: https://github.com/informalsystems/modelator/blob/dev/README.md

This command installs the Modelator tool using Python's package installer, pip. It requires Python 3.8 or newer and Java 17 or newer to be pre-installed on the system for Modelator to function correctly.

```Shell
pip install modelator
```

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

### Inspect ModelatorShell Instance and Class Help in Python

Source: https://github.com/informalsystems/modelator/blob/dev/ModelatorShell.md

These commands illustrate various methods to inspect the `ModelatorShell` instance (`m`) and its class. Typing `m` provides a detailed representation, `print(m)` offers a prettier summary, and `help(m)` or `help(ModelatorShell)` display comprehensive documentation on usage and available methods.

```Python
m
print(m)
help(m)
help(ModelatorShell)
```

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

### Running TLC Model Checker Commands

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Bash commands for running TLC, the TLA+ model checker, including setting JVM memory and worker threads, and executing model checks in standard or simulation mode.

```bash
# Running TLC

# A handy alias providing the JVM with 12GB of RAM (adjust accordingly) and using multiple threads
alias tlc="java -XX:+UseParallelGC -Xmx12g -cp tla2tools.jar tlc2.TLC -workers auto" 

# Model check with TLC
tlc -config <.config file> <.tla file> 

# Run TLC in simulation mode
tlc -config <.config file> -simulate <.tla file>
```

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

### ModelatorShell Class API Reference

Source: https://github.com/informalsystems/modelator/blob/dev/ModelatorShell.md

Comprehensive API documentation for the `ModelatorShell` class, detailing its constructor, methods like `load`, `parse`, `typecheck`, and `check`, along with their parameters, default values, and return types. It also includes properties like `autoload`.

```APIDOC
ModelatorShell:
  __init__()
    Description: Initializes a new instance of the ModelatorShell.
  load(file_path: str)
    Description: Loads a TLA+ model file into the shell.
    Parameters:
      file_path: The path to the TLA+ model file (e.g., 'model.tla').
    Returns: None
  parse()
    Description: Parses the currently loaded TLA+ model file.
    Returns: str (Success message or detailed parse error information.)
  typecheck()
    Description: Type-checks the currently loaded TLA+ model file.
    Returns: str (Success message or detailed type-checking error information.)
  check(init_predicate: str = 'Init', next_predicate: str = 'Next', invariants: list = ['Inv'], checker: str = 'apalache', config_file_name: str = None)
    Description: Performs model checking on the loaded TLA+ model.
    Parameters:
      init_predicate: The initial state predicate. Defaults to 'Init'.
      next_predicate: The next state predicate. Defaults to 'Next'.
      invariants: A list of invariants (strings) to check. Defaults to ['Inv'].
      checker: The model checker backend to use. Defaults to 'apalache'.
      config_file_name: Optional path to a configuration file for the checker.
    Returns: str (Model checking result, including counterexamples if invariants are violated.)
  autoload: bool
    Description: A boolean property that controls whether the loaded model file is automatically reloaded before executing actions like parse, typecheck, or check. Defaults to True.
```

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

### TLA+ Sequence Definitions and Operations

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Details sequence construction, element access (which is 1-indexed), concatenation, length calculation, appending elements, and retrieving the first element. These operations require extending the standard `Sequences` module.

```tla
(* Sequences *)             \* EXTENDS Sequences (should extend standard module Sequences)

<<a, b, c>>                 \* sequence constructor: a sequence containing elements a, b, c
s[i]                        \* the ith element of the sequence s (1-indexed!)
s \o t                      \* the sequences s and t concatenated
Len(s)                      \* the length of sequence s
Append(s, x)                \* the sequence s with x added to the end
Head(s)                     \* the first element of sequence s
```

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

### TLA+ Integer Types and Operations

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Details integer types, literals, ranges, and common arithmetic and comparison operators available in TLA+. To use these, the standard `Integers` module must be extended.

```tla
(* Integers *)              \* EXTENDS Integers (should extend standard module Integers)

Int                         \* the set of all integers (an infinite set)
1, -2, 1234567890           \* integer literals; integers are unbounded
a..b                        \* integer range: all integers between a and b inclusive
x + y, x - y, x * y         \* integer addition, subtraction, multiplication
x < y, x <= y               \* less than, less than or equal
x > y, x >= y               \* greater than, greater than or equal
```

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

### Reset Modelator CLI State

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_basic.md

Demonstrates how to reset the `modelator` CLI state, ensuring that no model is currently loaded. This command is typically used to clear any previously loaded models or configurations before starting a new session.

```sh
$ modelator reset
...
```

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

### Query Modelator State Without Loaded Model

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_basic.md

Illustrates the output of `modelator info`, `modelator typecheck`, and `modelator reload` commands when no model has been loaded. These commands provide informative messages or errors indicating the absence of a loaded model, guiding the user to load one first.

```sh
$ modelator info
Model file does not exist
$ modelator typecheck
Model file does not exist
$ modelator reload
ERROR: model not loaded; run `modelator load` first
```

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

### TLA+ Record Definitions and Operations

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Explains how to construct records, access fields, and use the `EXCEPT` operator for updating record fields. It also demonstrates how to define a set of records with fields drawn from specified sets.

```tla
(* Records *)

[x |-> e1, y |-> e2, ...] \* record constructor: a record which field x equals to e1, field y equals to e2, ... 
r.x                         \* record field access: the value of field x of record r
[r EXCEPT !.x = e]          \* record r with field x remapped to expression e (may reference @, the original r.x)
[r EXCEPT !.x = e1,         \* record r with multiple fields remapped: 
          !.y = e2, ...]    \*   x to e1 (@ in e1 is equal to r.x), y to e2 (@ in e2 is equal to r.y)
[x: S, y: T, ...]           \* record set constructor: set of all records with field x from S, field y from T, ...
```

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

### Define Initial State with Init Operator in TLA+

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/hello_world.md

The `Init` operator specifies the starting configuration of the state variables. It initializes `alices_outbox` and `network` as empty sets, `bobs_mood` to 'neutral', and `bobs_inbox` as an empty sequence, setting up the system's baseline state.

```tla
Init ==
    /\ alices_outbox = {} \* Alice has sent nothing (empty set)
    /\ network = {} \* AND so is the network
    /\ bobs_mood = "neutral" \* AND Bob's mood is neutral
    /\ bobs_inbox = <<>> \* AND Bob's inbox is an empty Sequence (list)
```

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

### Sample Jekyll Markdown Page with Front Matter

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

A complete example of a Markdown file (`blogs.md`) intended for a Jekyll website. It demonstrates the use of YAML front matter to define page metadata like title, layout, parent page, and navigation order, followed by standard Markdown content.

```markdown
---
title: Blog posts
layout: default
parent: Homepage
nav_order: 2
---

# Welcome to my blogs.
```

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

### TLA+ Whitespace and Precedence Example

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Illustrates how whitespace and indentation significantly affect the logical operator precedence in TLA+, specifically for conjunctions (`/\`) and disjunctions (`\/`).

```TLA+
Foo == /\ x
       /\ \/ y
          \/ z
```

```TLA+
Foo == x and ( y or z)
```

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

### TLA+ Operator Definitions

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Shows how to define operators in TLA+, both without parameters and with a list of parameters. Operators are associated with an expression that may refer to their parameters.

```tla
Name == e                   \* defines operator Name without parameters, and with expression e as a body
Name(x, y, ...) == e        \* defines operator Name with parameters x, y, ..., and body e (may refer to x, y, ...)
```

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

### Apalache-Specific TLA+ Functions

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

TLA+ module definitions provided by Apalache, including `FunAsSeq` for treating functions as sequences and `FoldSet`/`FoldSeq` for aggregating elements in sets and sequences.

```TLA+
(* Writing models with Apalache *)

EXTENDS Apalache       \* Import https://github.com/informalsystems/apalache/blob/unstable/src/tla/Apalache.tla

\* Makes Apalache understand that a function with keys in 1.maxSeqLen can be treated as a Sequence
FunAsSeq(fn, maxSeqLen) == SubSeq(fn, 1, maxSeqLen)

(*
Equivalent to the pseudocode:

x = initialValue
for element in arbitrary_ordering(S):
   x = CombinerFun(x, element)
return x

*)
FoldSet(CombinerFun, initialValue, S) \* For a set S

(*
Equivalent to the pseudocode:

x = initialValue
for element in sequential_ordering(S):
   x = CombinerFun(x, element)
return x

*)
FoldSeq(CombinerFun, initialValue, S) \* For a sequence S
```

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

### Running Apalache Model Checker Commands

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Bash commands for interacting with Apalache, including setting up an alias, type checking TLA+ files, and various model checking operations with configuration files, invariants, and trace generation.

```bash
# Running apalache

# A handy alias for calling Apalache
alias apalache="java -jar apalache-pkg-0.17.5-full.jar --nworkers=8"

# Typecheck
apalache typecheck <.tla file>

# Model check assuming a .cfg file with the same name as the .tla file is present
apalache check <.tla file>

# Model check assuming with a specific .cfg file
apalache check --config=<.cfg file> <.tla file>

# Model check an invariant Foo 
apalache check --inv=Foo <.tla file>

# Generate multiple (up to n) traces for invariant Foo
apalache check --view=<View Operator Name> --max-error=n --inv=Foo <.tla file>
```

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

### TLA+ Finite Set Operations

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Provides syntax for constructing finite sets and performing common set operations like cardinality, membership testing, subset checking, union, intersection, difference, filtering, and mapping. These operations require extending the standard `FiniteSets` module.

```tla
(* Finite sets *)           \* EXTENDS FiniteSets (should extend standard module FiniteSets)

{a, b, c}                   \* set constructor: the set containing a, b, c
Cardinality(S)              \* number of elements in set S
x \in S                     \* x belongs to set S
x \notin S                  \* x does not belong to set S
S \subseteq T               \* is set S a subset of set T? true of all elements of S belong to T
S \union T                  \* union of sets S and T: all x belonging to S or T
S \intersect T              \* intersection of sets S and T: all x belonging to S and T
S \ T                       \* set difference, S less T: all x belonging to S but not T
{x \in S: P(x)}             \* set filter: selects all elements x in S such that P(x) is true
{e: x \in S}                \* set map: maps all elements x in set S to expression e (which may contain x)
```

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

### Define TLA+ Examples for HourClock Model

Source: https://github.com/informalsystems/modelator/blob/dev/Modelator.md

This TLA+ code defines three types of examples (`ExThreeHours` for state, `ExHourDecrease` for action, `ExFullRun` for trace) within the `HourClockTraits` module. These examples are used by Modelator to generate traces satisfying specific conditions, such as reaching a state where `hr = 3` or producing a trace with distinct hour values.

```tla
----- MODULE HourClockTraits -----

EXTENDS HourClock

ExThreeHours == hr = 3

ExHourDecrease == hr' < hr

\* @type: Seq(STATE) => Bool;
ExFullRun(trace) == 
    /\ Len(trace) = 12
    /\ \A s1, s2 \in DOMAIN trace: 
           s1 /= s2 => trace[s1].hr /= trace[s2].hr
        

==================================
```

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

### TLA+ String Types and Literals

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Describes the `STRING` type and how to define string literals in TLA+. Strings can be compared for equality but are otherwise uninterpreted.

```tla
(* Strings *)               

STRING                      \* the set of all finite strings (an infinite set)
"", "a", "hello, world"     \* string literals (can be compared for equality; otherwise uninterpreted)
```

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

### Render LaTeX Mathematical Expressions with MathJax

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

Examples of using LaTeX syntax for mathematical expressions within Jekyll pages, which are then rendered by MathJax. This includes both inline and block-level equations, showcasing common mathematical notation.

```latex
The *Gamma function* satisfying $\Gamma(n) = (n-1)!\quad\forall n\in\mathbb N$ is via the Euler integral

$$
x = {-b \pm \sqrt{b^2-4ac} \over 2a}.
$$

$$
\Gamma(z) = \int_0^\infty t^{z-1}e^{-t}dt\,.
$$
```

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

### Instantiate ModelatorShell Object in Python

Source: https://github.com/informalsystems/modelator/blob/dev/ModelatorShell.md

This code creates an instance of the `ModelatorShell` class, assigning it to the variable `m`. This instance serves as the primary entry point for accessing all Modelator functionalities within the interactive shell.

```Python
m = ModelatorShell()
```

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

### Generate UML Sequence Diagrams with PlantUML

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

An example of PlantUML syntax used to define a simple UML sequence diagram. This code snippet illustrates how to represent interactions between participants and add notes within the diagram.

```plantuml
Alice->Bob: Hello Bob, how are you?
Note right of Bob: Bob thinks
Bob-->Alice: I am good thanks!
Note left of Alice: Alice responds
Alice->Bob: Where have you been?
```

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

### Demonstrate `modelator load` parsing error

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_parse.md

Shows how the `modelator load` command fails with a parsing error when attempting to load a syntactically invalid TLA+ model. Includes a `modelator reset` command for initial setup.

```sh
$ modelator reset
...
$ modelator load model/errors/TestError1.tla
...
Parsing error 💥
...
[5]
```

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

### Jekyll Page Front Matter YAML Configuration

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

An example of a YAML front matter block, which is a required metadata section at the beginning of Jekyll Markdown files. It defines page properties such as title and layout, crucial for Jekyll's rendering process.

```yaml
---
title: Homepage
layout: default
---
```

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

### Embed Media in Jekyll Markdown Pages

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/README.md

Examples demonstrating how to embed external media content, specifically YouTube videos, Vimeo videos, and PDF documents, directly into Jekyll Markdown pages using specific syntax supported by the `jekyll-spaceship` plugin.

```markdown
![](https://www.youtube.com/watch?v=aqz-KE-bpKQ)
![](https://vimeo.com/124148255)
{%pdf https://www.w3.org/WAI/ER/tests/xhtml/testfiles/resources/pdf/dummy.pdf %}
```

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

### Check Multiple Valid Invariants (Expected Success)

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_load_without_config.md

Illustrates how to check multiple valid invariants simultaneously using a comma-separated list. This example shows that all specified valid invariants are successfully verified.

```sh
$ modelator check --invariants Inv,InvC
```

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

### Parsing TLA+ Models from File and Source String

Source: https://github.com/informalsystems/modelator/blob/dev/Modelator.md

This example illustrates how to parse TLA+ models using Modelator. It demonstrates parsing from an external `.tla` file and directly from a multi-line TLA+ source string. The `Model` class represents the parsed TLA+ model, and exceptions are raised for parsing failures.

```python
from modelator import *

m = parse_model("samples/HourClock.tla")

m2 = parse_model_source('''
----- MODULE HourClock -----

EXTENDS Naturals, Sequences
VARIABLES 
  \* @typeAlias: STATE = [ hr: Int ];
  \* @type: Int;
  hr
Init == hr \in (1..12)
Next == hr' = IF hr /= 12 THEN hr + 1 ELSE 1

============================
''')
```

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

### TLA+ Boolean Logic Operators

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tla+cheatsheet.md

Provides a reference for boolean types and logical operators in TLA+, including negation, conjunction, disjunction, equality, inequality, implication, and equivalence. Conjunctions and disjunctions can be formatted across multiple lines.

```tla
(* Boolean logic *)

BOOLEAN                     \* the set of all booleans (same as {TRUE, FALSE})
TRUE                        \* Boolean true
FALSE                       \* Boolean false
~x                          \* not x; negation
x /\ y                      \* x and y; conjunction (can be also put at line start, in multi-line conjunctions)
x \/ y                      \* x or y; disjunction (can be also put at line start, in multi-line disjunctions)
x = y                       \* x equals y
x /= y                      \* x not equals y
x => y                      \* implication: y is true whenever x is true
x <=> y                     \* equivalence: x is true if and only if y is true
```

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

### Next Operator for Model Checker Evaluation Example in TLA+

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/hello_world.md

This snippet shows a partial `Next` operator used to demonstrate how a TLA+ model checker evaluates possible transitions. It highlights that `Next` is a disjunction of actions, and the model checker will explore any path where at least one of the listed actions evaluates to true.

```tla
Next ==
    \/ AliceSend("hello")
    \/ AliceSend("world")
    \/ NetworkLoss
    \* (ignore other operators for now)
```

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

### Attempt to Load Model Without Path

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_basic.md

Shows the behavior of the `modelator load` command when invoked without specifying a model file path. The command is expected to exit with an error code, indicating that a path argument is required for successful model loading.

```sh
$ modelator load
...
[2]
```

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

### Perform Model Checking on TLA+ Model with Modelator Shell

Source: https://github.com/informalsystems/modelator/blob/dev/ModelatorShell.md

This snippet illustrates various ways to invoke model checking using `m.check()`. It shows usage with default arguments, specifying custom invariants and a checker, and providing a configuration file. The output includes counterexamples if invariants are violated.

```Python
m.check()
m.check(invariants=['Inv', 'Inv2'], checker='apalache')
m.check(config_file_name='Hello.cfg')
```

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

### Define Core State Transition Actions in TLA+

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/hello_world.md

This comprehensive TLA+ block defines the individual actions that govern the system's dynamic behavior. `AliceSend(m)` models Alice sending a message, `NetworkLoss` simulates message loss, `NetworkDeliver` handles message delivery, and `BobCheckInbox` describes Bob's interaction with his inbox.

```tla
AliceSend(m) == 
    /\ m \notin alices_outbox
    /\ alices_outbox' = alices_outbox \union {m}
    /\ network' = network \union {m}
    /\ UNCHANGED <<bobs_mood, bobs_inbox>>

NetworkLoss == 
    /\ \E e \in network: network' = network \ {e}
    /\ UNCHANGED <<bobs_mood, bobs_inbox, alices_outbox>>

NetworkDeliver == 
    /\ \E e \in network:
        /\ bobs_inbox' = bobs_inbox \o <<e>> 
        /\ network' = network \ {e}
    /\ UNCHANGED <<bobs_mood, alices_outbox>>

BobCheckInbox == 
    /\ bobs_mood' = IF bobs_inbox = <<"hello", "world">> THEN "happy" ELSE "neutral"
    /\ UNCHANGED <<network, bobs_inbox, alices_outbox>>
```

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

### TLA+ Initial State Definition (`Init` Operator)

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/ethereum.md

The `Init` operator in TLA+ defines the valid initial states of the system. It sets the starting values for key variables: `balanceOf` is initialized as a function mapping addresses to natural numbers, `allowance` as a function mapping all address pairs to zero, `pendingTransactions` as an empty set, `nextTxId` to zero, and `lastTx` as a specific record indicating no prior transaction.

```tla
Init ==
    \* every address has a non-negative number of tokens
    /\ balanceOf \in [ADDRESSES -> Nat]
    \* no account is allowed to withdraw from another account
    /\ allowance = [ pair \in ADDRESSES \X ADDRESSES |-> 0 ]
    \* no pending transactions
    /\ pendingTransactions = {}
    /\ nextTxId = 0
    /\ lastTx = [ id |-> 0, tag |-> "None", fail |-> FALSE ]
```

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

### Execute `modelator sample` successfully with model and property

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_sample.md

Demonstrates a successful execution of the `modelator sample` command by providing both a valid model path and a property to check, indicating a successful sampling.

```sh
$ modelator sample --model-path model/Test3.tla --tests ThreeSteps
```

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

### Execute `modelator sample` with trace generation parameters

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_sample.md

Shows a successful execution of `modelator sample` including parameters for controlling trace generation, such as `max_error` and `view`, and confirms the expected number of trace files.

```sh
$ modelator sample --model-path model/Test3.tla --tests ThreeSteps --max_error=3 --view=ThreeSteps
```

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

### Reset Modelator Environment

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_constants.md

Resets the Modelator environment, ensuring no model is currently loaded and clearing any previous state before starting new tests.

```sh
$ modelator reset
```

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

### Display Modelator Sample Command Help

Source: https://github.com/informalsystems/modelator/blob/dev/README.md

This command provides detailed options and usage for the `sample` subcommand. The `sample` command is used to generate specific model behaviors based on a TLA+ predicate, allowing for targeted behavior generation.

```Shell
modelator sample --help
```

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

### Resetting Modelator State

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_load_with_config.md

Demonstrates how to clear any previously loaded models or configurations in Modelator, ensuring a clean slate for new operations before starting a test sequence.

```sh
$ modelator reset
...
```

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

### Detailed Analysis of AliceSend Action in TLA+

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/hello_world.md

This snippet re-presents the `AliceSend(m)` action to illustrate its detailed conditions for being true. It requires that message `m` is not currently in Alice's outbox, and that in the next state, both `alices_outbox` and `network` include `m`, while `bobs_mood` and `bobs_inbox` remain unchanged.

```tla
AliceSend(m) == 
    /\ m \notin alices_outbox
    /\ alices_outbox' = alices_outbox \union {m}
    /\ network' = network \union {m}
    /\ UNCHANGED <<bobs_mood, bobs_inbox>>
```

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

### Reset Modelator State

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_extra_args.md

Ensures no model is currently loaded in Modelator, providing a clean slate for subsequent operations. This is often used as a setup or teardown step in testing.

```sh
$ modelator reset
```

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

### Download TLC Model Checker JAR

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tutorial.md

This shell command uses `curl` to download the `tla2tools.jar` file, which is the TLC model checker, from its official GitHub releases page. This JAR is essential for running TLA+ models.

```Shell
tlaurl=https://github.com/tlaplus/tlaplus/releases/download/v1.7.1/tla2tools.jar;
curl -LO $tlaurl;
```

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

### Download Apalache Model Checker ZIP

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/tutorial.md

This shell command uses `curl` to download the `apalache-v0.17.5.zip` archive, containing the Apalache model checker, from its official GitHub releases page. Users need to unzip this and move the JAR file to their working directory for use.

```Shell
apalacheurl=https://github.com/informalsystems/apalache/releases/download/v0.17.5/apalache-v0.17.5.zip;
curl -LO $apalacheurl;
```

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

### Simulate with Custom Trace Parameters

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_simulate.md

Prepares the environment by removing any previous trace directories and then runs the `simulate` command. It specifies the maximum number of traces (`--max-trace`), their length (`--length`), and an output directory (`--traces-dir`) for the generated simulation traces.

```sh
$ rm -r test_tracesXX || true
```

```sh
$ modelator simulate --model-path model/Test1.tla --max-trace 4 --length 3 --traces-dir test_tracesXX
```

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

### Execute `modelator sample` without arguments

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_sample.md

Demonstrates that running the `modelator sample` command without specifying a model or a property to check results in an error.

```sh
$ modelator sample
```

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

### Annotating TLA+ Operators

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/typechecking.md

Illustrates how to specify the type signature of a TLA+ operator using Apalache's type annotations. The example shows an operator `AliceSend(m)` annotated as `(Str) => Bool`, indicating it takes a string and returns a boolean.

```tla
\* @type: (Str) => Bool;
AliceSend(m) == 
    /\ m \notin alices_outbox
    /\ alices_outbox' = alices_outbox \union {m}
    /\ network' = network \union {m}
    /\ UNCHANGED <<bobs_mood, bobs_inbox>
```

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

### TLC Configuration for NothingUnexpectedInNetwork Invariant Check

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/hello_world.md

This TLC configuration file specifies the initial state (`Init`), the next state relation (`Next`), and declares `NothingUnexpectedInNetwork` as an invariant to be checked by the TLC model checker.

```tla
INIT Init
NEXT Next

INVARIANTS
NothingUnexpectedInNetwork
```

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

### Annotating TLA+ State Variables

Source: https://github.com/informalsystems/modelator/blob/dev/jekyll/docs/tla_basics_tutorials/typechecking.md

Demonstrates how to apply type annotations to TLA+ state variables using Apalache's `\* @type:` comments. Examples include `Set(Str)`, `Str`, and `Seq(Str)` for different data structures.

```tla
VARIABLES
    \* @type: Set(Str);
    alices_outbox,
    \* @type: Set(Str);
    network,
    \* @type: Str;
    bobs_mood,
    \* @type: Seq(Str);
    bobs_inbox
```

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

### Display Modelator CLI Main Help

Source: https://github.com/informalsystems/modelator/blob/dev/README.md

This command shows the main help message for the Modelator command-line interface. It lists all available top-level commands and provides a general overview of their usage, serving as a quick reference for users.

```Shell
modelator --help
```

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

### Execute `modelator sample` with non-existent config file

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_sample.md

Illustrates the error handling of `modelator sample` when an invalid or non-existent configuration file path is provided, resulting in a 'config file not found' error.

```sh
$ modelator sample --config-path non-existing-file
```

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

### Displaying Loaded Model and Configuration Information

Source: https://github.com/informalsystems/modelator/blob/dev/tests/cli/test_load_with_config.md

Illustrates how to use the `info` command to inspect the details of the currently loaded TLA+ model and its associated configuration. This includes constants, invariants, variables, operators, and file paths, providing a comprehensive overview.

```sh
$ modelator info
Model:
- constants: {}
...
- init: Init
- model_path: model/Test1.tla
- module_name: Test1
- monitors: []
- next: Next
- operators: ['Init', 'InitB', 'Next', 'Inv', 'InvB', 'InvC']
- variables: ['x']
Config at model/Test1.config.toml:
- config_file_path: None
- constants: {}
- init: Init
- invariants: ['Inv']
- next: Next
- params: {'cinit': None, 'config': None, 'length': 5, 'max_error': None, 'no_deadlock': True, 'view': None}
- tests: []
- traces_dir: traces/Test1
```