Skip to content

Commit

Permalink
Merge branch 'main' into strip-startup-error-stacktraces
Browse files Browse the repository at this point in the history
  • Loading branch information
apalache-bot authored Jan 30, 2024
2 parents 0b7bcb9 + 61bb5d3 commit aa56d62
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion docs/src/adr/018adr-inlining.md
Original file line number Diff line number Diff line change
Expand Up @@ -122,7 +122,7 @@ Knowing that we must perform (1) at some point, what remains is to decide whethe
Additionally, if we do isolate inlining to a separate pass, we can choose whether or not to perform (2).

1. Perform no inlining in preprocessing and inline only as needed in the rewriting rules.
- Pros: Spec intermediate output remains small, since inlining increases the size of the specificaiton
- Pros: Spec intermediate output remains small, since inlining increases the size of the specification
- Cons:
- Fewer optimizations can be applied, as some are only applicable to the syntactic forms obtained after inlining (e.g. `ConstSimplifier` can simplify `IF TRUE THEN a ELSE b`, but not `IF p THEN a ELSE b`)
- Rewriting rules for different encodings have to deal with operators in their generality.
Expand Down
2 changes: 1 addition & 1 deletion docs/src/tutorials/trail-tips.md
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ invariant](../apalache/principles/invariants.md#action-invariants):
```

Our version of `NextFast` is quite concise and it uses the good parts of
TLA+. However, new TLA+ users would probably write it differenty. Below you
TLA+. However, new TLA+ users would probably write it differently. Below you
can see the version that is more likely to be written by a specification
writer who has good experience in software engineering:

Expand Down

0 comments on commit aa56d62

Please sign in to comment.