Ivan Gavran

I have a question about the simulate command. The context is this: I created a simplified version ([link](https://github.com/informalsystems/mbt/blob/8b8e346cd420b85b9788ab03c95c4dbf4071a7cd/research/ivan/easyModels/examples/simplified_token_transfer/TokenTransfer5Base.tla)) of the token transfer from apalache workshop. (The difference is that my...

Problem running HelloWorld: no upgrade path to the target dbscheme

2

Thanks for the very interesting tutorial! I was following along and failed to run the `HelloWorld` query. I selected the database and ran the query, and got an error `There...

We have a detailed README at the moment that contains all the necessary information. However, it misses an emphasized comparison to other testing frameworks. (Most of the first-time visitors to...

Currently, our tests are executed from the combination of the abstract test description (ITF trace like [these](https://github.com/informalsystems/atomkraft-cosmos/tree/main/tests/bank/TestDrainAllFunds), often generated by model checker) and the reactor (like [this](https://github.com/informalsystems/atomkraft-cosmos/blob/main/reactors/bank.py)), specifying how the...

Integrate Apalache Chai

2

Currently, for interacting cleanly with Apalache, we use [modelator-py](https://github.com/informalsystems/modelator-py). However, recently, Apalache introduced the server mode called [Chai](https://github.com/informalsystems/apalache-chai). `Chai` would give us the same functionality as `modelator-py` but would be...

[FEATURE] Easier debugging of TLA+ model using partial runs

2

Anecdotally, an important part of developing a TLA+ model and debugging it is using trace invariants to describe a sequence of transitions that should be possible under the model. Negating...

When running `quint verify ...`, the resulting ITF trace does not adhere to the ITF trace format: instead of being a JSON object (`{...}`), it is an array containing a...

Adding 3 convenience spells: - `setAdd`, to add a single element to a set - `listSum`, sum of all elements in a list - `listContains`, a boolean saying whether a...

Consider the following simple model: ``` module problem{ var x: str -> (str -> int) val X = Set("A", "B") val Y = Set("C", "D") val Z = Set(1,2) val...

ICS20: Correction to the denom in the sequence diagram

1

This PR addresses one imprecision in ICS20 README that may cause confusion in otherwise very helpful sequence diagram example. In the diagram illustrating multi-chain token transfer, there is a mistake...