### Python Dictionary Keys Example

Source: https://apalache-mc.org/docs/print.html

Shows how to get the keys of a Python dictionary, which correspond to the domain of a function.

```python
f = {x: 2 * x for x in range(1, 4)}
f.keys()
```

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

### Construct a Tuple in TLA+ (Example)

Source: https://apalache-mc.org/docs/lang/tuples

An example of constructing a tuple with string and integer elements.

```TLA+
<<"Printer", 631>>
```

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

### Generate Example for Test Execution

Source: https://apalache-mc.org/docs/print.html

Command to generate an example of a test execution trace. This is analogous to generating a counterexample when an error is found.

```bash
apalache example ChangRobertsTyped_Test.tla TestExec_n0_n1
```

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

### ITF Parameters Example

Source: https://apalache-mc.org/docs/adr/015adr-trace.html

Example of the optional 'params' field, which lists names that must be set in the initial state, similar to TLA+ CONSTANTS.

```json
  "params": [ "Missionaries", "Cannibals" ]
```

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

### Apalache Trace Output Example

Source: https://apalache-mc.org/docs/print.html

Example of the console output after running Apalache for tracing. Indicates successful trace generation.

```text
__
...
Constructing an example run                                       I@16:06:59.450
Check the trace in: <PATH>/example0.tla, ... I@16:06:59.563
The outcome is: NoError                                           I@16:06:59.571
Trace successfully generated.   

```

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

### TLA+ Cartesian Product Example

Source: https://apalache-mc.org/docs/print.html

Example demonstrating the Cartesian product of a set of strings and a range of integers in TLA+.

```tla
  { "A", "B", "C" } \X (1..65535)
    \* A set of tuples. Each tuple has two fields:
    \*   - field 1 has the value from the set { "A", "B", "C" }, and
    \*   - field 2 has the value from the set 1..65535.

```

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

### Generate Example Execution TLA+ File

Source: https://apalache-mc.org/docs/adr/006rfc-unit-testing.html

Command to generate a TLA+ description of an example execution trace that satisfies a test. This complements counterexample generation.

```bash
__
apalache example ChangRobertsTyped_Test.tla TestExec_n0_n1


```

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

### Python Set Construction Examples

Source: https://apalache-mc.org/docs/lang/sets.html

Equivalent set construction examples in Python, demonstrating frozensets for nested sets and handling of mixed types.

```Python
>>> {1, 2, 3}
{1, 2, 3}
>>> {frozenset({2, 3}), frozenset({1, 2})}
{frozenset({2, 3}), frozenset({1, 2})}
>>> {False, 1}
{False, 1}
```

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

### Example JSON Serialization of NameEx with Source

Source: https://apalache-mc.org/docs/adr/005adr-json.html

A complete example of a NameEx serialization including its name, type, and detailed source location information.

```json
{
  "kind" : "NameEx",
  "type" : "Int",
  "name" : "myName",
  "source": {
    "filename" : "MyModule.tla",
    "from" : {
      "line" : 3,
      "column" : 5
    },
    "to" : {
      "line" : 3,
      "column" : 10
    }
  }
}
```

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

### Example Trace Output

Source: https://apalache-mc.org/docs/adr/023adr-trace-evaluation.html

This is an example of the output seen after running a trace evaluation. It indicates the success of the trace generation and the outcome.

```text
__
... 
Constructing an example run                                       I@16:06:59.450
Check the trace in: <PATH>/example0.tla, ... I@16:06:59.563
The outcome is: NoError                                           I@16:06:59.571
Trace successfully generated.   

```

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

### Set of Functions Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a set containing functions. Each function maps a pair of integers to an integer.

```plaintext
F is a set of functions from a pair of integers to an integer. Its type is `Set(<<Int, Int>> -> Int)`.
```

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

### FunAsSeq TLA+ Examples

Source: https://apalache-mc.org/docs/print.html

Demonstrates the usage of FunAsSeq with different inputs in TLA+. Note that some examples may result in type errors or be undefined in Apalache.

```tla
__
Head([ x \in 1..5 |-> x * x ])                \* 1 in TLC, type error in Apalache
FunAsSeq([ x \in 1..5 |-> x * x ], 3, 3)      \* <<1,4,9>>
Head(FunAsSeq([ x \in 1..5 |-> x * x ], 3, 3)) \* 1
FunAsSeq(<<1,2,3>>, 3, 3)                     \* <<1,2,3>> in TLC, type error in Apalache
FunAsSeq([ x \in {0,42} |-> x * x ], 3, 3)    \* UNDEFINED
```

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

### Transition Filter Regex Example

Source: https://apalache-mc.org/docs/print.html

An example of a regular expression for the search.transitionFilter option, specifying which symbolic transitions to choose at each step.

```regex
search.transitionFilter=(0->0|1->5|2->(2|3)|[3-9]->.*|[1-9][0-9]+->.*)
```

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

### TLA+ Remainder Examples

Source: https://apalache-mc.org/docs/print.html

Shows TLA+ remainder operator (%) examples for different sign combinations, as defined by the property a = b * (a \div b) + c.

```tla
100  % 3      * 1
  -100 % (-3)   * 2
  100  % (-3)   * 1
  -100 % 3      * 2
```

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

### SMT Array Operations Example

Source: https://apalache-mc.org/docs/adr/011adr-smt-arrays.html

Illustrates the use of SMT array operations (store, select) and the importance of managing push/pop contexts for SSA assignments of sets. This example highlights how nested push/pop operations affect the scope of array modifications and subsequent selections.

```smt
(assert (= set_0 ((as const (Array Int Bool)) false)))
(assert (= set_1 (store set_0 5 true)))
(push)
(assert (= set_2 (store set_1 6 true)))
(push)
(assert (= set_3 (store set_2 7 true)))
(assert (= (select set_3 7) true))
(pop 2)
(assert (= (select set_1 7) false)) ; Without the list we would query set_3 here
```

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

### Example of Seq Operator Usage

Source: https://apalache-mc.org/docs/lang/sequences.html

Illustrates the output of Seq({1, 2, 3}), showing the infinite set of all finite sequences that can be formed using elements 1, 2, and 3. This example is conceptual as the set is infinite.

```tla
__
  Seq({1, 2, 3})
    \* The infinite set
      { <<>>, 
        <<1>>, <<2>>, <<3>>,
        <<1, 1>>, <<1, 2>>, <<1, 3>>,
            <<2, 1>>, <<2, 2>>, <<2, 3>>, <<3, 1>>, <<3, 2>>, <<3, 3>>
        ...
      }

```

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

### Expand TLA+ Examples

Source: https://apalache-mc.org/docs/print.html

Shows examples of the Expand operator in TLA+. It highlights cases that work in TLC but result in errors in Apalache, such as expanding a non-set or a set not of the expected form.

```tla
__
Expand( SUBSET {1,2} ) \* {{},{1},{2},{1,2}}
Expand( {1,2} )        \* {1,2} in TLC, error in Apalache
Expand( 1 )            \* 1 in TLC, type error in Apalache
```

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

### Example of Iterative State Computation

Source: https://apalache-mc.org/docs/tutorials/symbmc.html

Provides a concrete example of a specification that allows for iterative computation of states. The 'Init' and 'Next' clauses demonstrate how variables are constrained and updated, enabling model checking.

```tla
__
VARIABLE x,y

Init == /\ x \in 1..0
        /\ y \in { k \in 1..10, k > x }

Next == \/ /\ x > 5
           /\ x' = x - 1
           /\ y' = x' + 1
        \/ /\ x <= 5
           /\ y' = 5 - x
           /\ x' = x + y'


```

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

### Record Type Example (Type System 1)

Source: https://apalache-mc.org/docs/print.html

Example of a record type with fields 'a' (Int) and 'b' (Str). This syntax is specific to Type System 1 and will be updated in Type System 1.2.

```plaintext
r is a record that has the fields `a` and `b`, where `a` is an integer and `b` is a string. Its type is `[a: Int, b: Str]`.
```

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

### Basic PureConfig Usage Example

Source: https://apalache-mc.org/docs/print.html

Demonstrates defining configuration case classes with default values and loading them from multiple sources with fallback mechanisms. Includes overriding configurations with CLI arguments.

```scala
import pureconfig._
import pureconfig.generic.auto._

// Setting a defaul value
case class Port(number: Int = 8080) extends AnyVal

sealed trait SmtEncoding
case class Arrays extends SmtEncoding
case class OOPSLA19 extends SmtEncoding

case class ApalacheConfig(
  runDir: Option[Path] = None,
  serverPort: Port = Port(),
  writeIntermediate: Boolean = false,
  profiling: Boolean = false,
  outDir: Path = Path("."),
  smtEncding: SmtEncoding = OOPSLA19,
)

case classs ExampleUseOfConfigs() = {
  val cli = CliParseResults()
  val localConfig = ConfigSource.file(Path.cwd.resolve(".aplache.config"))
  val globalConfig = ConfigSource.file(ApalacheHome.resolve("apalache.config"))
  val loadedConfig: ConfigReader.Result[ApalacheConfig] = globalConfig
    .withFallback(localConfig)
    .load[ApalacheConfig]

  // Finally, override with CLI arguments
  // Unfortunatley, I've not found a robust way to automate this yet
  val config = loadedConfig.copy(
    runDir = cli.runDir.getOrElse(loadedConfig.runDir),
    serverPort = cli.runDir.getOrElse(loadedConfig.serverPort),
    // etc..
  )

}
```

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

### Apalache Lasso Detection Example

Source: https://apalache-mc.org/docs/tutorials/temporal-properties.html

Illustrates state transitions and auxiliary variable values used by Apalache to identify loops in counterexamples. Observe `__loop_InLoop` to pinpoint the start of the loop and `__loop_` variables for state values within the loop.

```apalache
(* State0 ==
    ...
    /\ __loop_InLoop = FALSE
    ...
    /\ __loop_isGreen = FALSE
    /\ __loop_requestedGreen = FALSE
    ...
    /\ isGreen = FALSE
    /\ requestedGreen = FALSE *)

(* State1 ==
    ...
    /\ __loop_InLoop = FALSE
    ...
    /\ __loop_isGreen = FALSE
    /\ __loop_requestedGreen = FALSE
    ...
    /\ isGreen = FALSE
    /\ requestedGreen = TRUE *)

(* State2 ==
    ...
    /\ __loop_InLoop = FALSE
    ...
    /\ __loop_isGreen = FALSE
    /\ __loop_requestedGreen = FALSE
    ...
    /\ isGreen = FALSE
    /\ requestedGreen = TRUE *)

(* State3 ==
    ...
    /\ __loop_InLoop = TRUE
    ...
    /\ __loop_isGreen = FALSE
    /\ __loop_requestedGreen = TRUE
    ...
    /\ isGreen = FALSE
    /\ requestedGreen = TRUE *)
```

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

### Load and Override Configuration with PureConfig and CLI

Source: https://apalache-mc.org/docs/adr/013adr-configuration.html

Demonstrates loading configuration from multiple file sources (global and local) and then overriding specific values with CLI arguments. This example highlights the need for a thin abstraction to ensure CLI arguments take precedence.

```scala
case classs ExampleUseOfConfigs() = {
  val cli = CliParseResults()
  val localConfig = ConfigSource.file(Path.cwd.resolve(".aplache.config"))
  val globalConfig = ConfigSource.file(ApalacheHome.resolve("apalache.config"))
  val loadedConfig: ConfigReader.Result[ApalacheConfig] = globalConfig
    .withFallback(localConfig)
    .load[ApalacheConfig]

  // Finally, override with CLI arguments
  // Unfortunatley, I've not found a robust way to automate this yet
  val config = loadedConfig.copy(
    runDir = cli.runDir.getOrElse(loadedConfig.runDir),
    serverPort = cli.runDir.getOrElse(loadedConfig.serverPort),
    // etc..
  )

}

```

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

### Command-line Tuning Options

Source: https://apalache-mc.org/docs/print.html

Demonstrates how to pass tuning options directly via the command line using the --tuning-options flag.

```bash
--tuning-options=key1=val1
--tuning-options=key1=val1:key2=val2
```

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

### Integer Type Example

Source: https://apalache-mc.org/docs/print.html

Example of an integer variable declaration and its type.

```plaintext
x is an integer. Its type is `Int`.
```

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

### Passing Tuning Options via Command-Line

Source: https://apalache-mc.org/docs/apalache/tuning.html

Demonstrates the two ways to pass tuning options: using a properties file or directly via the --tuning-options flag. The latter supports multiple key-value pairs separated by colons.

```bash
--tuning-options-file=my.properties
```

```bash
--tuning-options=key1=val1
```

```bash
--tuning-options=key1=val1:key2=val2
```

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

### Record Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a record type with specific fields and types.

```TLA+
{ a: Int, b: Str }
```

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

### Function Application Examples

Source: https://apalache-mc.org/docs/adr/011adr-smt-arrays.html

Demonstrate function application by selecting values from the SMT array at the specified index. Accessing outside the domain yields an unspecified result.

```smt
(assert (= (select finSucc_3 tuple_with_1) 2)) ; SAT
(assert (= (select finSucc_3 tuple_with_2) 3)) ; SAT
(assert (= (select finSucc_3 tuple_with_3) 4)) ; SAT

(declare-const tuple_with_4 Tuple_Int) ; <4>
(assert (= (select finSucc_3 tuple_with_4) 16)) ; SAT

```

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

### Row Type for Variant Example

Source: https://apalache-mc.org/docs/print.html

Example of a row type that can define the structure for a parameterized variant.

```TLA+
(| A: Int | B: Str |)
```

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

### TransEx.apply

Source: https://apalache-mc.org/docs/adr/010rfc-transition-explorer.html

Creates a transition explorer by establishing a connection and a running session. The channel is managed by the gRPC framework.

```APIDOC
## TransEx.apply

### Description
Establishes the connection and a running session for the transition explorer. The channel is managed by the gRPC framework.

### Method
`apply(channel: Channel): TransEx`

### Parameters
#### Path Parameters
- **channel** (Channel) - Description: The gRPC channel to establish the connection.
```

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

### TLA+ Test Action Example

Source: https://apalache-mc.org/docs/print.html

This snippet shows a TLA+ test action with preconditions and postconditions, demonstrating how to execute an action and ensure certain assertions hold.

```tla
__
* Execute the action under test.
* Note that we decouple Assert_n0 from TestAction_n0.
* The reason is that we always assume that TestAction_n0 always holds,
* whereas we may want to see Assert_n0 violated.
*
* @require(ConstInit)
* @require(TypeOK)
* @ensure(Assert_n0)
* @testAction
TestAction_n0 ==
    \E self \in Node:
        n0(self)


```

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

### Function Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a function type where the function takes an integer and returns an integer.

```plaintext
f is a function from an integer to an integer. Its type is `Int -> Int`.
```

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

### Install sbt on macOS with Homebrew

Source: https://apalache-mc.org/docs/apalache/installation/source.html

Use this command to install sbt on macOS using Homebrew.

```bash
brew install sbt
```

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

### TLA+ Specification Example

Source: https://apalache-mc.org/docs/adr/003adr-trex.html

This is a sample TLA+ specification used to demonstrate interaction with the Transition Executor. It includes constants, variables, and definitions for initialization and transitions.

```tlaplus
------------------ MODULE Test ------------------
EXTENDS Integers
CONSTANT N
VARIABLES x

ConstInit ==
  N > 0

Init$0 ==
  x = 10

Next$0 ==
  x < 0 /\ x' = x + N

Next$1 ==
  x >= 0 /\ x' = x - N

Inv ==
  x >= 0

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

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

### Install sbt on Arch Linux

Source: https://apalache-mc.org/docs/apalache/installation/source.html

Use this command to install sbt on Arch Linux systems.

```bash
sudo pacman -Syu sbt
```

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

### Row Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a row type used to define the structure of additional fields in a record.

```TLA+
(| f: Bool | g: Set(Int) |)
```

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

### FunAsSeq Python Implementation and Examples

Source: https://apalache-mc.org/docs/print.html

Provides a Python implementation of FunAsSeq and demonstrates its usage with TLA+-like dictionary definitions. Shows how to define bounded functions and use the funAsSeq function.

```python
__
# define a TLA+-like dictionary via a python function
def boundedFn(f, dom):
  return { x: f(x) for x in dom }

# this is how we could define funAsSeq in python
def funAsSeq(f, length, maxLen):
  return [ f.get(i) for i in range(1, min(length, maxLen) + 1) ]

# TLA+: [ x \in 1..5 |-> x * x ]
f = boundedFn(lambda x: x * x, range(1,6))
# TLA+: [ x \in {0, 42} |-> x * x ]
g = boundedFn(lambda x: x * x, {0, 42})
>>> f[1]
1
>>> funAsSeq(f, 3, 3)
[1, 4, 9]
>>> funAsSeq(f, 3, 3)[1]
1
>>> funAsSeq(g, 3, 3)
[None, None, None]
```

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

### Operator Type Example

Source: https://apalache-mc.org/docs/print.html

Example of an operator type that takes an integer and a string as arguments and returns an integer.

```plaintext
Foo is an operator of an integer and of a string that returns an integer. Its type is `(Int, Str) => Int`.
```

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

### TLA+ Type Error Example

Source: https://apalache-mc.org/docs/print.html

Example of a type error reported by Snowcat regarding type incompatibility.

```tla
__
[Queens.tla:35:44-35:61]: The operator IsSolution of type ((Seq(Int)) => Bool) is applied to arguments of incompatible types in IsSolution(queens):
Argument queens should have type Seq(Int) but has type (Int -> Int). E@11:07:53.285
[Queens.tla:35:1-35:63]: Error when computing the type of Solutions

```

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

### Inlining Example: Evaluating GlobalA(1,2)

Source: https://apalache-mc.org/docs/adr/018adr-inlining.html

Demonstrates the inlining process by evaluating the invariant GlobalA(1,2) = 9, showing the application of substitutions.

```TLA+
GlobalA(1,2) = 9 <=> (1 + 2) * (1 + 2) = 9
```

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

### ITF States Array Example

Source: https://apalache-mc.org/docs/adr/015adr-trace.html

Example of the 'states' field, which is an array containing all the state objects in the trace.

```json
  "states": [ <state0>, <state1>, <state2> ]
```

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

### Generated TLA+ Module Example

Source: https://apalache-mc.org/docs/print.html

An example TLA+ module generated by Apalache, defining states and an invariant violation.

```tlaplus
---------------------------- MODULE counterexample ----------------------------

EXTENDS test

(* Constant initialization state *)
ConstInit == TRUE

(* Initial state *)
State0 == A = 1/\ B = 0/\ C = {1}/\ D = FALSE

(* Transition 0 to State1 *)
State1 == A = 4/\ B = 0/\ C = {2}/\ D = TRUE

(* Transition 1 to State2 *)
State2 == A = 9/\ B = 1/\ C = {}/\ D = FALSE

(* Transition 2 to State3 *)
State3 == A = 16/\ B = 1/\ C = {4}/\ D = TRUE

(* Transition 3 to State4 *)
State4 == A = 25/\ B = 1/\ C = {}/\ D = FALSE

(* The following formula holds true in the last state and violates the invariant *)
InvariantViolation == TRUE

================================================================================
(* Created by Apalache on Mon Oct 17 16:06:59 CEST 2022 *)
(* https://github.com/apalache-mc/apalache *)
```

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

### Parameterized Record Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a record type with defined fields and a type variable for additional fields.

```TLA+
{ a: Int, b: Str, c }
```

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

### Infinite Sequence Construction Example

Source: https://apalache-mc.org/docs/print.html

Illustrates the conceptual output of the infinite Seq(S) operator in TLA+.

```TLA+
Seq({1, 2, 3})
    \* The infinite set
      { <<>>, 
        <<1>>, <<2>>, <<3>>,
        <<1, 1>>, <<1, 2>>, <<1, 3>>,
            <<2, 1>>, <<2, 2>>, <<2, 3>>, <<3, 1>>, <<3, 2>>, <<3, 3>>
        ...
      }
```

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

### execution

Source: https://apalache-mc.org/docs/print.html

Retrieves the example of an execution from an initial state up to the current symbolic state. Additional executions can be obtained by asserting constraints that alter the search space.

```APIDOC
## execution

### Description
Retrieves the example of an execution from an initial state up to the current symbolic state. Additional executions can be obtained by asserting constraints that alter the search space.

### Method Signature
```scala
def execution: Either[SatErr, Execution]
```
```

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

### Compound Action Example

Source: https://apalache-mc.org/docs/print.html

This example demonstrates a compound action formed by the disjunction (or) of two other actions, `EventA` and `EventB`.

```tla
__
EventA == ...
EventB == ...
...

Next == \/ EventA
        \/ EventB
```

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

### Invariant Filter Regex Example

Source: https://apalache-mc.org/docs/print.html

An example of a regular expression for the search.invariantFilter option, specifying at which steps invariants should be checked.

```regex
search.invariantFilter=10->.*|15->state0|20->action1
```

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

### Python OR Operator Examples

Source: https://apalache-mc.org/docs/lang/booleans.html

Provides examples of the 'or' operator in Python, demonstrating its truth table for boolean inputs.

```Python
>>> True  or True
True
>>> False or True
True
>>> True  or False
True
>>> False or False
False
```

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

### TLA+ Specification Example

Source: https://apalache-mc.org/docs/print.html

This is a sample TLA+ specification used to demonstrate interaction with TransitionExecutor. It includes constants, variables, and definitions for initialization and next states.

```tla
__
------------- MODULE Test -------------
EXTENDS Integers
CONSTANT N
VARIABLES x

ConstInit ==
  N > 0

Init$0 ==
  x = 10

Next$0 ==
  x < 0 /\ x' = x + N

Next$1 ==
  x >= 0 /\ x' = x - N

Inv ==
  x >= 0

=======================================

```

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

### Instantiate Parameters with OVERRIDE

Source: https://apalache-mc.org/docs/apalache/parameters.html

Extend the base module and use the OVERRIDE prefix to set parameter values. This is an alternative to the INSTANCE approach.

```TLA
---------------------------- MODULE y2k_override ----------------------------
(*
 * One way to instantiate constants for apalache is to use the OVERRIDE prefix. 
 *)
 
EXTENDS y2k

OVERRIDE_BIRTH_YEAR == 80
OVERRIDE_LICENSE_AGE == 18

=============================================================================

```

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

### Variant Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a variant type with two possible shapes, each tagged with a name and associated with a specific type.

```TLA+
A(Int) | B(Bool)
```

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

### MaxChoose Example

Source: https://apalache-mc.org/docs/print.html

Illustrates finding the maximum value in a sequence using CHOOSE with a quantified predicate. This method can be less efficient and may lead to undefined behavior with empty sets.

```TLA+
__
MaxChoose(seq) == 
  LET Range == {seq[i] : i \in DOMAIN seq} 
  IN CHOOSE m \in Range : \forall n \in Range : m >= n
```

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

### Common Apalache Configuration Parameters

Source: https://apalache-mc.org/docs/apalache/config.html

Example of a local configuration file in HOCON format for commonly used parameters. This file can be placed in the project root or specified via the `config-file` argument. Tilde (~) in paths is expanded to the user's home directory.

```hocon
common  {
    # Directory in which to write all log files and records of each run
    out-dir = "${PWD}/_apalache-out"

    # Whether or not to write additional files, that report on intermediate
    # processing steps
    write-intermediate = false

    # Whether or not to write general profiling data into the `out-dir`
    profiling = false

    # Fixed directory into which generated files are written (absent by default)
    # run-dir = ~/my-run-dir
}

```

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

### Set of Integers Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a function type where the function takes a set of integers and returns a set of integers.

```plaintext
f is a function from a set of integers to a set of integers. Its type is `Set(Int) -> Set(Int)`.
```

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

### Informative Counterexample with View Abstraction

Source: https://apalache-mc.org/docs/print.html

An example of a more informative counterexample after applying view abstraction.

```tla
(* Initial state *)
State0 == x = 0

(* Transition 2 to State1 *)
State1 == x = 0

(* Transition 2 to State2 *)
State2 == x = 0

(* Transition 0 to State3 *)
State3 == x = 1

```

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

### TLA+ Specification Example

Source: https://apalache-mc.org/docs/apalache/profiling.html

This is an example TLA+ specification for the powerset module. It is used to demonstrate Apalache's profiling capabilities.

```tla
---------------------------- MODULE powerset ----------------------------
EXTENDS Integers
VARIABLE S

Init ==
    /\ S \in SUBSET (1..50)
    /\ 3 \notin S

Next ==
    /\ \E x \in S:
        S' = S \ {x}
    /\ UNCHANGED S

Inv ==
    3 \notin S
=========================================================================
```

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

### Type Annotation Examples using isType

Source: https://apalache-mc.org/docs/adr/001rfc-types.html

Illustrates how to use the `isType` operator to assert types for variables and operators.

```TLA+
isType("x", "Int")
```

```TLA+
isType("f", "Int -> Int")
```

```TLA+
isType("f", "Set(Int) -> Set(Int))")
```

```TLA+
isType("r", "[a |-> Int, b |-> Str])")
```

```TLA+
isType("f", "Set(<<Int, Int>> -> Int))")
```

```TLA+
isType("Foo", "(Int, Str) => Int")
```

```TLA+
isType("Bar", "((Int, Str) => Int) => Bool")
```

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

### ITF Loop Index Example

Source: https://apalache-mc.org/docs/adr/015adr-trace.html

Example of the optional 'loop' field, specifying the index of the state where the trace loop begins.

```json
  "loop": 1
```

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

### CHOOSE-based Recursion for Min/Max

Source: https://apalache-mc.org/docs/print.html

This specific example shows the 'CHOOSE'-based recursion antipattern applied to implementing min/max operators. It highlights the issues with recursive calls and CHOOSE operations.

```TLA+
__
RECURSIVE min(_)
min(S) == 
  IF S == {}
  THEN Infinity
  ELSE 
    LET e == CHOOSE x \in S: TRUE
    IN LET minOther == min( S \ {e} )
    IN IF e < minOther THEN e ELSE minOther 


```

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

### TLA+ Set Comprehension Example

Source: https://apalache-mc.org/docs/adr/020adr-arenas.html

An example of a TLA+ set comprehension where membership predicate evaluation is delegated to an SMT solver.

```tla
__
{
  x \in 1..100:
    \E y \in 1..10:
      y * y = x
}
```

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

### Example: Non-deterministic Next state transition

Source: https://apalache-mc.org/docs/print.html

Demonstrates a Next state transition with non-determinism where \E i \in Int: i > x /\ x' = i. TLC would fail due to infinite choices, but this evaluation method allows for step-by-step analysis.

```TLA+
__
VARIABLE x
Init == x = 0
Next ==
  \E i \in Int:
    i > x /\ x' = i
```

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

### TLA+ Function Constructor Examples

Source: https://apalache-mc.org/docs/lang/functions.html

Demonstrates various ways to define functions using the TLA+ constructor, including single-variable, multi-variable, and nested functions.

```tla
[ x \in 1..3 |-> 2 * x ]  \* a function that maps 1, 2, 3 to 2, 4, 6
```

```tla
[ x, y \in 1..3 |-> x * y ]
    \* a function that maps <<1, 1>>, <<1, 2>>, <<1, 3>>, ..., <<2, 3>>, <<3, 3>>
    \* to 1, 2, 3, ..., 6, 9
```

```tla
[ <<x, y>> \in (1..3) \X (4..6) |-> x + y ]
    \* a function that maps <<1, 4>>, <<1, 5>>, <<1, 6>>, ..., <<2, 6>>, <<3, 6>>
    \* to 5, 6, 7, ..., 8, 9
```

```tla
[ n \in 1..3 |->
      [ i \in 1..n |-> n + i ]]
    \* a function that maps a number n from 1 to 3
    \* to a function from 1..n to n + i. Like an array of arrays.
```

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

### Polymorphic Operator Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a polymorphic operator type that accepts two arguments of the same type and returns a value of that same type.

```plaintext
Baz is a polymorphic operator that takes two arguments of the same type and returns a value of the type equal to the types of its arguments. Its type is `(a, a) => a`.
```

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

### Higher-Order Operator Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a higher-order operator type. It takes a function (Int, Str) => Int and returns a Bool.

```plaintext
Bar is a higher-order operator that takes an operator that takes an integer and a string and returns an integer, and returns a Boolean. Its type is `((Int, Str) => Int) => Bool`.
```

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

### Example Evaluation Steps

Source: https://apalache-mc.org/docs/print.html

Illustrates three possible outcomes when evaluating the non-deterministic Next state transition using GUESS Int. The evaluation can succeed, fail, or halt based on the guessed value.

```TLA+
__
1. (GUESS Int) returns 10. (LET i == 10 IN i > x /\ x' = i) is TRUE, x' is assigned 10.
2. (GUESS Int) returns 0. (LET i == 0 IN i > x /\ x' = i) is FALSE. Halt.
3. (GUESS Int) returns -20. (LET i == -20 IN i > x /\ x' = i) is FALSE. Halt.
```

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

### Example: Rewritten Message Set Definition

Source: https://apalache-mc.org/docs/idiomatic/003record-sets.html

The rewritten version of the previous example using the new record-based structure for message sets.

```TLA+
Messages == [ t1: [x:{1,2,3}], t2: [y:{"a","b", "c"}] ]
```

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

### TLA+ Record Example

Source: https://apalache-mc.org/docs/adr/014adr-precise-records.html

An example of a TLA+ record set that cannot fit into a single plain record type, necessitating the use of variants.

```TLA+
__
  { [ tag |-> "1a", bal |-> 3 ], [ tag |-> "2a", bal |-> 4, val |-> 0 ] }
```

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

### TLA+ Specification Example

Source: https://apalache-mc.org/docs/print.html

This is a sample TLA+ specification used to demonstrate Apalache's counterexample generation.

```tla
---- MODULE View2 ----
EXTENDS Integers
VARIABLES
    * @type: Int;
    x

Init ==
  x = 0

A ==
  x' = x + 1

B ==
  x' = x - 1

C ==
  x' = x

Next ==
  A \/ B \/ C

Inv ==
  x = 0


```

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

### ITF Variables Definition Example

Source: https://apalache-mc.org/docs/adr/015adr-trace.html

Example of the 'vars' field, which specifies the names of variables that must be defined in every state of the trace.

```json
  "vars": [ "bank_of_boat", "who_is_on_bank" ]
```

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

### TLA+ Integer Division Examples

Source: https://apalache-mc.org/docs/print.html

Illustrates TLA+ integer division for various sign combinations, matching TLC's behavior.

```tla
100  \div   3   *  33
  (-100) \div   3   * -34
    100  \div (-3)  * -34 in TLC
  (-100) \div (-3)  *  33 in TLC
```

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

### Parameterized Variant Type Example

Source: https://apalache-mc.org/docs/print.html

Example of a variant type whose structure is entirely defined by a type variable, which must be of the 'row' kind.

```TLA+
Variant(b)
```

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

### ConstCardinality Operator Examples

Source: https://apalache-mc.org/docs/print.html

Examples demonstrating the usage and behavior of the ConstCardinality operator. Note that manual use is discouraged and may lead to errors.

```TLA+
Skolem( \E x \in {1,2}: x = 1 ) \* TRUE
```

```TLC
Skolem( 1 ) \* 1 in TLC, type error in Apalache
```

```TLC
Skolem( TRUE ) \* TRUE in TLC, error in Apalache
```

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

### Generate Example TLA+ File

Source: https://apalache-mc.org/docs/adr/006rfc-unit-testing.html

Command to generate a TLA+ description of states that satisfy a given test action. This is useful for understanding passing test cases.

```bash
__
apalache example ChangRobertsTyped_Test.tla TestAction_n0


```

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

### TLA+ Module Example

Source: https://apalache-mc.org/docs/tutorials/symbmc.html

This TLA+ code defines variables, initial conditions, and next-state relations for a system. It illustrates how different range sizes in 'Next' relations can impact the state space, even if the invariant violation is found early.

```tlaplus
VARIABLE 
  * @type: Int;
  x

Init == x = 1
Next1 == x' \in 1..9
Next2 == x' \in 1..999999999999

Inv == x < 5

```

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

### Explicit State Computation Example

Source: https://apalache-mc.org/docs/print.html

This example illustrates a specification where both S0 and Successors(s) can be computed due to the explicit and iterative nature of variable updates.

```tla
__
VARIABLE x,y

Init == /
        x \in 1..0
        /
        y \in { k \in 1..10, k > x }

Next == \/ /\ x > 5
           /\ x' = x - 1
           /\ y' = x' + 1
        \/ /\ x <= 5
           /\ y' = 5 - x
           /\ x' = x + y'


```