From db471f821721028328b323eab0329e6f006a1fd6 Mon Sep 17 00:00:00 2001
From: Thomas Pani
Date: Fri, 23 Aug 2024 16:11:20 +0200
Subject: [PATCH 01/15] Flush SMT log before (check-sat)
---
.../at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala | 4 +++-
1 file changed, 3 insertions(+), 1 deletion(-)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
index 883ec6bc89..5019b7cac4 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/smt/Z3SolverContext.scala
@@ -486,6 +486,7 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
override def sat(): Boolean = {
log("(check-sat)")
+ flushLogs() // good time to flush
val status = z3solver.check()
log(s";; sat = ${status.name()}")
flushLogs() // good time to flush
@@ -513,11 +514,12 @@ class Z3SolverContext(val config: SolverConfig) extends SolverContext with LazyL
// temporarily, change the timeout
setTimeout(timeoutSec * 1000)
log("(check-sat)")
+ flushLogs() // good time to flush
val status = z3solver.check()
log(s";; sat = ${status.name()}")
+ flushLogs() // good time to flush
// return timeout to maximum
setTimeout(Int.MaxValue)
- flushLogs() // good time to flush
status match {
case Status.SATISFIABLE => Some(true)
case Status.UNSATISFIABLE => Some(false)
From 3c5f240d53e88ba04ff8b0647b058f4d4986f4ae Mon Sep 17 00:00:00 2001
From: Thomas Pani
Date: Fri, 23 Aug 2024 16:12:09 +0200
Subject: [PATCH 02/15] Flush SMT profiling info before (check-sat)
---
.../at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala | 1 +
.../forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala | 1 +
2 files changed, 2 insertions(+)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
index 11539bc03b..3de414aaf6 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/SymbStateRewriterImpl.scala
@@ -563,6 +563,7 @@ class SymbStateRewriterImpl(
}
override def flushStatistics(): Unit = {
+ profilerListener.foreach { _.dumpToFile() }
statListener.locator.writeStats()
}
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala
index 17f23c3a44..3fd7755c52 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/trex/TransitionExecutorImpl.scala
@@ -318,6 +318,7 @@ class TransitionExecutorImpl[ExecCtxT](consts: Set[String], vars: Set[String], c
* timed out or reported *unknown*.
*/
override def sat(timeoutSec: Int): Option[Boolean] = {
+ ctx.rewriter.flushStatistics()
ctx.rewriter.solverContext.satOrTimeout(timeoutSec)
}
From ecec7259b02e81657c9ca8e686bf071c6fc71f3a Mon Sep 17 00:00:00 2001
From: Thomas Pani
Date: Fri, 23 Aug 2024 16:14:42 +0200
Subject: [PATCH 03/15] Update changelog
---
.unreleased/bug-fixes/2962-fix-trunc-smt-log | 1 +
1 file changed, 1 insertion(+)
create mode 100644 .unreleased/bug-fixes/2962-fix-trunc-smt-log
diff --git a/.unreleased/bug-fixes/2962-fix-trunc-smt-log b/.unreleased/bug-fixes/2962-fix-trunc-smt-log
new file mode 100644
index 0000000000..7f0cf369a9
--- /dev/null
+++ b/.unreleased/bug-fixes/2962-fix-trunc-smt-log
@@ -0,0 +1 @@
+Fix truncation of SMT logs, see #2962
From afd4e4ed8f3daa199691787866fc0727cb3a691e Mon Sep 17 00:00:00 2001
From: Thomas Pani
Date: Fri, 23 Aug 2024 20:23:43 +0200
Subject: [PATCH 04/15] Fix link (#2961)
---
README.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/README.md b/README.md
index a1a0daa20e..a238a32b39 100644
--- a/README.md
+++ b/README.md
@@ -156,7 +156,7 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
[apalache benchmarks]: https://github.com/apalache-mc/apalache-tests
[checking inductive invariants]: https://github.com/apalache-mc/apalache-tests/blob/master/results/001indinv-report.md
[bounded model checking]: https://github.com/apalache-mc/apalache-tests/blob/master/results/002bmc-report.md
-[user-manual]: http://apalache-mc.org/apalache/docs/index.html
+[user-manual]: http://apalache-mc.org/docs/index.html
[user-manual-docker]: https://apalache-mc.org/docs/apalache/installation/docker.html
[user-manual-installation]: https://apalache-mc.org/docs/apalache/installation/index.html
[language-manual]: https://apalache-mc.org/docs/lang/index.html
From bbfcc7991f16f0af7263df989fdddbf675b98121 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Fri, 23 Aug 2024 21:06:23 +0200
Subject: [PATCH 05/15] fix links globally
---
CHANGES.md | 4 ++--
CONTRIBUTING.md | 2 +-
docs/README.md | 2 +-
docs/src/adr/002adr-types.md | 4 ++--
docs/src/adr/003adr-trex.md | 2 +-
docs/src/adr/004adr-annotations.md | 2 +-
docs/src/adr/005adr-json.md | 4 ++--
docs/src/adr/011adr-smt-arrays.md | 4 ++--
docs/src/adr/014adr-precise-records.md | 4 ++--
docs/src/adr/015adr-trace.md | 4 ++--
docs/src/adr/023adr-trace-evaluation.md | 2 +-
docs/src/apalache/features.md | 10 +++++-----
docs/src/apalache/principles/apalache-mod.md | 2 +-
docs/src/apalache/principles/assignments.md | 2 +-
docs/src/apalache/running.md | 4 ++--
docs/src/lang/user/top-level-operators.md | 2 +-
docs/src/tutorials/entry-tutorial.md | 2 +-
docs/src/tutorials/pluscal-tutorial.md | 2 +-
.../at/forsyte/apalache/infra/ExceptionAdapter.scala | 2 +-
.../forsyte/apalache/infra/tlc/TlcConfigParser.scala | 2 +-
.../src/main/scala/at/forsyte/apalache/tla/Tool.scala | 2 +-
.../forsyte/apalache/tla/tooling/opt/ConfigCmd.scala | 2 +-
test/tla/Antipatterns.tla | 2 +-
test/tla/MC_ERC20.tla | 2 +-
test/tla/cli-integration-tests.md | 10 +++++-----
.../SmtFreeSymbolicTransitionExtractor.scala | 2 +-
.../tla/bmcmt/config/CheckerExceptionAdapter.scala | 2 +-
.../apalache/tla/bmcmt/rules/IntDotDotRule.scala | 2 +-
.../forsyte/apalache/tla/bmcmt/rules/SubstRule.scala | 2 +-
.../apalache/tla/bmcmt/rules/aux/CherryPick.scala | 2 +-
.../stratifiedRules/base/SubstStratifiedRule.scala | 2 +-
.../io/annotations/parser/CommentPreprocessor.scala | 2 +-
.../scala/at/forsyte/apalache/io/json/TlaToJson.scala | 2 +-
.../apalache/io/lir/ItfCounterexampleWriter.scala | 2 +-
.../apalache/io/lir/TestCounterexampleWriter.scala | 6 +++---
.../apalache/io/lir/TestItfCounterexampleWriter.scala | 4 ++--
.../forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala | 2 +-
.../scala/at/forsyte/apalache/tla/lir/Feature.scala | 2 +-
.../transformations/standard/KeraLanguagePred.scala | 2 +-
.../standard/KeramelizerInputLanguagePred.scala | 2 +-
40 files changed, 58 insertions(+), 58 deletions(-)
diff --git a/CHANGES.md b/CHANGES.md
index c4b2efee68..93824cd5ca 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -317,7 +317,7 @@
### Breaking changes
- Invalid configuration keys found in configuration sources (e.g., `apalache.cfg` files) will now produce a configuration error on load (see #2125).
-- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache.informal.systems/docs/apalache/config.html#file-format-and-supported-parameters. See #2065.
+- The structure of the apalache.cfg has changed. All configuration keys that were previously supported have been moved under the `common` key. You can update your config files by prefixing each key from the previous versions with `commong.key-name`. For an example config file, see https://apalache-mc.org/docs/apalache/config.html#file-format-and-supported-parameters. See #2065.
- Introduce --features=no-rows for the old record syntax and switch to `--features=rows` by default
### Features
@@ -737,7 +737,7 @@
### Documentation
* Restructure and update the Apalache manual:
- https://apalache.informal.systems/docs/index.html
+ https://apalache-mc.org/docs/index.html
## 0.17.5
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index b5c9408177..82992bbb84 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -149,7 +149,7 @@ contributors and maintainers to make sure:
## Dependencies
For setting up the local build, see the [instructions on building from
-source](https://apalache.informal.systems/docs/apalache/installation/source.html).
+source](https://apalache-mc.org/docs/apalache/installation/source.html).
### Environment
diff --git a/docs/README.md b/docs/README.md
index 7492cec320..0c69f8728f 100644
--- a/docs/README.md
+++ b/docs/README.md
@@ -3,7 +3,7 @@
The Apalache documentation is written in markdown files in the [./src](./src)
directory and compiled using [mdbook](https://github.com/rust-lang/mdBook).
-To view the documentation, visit https://apalache.informal.systems/docs/.
+To view the documentation, visit https://apalache-mc.org/docs/.
## Building and previewing the documentation
diff --git a/docs/src/adr/002adr-types.md b/docs/src/adr/002adr-types.md
index 9f152a7b67..49686524c1 100644
--- a/docs/src/adr/002adr-types.md
+++ b/docs/src/adr/002adr-types.md
@@ -598,8 +598,8 @@ AtMostOne ==
=============================================================================
```
-[Snowcat tutorial]: https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html
-[Snowcat HOWTO]: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
+[Snowcat tutorial]: https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html
+[Snowcat HOWTO]: https://apalache-mc.org/docs/HOWTOs/howto-write-type-annotations.html
[ADR014]: https://github.com/informalsystems/apalache/blob/main/docs/src/adr/014adr-precise-records.md
[Issue 401]: https://github.com/informalsystems/apalache/issues/401
[Row polymorphism]: https://en.wikipedia.org/wiki/Row_polymorphism
diff --git a/docs/src/adr/003adr-trex.md b/docs/src/adr/003adr-trex.md
index 13ff622770..527c72b38e 100644
--- a/docs/src/adr/003adr-trex.md
+++ b/docs/src/adr/003adr-trex.md
@@ -116,4 +116,4 @@ explain how the parallel checker is working. This is a subject to another ADR.
To sum up, this layer is offering you a nice abstraction to write different
model checking strategies.
-[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html
+[KerA+]: https://apalache-mc.org/docs/apalache/kera.html
diff --git a/docs/src/adr/004adr-annotations.md b/docs/src/adr/004adr-annotations.md
index 0986b8a60c..5dd6af1057 100644
--- a/docs/src/adr/004adr-annotations.md
+++ b/docs/src/adr/004adr-annotations.md
@@ -158,7 +158,7 @@ This is done because the SANY parser is pruning the linefeed character `\n`,
so it would be otherwise impossible to find the end of an annotation.
-[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html
[JavaTokenParsers]: https://www.scala-lang.org/api/2.12.2/scala-parser-combinators/scala/util/parsing/combinator/JavaTokenParsers.html
[Java identifier]: https://docs.oracle.com/javase/specs/jls/se7/html/jls-3.html#jls-3.8
diff --git a/docs/src/adr/005adr-json.md b/docs/src/adr/005adr-json.md
index 786dfd3b56..17157286b3 100644
--- a/docs/src/adr/005adr-json.md
+++ b/docs/src/adr/005adr-json.md
@@ -201,9 +201,9 @@ In general, for any given `oper: TlaOper` of `OperEx`, the value of the `oper` f
The implementation of the serialization can be found in the class
`at.forsyte.apalache.io.json.TlaToJson` of the module `tla-import`, see [TlaToJson][].
-[ADR-002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR-002]: https://apalache-mc.org/docs/adr/002adr-types.html
-[ADR-004]: https://apalache.informal.systems/docs/adr/004adr-annotations.html
+[ADR-004]: https://apalache-mc.org/docs/adr/004adr-annotations.html
[TlaToJson]: https://github.com/informalsystems/apalache/blob/main/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala#L54
[TlaEx]: https://github.com/informalsystems/apalache/blob/main/tlair/src/main/scala/at/forsyte/apalache/tla/lir/TlaEx.scala#L10
diff --git a/docs/src/adr/011adr-smt-arrays.md b/docs/src/adr/011adr-smt-arrays.md
index c5c4106bd6..6e8bd08f20 100644
--- a/docs/src/adr/011adr-smt-arrays.md
+++ b/docs/src/adr/011adr-smt-arrays.md
@@ -308,7 +308,7 @@ The following changes will be made to implement the new encoding of functions:
The use of SMT arrays will be restricted to TLA+ sets and functions for the moment. The encoding of
additional features using SMT arrays, or potentially ADTs, will be left for the future.
-[KerA+]: https://apalache.informal.systems/docs/apalache/kera.html
+[KerA+]: https://apalache-mc.org/docs/apalache/kera.html
[core theory]: http://smtlib.cs.uiowa.edu/theories-Core.shtml
[arrays with extensionality]: http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml
[Z3]: https://github.com/Z3Prover/z3
@@ -316,6 +316,6 @@ additional features using SMT arrays, or potentially ADTs, will be left for the
[Version 2.6]: https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf
[TLA+ Model Checking Made Symbolic]: https://dl.acm.org/doi/10.1145/3360549
[Symbolic Model Checking for TLA+ Made Faster]: https://doi.org/10.1007/978-3-031-30823-9_7
-[model checking parameters]: https://apalache.informal.systems/docs/apalache/running.html#model-checker-command-line-parameters
+[model checking parameters]: https://apalache-mc.org/docs/apalache/running.html#model-checker-command-line-parameters
[represented internally in Z3]: https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arrays
[PR 2027]: https://github.com/informalsystems/apalache/pull/2027
diff --git a/docs/src/adr/014adr-precise-records.md b/docs/src/adr/014adr-precise-records.md
index 31e32e9e95..0878fcf9fa 100644
--- a/docs/src/adr/014adr-precise-records.md
+++ b/docs/src/adr/014adr-precise-records.md
@@ -15,7 +15,7 @@
## 1. Summary
This ADR extends
-[ADR-002](https://apalache.informal.systems/docs/adr/002adr-types.html) on
+[ADR-002](https://apalache-mc.org/docs/adr/002adr-types.html) on
types and type annotations.
Virtually every user of Snowcat has faced the issue of record type checking
@@ -665,7 +665,7 @@ default untyped implementation for the operators.
-[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html
[#401]: https://github.com/informalsystems/apalache/issues/401
[#789]: https://github.com/informalsystems/apalache/discussions/789
[Raft]: https://github.com/ongardie/raft.tla/blob/master/raft.tla
diff --git a/docs/src/adr/015adr-trace.md b/docs/src/adr/015adr-trace.md
index a8831f65bf..498cc323fb 100644
--- a/docs/src/adr/015adr-trace.md
+++ b/docs/src/adr/015adr-trace.md
@@ -467,8 +467,8 @@ write a parser of custom ITF traces. Hence, we have decided to keep only the obj
as the more general of the two representations.
-[ADR005]: https://apalache.informal.systems/docs/adr/005adr-json.html
-[ADR002]: https://apalache.informal.systems/docs/adr/002adr-types.html
+[ADR005]: https://apalache-mc.org/docs/adr/005adr-json.html
+[ADR002]: https://apalache-mc.org/docs/adr/002adr-types.html
[MissionariesAndCannibalsTyped]: https://github.com/informalsystems/apalache/blob/main/test/tla/MissionariesAndCannibalsTyped.tla
[JSON]: https://en.wikipedia.org/wiki/JSON
[RFC7159]: https://datatracker.ietf.org/doc/html/rfc7159.html
diff --git a/docs/src/adr/023adr-trace-evaluation.md b/docs/src/adr/023adr-trace-evaluation.md
index 3ae4cbecb7..77fe1ce54d 100644
--- a/docs/src/adr/023adr-trace-evaluation.md
+++ b/docs/src/adr/023adr-trace-evaluation.md
@@ -137,7 +137,7 @@ and trace `testTrace.json` (length 5, `x=1 -> ... -> x=5`).
{
"name": "ApalacheIR",
"version": "1.0",
- "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
"modules": [
{
"kind": "TlaModule",
diff --git a/docs/src/apalache/features.md b/docs/src/apalache/features.md
index fc14b1b817..047fde2a0b 100644
--- a/docs/src/apalache/features.md
+++ b/docs/src/apalache/features.md
@@ -4,7 +4,7 @@ Here is the list of the TLA+ language features that are currently supported by A
At the moment, Apalache is able to check state invariants, action invariants,
temporal properties, trace invariants, as well as inductive invariants. (See the [page on
-invariants](https://apalache.informal.systems/docs/apalache/principles/invariants.html) in
+invariants](https://apalache-mc.org/docs/apalache/principles/invariants.html) in
the manual.) To check liveness/temporal properties, we employ a [liveness-to-safety][] transformation.
## Language
@@ -66,7 +66,7 @@ replaced with a constant.
#### Records
*Use [type
-annotations](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html)
+annotations](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html)
to help the model checker in finding the right types.* Note that our type
system distinguishes records from general functions.
@@ -81,14 +81,14 @@ system distinguishes records from general functions.
#### Tuples
*Use [type
-annotations](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html)
+annotations](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html)
to help the model checker in finding the right types.* Note that our type
system distinguishes records from general functions.
| Operator | Supported? | Milestone | Comment |
|------------------------|:----------:|:---------:|------------------------------------------------------------------------------------------------------------------------------------------------|
| `e[i]` | ✔ / ✖ | - | Provided that `i` is a constant expression |
-| `<< e1, ..., e_n >>` | ✔ | - | Use a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html) to distinguish between a tuple and a sequence. |
+| `<< e1, ..., e_n >>` | ✔ | - | Use a [type annotation](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html) to distinguish between a tuple and a sequence. |
| `S1 \X ... \X S_n` | ✔ | - | |
| `[ t EXCEPT ![i] = e]` | ✔/✖ | - | Provided that `i` is a constant expression |
@@ -158,7 +158,7 @@ For the moment, the model checker does not differentiate between integers and na
| Operator | Supported? | Milestone | Comment |
|----------------------------------------------------------|:----------:|:---------:|----------------------------------------------------------------------------------------------------------|
-| `<<...>>` | ✔ | | Often needs a [type annotation](https://apalache.informal.systems/docs/tutorials/snowcat-tutorial.html). |
+| `<<...>>` | ✔ | | Often needs a [type annotation](https://apalache-mc.org/docs/tutorials/snowcat-tutorial.html). |
| `Head`, `Tail`, `Len``, `SubSeq`, `Append`, `\o`, `f[e]` | ✔ | - | |
| `EXCEPT` | ✔ | | |
| `SelectSeq` | ✔ | - | Not as efficient, as it could be, see [#1350](https://github.com/informalsystems/apalache/issues/1350). |
diff --git a/docs/src/apalache/principles/apalache-mod.md b/docs/src/apalache/principles/apalache-mod.md
index 2d35d6d7d2..4456ff566c 100644
--- a/docs/src/apalache/principles/apalache-mod.md
+++ b/docs/src/apalache/principles/apalache-mod.md
@@ -9,4 +9,4 @@ See the detailed description of the [Apalache operators][].
[Apalache.tla]: https://github.com/informalsystems/apalache/tree/main/src/tla/Apalache.tla
-[Apalache operators]: https://apalache.informal.systems/docs/lang/apalache-operators.html
+[Apalache operators]: https://apalache-mc.org/docs/lang/apalache-operators.html
diff --git a/docs/src/apalache/principles/assignments.md b/docs/src/apalache/principles/assignments.md
index efd5a49f37..7329dda90c 100644
--- a/docs/src/apalache/principles/assignments.md
+++ b/docs/src/apalache/principles/assignments.md
@@ -71,7 +71,7 @@ Apalache reports an error as follows:
...
PASS #9: TransitionFinderPass
To understand the error, [check the
-manual](https://apalache.informal.systems/docs/apalache/principles/assignments.html):
+manual](https://apalache-mc.org/docs/apalache/principles/assignments.html):
Assignment error: No assignments found for: a
It took me 0 days 0 hours 0 min 1 sec
Total time: 1.88 sec
diff --git a/docs/src/apalache/running.md b/docs/src/apalache/running.md
index 8f9bf86999..9a64a9df66 100644
--- a/docs/src/apalache/running.md
+++ b/docs/src/apalache/running.md
@@ -22,7 +22,7 @@ The most important commands are as follows:
the types of all expressions in the parsed specification. It terminates successfully if there are no type errors.
- `simulate` performs all of the operations of `typecheck` and additionally runs the model checker in simulation mode,
- which *randomly* picks a sequence of [actions](https://apalache.informal.systems/docs/apalache/assignments-in-depth.html#slices)
+ which *randomly* picks a sequence of [actions](https://apalache-mc.org/docs/apalache/assignments-in-depth.html#slices)
and checks the invariants for the subset of all executions which only admit actions in the selected order.
It terminates successfully if there are no invariant violations.
This command usually checks randomized symbolic runs much faster than the `check` command.
@@ -32,7 +32,7 @@ The most important commands are as follows:
the length of which does not exceed the value specified by the `--length` parameter.
It terminates successfully if there are no invariant violations.
- - `test` performs all of the operations of `check` in a mode that is designed to [test a single action](https://apalache.informal.systems/docs/adr/006rfc-unit-testing.html#32-testing-actions).
+ - `test` performs all of the operations of `check` in a mode that is designed to [test a single action](https://apalache-mc.org/docs/adr/006rfc-unit-testing.html#32-testing-actions).
## 1. Model checker and simulator command-line parameters
diff --git a/docs/src/lang/user/top-level-operators.md b/docs/src/lang/user/top-level-operators.md
index c9b8649e65..837623c66e 100644
--- a/docs/src/lang/user/top-level-operators.md
+++ b/docs/src/lang/user/top-level-operators.md
@@ -225,5 +225,5 @@ expression to SMT.
[Call by macro expansion]: https://en.wikipedia.org/wiki/Evaluation_strategy#Call_by_macro_expansion
[Alpha conversion]: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B1-conversion
[Beta reduction]: https://en.wikipedia.org/wiki/Lambda_calculus#%CE%B2-reduction
-[Apalache]: https://apalache.informal.systems
+[Apalache]: https://apalache-mc.org
diff --git a/docs/src/tutorials/entry-tutorial.md b/docs/src/tutorials/entry-tutorial.md
index b33c9dae59..7e8c1a8560 100644
--- a/docs/src/tutorials/entry-tutorial.md
+++ b/docs/src/tutorials/entry-tutorial.md
@@ -386,7 +386,7 @@ If it is your first TLA+ specification, you may be surprised by this error:
...
PASS #13: BoundedChecker
This error may show up when CONSTANTS are not initialized.
-Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html
+Check the manual: https://apalache-mc.org/docs/apalache/parameters.html
Input error (see the manual): SubstRule: Variable INPUT_SEQ is not assigned a value
...
```
diff --git a/docs/src/tutorials/pluscal-tutorial.md b/docs/src/tutorials/pluscal-tutorial.md
index 99f9746f37..967724cc3a 100644
--- a/docs/src/tutorials/pluscal-tutorial.md
+++ b/docs/src/tutorials/pluscal-tutorial.md
@@ -276,7 +276,7 @@ or drop us a message on [Zulip chat].
[Issue 1412]: https://github.com/informalsystems/apalache/issues/1412
[open an issue]: https://github.com/informalsystems/apalache/issues
[Tutorial on Snowcat]: ./snowcat-tutorial.md
-[Checking inductive invariants]: https://apalache.informal.systems/docs/apalache/running.html#checking-an-inductive-invariant
+[Checking inductive invariants]: https://apalache-mc.org/docs/apalache/running.html#checking-an-inductive-invariant
[TLA+ Cheatsheet in HTML]: https://mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
[Summary of TLA+]: https://lamport.azurewebsites.net/tla/summary-standalone.pdf
[TLA+ Video Course]: http://lamport.azurewebsites.net/video/videos.html
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala
index af1cde0362..649d83b7b2 100644
--- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala
+++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/ExceptionAdapter.scala
@@ -36,7 +36,7 @@ trait ExceptionAdapter extends LazyLogging {
def toMessage: PartialFunction[Throwable, ErrorMessage] = { case err: OutOfMemoryError =>
logger.error(s"Ran out of heap memory (max JVM memory: ${Runtime.getRuntime.maxMemory})")
logger.error(s"To increase available heap memory, see the manual:")
- logger.error(" [https://apalache.informal.systems/docs/apalache/running.html#supplying-jvm-arguments]")
+ logger.error(" [https://apalache-mc.org/docs/apalache/running.html#supplying-jvm-arguments]")
NormalErrorMessage(s"Ran out of heap memory: ${err.getMessage}")
}
}
diff --git a/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala b/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala
index dc1021df59..3c9d4ebdd2 100644
--- a/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala
+++ b/mod-infra/src/main/scala/at/forsyte/apalache/infra/tlc/TlcConfigParser.scala
@@ -9,7 +9,7 @@ import at.forsyte.apalache.infra.tlc.config.TlcConfig
* href="http://research.microsoft.com/users/lamport/tla/book.html">Specifying Systems, Ch. 14] by Leslie Lamport.
* TLC configuration files have a rich assignment syntax, e.g., one can write a parameter assignment. The syntax
* supported by Apalache is described in [tlc-config].
+ * href="https://apalache-mc.org/docs/apalache/tlc-config.html">tlc-config].
*
* @author
* Igor Konnov
diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
index f3902ddd35..dbe3854f05 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/Tool.scala
@@ -44,7 +44,7 @@ object Tool extends LazyLogging {
// If it is caught here, logging has not been set up yet, so print directly to `Console.err`.
Console.err.println(s"Error: Ran out of heap memory (max JVM memory: ${Runtime.getRuntime.maxMemory})")
Console.err.println(s"To increase available heap memory, see the manual:")
- Console.err.println(" [https://apalache.informal.systems/docs/apalache/running.html#supplying-jvm-arguments]")
+ Console.err.println(" [https://apalache-mc.org/docs/apalache/running.html#supplying-jvm-arguments]")
Console.out.println(s"EXITCODE: ERROR (${ExitCodes.ERROR})")
System.exit(ExitCodes.ERROR)
}
diff --git a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala
index 73dedcf455..37126f8158 100644
--- a/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala
+++ b/mod-tool/src/main/scala/at/forsyte/apalache/tla/tooling/opt/ConfigCmd.scala
@@ -19,7 +19,7 @@ class ConfigCmd extends ApalacheCommand(name = "config", description = "Configur
var submitStats: Option[Boolean] = opt[Option[Boolean]](name = "enable-stats",
description = "Let Apalache submit usage statistics to tlapl.us\n"
- + "(shared with TLC and TLA+ Toolbox)\nSee: https://apalache.informal.systems/docs/apalache/statistics.html")
+ + "(shared with TLC and TLA+ Toolbox)\nSee: https://apalache-mc.org/docs/apalache/statistics.html")
def run() = {
logger.info("Configuring Apalache")
diff --git a/test/tla/Antipatterns.tla b/test/tla/Antipatterns.tla
index 0b5c0f99fe..b8928a23f5 100644
--- a/test/tla/Antipatterns.tla
+++ b/test/tla/Antipatterns.tla
@@ -1,7 +1,7 @@
---- MODULE Antipatterns ----
(* Contains a collection of known-to-be-inefficient Apalache constructs, a.k.a. "antipatterns".
We explain why these constructs are inefficient in
-https://apalache.informal.systems/docs/apalache/antipatterns.html
+https://apalache-mc.org/docs/apalache/antipatterns.html
The purpose of this file is to collect known antipatterns, so we can measure just how
much they affect performance, across various versions of Apalache.
diff --git a/test/tla/MC_ERC20.tla b/test/tla/MC_ERC20.tla
index b1db62fce4..79a30b3b59 100644
--- a/test/tla/MC_ERC20.tla
+++ b/test/tla/MC_ERC20.tla
@@ -4,7 +4,7 @@ EXTENDS Integers, ERC20_typedefs
\* Use the set of three addresses.
\* We are using uninterpreted values, similar to TLC's model values.
-\* See: https://apalache.informal.systems/docs/HOWTOs/uninterpretedTypes.html
+\* See: https://apalache-mc.org/docs/HOWTOs/uninterpretedTypes.html
ADDR == { "Alice_OF_ADDR", "Bob_OF_ADDR", "Eve_OF_ADDR" }
\* Apalache can draw constants from the set of all integers
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index cfa06d6d28..90fd5c9435 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -362,7 +362,7 @@ $ cat output.json | head
{
"name": "ApalacheIR",
"version": "1.0",
- "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
"modules": [
{
"kind": "TlaModule",
@@ -437,7 +437,7 @@ $ cat output.json | head
{
"name": "ApalacheIR",
"version": "1.0",
- "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
"modules": [
{
"kind": "TlaModule",
@@ -1484,7 +1484,7 @@ An occurence of `Seq(S)` should point to an explanation.
```sh
$ apalache-mc check Bug1126.tla | sed 's/[IE]@.*//'
...
-Bug1126.tla:15:14-15:27: unsupported expression: Seq(_) produces an infinite set of unbounded sequences. See: https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs
+Bug1126.tla:15:14-15:27: unsupported expression: Seq(_) produces an infinite set of unbounded sequences. See: https://apalache-mc.org/docs/apalache/known-issues.html#using-seqs
...
EXITCODE: ERROR (75)
```
@@ -2407,7 +2407,7 @@ EXITCODE: OK
### check profiling
Check that the profiler output is produced as explained in
-[Profiling](https://apalache.informal.systems/docs/apalache/profiling.html).
+[Profiling](https://apalache-mc.org/docs/apalache/profiling.html).
```sh
$ apalache-mc check --run-dir=./profile-run-dir --smtprof schroedinger_cat.tla | sed 's/[IEW]@.*//'
@@ -2508,7 +2508,7 @@ EXITCODE: OK
$ apalache-mc check Test669.tla | sed 's/[IEW]@.*//'
...
This error may show up when CONSTANTS are not initialized.
-Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html
+Check the manual: https://apalache-mc.org/docs/apalache/parameters.html
Input error (see the manual): SubstRule: Variable N is not assigned a value
...
EXITCODE: ERROR (255)
diff --git a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala
index 42acd07bbb..fe61cd1edb 100644
--- a/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala
+++ b/tla-assignments/src/main/scala/at/forsyte/apalache/tla/assignments/SmtFreeSymbolicTransitionExtractor.scala
@@ -195,7 +195,7 @@ class SmtFreeSymbolicTransitionExtractor(
}
object SmtFreeSymbolicTransitionExtractor {
- val MANUAL_LINK = "https://apalache.informal.systems/docs/apalache/principles/assignments.html"
+ val MANUAL_LINK = "https://apalache-mc.org/docs/apalache/principles/assignments.html"
def apply(tracker: TransformationTracker, sourceLoc: SourceLocator): SmtFreeSymbolicTransitionExtractor = {
new SmtFreeSymbolicTransitionExtractor(tracker, sourceLoc)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala
index bad9234a93..25bcbce0ce 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala
@@ -42,7 +42,7 @@ class CheckerExceptionAdapter @Inject() (sourceStore: SourceStore, changeListene
case err: AssignmentException =>
logger.info("To understand the error, read the manual:")
- logger.info(" [https://apalache.informal.systems/docs/apalache/principles/assignments.html]")
+ logger.info(" [https://apalache-mc.org/docs/apalache/principles/assignments.html]")
NormalErrorMessage("Assignment error: " + err.getMessage)
case err: OutdatedAnnotationsError =>
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala
index 98542fe710..5ea921c3c1 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/IntDotDotRule.scala
@@ -51,7 +51,7 @@ class IntDotDotRule(@unused rewriter: SymbStateRewriter, intRangeCache: IntRange
case _ =>
throw new NotInKeraError(
- "Expected a constant integer range in [ .. ], found %s. This is a known issue: [https://apalache.informal.systems/docs/apalache/known-issues.html]"
+ "Expected a constant integer range in [ .. ], found %s. This is a known issue: [https://apalache-mc.org/docs/apalache/known-issues.html]"
.format(elems.map(UTFPrinter.apply).mkString("..")), ex)
}
}
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
index dab6a4474d..a56fbc8141 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/SubstRule.scala
@@ -31,7 +31,7 @@ class SubstRule extends RewritingRule with LazyLogging {
state.setRex(cell.toBuilder)
} else {
logger.error("This error may show up when CONSTANTS are not initialized.")
- logger.error("Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html")
+ logger.error("Check the manual: https://apalache-mc.org/docs/apalache/parameters.html")
throw new TlaInputError(s"${getClass.getSimpleName}: Variable $x is not assigned a value")
}
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
index 14076b0089..68843e7b59 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/CherryPick.scala
@@ -283,7 +283,7 @@ class CherryPick(rewriter: SymbStateRewriter) {
case _: IndexOutOfBoundsException =>
// TODO Remove once sound record typing is implemented
val url =
- "https://apalache.informal.systems/docs/apalache/known-issues.html#updating-records-with-excess-fields"
+ "https://apalache-mc.org/docs/apalache/known-issues.html#updating-records-with-excess-fields"
val msg =
s"""|An updated record has more fields than its declared type:
|A record with the inferred type `$thisRecT` has been updated with
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala
index c43c229095..5db8f5b4c8 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/stratifiedRules/base/SubstStratifiedRule.scala
@@ -29,7 +29,7 @@ class SubstStratifiedRule extends StratifiedRuleInterface with LazyLogging {
(startingScope, binding(x))
} else {
logger.error("This error may show up when CONSTANTS are not initialized.")
- logger.error("Check the manual: https://apalache.informal.systems/docs/apalache/parameters.html")
+ logger.error("Check the manual: https://apalache-mc.org/docs/apalache/parameters.html")
throw new TlaInputError(s"${getClass.getSimpleName}: Variable $x is not assigned a value")
}
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala
index 09d5a2e0fb..6bb5543ae7 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/annotations/parser/CommentPreprocessor.scala
@@ -15,7 +15,7 @@ package at.forsyte.apalache.io.annotations.parser
* Perhaps, the first step would be to write a precise grammar for this lexer, instead of write the spaghetti of
* if-then-else expressions, as we have in this preprocessor.
*
- * See the annotations HOWTO: https://apalache.informal.systems/docs/HOWTOs/howto-write-type-annotations.html
+ * See the annotations HOWTO: https://apalache-mc.org/docs/HOWTOs/howto-write-type-annotations.html
*
* @author
* Igor Konnov
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
index fd936fcd77..98df35bf3a 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/json/TlaToJson.scala
@@ -216,7 +216,7 @@ class TlaToJson[T <: JsonRepresentation](
factory.mkObj(
"name" -> "ApalacheIR",
versionFieldName -> JsonVersion.current,
- "description" -> "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ "description" -> "https://apalache-mc.org/docs/adr/005adr-json.html",
"modules" -> factory.fromIterable(moduleJsons),
)
}
diff --git a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala
index 57b9fbf46c..d1fa21b15f 100644
--- a/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala
+++ b/tla-io/src/main/scala/at/forsyte/apalache/io/lir/ItfCounterexampleWriter.scala
@@ -56,7 +56,7 @@ object ItfCounterexampleWriter {
)
)
val descriptions = Map[String, ujson.Value](
- FORMAT_DESCRIPTION_FIELD -> "https://apalache.informal.systems/docs/adr/015adr-trace.html",
+ FORMAT_DESCRIPTION_FIELD -> "https://apalache-mc.org/docs/adr/015adr-trace.html",
DESCRIPTION_FIELD -> "Created by Apalache on %s".format(Calendar.getInstance().getTime),
)
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala
index 0300e299de..9790527c08 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestCounterexampleWriter.scala
@@ -231,7 +231,7 @@ class TestCounterexampleWriter extends AnyFunSuite with TestCounterexampleWriter
"""{
| "name": "ApalacheIR",
| "version": "1.0",
- | "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ | "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
| "modules": [
| {
| "kind": "TlaModule",
@@ -334,7 +334,7 @@ class TestCounterexampleWriter extends AnyFunSuite with TestCounterexampleWriter
"""{
| "name": "ApalacheIR",
| "version": "1.0",
- | "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ | "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
| "modules": [
| {
| "kind": "TlaModule",
@@ -505,7 +505,7 @@ class TestCounterexampleWriter extends AnyFunSuite with TestCounterexampleWriter
"""{
| "name": "ApalacheIR",
| "version": "1.0",
- | "description": "https://apalache.informal.systems/docs/adr/005adr-json.html",
+ | "description": "https://apalache-mc.org/docs/adr/005adr-json.html",
| "modules": [
| {
| "kind": "TlaModule",
diff --git a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala
index de50228e00..2fa7537f00 100644
--- a/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala
+++ b/tla-io/src/test/scala/at/forsyte/apalache/io/lir/TestItfCounterexampleWriter.scala
@@ -84,7 +84,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
s"""{
| "#meta": {
| "format": "ITF",
- | "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html",
+ | "format-description": "https://apalache-mc.org/docs/adr/015adr-trace.html",
| "description": "Created by Apalache"
| },
| "params": [ "N" ],
@@ -180,7 +180,7 @@ class TestItfCounterexampleWriter extends AnyFunSuite {
"""{
| "#meta": {
| "format": "ITF",
- | "format-description": "https://apalache.informal.systems/docs/adr/015adr-trace.html",
+ | "format-description": "https://apalache-mc.org/docs/adr/015adr-trace.html",
| "description": "Created by Apalache"
| },
| "vars": [ "a", "b", "c", "d", "e", "f", "g", "h", "n" ],
diff --git a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
index 780320bf44..2cd404bc53 100644
--- a/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
+++ b/tla-typechecker/src/main/scala/at/forsyte/apalache/tla/typecheck/etc/ToEtcExpr.scala
@@ -898,7 +898,7 @@ class ToEtcExpr(
case OperEx(ApalacheOper.withType, _, annotation) =>
// Met an old type annotation. Warn the user and ignore the annotation.
logger.error("Met an old type annotation: " + annotation)
- logger.error("See: https://apalache.informal.systems/docs/apalache/typechecker-snowcat.html")
+ logger.error("See: https://apalache-mc.org/docs/apalache/typechecker-snowcat.html")
val msg = s"Old Apalache type annotations (predating 0.12.0) are no longer supported"
throw new OutdatedAnnotationsError(msg, ex)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
index b5a804cd35..34908a3d67 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
@@ -24,7 +24,7 @@ case class RowsFeature(
/**
* Enable imprecise record types, see the discussion in ADR-002.
+ * href="https://apalache-mc.org/docs/adr/002adr-types.html#15-discussion">the discussion in ADR-002.
*
* [[ImpreciseRecordsFeature]] is mutually exclusive with [[RowsFeature]]. It is present only for backwards
* compatibility.
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala
index 7ca7451a75..5ce282566a 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeraLanguagePred.scala
@@ -109,7 +109,7 @@ class KeraLanguagePred extends ContextualLanguagePred {
}
object KeraLanguagePred {
- val MANUAL_LINK_SEQ = "https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs"
+ val MANUAL_LINK_SEQ = "https://apalache-mc.org/docs/apalache/known-issues.html#using-seqs"
private val singleton = new KeraLanguagePred
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala
index 5e481b5e01..2938f3b561 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/transformations/standard/KeramelizerInputLanguagePred.scala
@@ -80,7 +80,7 @@ class KeramelizerInputLanguagePred extends ContextualLanguagePred {
}
object KeramelizerInputLanguagePred {
- val MANUAL_LINK_SEQ = "https://apalache.informal.systems/docs/apalache/known-issues.html#using-seqs"
+ val MANUAL_LINK_SEQ = "https://apalache-mc.org/docs/apalache/known-issues.html#using-seqs"
private val singleton = new KeramelizerInputLanguagePred
From 19963f413ae4ce8f65ee96292b3ba7d824a58ebd Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Fri, 23 Aug 2024 21:21:13 +0200
Subject: [PATCH 06/15] fix formatting
---
.../src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
index 34908a3d67..867b9b9f77 100644
--- a/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
+++ b/tlair/src/main/scala/at/forsyte/apalache/tla/lir/Feature.scala
@@ -23,8 +23,8 @@ case class RowsFeature(
}
/**
- * Enable imprecise record types, see the discussion in ADR-002.
+ * Enable imprecise record types, see the
+ * discussion in ADR-002.
*
* [[ImpreciseRecordsFeature]] is mutually exclusive with [[RowsFeature]]. It is present only for backwards
* compatibility.
From de60a69dbb5095edf4cf64769705c46e10f83423 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Sun, 25 Aug 2024 14:26:09 +0200
Subject: [PATCH 07/15] improve the error message about expanding powersets
---
test/tla/TestSets.tla | 5 +++++
test/tla/cli-integration-tests.md | 10 ++++++++++
.../scala/at/forsyte/apalache/tla/bmcmt/Limits.scala | 4 ++--
.../tla/bmcmt/config/CheckerExceptionAdapter.scala | 4 ++++
.../at/forsyte/apalache/tla/bmcmt/exceptions.scala | 11 +++++++++++
.../apalache/tla/bmcmt/rules/aux/PowSetCtor.scala | 11 ++++++++---
6 files changed, 40 insertions(+), 5 deletions(-)
diff --git a/test/tla/TestSets.tla b/test/tla/TestSets.tla
index d52033d064..4ff544970d 100644
--- a/test/tla/TestSets.tla
+++ b/test/tla/TestSets.tla
@@ -145,6 +145,11 @@ TestExists15InPowerset ==
\E S \in SUBSET Set263:
S = { 2, 6 }
+\* This test is expected to fail. It should be run separately.
+FailExpandLargePowerset ==
+ \E S \in SUBSET (1..30):
+ 31 \notin S
+
TestForallInPowerset ==
\A S \in SUBSET Set1357:
6 \notin S
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index 90fd5c9435..1cb1d9411f 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -2668,6 +2668,16 @@ $ apalache-mc check --length=0 --inv=AllTests TestSets.tla | sed 's/[IEW]@.*//'
EXITCODE: OK
```
+### check TestSets.tla reports an error on FailExpandLargePowerset
+
+```sh
+$ apalache-mc check --length=0 --inv=FailExpandLargePowerset TestSets.tla | sed 's/[IEW]@.*//'
+...
+: known limitation: Attempted to expand SUBSET of size 2^30, whereas the built-in limit is 1048576
+...
+EXITCODE: ERROR (255)
+```
+
### check TestCommunityFunctions.tla reports no error (array-encoding)
```sh
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala
index 181e77a20b..75701a5d20 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala
@@ -13,9 +13,9 @@ object Limits {
val MAX_PRODUCT_SIZE = 1000000
/**
- * An upper bound on the size of an expanded powerset.
+ * An upper bound on the size of an expanded powerset, currently, `2^20`.
*/
- val POWSET_MAX_SIZE = 1000000
+ val POWSET_MAX_SIZE = 1048576
/**
* An upper bound on the number of rewriting steps that are applied to the same rule.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala
index 25bcbce0ce..1aa02ad85f 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/config/CheckerExceptionAdapter.scala
@@ -85,6 +85,10 @@ class CheckerExceptionAdapter @Inject() (sourceStore: SourceStore, changeListene
"%s: no rule to rewrite a TLA+ expression: %s".format(findLoc(err.causeExpr.ID), err.getMessage)
FailureMessage(msg)
+ case err: RewriterKnownLimitationError =>
+ val msg = "%s: known limitation: %s".format(findLoc(err.causeExpr.ID), err.getMessage)
+ NormalErrorMessage(msg)
+
case err: RewriterException =>
val msg = "%s: rewriter error: %s".format(findLoc(err.causeExpr.ID), err.getMessage)
FailureMessage(msg)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala
index 482c0d5fbf..b21aa9c915 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala
@@ -22,6 +22,17 @@ class CheckerException(message: String, val causeExpr: TlaEx) extends Exception(
*/
class RewriterException(message: String, causeExpr: TlaEx) extends CheckerException(message, causeExpr)
+/**
+ * This exception is thrown when the rewriter meets a generally well-formed TLA+ expression
+ * that cannot be handled due to some known limitations of the model checker.
+ *
+ * @param message
+ * error message
+ * @param causeExpr
+ * the problematic TLA+ expression, may be NullEx
+ */
+class RewriterKnownLimitationError(message: String, causeExpr: TlaEx) extends CheckerException(message, causeExpr)
+
/**
* This exception is thrown when QStateRewrite cannot find an applicable rule.
*
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
index 5d67003924..9d9fdb18bf 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
@@ -3,6 +3,7 @@ package at.forsyte.apalache.tla.bmcmt.rules.aux
import at.forsyte.apalache.tla.bmcmt._
import at.forsyte.apalache.tla.lir.SetT1
import at.forsyte.apalache.tla.types.{tlaU => tla}
+import com.typesafe.scalalogging.LazyLogging
/**
* This class constructs the power set of S, that is, SUBSET S. Sometimes, this is just unavoidable, e.g., consider { Q
@@ -11,7 +12,7 @@ import at.forsyte.apalache.tla.types.{tlaU => tla}
* @author
* Igor Konnov
*/
-class PowSetCtor(rewriter: SymbStateRewriter) {
+class PowSetCtor(rewriter: SymbStateRewriter) extends LazyLogging {
// Confringo is the explosion curse from Harry Potter. To let you know that your SMT solver will probably explode.
def confringo(state: SymbState, set: ArenaCell): SymbState = {
@@ -40,8 +41,12 @@ class PowSetCtor(rewriter: SymbStateRewriter) {
rewriter.solverContext.log("; %s(%s) {".format(getClass.getSimpleName, state.ex))
val powSetSize = BigInt(1) << elems.size
- if (powSetSize >= Limits.POWSET_MAX_SIZE) {
- throw new RewriterException(s"Attempted to expand a powerset of size 2^${elems.size}", state.ex)
+ if (powSetSize > Limits.POWSET_MAX_SIZE) {
+ logger.error("This error typically occurs when one enumerates all subsets:"
+ + " \\A S \\in SUBSET T: P or \\E S \\in SUBSET T: P")
+ logger.error("Try to decrease the cardinality of the base set T, or avoid enumeration.")
+ val msg = s"Attempted to expand SUBSET of size 2^${elems.size}, whereas the built-in limit is ${Limits.POWSET_MAX_SIZE}"
+ throw new RewriterKnownLimitationError(msg, state.ex)
}
val subsets =
if (elems.nonEmpty) {
From 0c6b10779a6f006480af17dfbc2289195169f668 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Sun, 25 Aug 2024 14:31:29 +0200
Subject: [PATCH 08/15] add release notes
---
.unreleased/bug-fixes/2969-powset-expansion | 1 +
1 file changed, 1 insertion(+)
create mode 100644 .unreleased/bug-fixes/2969-powset-expansion
diff --git a/.unreleased/bug-fixes/2969-powset-expansion b/.unreleased/bug-fixes/2969-powset-expansion
new file mode 100644
index 0000000000..2faa13c9c9
--- /dev/null
+++ b/.unreleased/bug-fixes/2969-powset-expansion
@@ -0,0 +1 @@
+Better error reporting for hitting the limits of `SUBSET` expansion, see #2969
\ No newline at end of file
From d910530c7ce77cda1fcb3f38c81d3b77059f7794 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Sun, 25 Aug 2024 14:34:06 +0200
Subject: [PATCH 09/15] fix formatting
---
.../main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala | 4 ++--
.../at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala | 3 ++-
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala
index b21aa9c915..82de2da58a 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/exceptions.scala
@@ -23,8 +23,8 @@ class CheckerException(message: String, val causeExpr: TlaEx) extends Exception(
class RewriterException(message: String, causeExpr: TlaEx) extends CheckerException(message, causeExpr)
/**
- * This exception is thrown when the rewriter meets a generally well-formed TLA+ expression
- * that cannot be handled due to some known limitations of the model checker.
+ * This exception is thrown when the rewriter meets a generally well-formed TLA+ expression that cannot be handled due
+ * to some known limitations of the model checker.
*
* @param message
* error message
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
index 9d9fdb18bf..78b11e9628 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
@@ -45,7 +45,8 @@ class PowSetCtor(rewriter: SymbStateRewriter) extends LazyLogging {
logger.error("This error typically occurs when one enumerates all subsets:"
+ " \\A S \\in SUBSET T: P or \\E S \\in SUBSET T: P")
logger.error("Try to decrease the cardinality of the base set T, or avoid enumeration.")
- val msg = s"Attempted to expand SUBSET of size 2^${elems.size}, whereas the built-in limit is ${Limits.POWSET_MAX_SIZE}"
+ val msg =
+ s"Attempted to expand SUBSET of size 2^${elems.size}, whereas the built-in limit is ${Limits.POWSET_MAX_SIZE}"
throw new RewriterKnownLimitationError(msg, state.ex)
}
val subsets =
From 8195978e17b2472e141692d1476ba2d130bba0b5 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Sun, 25 Aug 2024 20:45:46 +0200
Subject: [PATCH 10/15] fix the message as suggested by @thpani
---
.../main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala | 4 ++--
.../forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala | 8 ++++----
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala
index 75701a5d20..d5b8bad29d 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/Limits.scala
@@ -13,9 +13,9 @@ object Limits {
val MAX_PRODUCT_SIZE = 1000000
/**
- * An upper bound on the size of an expanded powerset, currently, `2^20`.
+ * An upper bound on the size of a base set that is expanded to a powerset, currently, `20`.
*/
- val POWSET_MAX_SIZE = 1048576
+ val POWSET_MAX_BASE_SIZE = 20
/**
* An upper bound on the number of rewriting steps that are applied to the same rule.
diff --git a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
index 78b11e9628..124f4a968d 100644
--- a/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
+++ b/tla-bmcmt/src/main/scala/at/forsyte/apalache/tla/bmcmt/rules/aux/PowSetCtor.scala
@@ -40,15 +40,15 @@ class PowSetCtor(rewriter: SymbStateRewriter) extends LazyLogging {
}
rewriter.solverContext.log("; %s(%s) {".format(getClass.getSimpleName, state.ex))
- val powSetSize = BigInt(1) << elems.size
- if (powSetSize > Limits.POWSET_MAX_SIZE) {
- logger.error("This error typically occurs when one enumerates all subsets:"
+ if (elems.size > Limits.POWSET_MAX_BASE_SIZE) {
+ logger.error("This error typically occurs when one enumerates all subsets of a set:"
+ " \\A S \\in SUBSET T: P or \\E S \\in SUBSET T: P")
logger.error("Try to decrease the cardinality of the base set T, or avoid enumeration.")
val msg =
- s"Attempted to expand SUBSET of size 2^${elems.size}, whereas the built-in limit is ${Limits.POWSET_MAX_SIZE}"
+ s"Attempted to expand a SUBSET of size 2^${elems.size}, whereas the built-in limit is 2^${Limits.POWSET_MAX_BASE_SIZE}"
throw new RewriterKnownLimitationError(msg, state.ex)
}
+ val powSetSize = BigInt(1) << elems.size
val subsets =
if (elems.nonEmpty) {
BigInt(0).to(powSetSize - 1).map(mkSetByNum)
From 3330b194b811c4b3b9984ec93be28565969a7000 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Sun, 25 Aug 2024 20:48:04 +0200
Subject: [PATCH 11/15] fix the test
---
test/tla/cli-integration-tests.md | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/test/tla/cli-integration-tests.md b/test/tla/cli-integration-tests.md
index 1cb1d9411f..676077e0d7 100644
--- a/test/tla/cli-integration-tests.md
+++ b/test/tla/cli-integration-tests.md
@@ -2673,7 +2673,7 @@ EXITCODE: OK
```sh
$ apalache-mc check --length=0 --inv=FailExpandLargePowerset TestSets.tla | sed 's/[IEW]@.*//'
...
-: known limitation: Attempted to expand SUBSET of size 2^30, whereas the built-in limit is 1048576
+: known limitation: Attempted to expand a SUBSET of size 2^30, whereas the built-in limit is 2^20
...
EXITCODE: ERROR (255)
```
From 0a02809f106a78ea414deca74dea6bdddfb894a1 Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Wed, 28 Aug 2024 21:43:10 +0200
Subject: [PATCH 12/15] update the landing page
---
.github/FUNDING.yml | 4 +-
FUNDING.md | 3 +-
README.md | 102 +++++++++++++++++++++++---------------------
3 files changed, 57 insertions(+), 52 deletions(-)
diff --git a/.github/FUNDING.yml b/.github/FUNDING.yml
index cc0587d78d..54bc76b169 100644
--- a/.github/FUNDING.yml
+++ b/.github/FUNDING.yml
@@ -1,6 +1,6 @@
# These are supported funding model platforms
-github: # Replace with up to 4 GitHub Sponsors-enabled usernames e.g., [user1, user2]
+github: [konnov] # Replace with up to 4 GitHub Sponsors-enabled usernames e.g., [user1, user2]
patreon: # Replace with a single Patreon username
open_collective: # Replace with a single Open Collective username
ko_fi: # Replace with a single Ko-fi username
@@ -9,4 +9,4 @@ community_bridge: # Replace with a single Community Bridge project-name e.g., cl
liberapay: # Replace with a single Liberapay username
issuehunt: # Replace with a single IssueHunt username
otechie: # Replace with a single Otechie username
-custom: ['https://informal.systems/', 'https://viennabusinessagency.at/'] # Replace with up to 4 custom sponsorship URLs e.g., ['link1', 'link2']
+custom: # Replace with up to 4 custom sponsorship URLs e.g., ['link1', 'link2']
diff --git a/FUNDING.md b/FUNDING.md
index 7d6cffe670..8e1aff6ba2 100644
--- a/FUNDING.md
+++ b/FUNDING.md
@@ -1,7 +1,8 @@
## Apalache Funding
We are grateful to the following organizations for financially supporting
-the project Apalache for significant duration of time in the past:
+the Apalache project (in the form of grants or employment) for a significant
+duration of time in the past:
- [Informal Systems][]: 2020-2024
- [Vienna Business Agency][]: 2021-2023
diff --git a/README.md b/README.md
index a238a32b39..bc8ceced3b 100644
--- a/README.md
+++ b/README.md
@@ -12,16 +12,19 @@ alt="Apalache Logo">
[![main badge][]][main-ci]
[main badge]: https://github.com/apalache-mc/apalache/workflows/build/badge.svg?branch=main
+
[main-ci]: https://github.com/apalache-mc/apalache/actions?query=branch%3Amain+workflow%3Abuild
-Apalache translates [TLA+] into the logic supported by SMT solvers such as
-[Microsoft Z3]. Apalache can check inductive invariants (for fixed or bounded
+Apalache translates [TLA+][] into the logic supported by SMT solvers such as
+[Microsoft Z3][]. Apalache can check inductive invariants (for fixed or bounded
parameters) and check safety of bounded executions (bounded model checking). To
-see the list of supported TLA+ constructs, check the [supported features]. In
-general, Apalache runs under the same assumptions as [TLC].
+see the list of supported TLA+ constructs, check the [supported features][]. In
+general, Apalache runs under the same assumptions as [TLC][]. However, Apalache
+benefits from constraint solving and can handle potentially larger state-spaces,
+e.g., involving integer clocks and Byzantine faults.
-To learn more about TLA+, visit [Leslie Lamport's page on TLA+] and his [Video
-course].
+To learn more about TLA+, visit [Leslie Lamport's page on TLA+][] and his [Video
+course][].
## Releases
@@ -39,54 +42,54 @@ You can also find Apalache packaged via Nix at [cosmos.nix](https://github.com/i
For more information on installation options, see [the
manual][user-manual-installation].
+## Success stories
+
+Check [Apalache examples][] that demonstrate how to use the strengths of Apalache.
+Also, check the [standard repository of TLA+ examples][].
+
## Getting started
- Read the [Beginner's tutorial][].
-- Check the material at [TLA-Apalache workshop][].
- Read the [Apalache user manual][user-manual].
- Consult the (WIP) [Idioms for writing better TLA+][idioms].
- Consult the (WIP) [TLA+ language manual for engineers][language-manual].
-## Website
-
-Our current website is served at https://apalache-mc.org .
-
-The site is hosted by github, and changes can be made through PRs into the
-[gh-pages](https://github.com/apalache-mc/apalache/tree/gh-pages) branch of
-this repository. See the README.md on that branch for more information.
-
-The user documentation is automatically deployed to the website branch as per
-the [CI configuration](./.github/workflows/deploy.yml).
-
-Our old website is still available at https://forsyte.at/research/apalache/ .
-
## Community
- Join the chat in the [Apalache zulip stream].
- [Contribute](./CONTRIBUTING.md) to the development of Apalache.
-## Help wanted
+## Funding and Sponsorship
-Want to contribute? Here is a list of issues that could be solved without
-knowing too much about the internals of Apalache. Solving these issues would
-improve usability! Please comment in the relevant issue, if you are going to
-solve it.
+Currently, Apalache is not funded by any organization. As a result,
+it is de-facto funded by its current maintainers and contributors,
+including [Igor Konnov][], [Jure Kukovec][], and [Thomas Pani][].
+If you would like to sponsor the project, please contact us.
-- Writing annotations in the JSON format: [#804](https://github.com/apalache-mc/apalache/issues/804)
-- Add support for VIEW in the TLC config: [#851](https://github.com/apalache-mc/apalache/issues/851)
-- Translate `\E x \in STRING: P` and `\A x \in STRING: P`:
- [#844](https://github.com/apalache-mc/apalache/issues/844)
-- Interval analysis for `a..b`: [#446](https://github.com/apalache-mc/apalache/issues/446)
+We are grateful for the past financial support in the form of grants or
+employment from the following organizations:
-## Industrial examples
+ - [Informal Systems][] (Canada/Switzerland/Austria): 2020-2024
+ - [Vienna Business Agency][] (Austria): 2021-2023
+ - [Interchain Foundation][] (Switzerland): 2019-2023
+ - [WWTF][] (Austria): Vienna Science and Technology Fund 2016-2020
+ - [Inria Nancy][] and [LORIA][] (France): 2018-2019
+ - [TU Wien][] (Austria): 2016-2020
-- Check [Light client specs][] and [Model-based testing][] of the Tendermint
- light client.
+More details on the [Funding page](./FUNDING.md).
-- Check [Tendermint specs][] to see how we use TLA+ and Apalache at Informal to
- design and specify protocols for the [Tendermint blockchain].
+## Website
+
+Our current website is served at https://apalache-mc.org .
-- To see more examples, check the [standard repository of TLA+ examples].
+The site is hosted by github, and changes can be made through PRs into the
+[gh-pages](https://github.com/apalache-mc/apalache/tree/gh-pages) branch of this repository. See the README.md on that
+branch for more information.
+
+The user documentation is automatically deployed to the website branch as per
+the [CI configuration](./.github/workflows/deploy.yml).
+
+
-## Performance
-
-We are collecting [apalache benchmarks]. See the Apalache performance when
-[checking inductive invariants] and running [bounded model checking]. Versions
-0.6.0 and 0.7.2 are a major improvement over version 0.5.2 (the version
-[reported at OOPSLA19](https://dl.acm.org/doi/10.1145/3360549)).
-
+
---
-Apalache is developed at [Informal Systems](https://informal.systems/).
-
-With additional funding from
[](https://viennabusinessagency.at/).
-
-Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](https://wwtf.at/about/).
-
[tla+]: http://lamport.azurewebsites.net/tla/tla.html
[microsoft z3]: https://github.com/Z3Prover/z3
[supported features]: https://apalache-mc.org/docs/apalache/features.html
@@ -166,3 +159,14 @@ Past funding from [Der Wiener Wissenschafts-, Forschungs- und Technologiefonds](
[apalache-mc.org]: https://apalache-mc.org
[TLA-Apalache workshop]: https://github.com/informalsystems/tla-apalache-workshop
[Beginner's tutorial]: https://apalache-mc.org/docs/tutorials/entry-tutorial.html
+[Apalache examples]: https://github.com/konnov/apalache-examples
+[WWTF]: https://wwtf.at/index.php?lang=EN
+[TU Wien]: https://www.tuwien.at/
+[Inria Nancy]: https://www.inria.fr/en/inria-centre-universite-lorraine
+[LORIA]: https://loria.fr
+[Interchain Foundation]: https://interchain.io/
+[Informal Systems]: https://informal.systems/
+[Vienna Business Agency]: https://viennabusinessagency.at/
+[Igor Konnov]: https://github.com/konnov
+[Jure Kukovec]: https://github.com/kukovec
+[Thomas Pani]: https://github.com/thpani
\ No newline at end of file
From 415ec70cad012a2f1d114f2fe3b1dd4da2e8809a Mon Sep 17 00:00:00 2001
From: Igor Konnov
Date: Wed, 28 Aug 2024 21:57:56 +0200
Subject: [PATCH 13/15] add the "reloading" image and more info about
sponsorship
---
FUNDING.md | 6 ++++++
README.md | 5 ++++-
assets/reloading-apalache.png | Bin 0 -> 1065647 bytes
3 files changed, 10 insertions(+), 1 deletion(-)
create mode 100644 assets/reloading-apalache.png
diff --git a/FUNDING.md b/FUNDING.md
index 8e1aff6ba2..1920d637ca 100644
--- a/FUNDING.md
+++ b/FUNDING.md
@@ -1,5 +1,11 @@
## Apalache Funding
+Currently, Apalache is not funded by any organization. As a result,
+it is de-facto funded by its current maintainers and contributors,
+including [Igor Konnov][], [Jure Kukovec][], and [Thomas Pani][].
+If you would like to sponsor the project, please contact us, or
+simply sponsor us on GitHub by clicking the "Sponsor" button!
+
We are grateful to the following organizations for financially supporting
the Apalache project (in the form of grants or employment) for a significant
duration of time in the past:
diff --git a/README.md b/README.md
index bc8ceced3b..fc0b76c80e 100644
--- a/README.md
+++ b/README.md
@@ -64,7 +64,10 @@ Also, check the [standard repository of TLA+ examples][].
Currently, Apalache is not funded by any organization. As a result,
it is de-facto funded by its current maintainers and contributors,
including [Igor Konnov][], [Jure Kukovec][], and [Thomas Pani][].
-If you would like to sponsor the project, please contact us.
+If you would like to sponsor the project, please contact us, or
+simply sponsor us on GitHub by clicking the "Sponsor" button!
+
+![Reloading Apalache](./assets/reloading-apalache.png)
We are grateful for the past financial support in the form of grants or
employment from the following organizations:
diff --git a/assets/reloading-apalache.png b/assets/reloading-apalache.png
new file mode 100644
index 0000000000000000000000000000000000000000..c66d1c5525297fba998e0e966964c8265ff8b3b2
GIT binary patch
literal 1065647
zcmV*7Kytr{P)EX>4Tx07!|QmUmQB*%pV-y*Is3k`RiN&}(Q?0!R(LNRcioF$oY#z>okUHbhi#
zL{X8Z2r?+(fTKf^u_B6v0a3B*1Q|rsac~qHmPur-8Q;8l@6DUvANPK1pS{oBXYYO1
zx&V;;g9XA&SP6g(p;#2*=f#MPi)Ua50Sxc}18e}`aI>>Q7WhU2nF4&+jBJ?`_!qsp
z4j}paD$_rV!2tiCl(|_VF#u4QjOX(B*<2YH$v8b%oF%tU$(Xh@P0lb%&LUZYGFFpw
z@+@0?_L*f5IrB1vJQ>S#&f;b8cV}o=_hCs$|GJ-ARc>v%@$zSl&FIdda6Uz_9&dgda5+tXH875p)hK-XG
zi{a1DP3Mcn%rFi&jU(bQ*qIqw9N}^RX3zXt6nSkKvLZX!I5{{lZ7prSDAa#l{F{>Z
zc9vd*f9@GXANa%eSALld0I;TIwb}ZIZD|z%UF!i*yZwjFU@riQvc7c=eQ_STd|pz-
z;w)z?tK8gNO97v2DKF^n`kxMeLtlK)Qoh~qM8wF>;&Ay4
z=AVc79|!(*9u^V&B)*6*lto0#rc5AAmbF{R6Nm+wLWV&2pPKj&!~Ue%xt59A_z}>S
zSOTRX8bE#?04OREAPIY9E70$K3&uwS`OS;bnV6mX&w~DaSGY|6$QC4jj$=neGPn{^
z&g`1}S^_j607XCp>OdRl0~5dmw!jg%01w~;0zoK<1aV+7;DQv80Yo4d6o9p$7?gso
zU?->sb)XS6gEnv&bb({wG&lz?fy-b7+yPQB4xWH1@CwX85QK%u5EW8~bRa{>9I}O2
zkQ?L!1w#=~9FzzpLqbRb6+r8tQm7oNhU%ea=v(M0bQ-z<4MVq}QD_qS6?z9FFbSr?
zTCfpp1+!pJI0%k}7s1K!GB_VDg15kxa07f0?u1Xnm*5dt3O|9T5r7a8I--j(5f;Km
zLXmhR2@xTykP@TC$XgT!MMW`COq2`C9~Fh-qL!gnp*EwcQ3p_+
zs6NzH)F^5S^$|@*Yog83&gcMiEIJvTi!Mf2pqtPg=(Fe%^f>wz27{qvj4_TFe@q-E
z6|(}f8M7PHjyZ)H#*AU6u~@7+)*S1K4aIV>Vr((C3VRTH5_<(Zj(vk8;&gDfIA2^m
zPKYbSRp451CvaDA6Sx_?65bH+j1R^0@XPUK_(psWeh5E~pCKp{j0vuUNJ1)MEuoUo
zMmS5jOL##f67`5q#Bid3xQ19sJVZQC93{RbQAlPaHYtH5A#EY;C!HeQBE2A!$wp)k
zay(f~-a>9BpCR8TzfqtnSSkc4@Dx@n)F^Z+Tv2$Yh*vaJ^i*7|n6Fr&ctmkX@u?DC
z$w-N<#8FzMRHJlM>4ws@GF90|IaE1Ad9!kh@&)Bb6fDJv;zQw4iYWUiXDDM-gsM+v
zQ@PZ2)JE!A>NpKUGo}U5QfZ~MZ)k(GDHV!}ol3Myo=T0%aTO^Yp&QWy=;`z_`eFKY
z`a4xERZmsE>L%4T)hnv6)#j*qsPWZG)Y{cX)ZVEx)P2;`)VHa3so&E;X_#q*YvgL|
z(KxH|bPjEf%N*{Uk~xRx+}4CO%`_u4S7`3j9MGKB($@0R%F?RRI-~Veo38DlovOV<
z`-JwS4pqlZN1(Gq=cLYKh6=-zkLZ@rEqJ6vJJH{f4iNjE!Q9HW+moJu+4^4lvF)ZZ*DZ
zLN;+XS!U8;a?KQD$}&we-EDf=3^ubjOEIf48#0H@9n1yhyUm9!&=yV>LW>5A8%z?@
zlbOS8WsX|XErTr!ExRnASs7TxTWz!IxB6&pZ=G)4Xnn_qViRanXwzf!tF4(W*S5y?
z+FbHn-?^*jcF%ooXKu&0+hcdro@yUrzrnuO{)2;~gUF%HVbamSG10Ns@dk^=3S(_%
zop(Yzc{#0iI_C7&*}+-teAxLH7p6;^ON+~+dB*ej^BU)kx$3!cTZVb0Xx4mvs
zcU^amdxQG}4}A}wN0Y~dr>SSE=RwbBUe;bBuMV%*Y-jdL_9<_~+t0hid(emC6XjFw
zbKh6bH`%w{0a^jvfaZXyK*zw9fqg-wpantIK@Wn>fV8I2F~=-fTgudr?_nHF76Ya
z2X6;&lJCkd=T9WLCY2{WN_I`&o;;c2o>GzWRKONg3!bO?r`DyuP76)jpY|y|CcQla
zmywupR7eq~3Hvg&GxIWsv&^%Kv!u(Mm+f3OB?=NXWkcDEvb)7J+0WE~#6+@QGMeL-
zQhTd=lZbfxFY`c=@XrK@^Z>#r_a
zJ-)_o&4IOqwP|aAD6}ptFMPQ!W?fH_R?(WGvGsoITZV0)e^+=6ZO?$0o?WWq-yLr2>
z?D5#sR;N{0TK8_RVDHU(zxvJwqlSuon0-0>9yUfd_J7U#y17ZCskG_Ce&K%UfrtZr
z&5q5@Et)N5t#GTPb@E`s!OP!xf79K@Y^!glx0fCQha`s{f1CL2^}|7jdylY=w0&pz
zU2O-oqofn+T;4g=mC_~cj_V#i8hEs~$EBy^d&}?lAJaWnb6n+k*$Kjlq7$D^=AWEC
zm38Xr>EzR6y-RxUoQXYituMT9@NCf8^XGieo$2@NKY8Bu{ILtp7mi+JUF^E#aH(^^
zexTzA`yV<69R@px9EZ9uJ6-M>o;Q5riu;w*SG}*EyB2Wm(#ZUg;pqt>?FMZqM9Va~FNLGD$lbNT*KP&%S`^@CocfWZ2GB6c8HU3=m{L`|I+Sd?{wJo{Z|>UW?q-PQGavbE$eOnyO?(qGr8}v?<+r;e(3oa^zrVej8C6_
z1NVgU`*8t=>i_@%24YJ`L;(K){{a7>y{D4^000SaNLh0L04^f{04^f|c%?sf00007
zbV*G`2j~bK6E_X)s!<65000?uMObu0Z*6U5Zgc=ca%Ew3Wn>_CX>@2HM@dakSAh-}
z001BWNklbI$loCN^;o3HgPPlq8T8mjDIoEtMaoeW}3P
zVimL$mm)=iw73LFNFX5u;%*Zg*E7eqEqUbqW9>O9?Vf90XXcu-XV!Vv^W68>?ky(U
z6Cs2^RhCGl01!eTrNn!SR1zg6WmzGFAW0JPJg2f1kx9@>A(g^fi*t@BiYUtxr4+^(
zy!TjZsmhWx%c!cV{vJ1ENS|!NaM_D4VtKI0(qfk@pZfytzwH5j{GFfBJ6w<^9m?P^
zX+ltr<+4kAs=*a6x}1J_n3uogrQG%Nd-&IX`52U7Ov>2!G^O>FWl6vxrKDdS;)F|2
z=7Q&*$Dk^B;qzX^Prmh2zVwkV(A&90Dx0KHino@?2wVtQ5m>4gIsdt5a^+Re<44#3
zh=(6}kk`KImHhr|exEOV?!Wk#x4aKI)MOze7KX|@R72vTg0n9?jrY9&J-q2J|Arf`
zyP4??883YCrCfE@^Z3P2Z{=g}x|-fxAZs*m*3%#K&{|OWir4_F8`Q)tmXmdp{3A5@j@!
z2DYk5n<;S|v%I{_QZ>(&uepT3fA?SWqn~|?Pk#IpTyXYjyzR~Z%ymDwoj?Dbw-Qy7
z%(U=jNgT&CI&FlO^aec+EzR-F7oNoLzv*?jcHoo$_Gxba;x^NN)smr
zXDvc&nv;fSTzDM4{vzN1=Ivw#R!yvD|DHp5@6akD2t}M2g0QqF+RV=%B+4Xbp1qZ;
zUikuSnRD%rf5!K}^-Id0A{HqiX|!6j+6~HTfVCwm7IX*mtXVt3)>F1HG0|Yv%oO?1
z^TY4mz@8n81Q+8SWQ_!q)Mp!Kh@ymEZ<#cWm|Z(dtKDQU=(DuA#4zu3%Bd$Y=nvSn
zYY$~%Szcb|l+(6y_F3m}(@%cM|fr;8814WSN!427;iRt;=afE)Vn{+!s9&>lcBxDdrt@f
zV@&;iAjm*PiE6?pzx+Y=9XP;S|MH(19x72nqeXUX(#y|hL;vrb|Ajz`$IX*KVD?+1C$J3qzu
zzIz=aNFtL^+6o~9QDSIz+IS?()e^a1;$vU))fpaO%UM{8BeU%mYe{N$$V=q=`qr<2@%?X4{A?b2>G30_g!fJtJKhGDsT
zkf=FNZecl4J$QEW&X8A+1STOQCzQ>rp&Vxq;q{kxf*
z9OqB|{PkRT(Z$?-*TcNyAO4X;2j+-WL}DVG_rz&LUYqC2<_v#UKa)4dxQ{p@5!qYCmbi8aRM)W^>1>_iN}yT#|_ur#MK}F0+CFK
z;}jz`WtGz#F00cW-(N!a5?8;Jqbn
zMzqG8%y;LRoa}JPMd$OiZ+wMwo_Q`+8Mx=xM_JmtM6=xiCy3*i%9jW&(6J`Zhva@h
zG#+^FD=z2B!;kZ_7rl&6zxN9~b;mA5sc5HT03-Y)2_fK|r&I%e`wdsI>(EnN_q|_o
z(~aNedtd(!A9~m4NQoG4&Cu-+30~lXAOw#xioy;UR$b1&_`8$=Yzq<>#>V#Py6#jC0PJ7xRJleu^J`{bx`Z;yA?$
zkIGU^7BTF1@vdNIdYrjK`&qrF!@qs#U7U69Y5eQ^Kf(vzeKm*(qho{+%*@QNxVT7J
zR^F5+CWoE++yY}oPHU=Xjs@zdj1Ja3z
zSH9w9{KqH%1Dr=hiv4@{@tW7XmTSKEBZ38^G)cpd4@)AG(CLg**^2r3JzR3>GkD|w
z`7<7R;tBrlZ{N;v!I4I7@Bte6evucy?sCq!U@QOijW2Tg=_hmH1sCw>
zolo(t&tA_H_wOf(n+RcW)**x-iZwlVm}kBC4F2dZewWXF{&Spi;;D?M<9y~LUt-(s
z`$(b&sYsQM
z{rwwx_3yrvlTJ8;lg^mn%b))WpLzdR_|Uul1K|bDq)pmrF&Oj-Qevx$e6Y-#6W8;K
zKYanK*H5#&XOZ{4{R89&L3vG@Hn1K{64P!sDatN$%ZGUR>o4LR?|dik`r8ljA0PWK
zHk`ScuYdDf?09GgFMHk#5W$c{F`e-?#~ix_X9II{b3FOvcAU!j_!r*CKfUiC7!C*A
zbkmLO*}j`U`JFeg_`N^G_J$-%qoqP?jZg}rz>p=5K6x|Ge%^)L`@miFmj`Gcv-`n=%xL01`0O-T~M*ev#&UZlP=iA!MW|+a^tUf=Ud*(S3Y|!|M}VLkVx8%afA~n
zZJ1wNCP@;~X3XL4KBhNjyz2w+dx4^LEzGZs68yf5n0Ob`cc<;RMzhBiBPtzUUNw`>%hC
zuYc#8-0}0fS>M@+>1uX9ypzFliIxT>H9`oS1MnE5u+fl-*4`BtPR8@{r_1`O9W4f{^
zkWvvv1}PPlt?sl*T)3Kr+*
zPys?w!2lF;^f2m8s<}&M
z`}Y;>*}0d^8`raHx(%k@VoOWQ^p=)U)c1A-{HIAmr_*Bpfj!L49cE&>%}ZW(1s6U0
z8T{TKyqqhpyo6P=V+1OoURy0CtyYT=0znF*$PjQeGL3TsvQ)BV%Vt{RO{5Y8@2Sd?
zs*sNVKHv_fY{RJ53TPXfz^B4CTOMi-Igo5k4Tjqmjfl8S*f>dV-~V
zp17rnnzfkYEyQvCJw;LAoLd3(Wm!_Xg4S4zxE0Zv8DrBi8;LtHXpi*{EhI^j&>Cxz
zHJb<_Df60;mt{rPYLc~Ll19YXWE+)gye}9GdH|%2CMK@IToftNM$F_yi>m0efA0=l
zHK09a2x3Uq)F>S&27Ri$zmC0U#xgJ;#O;-piLXJ+jrai$5u
z;hdw<$cUndG)sxKB93E@I%*?lpK}V0R>asu#<9n3q0ul1=_solUpZ`9((ezk)?myvB4Ns14=E3W5d{3
zhsqXc0~6z8teTlXDo<{6hQo?}-a{LO7yQ~wDuq%CIXYMPTDU=hjx|Doa}`+}Ap{s>
zFxu2#jYexj9LE@AaK6IJ3Jjcn*6B1_O$LK5c#r{FjV4CNXro8(H|RzTGSC}#@zOFr
z-C+Hu4S45pl>;O~3WSg-1`f-qgGy;%6oGo*C<$6Cq|^+C1Iof8L|q@Xgl3lFZHZ77t#*V^
z)u?el-E)Gk0f+aVD2fn1fT9+5s+>VFU~HlT0xEB@)?ux~IXikbH7Tkat;c)IH9!0=
zKfU&sJo)6~*rEh4h@-lR1DL1=5!O1K_Y8*>gS^jcUi%83{oJ$Ia`Z;<9vm30(V`|8
zO4no|N$U4I7if1f)~uW0_^lgx#(8J3anoABV{Ki#?dbVcwyK3m;Xy()4jZ?uUv*RPuF27YG5a&Bxx8LjTj|7^uZSn=>%FDoMQywo(3sLt|&1)
z>+)yu+CO?V$DFj8u~iwJsRnaP2Oz11L=imJ*?Nsq$$_~;EcNF3qd)yUnqv*dCdc{f
zzkL%5$x}~mNBA1_3sPO5&(1yEd-vUpPqtXIb`@GnLa4>ZvaBeok}5BtazsMXOf!6dbsHwg8qi2#^HH7y9R@1=gyr3ACN&pka$;Pfboe*vPOmwfq-Yz=G7dtbpx~O#_3Eq
zK?Mp|?`PpX!U>#r1TX6ID=cH}j5Jml;V?L|q^?Cmj%qv*MM>R{ltL=dk*Cp=xT25r
zIlbk1Y&k$g)cpaFN}{!{MOZ0lv|BXWZIFQ|jS@9&1Ca&?9nhtBOd)bxo@rDoJW%
zDvAgpu(WW9W+TQJiHK|P*X#AD$`V^uIBRPxjERXBIu>ARfi#4Gw-#K5Epw_t4ka8sFpmp@GtW5#VmR*TV;F09
zSe!pRIu8O{Rfqr+opFQ=D6Mfe5CWvlnAPiMnA;2GFei-+jIdHs6jYT(2B->4l^1BE
z7}7-&h^NPJk%ly((_RHA9(dpZ>~M%0VGr;93f~AJP!x_di}Ajq-EN|dM2Ub@kY&jV
zhMt={%>4Wk&iNH8R}@3=Ia8~eoPNeJG+T4W5gTVlRIMVpw&=Uz8kKe%brU@Q9@EB^`aK%+u5_Mv%4iupx
zFNaU}!%%-!3T9VNf$|(&Jb>2~&54-x$E;!K1|a;eRU~6-d{PtzRav5?q$r29+6|^=
z#%Z=wbXp5@N_jf1Ce3C>8XJPE4aw!jg}R5Pg6WwF)^1$Q%*=F6RwF$+3yLVxL{WXd
zz>{Q}bIv`5=Uwq^&OY}P#>ShYd#cY)S(g0Im)4p_BO!M=-C~)-4e3lYxb(_PIQjJB
zLHOGE85zGvp1Z9ohQr}XO%9=62cr!>1gxw3cAn>TKOFU8DQoW0?+->q{7CJxqcfyY
zT9FU)5s#=juM`5QjiD%t6*r~^6*XaT-sAicP!RCWQ=IfMy&KNx{OQgLD^{NOeL=j6onn-Qc8@SRcr%5~Kj(
ziHxAr&WN;P&Fl;da|`%N;L7^pc^A-H5oaldtr(WI>Y-zSFrLB=K!Y*{>me@!wiI|5
z>S8Z6T17~05Xyjr2OoZjV~;zA|NEA|<5QpbS9a~%!991~MLz7axVQkpp^aH-+9nbR
zU2m8ZPdw
zZXHn^VF$eia+mtpZUur>Y7V)j*1rB*_Tg_{GnzXJKwHtybXV
z(>8L_X-5%ENkvKJOA?cin230EDFg(Vo}EC)l7*!{tJiF%)rj#H!iaQu@9FjWNGXX-
zy^n6Y?N>A>41e~f-{-gfoU<9W4tql6oTpLX(p#8iH#!G23J<3
zQA(0Dkr<*VLg|2zHNg_n(e5;{wg6EVzs^{Tem_Ub+AShbJBU*Lul?+uTM=w(0trHZ
zj-b(QFtjDPt8l&s21QX&Ryk!^UsX{ce4xxL<`xbzv!Tt=XH9a>GtXvN792c02M&U_
zxT?SwCAO@{tCFJ1v7w-(WPY&7aa)h)YQvL^Z{MQ}MvIL2FT
zHmzOH(!qncL5X%1lbw{4wjRai^)p~SS}BqwL#qg99mA?mr7YffI@4{uay+(U8`B#m
zxbVtnGJaHxAle+6hyO_PTT
z5`kmGjL`;=SQ`+cPHbr75wf7sQFJC#qPP|nlcaXClQbns
zA_TrB8o>1QB`iT>5qTJE3SMIGI+K<{AituBh)0%L<}p(Lbu2ApobTp
zqU@qY$*ReORg)>LmL}i{zQEh6)|kCO2!)geYc0MEG{z&=ZC*v?b2^wBahZO
zjaXt7i2t$Qw9;rP(L$kxqAFnh+D*(ISYqzL0?jOD-P$R{5pv`K7YNSPL^A}Gs_#3F
zVQRWbQ7z!;v3AWANg`oHE|gR#U7I1+S&R~>09m3D(lN2B&6O{`oVcyYtLSGZQG4;8Z9&-070{~&}BHN1@L~a
zj}YLzMJh#-BxG>{7DDCl-i+|&EhIZstp
z6vdEY;EAPVywyaBz+;bYqmia{Uy!4-F9lj@gjNWp==b|8qSIh7AW$+hJBid5yaPPi
zQ(pnHI3v$X+@PcpWsEgCWF}_e&>WIL7N>-=q9_W4kXYyNA&i7ng_eS0zl%|d&Nyt@
za15dnBvCvvxoZ5K=lP0I7kmIAP+HSYGsc=tW+$haXtkjN;ROPPk(yQ%6FZA=1q68H
z!R-iA&N%OE)*rW;i!Zqt6Eus57whxj1a2fib|%_L<O{Xq&AfFU3I_=h?9nP+q5tFNLYB9QRCYkpV@0wzMrS_D5r
zd}@*=$l{DOGwWHN>r!+}Tp7TDD;>@TtUJ;h6M_$T2TI0dS(|p&pgX_7@mr2#^~`FF
zGWe>#HzOmo$uK6v=!jU?B1o{Hg{0j~(ZaEI%`{mnu0=3i8+XB3A_1W+Fa*4h@Fc+bN80U8;cv~@G*
zpL;s1#>beMo~-w_);Mo#16C`_vclPl()K7T%lZwg*>dzoPC0cemtB4dLb9^A%?g(p
z)lcE6k+CIhG^xrF@%4_Zm2vcO#}QV9>$<)TMrjRg3`Xn!maeY3X`bguAy85>81%8u
z62~#Y*FsYi8MHCzk>gz13TNGlK_W#h6sb}2D2`*ID5^!}x|piEKxj?ye#MzS5?K;b
z;H(?n@Q7TGNOYd(BuRq$Z?W(r5w4niyOlp%Yw;n}3|>moEM|6g7F&204|Li2_>;
zI6zs3l_FS23N=PXC=|n`AqdF3md793&Y?YvqPu`!ux*6#Jl$x})aMG;AoAQ1!`pag9dzUS%aG0Mfjx4-s%9=QEMlC(i^
zAhgC4P$P$}DlNUGWwchz%+8>iaLh5saqO1k>9nU=S{#xO>p1+8gDgfas@4&6bMw6C
zJ@4b5yYA)ctG~jFp8q1g_wDa8SkA%LojNkL3OCGiilQLT2bdJ5rpB0EJ;U7G0)s)$
z`t=)GyJme|?2f4A3d(9w|6W2^hBd1;uy`=%-rKg(oi7+0n;=P(+OZfp5JHL-p`_Jp
zkt8X5c6Pb*mit-SS25Gt#G#!zWlte}LaZZv1xb>D@MLL9lBEPOBEt$ctvd<|!(h&`
zZgMjO(5MySoMqX{=)e(2+FM5>Nm)I$icmO0uWr7V
z`Gb9CX4Wx1Jw1x`Ikbc{ifJ|yya4A)(kN#86Fd3EjdyVCjrS39&FWRFIqKL=bS9cB
zKhqKCO^&W^cYxBccFkI(P+WV>4fGdEwAU!8_o&h2RY|+uCP`8vUB|0-Z{NYeod>w!
zj0-b6(83ThC=}V?F*b6o(2_4za1-Xr&eHb{jP+KD}NS0N2O)001BWNklUA?l*F-EX{!&;0^`R;eF<;!3CHsfQfIsNoA
zR~(!uifV_%*O3^bHCh>@)@Yp)ykY0|gDfpnOtfa{G{y;z6$MoURuUN@xRu6P*$S<6
z?fT-el^r=hjOxuXpLTnK;h=(`>#v>_Cqk;H
z32yDwfvYNxK4udaUVH&-)~)B@fq9k}>a>F|DwY=(QCcIFBGRUg^#@C@zl;=uH@@+&
z_?tKW4P)6jPd@rYU896Tq3UrP1wJ@jX=z3ou5Zcb3Q`eMELp0qW7F(fHmqKYPU?F+
zvd4}*ha`=lf_Bnjc6<%{p4?A=VZeFkoyT)7{f!mk<3_0?rPRvWD6L4w4Pz4%1S!bN
zf{E!dY^YuDxx)wPE-z9H26*St$`EV~wt@pJY*@RF^Ph1Z^M@8VbZ~)Ivr~()-V;UU
z*I5Y?Ydu9?k!3CB4=;20&?5bAj_`^|N0h_b4TIj(+E3Py(Cu4T)4CkJE
z7H6Efnc3CT2vMII8$9|*>`Z~yg4pP~#(Bxi%xZRR-^-v|@YuGe5ME<+?beie1xT{A
z7NYWDNmt&?y61g`w-wJg=Uj9K58V4Ocm3)fl#A-VI1<;7U;`mUy&tsV
zq?1n|){-y%`?q<|JKo3bx7@+}!6jsBkUAzGmLw*kk)((qaV1>$rt~fCQTCLs8)CfWmVP!G_`Odq(e%OvQE_JUrASfc}m6`V9ZJxvrv{{sj@XQIjU>T$9$sC-FhtW6M}VKpR3fz}Ek
z>crm>u_ui1Q6pl60I~*WJpYe
z){0@bPfEnbnGLL++DO?8cvf3Z
z7^Tc;Z^8b@mbvqmdzqe?<(uF9Hdnp$)kr6~_>7^QVdqm+}j
zo~1iz9b^CL{4RK)D;S|;05?0ITGp$IhNHm$4$LDnNuDx%$P*Fvil
zSnE+LW@dUL+O;Sa6#IAdIIy#e9|}?}iA_XR=5>G3wd-2fe^K`Zk&>D*2oVz#Gh|T<
zf>9RiJr)y>#Gdf9i(OU~QmQ&(tZTulopqROtzz*|mk5m!
z5XX{cvpE{83M;rP6!6sJPqF*S-MsNn-^g<>xsn}E?&iKb?x(jnz*oLD7s`^#S4bm>
z6GNj>n_o%XWND#5ij)g4xR~RQJ8sk;?8^A&uQ}*a(@fjAp`_?~28$Jjly=f)qBB9P
z%!*KZq(;PXJRr`ckxHHK1#W-|gO$Ol6ZibzCQRmb0c
za?OpzX~g!2=9n3uWw787L`bO-GStz|I3l?>KR}gag{UIt+2oE=2e=9fL
za4T_KuY)fYMn<$79V7}R4O-W+6<^iLqY!Z6h5sL3c)t9_@38%e1ulIKBzhb|O{CM<
zj0i%6lz~<=V?jW%toi9Rck-X#_%RROzMr#Cf95FS!ipoIl^Si~ep(SQG^k|m$e3+#JCCz9ITZI}xNnIxt;u=KQN;1p?AN}y>Df5D&-{QLO-^~LL9^mY=
z&ZQYolbS`ePN{4`@G(U-tfRZyaNk{z@c848aQ|(G*#A_8t;TrS%U{B<>(Ha~azu>E
z2SZGh)J5G{w3b|W-m|#l7q@Z!^|vtFc?3#LD{CT^q}R`x7@x!u==Qo~t%Ni-9NxRg
z8(#ibY&vE$c?s>-7>D-mr?;>~)hkI&gNAMptfi4Pu+B0Z6m^s`NQ%5-X|Yf6hIMO?
z;?6tnVb7lZj89C^Uz!_5oHL?Wq9Vay*d=WwOioO2!wt7_-(CACyYPv|*Es*YXVDmI
zF`Tc9tQU|r>Y1XY{xU)t(qw``x5v+~zZW5ECvRqEH3#?hX(nU1k$Q=+xJpo|iY#f=
z;@?P!Xrw8=at!^EOK4$OJlv%mlq+QM2ywPYV$0St7!*ip
zNKKQa!$XF{KKZgkiWqcRlV&3s6oWb%90cW{LUhcZ(K9=Tt
zU}4Z5Fh93IBWd7DM+lB`SV0B5pW4O3!DVJTvmD%cfCp}Wm>+!W8eCzCbhPq06-AY!
zq-3nwAq+jY-Eb$r`0<^@#S{H<1Px0&mRS4j
z^=!NONxnCK4HrK1V%AP*!$>y
zl#(>#CcXJ(jEY9JUt$Z7&J0gIx|2I^yO&2Fdx9T*`KK%_ED}l&R)ALwdR?k~NM$WL
zRy3O#aooUGIr*^S@LZRtp4`o@$Cp@|>r)Lu_?k?3=Sk8CAM7ZSW(Zy}H@8T$F@Ypz
zX>rK94Vw@`)M*tW9JRP4Gz8~Jl9Vz?N*^%N(`lrfefnu!_vEceEf7^rppEvma~lH1
zpmu+Brtqqs|2+Q0>`7M7_7mJPETi9*c3f9$jP
zTp>jb)bhMUDuEcyk~!zx4@
zh~e^p&wTQ8Y(4o5&N}-728R!F^G|N%9dCIngQaD(ijh7L#|g1e7-?`-fv|ycU>O#U
z-q16@oHI2sh98Yc#3rr_Z)QI)W1%_b;*QKuSIEy^8n
zHvK3;rv#)rVeP8b%uHlNLa|}vI>yG^gnmh@)uoaikAfwQjH&S%_U_xoCqD97dV@JmJ98^b2M16Jl&r~@wGIe0
z;sgj7tuflr?e=N4Gghx&&wcki!cm)#XJ*w#)~($@cX1aXh#H8O7Hdni0WB0Z2%dU$
zH}i8Pc{$`OU;Y+{7rG!|P?W^cXckdOw61F`1zdggmpS9?)A;HazruIE`dxP3zaM~!
z<`mLPhNI8pvDVe8u+eAu^algV0W2=`x$V|_+4kfPv`8VUlNwPJ)x9OoP?4mYm-s>K>-hri^Bd-rhj
z4L1|j(3^g@%h>o7!3mrQxMGMM=5(?#ie<1vW$
zR>dgEP>*FAqbXg%{J}*Yxc6a-eu*d~B441$Je!)$x-Hh%K;N1%#nr4uYIEfah|=|H=kF?X<}ur)Rp#N=JY%{Sgh(wN3tPpD!d
zks@p@@Oa?~BUfv@HN|qT;ENynGWXnlJMluwgWtWMzq;qIX(SDX3q3k<8$YPfT3~&J
zmkJZt$*J3aaR;sG4pE`8OOD9LOthwGBr*M^I+bT+Ee`ebqE2o_k`N?i&(TmFc5OSz
zZ9lsk+t-Y@rdc|$L?r}+e2JMjWoc=l7Vdxp+ZTD&Oa7R&ks-Xm4lAnRXq?AHIBQ88
z3Xh|5wZZbt3(n)Q#~C>sHP@^=vME&hwbt_jL{&m?Mtk8rKv<5cM9Q
za4hazjYS{Ad)X0uc!&
z$2+*n<1336F&>HcfnKjqlBGCh$%jKY;wm{XNmi3R>1mI3(6MHIagoGmjF2oXED$9T
z#gQz&QiuQ|NMbRX9q_eM9z_unMJyr~d-KSo!fQu9v;-><)kyIa1}R5PPzs``{%{=|
zENDyC5qNLW!C)&-HykjHuztg
zTeY^1!VPR6*>H@_j`RP>dedlK&$`U>cTdms4tqNLOv%YfauPBpkOT-2hJch&L2MAM
zYPH%$t5sU+>h4umbuYVHt6ZhMw0mhe;8GCnr6{7y0R214fKBxj!X-tY8G
z_tYQm=WM9e-;Xb(GO~BAs;{J$wk?
z)$HzGVXs}_I}oFS*aQ?BL&|nYqZn_lQ`-*bJG2_$2hQWVq&6E_pfb&(nS+*;szQsw
zB3Brqj_5)#Tg;hkl$2Fuxm>cmVo}Plc6iFIcbuSJ&UxmmC+X$_=?sN3Y4c}tJf6DS
zqu4O~^e_Gtzww*z5`gtMLVAVH3Oehk##3U9>@D^fO-nX5#+*L$BJHYA#*Pj|
zrU%8|qf}C3*EZJatfMH3eW%E(X|T@H`y~&)@g83B%DWkjCVcoqf5FbhIldEIJa+{t
zGlWuTEhxqY>y{k9@hES5$J_bPhyIe!|II(A&tp8|M}PE(dGD{im%Z~dGL@rqOAccXQFluYUcb&Y
z#}0Gh!a0mAIsd{Q^`eIm$;*t%#)!V_XjdIYQL(7^xZ#%TScWUC>LvBAhZbxDTIA%#
zn5vp!LyzrS5P>Kot9pi+Xtu9AKv5JlJ1ys*zd-CI3QbW|_$XN4T0>=uD;LfpbihW3
z>l^|w2KpXMnG|oOz^)8NR!P|O0hA;w6+#CVc22fYGG42gUA}^hDR*~d>spo&SD*jW-`-(ad<+z4!B#e}0k|o;^dm^2n$WQm3u799&ZhoapGXmiPbB
z``9{Kaq`)d{KSv_Ea$(v10JT+jr}~A_lY9`AWO-zn{m&pZs)td_Z>X)$mgl&mS*1b
zv5))%v4&C`%B-Y!4pZbT>lHDkN{TH9$FaGr76tWtGW{J`Pp*3y0q8yh5<$2l5Z|DE{`TxX!
z{IMV7@dHbCkuU1@6)UBFLEDPf|&;yu=hamB^@`#-`bKlT~uK?IGGIi5&1O6RXJlD*~kNSleQKeUsU2MsM4Fen1^({MX<9zj)&LNBPJ{KFt5{-~Veaow~$7
z{N<;(bgD-B0&6`&WVEXmttG9i6JX1?bgssQh!zlAfvaPJVrhlQK`00=4enKyTun{0
zqU+MoHk!ibR)Onb_oBtwuQ@!*afMKd)-4&2OWL+&JjwX?|M3U-gFk#fdwYA_aQ&@x
zZNaDh{t=|in2guZMzgoKgH!>bBN2-(C6lcYUczeLu)MgU%%_aZnBW2~I*KYmXZL0^
zg7$1&J7IHsowLuK!md31Do}_59St(3n1ap)(Z{wrm)ahM>gy|@!FeB=@Bg;p)=;+&y-~zeI5k`WHv|+{iff1wWi0$odo_+i|
zE??LI3)Ogyh$OE{=JkrLLmLENBc#QVn3#96T>FPNSUPp)jP+=femKe
zF4Dl>mWW=?RH)lORODybkQ
zQ3$1(Y;0kSW^d<85^_{Y?>lO{fGi?Mir^$8Ce*t%#-zJ*FCvJ5T`b5=#QcoDmj_)emQPP`%K
z@xft?z|jy)Lp7;bELM!lwdAzu0)1ntsu8`jY;LY&`Yw9j;v7MQR9bG8`)}2^Pw7oP=HP5hA&qvOGOcUbU7r=Qlur|*Tue!(Kwgf)6Tnn
zHkcY*hH99JefSzbOY1c2N-5JItp^&bAM(ssSKG!Yj7hn(t7Kbk(uzFgDjj86?hoO{
zn3OXdGKK)&IkZVMV04nnWK6;PmKGQ7ei}{)7>{zwazwLQ5v(B3O9&ZVmp0llM!ZbK
zo)lyU9Tk1uP>sf@Oyjh``eglWR!byFxy|z&7r;f2LgKp~g&;FUI+%$_qbN)oq-BJi
z-7AP}$Oy*_DKwb?i3Ty)o>U~tm~6vkNz<;#%N%EyxUR>yjxaR0JoH})iy}gy;k;QB|WVRBV$2o^I$@Vm=MwGh1+YX&edf#D+DLOA$EM~NAoic4#
zBiLSGFpR5;-gQW$_pKYF(P-Z}(ew>Aw73|E-S7etur^&IlLqG^Hlz)<(K(ZG#cH;L
z6p^45i^dY2N1B4r_DsrAI)t^vj7u;YVzPIqte?d9j=pJhk3!;pa
z;~cLXyNfx84sUVk@;O{%k+vi&5^-GT65%bbv6whQcn}g|0A)%#+afZ@+E&GMZH*UR
ze38{o0~WTY2QboLadaVIbdFM*%e$A@+?*g}V7Z!O+aA|~5{g{sh?q$HLP1t#Y#!WZ
zv09-`h7^LP?+89nO~%ySlB}?-ZB96U<|3|(w9B;hB_xLcQX^%=6o#gqanJp?@bU-l
z=iTpqAM4X?&Yijh9)A2k{W!n-Tkq%j$6ll;M(A84jf70ly98eG*5bO3uB{Ogv`Fug
z7@*WSxhV)fU_+0oGE`=;-Y08fTeG${!F$VMIZGMd)?%a~MuoHK923GPl~PICrpI|t
zjDbAM2T-6HtiUOXQWZ(5T(#+fDu(~3BA-&^RoY$%M?Nl7Hg4G?q{QTkWwS^Y=0WJA
zPtKjPSjS`|ED;+Ui~-m85YkH|%0OTDUjtYQ$g>J54Mt}PqEsadsBjJ+EYe7tx*;Pb
z+okOZ#AL?`0zpZhl?dtg-7=HM(rwAda>ze5_2{xWEoa#b
zHnJ{#zQ*JU-XtYySCCu+qhiFoo`Z^v)=NAs#^kK#j<9rOc}Y2JFk=k+*4(QvIWH{J
zjWN#G#2B!xKw;>Y7T5I@S&sKTMO9&gqv^Y3Nzbx0FiMG$hHkb%D~*u`B~{wkDR8mD
zj7nV7k!elW^=uzHNKlcc@2KkrYKzhpxy%UOqqN?)y|;ajr=yxwSl1w=rCwSzAZ3MK|0S3eXy8Zu)EkpMTznit_B^`7Q54dpuRRp#~2w;COF&C#hz8SLKG02
z1PcvPBaMbAv2~C1l5sgn&);H+3@P){;Gy;CQAX@sa%Z6k9)y;tq9iMFTu1`NY`Mpw
z?E_pm^8%qy_mXn6q^(8M#dlJQO7@-QF%;D?#*)Rg&{
z5ERiR_}6$e9hyu!oJ%=RA1ycCaU&h*>
zH7VFz>=B&9b)cLf(?zmrDhSFGM8GJ4w-%|h#0IbqrPBql$iR7UO=7c1sfi?ap}?Rr
zLmw98RYqMmlx5D=fi-5cT^5TDDIqT=l*NRuv-sXK9#`xw_E4EZ<*;1NFqy=LbXg5T
z!orbFM))pL6jf^3sB(f2%r4I^#x6g8&ynYbK*n
z8aAXNpGDN4K-6w|cPms%&G
z&LyUYmTB1&q#`RTgwoh1;Jbc^s0gZQfzSb=py@4r-KX;$uvmx@qZLvK`rf5jW4=yi
z3YMz{M~)sMM$f4;r^&}7+PWq-jw&DF23Aw14SAW-UA0Pf7T+Z}Y6u}cH#)F>WR24o
zP7&HP_*c0`MMJK~M5pO%hYgOb%*o3PkE3yxpd#IT2bzG+Ah`72mV-^&dWVk!rxNHi
z+GgM;q*)-yK7B7{c*n#7M4sMbc@pcSjKsF4Z#xt!u^pr%k|IXA$#8w2KypzcrC>Z>
zqq998kIX#97`mpV*-Hx=jHK^6GN~99W2}v7@RvG?07}z!4N>+f)~N!*K))OoXGS0b
ziPNF4!c{$zbk6i$n&G_g18YeUdJjRMM52Sc=-9sI04_RQ7-E=My0%Rsz66ykf(>NB
zAcLmwlk+6c(?YXpmPjQC!LwM*@iCGWf?y+=mN*NADO2QNuy?zGr4)u}a#B+5kZ(&vRm#>~%^!sj(xjYtKSU7`nM#!-0>%@#_S!9e
z>_7ZZ^uFh@$DSe24P{oLR7MCfJ*XlA)T;)iGYAS56;Y&ooe=3#B9uVtbcp9!
zPH#JkJY&AMn;v2m5rGY!W5ZKE;xdSl#>!`EnC|MIdkR=%bk`Z*KKp>ohNwUf&2K5@BB_C<0+4Q
z>8nU#kXmu*$RRr4V|{{5J@CLQxP0*vSI+LDE0`WM-23YL*gmk$*)!+qJCE-@);pw@
z1L<9`n6FR+{36qevMh+sr)=|hjFO4?M*yKBAtbRPL|Cm>3E0vnpiiz!N>fpmB|gA-
zZA4X7``PHLK!U3orpC66*Tw`9((^IADBHHdS%*-P(P%=9k|NI%P=-J-0y8R*Wrnpq
zgn(26A9_rgQ+F++QHisj-~v)As!>VTbi?-^keNi84Cex)yo3O4Tcb0{vRfjxq>Gl$
zHr#gmO9CR>*Ejvxc$=>+Fm
zqVnuq*<&^Da2*(3;H^iAltb#RN1(`x3`AsYv%&|pF4*xs`UJb1nH47sij(Jv{6{sQsxGeE5?&?${w2m(QD5tNmBg?it1XcG_Ilf=^RDZ=;XIQmPij3{<#e@$
z2q8$EPa9xQB+HYK5v(U4Y(`m@(KQ`PC%Bf$3`B(#iYPPzkItYd(j`*{fk9(bj`IPT
zDYDXFOqQ(CO_%a*I-?jBc<&K-vMi@-EGjCL8#19XVDgL*1wv*N*@&*~5Hetl+|La+
zT}_POYezL2K?gb-*2;B)hoUOUvb0T_PN)0OnzAejA<}m}AZYeh*gld8gKZr}F{Z9-
zh-fTwKSdcP}=UGPIG(@1ta+H#|U|HW>=lYi%CoeO4XOUVG9R!zhq%rtJ
zT=(gBpJxTO?XkVbEhGKh5jz1v44+T3vt4D4T+Ndb1x?c?C(@OgX3rsl!naVU9Erx0
zY`s@qH>sMcpmQxj2I8W__Zm8YEU(0^I4pZfL30nuZ*xDHJKYstac*nndCzG`)kNxwbX=_M^mWB`_
zp?8=d@Lj;@44oT7=NOk2G6)bNZAzp>X_F!!B2rcr&O3^#V7XY3dVRok0T~rCNb;@e*JBhp*t;Kwo>ht|$6{>m7Ms?F+n3Tkq$|Gn4b|Q!fxY
z67wTQoF%<0Wr0?PrtQ$$&^9eak)w^I_sJ$5MZ~sYp!}-@M-&538W$T_OB(uF0)&_!&1d&{JN-Hvzv#OT~yeFX;
z=b$~hOi{LRHD+^bo3)K~-t~ju$3t&=h$o)LXVXAYWRzurF*#8PR;!w*lGqWmq@D*Gaea@JF;z1f
z4MNa&4N{5ZbP5qkvYF>)k!aQg1Tt0E4MTg^wFn$B3T&UAZ}08Z1sqZcy4DhXB+8U=
z&rQnYJ8S9sn%=jRqY7L1kQYcH>DnGSK$Tk8rGZIEY}clXzYm1kC(+e`myseb>3f?Z
zH3PFpDTVbOBy_GP4)F|9aEH8_46O%_-t|Z=QMsWks+6g2mPxSp5c@!;^8|MD5_>hC
zpd&$veL!8as>zLp=&`{ki@1b-)u#J?R0twjrcp*EenJeCS#s({=gIOM7X(Ey!gU=|
zD748ic}dp`R&|5U6r;(A5CgNl8P%vl28rt|naR?b=sm$Zf_EId{y2w@9OnG#GgL*9
z?l3mZE>Q~(9XoWDKyj<1kogI9FPAW-6AdRH$8loQ}ItE+^wrh!A
zqLe{uGno4VSyAHpmU0m8M$-`+2d9h=ROqpx4gD~iWFR0@imvSu-lv#lQKj!63)&{Y
zr|@{+6M8?igJ`tQ(hwdjJ~$A8&i6PQaEplV16t?kpfDjrMnzM%6nRdbr2%s`U*Nn&
zX%I4S?D#f^4j)L*Nv6<7lV>F+OTUj0BV}2oXI)54o{^OXQAWIQOgAcyTyuzx_4VY4
zX%n>C#WYKbI5bm;1ny**+Y+%nQR|J#Kx&jo%|WSFcZRhcWmce!CeJidNJNNiZydmS
zPgRr{oe>#YAhIMTUR~g(-)nk?t?iLg4b{!fFi)h|XBd`3A^80`vXqi~RS)N-N{t*s
z49|-GI#!dV$PB!
zqxI1N3hVpy67ZgCG{SmE8+u05ino9FJ17gu=RWrjTzC8!CvHE+KRuQqi?qFs-Xm06
zpXXJEcPW#oGR?v3uSXlhmD88$cjvh1(OR;7U^C@VgyG7ST|9y=SSDK)8wb`XCnKVY
z_};PHT`)hpNSQh*h%wPPqZBObB~>-TG#N@LoU}ygh*DtNjx2NZonvgq7?nCYUEfkD
z!)mt2wZ{%~<;o@UJdu`
ziRos+bhE&Vp3cI?!7-~YS$1vjv29P?_rz%F`V|pNHijSl;UD10u`T}gZ~uCSLx){XFuyM+caMPA?!S
zSzB968#re%S(emF1-kSoWs!|zK3}qtPY6CjP#|DjOvs}n0Cn3SqhwT6nCX
z5xk)5ZK~rEsq$>HHl`Ua@xgmK>yf2o>+qD@@41~|C13s0&W**&+D)J5S~-`t>Wde+v~Y1@{rUl3)F8Nq6|
zVLTZDj;>#%+@^!BttqPvX*9V=L$<;)Jy7yX@A+BY^Pcze-gkeHH@)t)-0{+zxpMgm
zfAuFH
zQ6jv-TZ@mLEGyHdQ70xr@F~CC)D0n6jvQIz)vtXyN3J`_7a#i+)AfvIH3v<)?BHpe
zjsph|vRbVOE)BSAYa_;^!)$G=vA(&P?EEE+De%1~AC2)bu)ev45R%E-h}m+7
zWwYYQwTGFC(ExymEauC^n^B&P0~3rf?Cs1bs|2vS{`%uwICq}&=Puy;h{+0!O!a<~
zay--;#ldl+$cqA1q!)Fjvh)J;J>EywrdurbW_SeYHq6nxw(ySKPdWF{DTu+(jfWjC>=RLSUS(V7B
z2z5=6j?M*S-l0c1(I!PTFAOmbLJ|-{L`O-P7AvlhCEa7kQ;mmbVgHbY~o!&$~?h$Jo}{mlv#>&eT&K@*WYjrAqXy>y-eG76sjOZ
zfsK6&Wc>Iy4AqtATBKq{6QDo>$CM$D{Og1OD5a>FKAlb2l^Z34}
zaY>vtLymYKT&5)XXqqwAod+e!vkD_UZPSvOB0W>e@qIt^F7jf`
zr#|^vzWA9h5c`M^9Y%-*$O=%Y478xBdqmV!;|b_UJ~nI~IEWM(GHT90_adv=93LUm
z8PX*1r&cA04_%A59hWX$ppYYa)qt?9udlJTw!y`Vm+@W7jywCcVLVym29Zf1{^Z=sao@`at@>`c_*uJ4EH0{0VTLlvkzm~_Wu(WNMZG}k9K2%dz#-gmi`to<%)pG%oNWfx92%*m$+PI6%52xp%?o7fa>OIbyv(YU@JoOa3eGCi=)=Jq--zHkbxrn@`?lcz-x
zl5$j$4+FXNmaI%2>+6TMSk6}jA8@N0q+&c8;fS=cBg;nM6r-}DP@1+~(mKazZ3Kl(
zv9Q`vFD&g|Lv(7$i;fUR(GP5!vdGaP&^t$Pmd3T1y`nJrh~9d$n^s#HaY6_mv$hmIa$u~<-zMl_2hlWL4olDcgXQgiCmi%>*fa{uid
z*gDA0#U;)yiaV)_jIa`X_(LDZcaCaQ
zq)qL7#iYy;(NT=Xm`u~z9$g7;d-=_L=l8yyHZ=50%WwbU2YB=!zCvCW2oaf7NsJLf
z(b^UpI^OwRZ{_F>Yy8eb
zwy~6Q#NPQUxW*D}WHOQv8F()(o11GaR||v)tZj_B?=^RD=-PvHPP4goh$p}N3?KW*
z-!j|XVPkWfOe7{lRZVcwa%txhXvKqXdVp6va357>ICl6N_AV~@jbHsucK3FP7(yF|
z%`PYvY1)Q-tT}Y#5cBz*`QC!gw#n&a41`G6b|{rZ{-P)oI6BX9jl;S`yhr#HwbdCe
zIBeIGtHkwk1LNju&w8Hcn4+Mr7kHO=CyRQX#Ec;mZQB%cOoOuAuiH)F(Zp!z`xSYf
z@Bf)$0B$R#$&Drkhn6JRm>X!dSM68TXhc)j*dg=mof|^iY9Bfkyk|AoOtdlkm09ZR
zU}K0xh!s%|)gzi!QzMP0cRjDZ?|xqMx>xcyANwmFd-5D7ZoLjKTAF@|7^u#+PuaPo
z3u$J?mz;PBk3I4ge)pF@K(lHot8%EeafC1^vYEyd2G`eQW6fwfMim+LqNbns=)j<4
zHc4=>L*18z|MNfpuRQ+5WBk(3zK6bV7#|u@n2ZxAP9O(>kI|a>e4Y-SvZQSqin63_
zSM2PrIDPJUzVi4NX$E`UqN(vhLg)#2#$}1h3%u{>x)s|8H#mGGWh@ULIn2HH-b;+0
zbLY>bin1ti&azl6u&pK9hycFug)gwTH)r!`!OLEK7vqCDQ8&yM7m|WWs>~pyj=>PZ
zkc&u{)Tkrh`)|IRuRQiBmrn0+<kw7S
zSf&nCmuyu&5Msav$ALo|^enjj?h_onVT&i9e1hGb9ejucF*vzIVAXW^(4{O?v*4zi
zuV;PZMsB$AT0Z{qPtfmL`fdT%>{~k9rlp#cNuBOGHVzzRvQgsWiY$XO=TGuuZ~Hgw
zT)NDs{`T*A;hBy?2(qCZT1Eyt56P{eJukiE7Dm$vXV32O{F5)z?AGYa5T(Ws-N1>A
zo2(~!p5ax6S1oV*j&I_Jf8=}ke}C)!{NW$`HPgu+T`bQ|h_n
zeeZrBwzYWMV!a|CRf#Zf49Xa$8wRZnPIy+$65BRIe8s2jGAjM{tRo;$nM5l|)1>OH
zOa_XH;?|q4<@S5;*D5dCK$7FlL`oT@s);D?Tt4|_=
z!nG;(qO=}z=<}f-Fm>m4wnt=tpV`|1LiF
z>CZ7gyMQjHi%>sw76YAg^f-FwK*3G79OuZ2C&=T4vH)1UY}CR~NR
zU5&vhjMjKk?$P@m*R~+w_22Mv9(wabv_1U%&;1I^i$i2jXyUNZy2`&XCZ}@_>pMi|
z$wqMfiR<`R-}OEG^B2C%hyVC5@GFPO5;@xUjzzoRwiCB-_si~NJRLDVHRsV6zr>Gz
z=?A&*3-@#U@F5u5Go(m0SUM&v{Gwk0@WGG%HsAb)H}Y-o{8sLJ@TFXT{f#{GkDo^r
z0@Ww>hL95LJ+^l=O-)v&t?%|VTWlO!W8=U&&p!8b+RA!p+YUrTX@!h|vM7iyU~dguLj@smIE<9zjr$C+JPaqi?L
ze&ZK^6T4`J_brSk6E2*;kYX#&BV=+-Y^+T|HvcmnOhvA0-~XGMCZTttSndF#F9
zHE((yjh{0;RB`9sck_}HxAM$aU*uPR?$_xTeR66IGecRHv~_}h*6oU{%=n-GmmlKk
zr=R4XKJz)QyWu$N2e!C$WyZ5lo??D^F>L!B-bX}8_F?N9%m{w#{qN)Q@(MroQ~!m_
z&+X!(qpB)as}*hAAhn{i{ctzT$SQ-$1Sf94p6%-n()FI5y#-OT-)eAG+)FJqsj(=_
zHJ$a`b6TaR$+aR7%lY?du+ZoJCO#AX%TD86guOux?N)qP3x{O0?3cYudW~
zcX@C7#PYf79Cnu6Wc&X;eU-AkU;p7f%jI%F?W_HYhwN&PmiNitEyTWk`)c;;zv*NR
zA@vpSzevCZ&&I|Evt@!)xv-+^S3LUY$
zZn>5lZoZbsAA1~x$Hs`1nr5J~&8}QYYyYyKcS~fMdXGD`$B`TFB43A77hXV*G_D!Y
z=FuZuzz558G(|~;G=aPCy`6hseh*Kde1^%!0bY3e4FCLhUr3b`S?YAVYViY5xnyH|
z#Et$4h%_MCJ$u>P!leaL3RISH>GC}
zT}%JvlkDuxQK2LfhkA%)`*AVlbakaL>x$zqy@unjILtLikMosBp5&S5pTR_p)G1@t
zbsbrja{Kwvk=S%Ay4fC^TWj2S^YwiEuRhLfF~^i9)hS7dcaFTsS*>P6|E(sg
zz(_Gj+%WBqRWJce2RC&qP#wND!*`4oxU5C2k$!EVzwHaB8OFVJv
zA5m*H>jw?XWllTqsj6z9sxM7M=MuY^5n|28R)zH$FTC&qJEtu#z3XMX{&lb6OJDp)
znsyH<^JLixsqr_<6+%jGzWH{Zd;S!^{%h~y+0&16`>nT9Rs}n|my9>zCgZ}p@x=#tCduHv)O)ip)?W3@C|Q&Jx5PmOVhPnIKRh>
z=U>2{>JYl1_Z}G{E(ClWUP>y(3(9dxFB=ZsxCNzS>-ZXbSJI16AQNGUY?625=&lN?H
za{H!8F(jF4qE6g$4M&b$%VN>+!qewyR=Wt9BZNwA0DYg>AOn?JDFLC!6pA;#^;MMP
zf^(N=oP6RmJ9~R6!{)<~$4>)CQI^;ssJn)>^)au0?cIo=Ir+p>eDHmLM%cfmxb*ky
zI+W4-)qB40x#`whxaOv9sw)~SddAf_eJ@qXe7;BL
z`t(4MEZQMjY&XHA3EU?X3rS&8r{eHTS=PpZkel;;An_
zgHfr@EQv6IC{ky$5JPscu-tX;UA*Pn-^OP@^;!Pr5B?hOA}hP3s>Vzv>+J3A(DzAv
zlR}_Oqzy5Bf
z(+BCBj!%E$i^%`xpLQuKH;@LR0F+>|1}APi!i~2cWcRYgx`q%VP2(9A6{G}7oXvcZ+#{AzT!4M`SU`uz{{LqGEUC{?67AO=o@NH+0YY7XStkl@X#hgNzR@sfxW$CkuI&lXkkvm>~
z6a80rIIz9V&9~gaC;sZwTs-##CT9C_hpy|eLnUMDTYL$xc<2?p`E3vJ2fzFKoIk$<
z4s=ZH0zyQGp<*w3be^&5=MV!2uifId>+a43?J;p?{M@58@1RXeZ
z{Q*wgah&5vZlbrA=mjQAAf~3NQ~X3qgiib*RS769`Icl*l;FxX{^b@aU*0JsAi
zpek|BVqMSXM#-`3uHogceSnXC)ra_jScbVt!UCw@&
zyt!7^UZv8mk}S)XWFyNPHfHND2AZLPp$P_P2FAcJGr%;<3=kb*x}$qyW_p@#RzuT7
zdjJE*ZX~ZVlC{~|Ri!G`UX_(qx!&!p?>X;$cu!u5=&6VbNfoNhoA;h`-v9DEzvnXb
zOJk1RwT}~b-p=EXeU;H<6A=U$Q?R?egE1x9bW9j{R1F-xeSwEQ{0?3|_o}ODCFDiH
zk;6yW+1YWRR9v&;&KQXhmf?7dxO0?y?mfiz?uav|Pg9u@mKrG(#yCo|Xk-1fR+!qI
zEor)g&|^OR7k|JPKJy%93Q`!F#=Wnmsgc&HpJc5lg<)Z_Pu>hkQwwrTT3ln2TA_s0+<>u90j5RH9%DuN0PBJZp1sbHTSl-{|
zyTAVdIoPxegUNJ?l%PaInvS_}?JVDN=fi{@$+`2V
zxPJW_O=S?Zg}Qmm;^dW>rb2s)UO(n*Pkxzu-*qQPZ#hUUa+nF9RsD+{N8$R;!Zzmb}
zoIn32NfdM2(c5|Tr89i#Z@=o)XO*1!l=r;OP187LglJkTu$U=g>UI#}c^*Yt;`z+j
zIC~MuMN!Z+b=!;9Z_&QXat0@pEdX$4Yu28-NtMg+c3)a~Yzv`CyajE;_3Dfgkxe4}Rc2h$>FpeU!Q74tUJA^m`z*J)ncoaQ)_0
z4jkK0Gyp;$}qy_FEvw*);2sv<9@vxmQu(s`ZR
zhe%OWq-jcjzDG&Mh4nYsE^o4Qu*=+Xg7j;wtXm+F%M#bhH6hxAIPviV!KKS*Das0J
zxVCnMs?8NF3e(c9og7?y9$^@fBne3z^W>9X=d+)Fg3FgTSX`WML56$g*JhS$D1>lv
z17(RZ1=>?+DVQ5{@H|0LWYo=G-m7}sGo_|74v6DuwK@HMmt)5cx4;SyAuWFBaroF_
z7MB;Ck6twRkw=t-_)&=GduXN5%K6jFss#qsZfhfCO<7NwUyOP0Bk$nuleciY3jg#$H6?Iu*Oo6c_hi_lyM}Fq}x&M8)v2shFqj#-x
z==OaazjM`*XItLI-gPBg_)Ae&SYOdUyhyZ~aQCD4aq9!OQF#@)t=Jv!lBQEOH@6(I
z(m2XxWelTq%>JV*1dE!bBV9Vn9y{qeD+d>e=6fy%5KG;-GsQL*<#{AY;s}~$20_E-
z^ah1USy-K$-S>6VIIu~(U2f}fnx<}voR0oH*YCHKPvh<%;hsl(*O;}|{hJidSD66X
zvj5ONdUFX{3#e#iyzY8(sQ?ZdmRBWdp3_~3`S5prh@bemALSQ*6o?a
zmw4{^uW{q%6-4m%Ol^?10aMPJfJV5+vOgd5tsi@oU;C|J<`;hD6MXPH9(7<&VJQnk
zQB;&=-h%Qf5GC=P;)g%+z5LkE{SZwj=hk-}p|=uo{?geQlj7|;_hOHyrWHkFIC95f
zR*o-_EXT|p=phrQJ`u9b*S0RTV2^g{d72~%nOlhX#!F99j2loeSnPB6eRn&0yR>M}
z`B(R{%aMY)g@o_;?ho_d{OHH|j*ovEx4q*|WT>%qGm8Y$Qngv41{DabXegQjzvHq0
z=n5bB=p#J%zWe#$x4HMGp`HzE1@7+^RY@ZaqueDYeCI#@2=D&TNgny=yAd(aSfV7P
zHnsDWwradRD(rzHt93Hg`8@tn_JF^*L3`7W|6l&HYaU-0pKSFqDqY|CP)t)R9FArw_v
zVnstEONiiK{Xf4&Z`tF8*T2ct8<#n8#}SU+ascHyOO6um`B9fO7tft%bL%GBlLS4_
zZM-Zz{`eQE+w5*<#d_Pl*bc>o5Ip(x*ZJ*#^DiNSOINON_0nZ7U$}y-LDt}F4}}}x
z6-B{xnv$kt$|`lLyM0SYWiiH`t6>t)?gb~?kYs5=QRV1JV8e`~cP?|_&UtRV?;tv9
z(Cs}{6a^a_8>DGEi^EaAL`Rx&F=qdv74ANHH>!oA?Zup0E6_p{`T1079MS0C54
zX<0J@D-4Y+@w<{z6>Lv8@na3fedc9p7>_42@Nb^wC?)CjI;^c<xZ`o;*gh7PI;^brnHwYy@@5*U(t*i@cC|e-6@j$ch;DExUgkk9F
z*Seu7GFOvY+NGUSP)2b;S*47|o77F}0A#`qdqgVb{$7@5_-#a2RaMlrY5&BADa8b$q>E6Ryah+0Bt?}Y6+HT(N7%Qzl
z{^XB8%~!wrBvolBGegwtv9fQ4B-xwPCj^0`@@mh8(?9sGcL2~?f%_l0o!*>wH*~vw
z@dM`pqp1*01C=2R1^W-}M`+j`4QXmgSu{u+P-PH$K3Yl?f;`PJg`u%6@mxSBfm7$+
z;P$(2rMKK?l#kz%pn0AvjDh}KpD2o{ZOz8kW(y4|Svc55b_|6~sVUuL*l*)nl%~_^
z5JgctuyEIu1f;C#&nGM&93X;*tjf?H)FxwYFy~~KZDw3$DypiTns&R?b&1lFF!Vv<
zw$JSZy?)!FFMz5r1fI{8tCuKjPBa&A{LTaHKemLaGxB^&>;+UsLD+81F(9O6TuwQ5
z*Kv@pIgjFi!j$ce=u{Sa)6~6RRaFs20ZIviZh(pf%Lf-2tn?_$hNhM00St%3nHs|P
zLN|rBk}|8gzIKBfI~#Q8JDhyyJ@oo9#+C>zD9ijUwn1$ekH-W-z}(z`_4PHjcCPc#
z!?$zd-X#tnIf$uhc6TP&MpGL_({?y}+q@)65K_!+9k0qV!4{ipoE~??b7dbkxCLrE<;p%9;T{h(zd!Cs_c22v{pzZSzcadWn~4aBx#z>
zGN$*2gSKtxgp_1iijp2-7`y+!9li+RsElqRS+~V_&C+U*Bggk~@X#VrqN$s*g;B`%
zA?`Bhi=rUU-E}lhM@*{`wayVwm+UD!#jA4)RJjlpf&iuW_fjqeXFbV`*XBlkak#SW`kg3E5ane
z1_FN&5iBMwpIG6Col
zGdNHZC#||m(a=VWH4Sm(o*z#>`2?T()bH`it1mi|y>ha8&-c-u#*ZVC=&jA44Bhs9
z-=RhJ9bRH#vCGwKms{JBCI})&-fr54!xpYlINImI_uoSm43S+pde<`6&lyj4u;#6N
zWCv$yp>J8{hCns+7P|BnyLgEvuX2)Jm)Ql2oDG-DvZSdjRb}W6dOZ8ea}+w`Pb!z|Uc2-Y5;nE$*`5*q5f6AoX;PUzfwzlD~KJ&NK)^ht@w>hAz
zQmwVBLDq2b%sP)f_Fp)3{2+@*mmqAwhrvpRX*pqcI&3BDmORgqQniv)S0i1#aE|wV
z_`Uq>|N7tY$xr?Z{`#*z$NH6H_PRL<^ebBLfZ`Tco?_qkhlb9q9iIb4|L7zAYv5n&zXg_q>?o~~ZSJaJDk_hRB
z;43TpIDY)NyB0OAGE}3LqTA^bh9OEh33QgZxV&^a##+PCqlZ{sU3S~OSkGjw`&U<6
z_>!D0d-`)-rumq(81ak0^a~6Y`;3P}Y+X}iInzl>QDkIU>V_qOhmtTD^y&Az6lLZ(
z3)*R=MceEfd%Lpxkli#^T}vO*_n(q*JETbT+8(^*Y3f#~pW^;MUuYA=*@!+PIoSDTNmX
z1W`z*-*ag}bxqSiuZ1xQ@Ca|>2x@F
z@E|Mu7U^_7`g0MzevGxWFfvQ0)1ljS_LU$A5E|~f`wkWt=Qw&~KgW+9X3*=iv$^f;
zJJ!8kg>aeYMS*Mwnom6O1kXJ4O=mIll;al33eRtl5}L+1$fcEdo+9bQZ7M;=!l1|V
z&pyMM)2Go0(%lhF;o{)-`meg}x=i6S9Qz4ND>F}lSK;(+uN+Z-2)xIU9#3VIoMvrhcSCzVEL9Oy8R)1&!eiU
z*&!j7n$chPrUjjj=J4Tz%r6Xh;9d9e;6wYk@80`SBA_f97Z)QnQhW3V^H{0fmP5e4
z1N-=%@A)1+_K}Zq;`psB%`YI82IV1yW@)fQCr*e$7tJNKg3?i^SCm($u6@3uh)nrqkBxNzwbzVbQ!$|)CHAc
zW$O{KB?yD98>-CG?+;L3K|2O9&xxX#Je^`qMHG8nx_E)%aN8BkEj%F4b0?jzYpSxu)81^$
z(eDk2qJ$vwNqRAHx6^L-j4NugoZX$FBkmfv+I%ZqJ^%LBsCRt
z^YheI#oCoMeC2peqAffd;bh^Ba9QkrJ51Pn5O~^y%E{~N+D%23*2GEj7F9V6@%)fW
z=WpE5(cDZ1S*S|~7(XB8LTyu`(em+ANW+;h)8eDH%G
zq}%E8yTAMUjD{&n#z+y8#C=zsD@9`)c7{XpEa%o+Z=tuWc=)0Ba`3=WPMTU$GvKX;k!o4bsM6XGDmRxUnn5B4CWAc;HFH8WCUkypI(
z%4>{96XLK#5JaTolpAX|2)&Td3-P3fmYVVIgtMpL#l=OkEO%;%vYc(>-C&@Z6=G#s%^tk9h0?m>sWc_VRxauz3C`R(0Gi7lUAMJSPWJ=`FI#cGo=9*x^o@o<`+<2fc8BO
z9N3Q^Xmm?m55usfah7c}ZSX^djsk+jP6Km0KJR}T@0uJfnWhs4gFad*Ol{h;+wkU_XDCdH4lEz}u1ERaAN)t)H=H^5
z2HQJZfFmn=o@~Eg}?=wTZ-KueN@_kPQJ`SBnBNq*$N
z{ZanrGoRys|Mh=KnS(Dwv9fB9=cH8D6
zag^tw15H&y(HN5c9NqbOy8St*71qc-2)&E*^L^qZp|N&$)=C5mg9Wafzs?sw|5c=b
zFb?q|4?IB_2TZdmqsh1(xNATX`4NNuB6(i2va+B1?!Di6WQ8J*yN-&iG`{b(&qI%e
z`2~hML%Ko2bSK3Ywc8CLuxbak5Vx#R_@oH}4ykxdLzC?Y>%^X3-4PM;*v
zvjv0iJBo8nd)->W&GlV==l}jgY~^$R$p`U$_nci@TcfHBT035VZavnfHYnv&S5V|N
zZ=StKQB+iA#mdSG#E_L4LW>yzI|x0bw6j_;NqQ*dv9z?pyB~Z2*%I%)FhD35o94b(
z)o!M1(rHE#B=q7r;%LBhQWFL9B+B
z)53)W`<};WJVj{Bcs%CZn-|#5I%LxnS-U6zCO1*V`G?gWvPDmTDCG>+nW@?yhPOxK8Qsa9b*)&CK
z#WYQ4G`*&&(aNJN;L_y{&Yru%V15O&ci9S%(qlZ%SYAFrk!6ITavNx0v3Bhy(@8-v
z7Dy2?nPgCdjwEH3Q3&>`{#rp&2xLs=VMed;=gCw-R79>blAPB-Afr7PG5syw5p
zW!qFrlCVQojk&sZjT_@_?tkCAq4y{BmJ|FaWPEeX%inm#?XPdILG>sxlD;ljR%Npqkyug9B{LrV&8!lY9%FXo+(rJqC
zyIkNKYg^Q%D;Sm1RCz@w>d;ur#`*^7IBf@E6;gO~x^eqVbMjzg45MMrkwdpL9UD%c
zdY=34zMpPqKvjaREXcauOeyC2ebUJ;r75WuY;9$nJ-^1udv4|Mk>fne8Pc?(sRU6N
zGB@Zss70-u|5RzpO41uFkQW8LUWa}!#t%J5BhnJ2!s<4r&xT~vlyoF`;<1-_;!BUC
zfaw_i?V10`GmoEQdwqzsK^ws#sD;}~S2S+xF)g|M$eo;e_7s;cT;$3tmnd%J=uEe{
z*)@6YHfDPhUsby^;{2PJc;JzDvOKqs@pw#K=d52^C$O5THYDAM;c&>p;v(QAWZ|DaHz
zp=k=rET_x@dYvvsmUHHnGYqe9I8SJ4sbtkET@1eO=;d{7DCz>^xsPmPZH;Sdmx#1a
z;Q1&m@MYLa)t&97YKL#NsMy%p;PmM;^yd@qz2`3OxYMWC>u~c*ir_6+UyYUPGNrf4V&%gMXm$!K%Jb6&8Aoruo#lheoc+c*XB$%i
z!oGD42s9W&k=AG;s
zE%C~8XL;@UGh{m{suDzrPnP9KEAc%KgQYYEV+!g9@}j2G?^9csM{7+@PKh>}s;)_T
ziOYMf492$B8L5~|4V6*kg^PLFd#$d(Y_K>$Xw|rL;N9=Omk)mEgG}==Pki-hbl#!1
znkT;W4f3)j|2ANox|LEY0wCM0`0*e9X@2oHf0h66sXs(k&bR+R{`Wsid2G|m#_WZSFkxK0+2oxbxX!|3mN4r-tmr;yz%BKHpgpZ
z*@(fw*+-5aKgt*CCn0m$zD*5fRZ`atxh+A%aA=uKB$G7d*(Xl%kw?Crdg?(2I&_x0
zvMdSPLEoM{waE&uoxRHCQ&)NE>!*-L;DtU~Nv5_Wt5bCBhND$kV(JE42`1Z9uAaZf
zES3_JK{=^dJHN@dff06q9i8ErXVHzR}NB)8qU3Oj>~6m
z63D;}mXwRH+l%IWt6S9AyyT_l&at@qEGkPdBcJW@m_R0!Swk*M2h#G}h|x9|-1jwF
zXkLEy40EdqFQ0gW;cm+APKwe2N(B_TLG)S(r!A?Q8s!VLrwAiWs65K4VSFRy$uB-d
zH3H8%QoI`)xgkYe8Md|^1TjwLp)7d))$?p`k678ag!WvbPf=8K<75V{uIrj4=(4hU
zh|{NDWA~D?l798EXSsUu27!txi<+nTb)IQo)4AYb#4*1p&e~c?@7kTO{-(-7Z#GBLW2nn62=Q8b#
zn}mDXBh6BbwFG{`v=}nlE*XxtP{POa6PmK7sTvCF2-uyZ$A3j*
zBvSYYrLk__hYs8prmQQ!W^G`9DTj0#8GmN*!U?2`6!Z4;WPIf2Ssa0B4
z{uBdXHy{8KORkq>Nj7?kY+ScstAa3!$+E2V&NMUv{4k&_Dt6Y#oO}H$kx1CRF=1zOL|ry0
z>G%`V@z`zmlwy(<$j}|AmoKbw@yZ1b9$7^Z5aRh
zcu_S>Z@}L__Dy2X2cxh;xJ+Lqagnr=I7(>zn#cd*F_!i%^32~q$#i{!-EK&_35BT;
zs+G=5Ig`FtrlL*_-mc-|t5;C9i)H!q|MVF)E^kv#K{T4Y_3h_*j#6&3=_$p=<|e)h
zc>jAo#8c0IjTfGNl{@aZiz=&W(smu_d1P5m6vo6!JmV_lc}iItHf{{r9d1+Q4WnU>
z)}e#RSG6c)rmjOTfbvmw3=dHI{CdFAy}L|(+3FQ2EW3|gx8YiDS!TlG|hRD!aB
z@oviI)h(XOzQN1Syujr%m!WVJ>?nw-TXmKYtskr?2!e>F8uR*#Z}L0;=kK$6U_ZCq
zejiQNP){s*WLyN=+dSV&YdlYpPIDgr+b@w#x4V^*7cjwo80`=UEkR^H~cB{DiU^^5*Gly!4GzEH59#w;|_V
zxxyPSUcwZhT5FENSz@Y|su~0leiT4ysWZXO)iGcByRWl$@douy1=gd+kVFY-Iwt9K
z@TG^<(DM|#dCFsd^<_MK=KBk5Zw>j2zxb^4@8<%eDrhDC;E2{qr-LbKUjF85{K2Pw
zkKNIjh2A2O4ylF9SFUY?_Cjjw@|C6UQ{@$Z^!tCxXuQdV*RGJ>sQIOz{tX5P`tCX5
z`FM^0Uln4Di%ab0JACf1zsTb90`GeGUbb)SV8%7%(1aE#oLV9bU8cA86iSDT(~K|v
z?X#SI{SD$?$g!hG`Ql^G;2A+NvMeOM7KW$YFsCdLN)h>rX5;CYtICkVtE??QE%ANEcE2y!kJ=i0{`8F*CUBSKg-j8Y`
zKKGZO7<*D)dX6yb$N$h{P|zz=q*Rdb|$Qy
zyW-S@!h>2st(;e0YPVe#ipl1b|LvE5gUnP+M-#|hM5dH}yDe)FN>Vp9olb{Zlmww7
z2o?Fd&kMNr<~pHNRJy^Jidwkb>k0?KESrkO`2pM4GtQj8z}Zu0`SO4M
zCS5NooBx9
z(d+dXPb|aXm|ywlzfMt(DbfZCg(nqF1)>&sG9XI}uoYT^HE`jL%WU1;;@Y(h=iC^!
z@idht>cmu~YlNH1kQD`1Kz}etT?gD)+v4h9e}zFmp{X*y@^?@1C%^j{iZ*8*tI%Sp2}H2RUVIjUW0LY1q0x
zWq32Am`ZlHQlt&Bb~x*4bl?-l5!30EEX!RIMZeG0i|hO!zx{hObwQIWvI3gY4U~#D
z2ix~Tr1bE-5GyLGrluJ0@XXUMbLRX7wnp0oxRMAZB;7t)KH~b-
zb-e8wD>T<`Zs3W)Em*X6I|w1#CDz*peLCj!OBdMKyuslE`?-8}9h)kqS%ohGiZ;5^
zkDSuV6lL2?R!|GhzrI7TzQgY5uUKB#M?PsVMT6%nywD|>_+G$hnj*Bs)COM$XcMx2
zVT04ppW%hCzsR{$Yxn|aBnZcG5W+3P@+v2pla!`mb^kunxgOUpUF6)Gmz??lw^`p)
zD({`$b?YJD*%`6BGh%UHjF}pqfBFULQc#x`TUw_wY_py9e+9g*odnor%6JFsr6Q
zx87g%wnA!;(j9u?%<%1?P~J@Tog@i)?tn;M7+@RAv?Zrm=^~Iiy@0i~8`PC+peq9l
z%L`PEVYD+L@_K|p2PwT7jHsw`(sD#o7fw3~kVBwjmkCLO-;J=I+km-A=!85S(Va_(
zLZ399Af=|vC5^H8jUez`-nAcv)L612CpS6W#U3mB=XvvuH^G1>ReJ$I7{r*uxU5GZ
zQCg6fg@bu0MVz>-Ro@TE(u!WxrG#G9usf(}{Ue-PVP@*;Ibo97{H#b~s_qmMp}5bh#aTffP0Cu8TzmTNGh1t(+o
zYpNzkX;>HxnCy%}3Z`{|^4;O0gmw}xy9W=zwIg1}9f7Z>NLnu_h+A@RVcyXvvNxkWPqukp##hB)k!r6X2XmK?0E
z^^v*IbnSeXl+3Tpaqk27G2GeZ!mAf3#sxxn6nW)5_CnC>^(eBOG@VkGIXYHUCTC%x
zM<-4g?Uv-3o9f%9Ey$XNz>f$$k2D|CGzP6LR@JBwZaHy`YT9t&jmtC@bfP{=DH<$z
znn^aMw1&Wq_ag(MJ$T~#gxrr>!$CkA)5NOc8Ana;#RiLAQ(Z-Z2
zHH0#RM$lTi84L#PkgA!2PF7tUWI-LXusH3UJ3!Y7@KSU#|yPA{gc
z3MScb28SCDM@Sl61iWy$*j_*oMD4>*5GNtS;SNEpT?|g5nC4C;&b9aN4
zl_fmo8f%5uHVX}PRm`Fh_J)3YzPP={86;A86ovCR27x9FBXpohP3AyO?fI2WGPgOY
z1wktVA1p4r32GR*s3cJ`F2*eGA8_a0x3RRe#Kw(Hp8fk5sHTRwZjZ?%ogE}nh2)h3
z|2*=6_wdxSU!#~z@dgn|l%Olc?#2*nB%XF0gvMHwa6gCDf^j;cC+jaO6=>(d%@u
zMMGT(ilU~$`Pj6Oh`^(i6@C)1ySeU=qPYbn2t;P$#>jEBi)8M%S&!v*<}6N1_F-Hb9dSmS)g2wemrL!*0
zBxO>OrehWt`dq(x0}()H5OB+_Cm8KcIrsWyV!uaion0mhTv1n4t`V!6f~qLd5ojr~
z229a_)kxu^r8gT;gkgv$6;)GFN`nd|O(dLWZCD~}K^!EQ3Tz9u6Rmu?svMxK_A>5x
z=dIj%@)kBWZ*c9>b+*^X46jUF!KedQj8_gc7bPLmQ&hIWOEhUV#N-t;p3C4C9$Gkc
zPtzDYrI;VglNM7aFZCs9ky6Oq&SZioZavB~
zPd|s$uon+5jKKF|lowDm2Hnv}Eh(#%+T?`YgnTlA%0d8A3g@wlTyab3pizyrGn0wB`qY!k0
z9=`O*a<{pcR?-N_ij=sUP*amm$H>S**OYZveaeZwK5Ac*5W@+EYAGplm(P)G%4Kxx_YnKerNThVHTL_ERPHJD)g_Fc*
z8C8)YwMJNpCqp-Ashbw`V=!2PSW}CP%wh<(~4y7>+78VKpfbq^YMKNVsO{l8OHMOBeHa?*Y(ZZvyDx!YGWIU!ZW_B-H
zX($Urw5s`*_ddcmo_>jD+_+_ga9cIs_bDnDR~ZBzQVFJZN_;3`ny0WBkm4O%q_SrY`_OtqR$3ZxgI
zaJB;9Q)Jl$V;oze5#R@ri=nG)CZk@yPT>0lapEitPV3G%9Z}kp@BR4q
z@W!iWc=?4FT7x=7%X5@vjVQpRhHls;YJJgpo+G5Cs!JLL(VWln!2vtNAscHuEG_TH
zLowRgCh#Nb8s?W4+1lJBYbn}F3%cEi>o?b^U0;r;6jDS4e&S^BLQ$kn{@&~LT&<9g
z@w