One thing that is really missing from the TLA+ ecosystem is a way to get a convenient json representation of TLA+ source code. It would be very useful for many reasons - in informalsystems/modelator@a351c2f we do adhoc parsing of TLA+ in many places.

1. Parsing the states in TLA+ traces generated by TLC and Apalache
2. Parsing specs in order to get the EXTENDS list
3. Parsing Test operators

I think there might be more examples than the above, and I suspect things will end up being added to the list as our work evolves.

In short - I think for the long term of the project we need a robust TLA+ -> JSON function. This issue exists to gather thoughts on potential solutions.

Many partial solutions exist

1. SANY - the official TLA+ parser.
   It is integrated into the official toolbox and works very well - but the only external output you can get from it is an esoteric XML dump.
   The command is java -cp tla2tools.jar tla2sany.xml.XMLExporter -o spec.tla > spec.xml
2. https://github.com/tlaplus-community/tree-sitter-tlaplus
   This is only a treesitter grammar and is information lossy (cannot get identifier names).
3. https://github.com/tlaplus/tla_python
   The parser seems generally solid and useable however we found an issue. Moreover, the parser is a translation of an Ocaml parser and is generally opaque to read.
4. https://github.com/japgolly/tla2json
   Brittle - does not handle negative numbers, for example.
5. Apalache parse command
   Apalache leverages SANY and can dump a complete .json file containing it's internal representation (IR)
   The command is java -jar apalache-pkg-x.x.x-full.jar parse --output=out.json spec.tla

I see a few realistic possibilities

1. Leverage apalache parse to get the Apalache IR. Then we should implement a proper transformer for the IR into something more workable. The downside of this approach is that the Apalache bootup time is slow - running parse is not particularly fast. This method looks like TLA+ -> JSON = TLA+ -> Apalache JSON IR -> JSON.
2. Leverage SANY. Running SANY directly seems to be quite a bit faster, so we may consider implementing a transformer from the SANY XML into something workeable. TLA+ -> JSON = TLA+ -> SANY XML -> JSON.. Ruled out based on @konnov 's experience as being too expensive.
3. Expose the parser that we already have so that we can reuse it more easily across projects. (Implies maintenance, feature creep).
4. Use tla_python and fix the issues there.

The above four solutions each have pros and cons.

1. Apalache solution:
   ➕ We are connected Apalache development
   ➕ It will definitely work and be correct as it leverages SANY
   ➕ I think it will be easy to implement
   ➕ We can already get Apalache traces in IR JSON format
   ➖ The runtime cost will be high for each invocation of apalache parse
   ➖ Cannot parse arbitrary snippets (Need syntactically correct TLA Module)
2. SANY solution
3. Existing rust adhoc parser solution:
   ➕ Parses arbitrary snippets
   ➖ Adds a rust dependency
   ➖ Not battle tested, not feature complete
4. tla_python solution:
   ➕ Parses arbitrary snippets
   ➕ In python
   ➖ Not battle tested
   ➖ Buggy

Please note that this is a blocker for further development of MBT-python - unless we do everything adhoc.

Any ideas? We could stick with mbt-python of course. I'd like to finalize the name before making the repo public (
#11)

In abd3912 there is no support for interrupting long running processes (model checking) in a nice way that will return partial results.

The problem is that modeling work often involves a lot of stop-start, ctrl-c, ect. This way of working should be made easier and smoother somehow.

Note: I don't think this problem is easy to solve in a nice way

Approximate location, for commit d989ea4, of relevant code to be changed.

Relevant TLC issue about new format dump feature.

Context

There is an extremely basic unoptimized version here

https://github.com/informalsystems/modelator-py/blob/bc71f46f0e0cfe85843c63d46c590fce51cbd0fb/modelator/scratch_subset_selection.py

, which could be replaced by a more optimized version using some efficient array encoding, by for example using numpy.

A real long term implementation should probably be done in Rust.

Issue created at d989ea4

Suggested location of code that would have to be updated to implement for TLC: here

Thanks @rnbguy for the suggestion.

Tools in the python ecosystem often leave cache directories (__pycache__). These occupy otherwise empty directories when changing branches and get in the way of having a clean workspace. It may be possible to add git hooks to automatically clean up these empty directories.

See this [stackoverflow post](https://stackoverflow.com/questions/1504724/automatically-remove-pyc-files-and-otherwise-empty-directories-when-i-check-ou

and this gist

python to 3.10
pytest to 7.1.2

2285f5b only explicitly supports unix like OS's but perhaps some effort should be invested to support windows too.

Supporting three OS's is a lot of work though and requires rigorous testing.

I am getting the following error on Python 3.10,

Exception ignored in: <function Pool.__del__ at 0x7fcbcb5e9630>
Traceback (most recent call last):
  File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/multiprocess/pool.py", line 268, in __del__
  File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/multiprocess/queues.py", line 375, in put
  File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/multiprocess/reduction.py", line 54, in dumps
  File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/multiprocess/reduction.py", line 42, in __init__
  File "/home/XXXX/.cache/pypoetry/virtualenvs/modelator-py-5E8ZuFvv-py3.10/lib/python3.10/site-packages/dill/_dill.py", line 573, in __init__
ImportError: sys.meta_path is None, Python is likely shutting down

the problem goes away when I switch from pathos.multiprocessing to in-built multiprocessing library.

@danwt is there any specific reason you were using pathos?

recordclass uses c backend, which fails to be built on a custom build/ci environment.

dataclass offers the same functionality while being a python native package.

The TLC output when the invariant is violated already in the initial state (such as this one) will not be parsed correctly by itf.py.

The problem is in trying to match the exact output (which was taken from traces with more states), here

This is a rephrasing of the 'traces/tests/counterexample' etc functionalities.

In informalsystems/modelator@a351c2f the user flow for writing 'tests' is as follows:

Write a spec something like this

------------------------------ MODULE IndicesHistoryTests ------------------------------
EXTENDS IndicesBalancesExec

VARIABLES 
  \* @type: Int;
  nsteps,
  \* @typeAlias: HISTORY = Int -> [action: ACTION, actionOutcome: Str, balances: BALANCES];
  \* @type: HISTORY;
  history


\* This predicate extends the Init predicate with history tracking
InitForTest ==
  /\ Init
  /\ nsteps = 0
  /\ history = [ n \in {0} |->
     [ action |-> action, actionOutcome |-> actionOutcome, balances |-> balances ]]

\* This predicate extends the Next predicate with history tracking
NextForTest ==
  /\ Next
  /\ nsteps' = nsteps + 1
  /\ history' = [ n \in DOMAIN history \union {nsteps'} |->
       IF n = nsteps' THEN
         [ action |-> action', actionOutcome |-> actionOutcome', balances |-> balances']
       ELSE history[n]
     ]

\* The view for the tests
\* @type: <<Str, Str>>;
View == << action.type, actionOutcome >>

\* The set of all actions in the history with the given type
Actions(type) ==
  { history[i]: i \in { i \in DOMAIN(history): history[i].action.type = type } }
    

Test2Steps ==
  nsteps = 2

Test3Steps ==
  nsteps = 3

Test2Claim ==
  Cardinality(Actions("Claim")) = 2

Test3Claim ==
  Cardinality(Actions("Claim")) = 3

Test2Free ==
  Cardinality(Actions("Free")) = 2

Test3Free ==
  Cardinality(Actions("Free")) = 3

Test2Freeze ==
  Cardinality(Actions("Freeze")) = 2

Test3Freeze ==
  Cardinality(Actions("Freeze")) = 3

TestIndexTakenWithoutReserveAndForceFreeze ==
  /\ \E index \in TakenIndices:
       balances[indices[index].who].reserved = 0
  /\ Actions("ForceTransfer") = {}
  /\ Actions("Freeze") = {}


TestTransferFundsViaIndices ==
  \E a1, a2 \in Addresses:
  \E s1, s2 \in DOMAIN history:
  LET S1 == history[s1] IN 
  LET S2 == history[s2] IN
    /\ S1.balances[a1].free + S1.balances[a2].free = S2.balances[a1].free + S2.balances[a2].free
    /\ S1.balances[a1].free /= S2.balances[a1].free
    /\ \A a \in Addresses:
         /\ S1.balances[a].reserved = S2.balances[a].reserved
         /\ a = a1 \/ a = a2 \/ S1.balances[a].free = S2.balances[a].free


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

Calling modelator trace IndicesHistoryTests.tla <cfg> is a complex operation. It

1. Does some adhoc parsing to find operators prefixed or suffixed with 'Test'
2. Creates a .tla and cfg files that extend the original spec, and add a logically negated operator
3. The new .tla and .cfg files are checked
4. Counterexamples are parsed and returned.

I propose that step 1 and the overall user flow can be changed in the following ways.

1. We no longer use the terminology 'test'
2. A user can generate trace(s) that are executions whose final state satisfies a predicate P by writing an operator with any name in any of the .tla files that are included in the spec (via extends for example). But they must prefix the operator name with a \* comment and a keyword. Like \* @trace (ideas welcome).

Put simply I think that moving forward users should specify trace operators written like

------------------------------ MODULE foobar --------------------------------

EXTENDS bizz, bozz

\* arbitrary TLA+..

\* @trace
CrashedChain == ...

\* @trace
NegativeFunds == ...

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

Moreover I think we should reserve the 'test' terminology for actual tests running in the repo of the SUT

Users would like to generate multiple traces violating a single invariant using TLC.

It is possible to do this using TLC's '-continue' parameter. It just allows model checking to continue, using the same algorithm as normal but without the early breakout. This means

1. tlaplus/tlaplus#690
2. TLC will continue to check unbounded state spaces.

this makes any solution that uses the technique a bit finicky.

Alternatives: use simulation mode.

Currently, if TLC is run for an invariant that holds, it will simply run forever.
We should add a timeout option to the call in tlc_raw and handle timeouts in tlc_pure

Raised on 7abdf5f

In contrast to apalache raw, tlc raw does not offer any cleanup options as it is not clear how to deal with the various files and directories that TLC writes to the filesystem. The cleanup functionality is offered in tlc pure because in that case a temporary directory is used. The -cleanup arg could be parsed in this case, but it's not clear what the effect would be. Elaborating: it's not clear if the -cleanup flag might delete some desired output files or not.

Some of the older fixed-release Linux distros still use older versions of python by default.

To support them, the required minimum python version should be lowered to 3.8.

In abd3912 the tool runs without tagging outputs with the version. All outputs should be version tagged in order to help create better bug reports.

The tool currently writes output in json to stdout but various internal procedures should be designed so that they can be queried for their progress.

350fcfe

I'm currently working on a cli tool. The short-term goal is to make the tool into a 'swiss army knife' of simple programs which can be accessed via cli args and/or json input on stdin.

Currently two commands are supported: apalache raw and apalache pure. The raw command provides access to Apalache as normal, but with some nice optional UX improvements. Arguments can be given to the program via cli arguments or by sending json data to stdin. The pure command only accepts json data in stdin, and returns json data in stdout. Both functionalities can also be called directly in python code of course.

I think now is a good time to receive feedback on the APIs/ UX's. Here is a more detailed description of the functionalities:

apalache raw

The apalache raw command accepts arguments specified like --<arg_name>=<value> or simply --<flag_name> for boolean values. Fire is used for the cli.

All Apalache arguments can be given as key value pairs (or flags). The full API is supported.

The following arguments are additionally offered

• stdin (if this is flagged, then read arguments from stdin instead, see below)
• mem (if flagged, read all Apalache output, inc files, into memory for later use)
• cleanup (if flagged, cleanup all written files at the end)
• jar (specify jar path, required)
• cwd (specify cwd for Apalache process, required)

If stdin is flagged, then instead read a json, like this from stdin and use that.

Examples

You might do

cli apalache raw --cmd=check --inv=Safety --file=spec.tla --profiling --jar=apalache.jar --cwd=~/myspecs

#  or

cli apalache raw --stdin < raw_cmd.json

apalache pure

The apalache pure command reads json data formatted like this and uses it to run Apalache.

Just like for the raw command, a jar path must be specified, however, in the pure case, the --mem and --cleanup flags are assumed true. Additionally, all of the input files and their contents must be given in the json input.

The return value is a json like

  {
      "shell_cmd":<the shell command used to run apalache>,
      "return_code":<subprocess return code>,
      "stdout":<apalache stdout>,
      "stderr":<apalache stderr>,
      "files":[
          <filename>:<content>,
          <filename>:<content>,
          ...
      ]
  }

Next steps

Next I will probably implement a download tlc, download apalache command(s) or similar, to pull the jars. I will also implement tlc raw and tlc pure with the same designs as the Apalache commands. I don't think it will take long.

Feature

Wrap Apalache with raw and pure functionalities (as is done for TLC in a269ae9)

Summary

c2a3f87 snapshots the codebase in a state that implemented wrappers for the Apalache model checker v0.17.0.

Apalache is now at version 0.19.x and has undergone changes in

1. The way it writes to the filesystem (the output paths/directories are different)
2. The structure of the traces it provides (now gives Informal Trace Format)
3. Possibly some changes in the cli

We should update to keep up with these changes.

Steps

• 1. Checkout the snapshot and try to use it with Apalache 0.17.0 to see the goal.
• 2. Compare with the way the TLC wrapper is implemented
• 3. Mirror the current TLC wrapper, but for Apalache

An example of 'trickiness'

In Apalache 0.17.0 it was necessary to parse stdout to read the name of the directory that Apalache wrote it's output to. This lead to a solution here. This is an example of something that I'm sure has changed. Therefore this parsing may no longer be necessary.

There might be a few small tricks/non-obvious things going on here. Please ask me for help if you need it.

Resources

The branch

https://github.com/informalsystems/mbt-python/tree/danwt/apalache-0.17.0-checkpoint

checkpoints the functionality when it was implemented for Apalache 0.17.0.

In 2285f5b every parameter is left to the user to specify, but it might be a good idea to specify some sensible defaults. For example: number of workers used could be set to always match number of hardware threads.

This error is raised when apalache command is failed on top level and modelator-py tries to read files from non-existing directory.

Feature

The user would like to extract zero, one or more traces from the stdout of TLC and get them in Informal Trace Format.

Features

• A JSON Boolean: either false or true.
• A JSON string literal, e.g., "hello".
• A JSON integer, e.g., 123.
• A big integer of the following form: { "#bigint": "[-][0-9]+" }.
• A list of the form [ , ..., ].
• A record of the form { "field1": , ..., "fieldN": }.
• A tuple of the form { "#tup": [ , ..., ] }. Will never be supported.
• A set of the form { "#set": [ , ..., ] }.
• A map of the form { "#map": [ [ , ], ..., [ , ] ] }.
• Multiple traces
• Lasso traces
• Ergonomic cli exposure
• Cli docs
• Prose docs and usage examples

Resources

• Informal Trace Format
• https://github.com/tlaplus/tla_python/issues/3

Apalache should be run using the right JDK in order to get it to work on arm64.

Currently modelator-py is a dependency on modelator. But both of them use the same name for the CLI app.

Since modelator-py because a python library for TLA, I suggest removing modelator-py CLI in favor of modelator CLI.

Bugs may creep in if versions are not kept aligned.

Here is a hook

-   repo: https://github.com/pre-commit/mirrors-mypy
    rev: v0.782
    hooks:
        - id: mypy

The rev field should be appropriate.

I had a branch including code from tla_python but accidentally deleted it - I should get it back.

There is a branch

https://github.com/informalsystems/mbt-python/tree/vscode-configuration-template

containing recommended .vscode settings.

It should be documented, to get as many users as possible to be aware of it.

Currently (4380488) it is assumed that users will supply their own model checker jars when using the tools. However, we require jars for running tests. For example, the TLC jar path in the tests/ directory is hardcoded for myself.

More generally we should decide how we want to deal with the model checker jar dependencies

Avenues:

1. Implement jar management/downloading/version control (this could be a useful feature by itself)
2. Force users to supply the jars (does not solve problem with tests)

Ref:

(env) uditgulati@Udits-MacBook-Air transfer % modelator apalache info
Default location for JAR file: /Users/uditgulati/Library/Application Support/modelator/checkers
Looking for version: 0.30.1
Looking for file: /Users/uditgulati/Library/Application Support/modelator/checkers/apalache/lib/apalache-0.30.1.jar
WARNING:root:Error while checking the existence of the jar file
Apalache JAR file not found
(env) uditgulati@Udits-MacBook-Air transfer % ls /Users/uditgulati/Library/Application Support/modelator/checkers/apalache/lib/
ls: /Users/uditgulati/Library/Application: No such file or directory
ls: Support/modelator/checkers/apalache/lib/: No such file or directory
(env) uditgulati@Udits-MacBook-Air transfer % ls /Users/uditgulati/Library/Application\ Support/modelator/checkers/apalache/lib/apalache-0.30.1.jar
/Users/uditgulati/Library/Application Support/modelator/checkers/apalache/lib/apalache-0.30.1.jar

Leverage apalache parse by inserting states into small modules and parsing the modules - thus obtaining Apalache IR.

Related:

• See apalache-mc/apalache#1080
• Depends on #13
• Depends on #9

The best way is probably as follows:

Given a snippet S with identifiers (variables) x,y,z generate the following string

------------------------------------ MODULE spec -----------------------------
VARIABLES
x,y,z

S
===============================================================================

Note that this creates a sub-problem: determine the necessary variable names from a given snippet.

For the case that the snippet is an extract of a counterexample contained inside the stdout of a TLC execution then we should be able to use the VARIABLES declaration from the spec that was model checked. As this is the target use case, then we can use this solution for now.

• Consider pydantic
• Consider various configurations for mypy

Thanks @andrey-kuprianov for reminding.

Given a TLA+ spec there should be a quick way to learn the structure/format of the JSON that traces of the spec will be given in.

It may be useful to use the Json trace functionality that is included with TLC

Resources:

• google groups discussion
• module

To consider

• is there a performance penalty?

Currently (4380488) the CLI uses Fire which is a solid CLI library. However no documentation has been added yet.

Blocker: it might be better to wait until API's solidify before writing documentation.

In 7be09b4 the docs are not good

We must think about how to expose the functionalites contained within the project

Avenues:

• Published as a python package on a public package repository
• Available through Foreign Function Interface (FFI)
• Available as CLI tool

ect...

Great project, @danwt !

However, I was not able yet to get it fully working:
While I was setting up the framework and running commands provided in the CONTRIBUTING.md, I noticed that the test test_tlc.py hangs.
(Running poetry run pytest tests/tlc/test_tlc.py -s --log-cli-level=debug.)

I managed to narrow the problem down actual running of the TLC solver (in raw.py).
Specifically, the command that is run in a subprocess is java -cp /Users/ivan/Documents/codebase/modelator-py/large/tlc_2_18.jar tlc2.TLC -cleanup -config HelloWorld.cfg -workers auto HelloWorld.tla.

This command is run in a temp folder.
When adding a breakpoint in that folder and running it on my own, the TLC solver hangs with the following output:

Exception in thread "main" java.lang.NoSuchMethodError: java.util.Optional.isEmpty()Z
	at tlc2.TraceExplorationSpec.generate(TraceExplorationSpec.java:71)
	at tlc2.TLC.process(TLC.java:1244)
	at tlc2.TLC.main(TLC.java:352)

I am adding the relevant TLA+ files:
HelloWorld.tla.txt
HelloWorld.cfg.txt
My java version is 1.8.0_321

User story

A user has a list of traces which they are using to drive an SUT. They know that one or more traces from the list are causing the test to fail and they would like to identify the trace(s).

First prototype

Expose a binary search algorithm which reacts or to takes user binary choices as input (True, False). For the first prototype this should be done in a more offline manner, as designing an interactive search is a more challenging UX problem.

The user should submit a list of traces T and a list of binary choices B. The tool will return a sublist of T, T' by deterministically following a binary search algorithm according to the choices in B. Notice that in this design, the user will progress the binary search by providing successively longer lists B. The user is free to do whatever they want with the output T', for example they might setup their environment to automatically test the SUT with T' as input, and feed back a longer B for the next iteration.

Second prototype / full version of feature

I'm not sure they best way to design the UX for a more serious version of the feature. Any thoughts?

Leave until merge into monorepo