Repository: informalsystems/modelator-py (language: python)

Issue:
Feature: transform traces in the stdout of TLC into Informal Trace Format
# Feature

The user would like to extract zero, one or more traces from the stdout of TLC and get them in [Informal Trace Format](https://apalache.informal.systems/docs/adr/015adr-trace.html?highlight=trace%20format#the-itf-format).

## Features

- [x] A JSON Boolean: either false or true.
- [x] A JSON string literal, e.g., "hello".
- [x] A JSON integer, e.g., 123.
- [ ] A big integer of the following form: { "#bigint": "[-][0-9]+" }.
- [x] A list of the form [ <expr>, ..., <expr> ].
- [x] A record of the form { "field1": <expr>, ..., "fieldN": <expr> }.
- [ ] ~A tuple of the form { "#tup": [ <expr>, ..., <expr> ] }.~ Will never be supported.
- [x] A set of the form { "#set": [ <expr>, ..., <expr> ] }.
- [x] A map of the form { "#map": [ [ <expr>, <expr> ], ..., [ <expr>, <expr> ] ] }.
- [x] Multiple traces
- [ ] Lasso traces
- [x] Ergonomic cli exposure
- [ ] Cli docs
- [x] Prose docs and usage examples

## Resources

- [Informal Trace Format](https://apalache.informal.systems/docs/adr/015adr-trace.html?highlight=trace%20format#the-itf-format)
- https://github.com/tlaplus/tla_python/issues/3


Discussion / hints:

Fix patch:
diff --git a/README.md b/README.md
index fdd7592..7d69fe5 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,23 @@
 
 [![License](https://img.shields.io/badge/License-Apache%202.0-blue.svg)](LICENSE)
 
-Framework and tools for model-based testing (Python code only. Rust code can be found at [modelator](https://github.com/informalsystems/modelator))
+_**Lightweight utilities to assist model writing and model-based testing activities using the TLA+ ecosystem.**_
+
+## What is this project?
+
+### What can it do right now?
+
+Currently there is a cli implementing utilities:
+
+- [x] Run [TLC](https://github.com/tlaplus/tlaplus) model checker without side effects (runs in temporary directory and is cleaned up)
+- [x] Run [TLC](https://github.com/tlaplus/tlaplus) model checker programmatically (reads and returns json data)
+- [x] ~Run [Apalache](https://github.com/informalsystems/apalache) model checker without side effects (runs in temporary directory and is cleaned up)~ (needs patch)
+- [x] ~Run [Apalache](https://github.com/informalsystems/apalache) model checker programmatically (reads and returns json data)~ (needs patch)
+- [x] Extract traces from TLC output in [Informal Trace Format](https://apalache.informal.systems/docs/adr/015adr-trace.html?highlight=trace%20format#the-itf-format) format (concise and machine readable counterexample representation)
+
+### What will it do in the future?
+
+The model-based testing capabilities developed at Informal are currently in the [modelator](https://github.com/informalsystems/modelator) tool and are being migrated to Python. Please expect more utilities and more tooling soon.
 
 ## Running the code in this repository
 
@@ -15,55 +31,57 @@ Framework and tools for model-based testing (Python code only. Rust code can be
 
 The Python version used is `3.9.9`.
 
-### Running
+The project has _not_ been published yet so the tools should be run from a development environment (clone the repo, install the dependencies and run the python program directly). It should be easy because we are using [Poetry](https://github.com/python-poetry/poetry).
+
+### New workstation setup for developers, TLDR
+
+1. Install `pyenv`
+2. Install `poetry`
+3. Clone this repo
+4. `cd <repo>`
+5. `pyenv install 3.9.9`
+6. `poetry env use python`
+7. `poetry shell`
+8. `poetry install`
+9. `code .` to open a VSCode instance with a Python 3.9.9 interpreter (assuming VSCode)
 
-With Poetry installed `poetry install`.
+### Commands for devs
 
-- Run the cli program: `poetry run cli <args>`.
+With Poetry installed run `poetry install`. Then
+
+- Run the cli program: `poetry run cli <args>` (entrypoint is `modelator/cli:cli`)
 - Tests: `poetry run pytest` or use your code editor. VSCode has built in support.
 - Tests with coverage: `poetry run pytest --cov=modelator tests/`
 - Tests with logging output to terminal: `poetry run pytest --log-cli-level=debug`
 - Specific test: `poetry run pytest tests/<dir>/<filename>.py -k 'test_<suffix>'`
-- Specific test with visible print: `poetry run pytest tests/<dir>/<filename>.py -s -k 'test_<suffix>'`
-- Preview the pre-commit hooks: `pre-commit run --all-files`
+- Specific test and display stdout: `poetry run pytest tests/<dir>/<filename>.py -s -k 'test_<suffix>'`
+- Run the pre-commit hooks: `pre-commit run --all-files`
 - Run linter manually: `flake8 .`
 - Run formatter manually: `black .`
 - Run static type checker: `mypy .`
 - Sort imports `isort .`
 
+### Commands for users
+
+Please see [usage](./usage.md).
+
 ### Tips for VSCode users
 
 VSCode has solid support for Python development using Poetry. If VSCode does not pick up on Poetry then try navigating to this directory and executing
 
 ```
-poetry shell
-code .
+poetry shell;
+code .;
 ```
 
-Ensure that the bottom left of your VSCode window shows that you are using the correct Python environment (see contents of pyproject.toml for the correct Python version).
+Ensure that the bottom left of your VSCode window shows that you are using the correct Python environment.
 
 The branch [vscode-configuration-template](https://github.com/informalsystems/mbt-python/tree/vscode-configuration-template) contains a .vscode directory which can be used as a starting point for configuring your dev environment.
 
-### TLDR
-
-In short, setting up the repo on a new workstation might look like
-
-1. Install pyenv
-2. Install poetry
-3. Clone repo
-4. `cd` repo
-5. `pyenv install x.x.x`
-6. `poetry env use python`
-7. `poetry shell`
-8. `poetry install`
-9. `code .` (for VSCode)
-
 ### Troubleshooting
 
 This project has been setup following the guidelines at [this](https://mitelman.engineering/blog/python-best-practice/automating-python-best-practices-for-a-new-project/) blog post. The page contains useful context for troubleshooting.
 
-If having difficulties with `poetry install` on linux due to a missing `_ctypes` module then consider the advice on [this](https://stackoverflow.com/a/41310760) stack overflow page, and on [this](https://github.com/pyenv/pyenv/issues/2137) issue.
-
 If having difficulties installing poetry using `curl -sSL https://install.python-poetry.org | python3 -` on MacOS then try adding `eval "$(pyenv init --path)";` to your .bashrc or .zshrc file (given that pyenv is installed).
 
 ## Contributing
diff --git a/usage.md b/usage.md
new file mode 100644
index 0000000..c331b33
--- /dev/null
+++ b/usage.md
@@ -0,0 +1,52 @@
+# Usage examples
+
+_This document is a work in progress and not all features are documented yet_
+
+## Extract traces from TLC output in [Informal Trace Format](https://apalache.informal.systems/docs/adr/015adr-trace.html?highlight=trace%20format#the-itf-format) format
+
+The TLC model checker will generate counterexamples written in TLA+ and embed them in stdout, interleaved with ASCII text. This output can contain 0, 1 or more traces. Run the `poetry run cli util tlc itf` tool to extract a list of traces in the Informal Trace Format.
+
+There is more than one way to run the tool. The tool always writes output as Json to `stdout`.
+
+### Option 1: provide TLC's stdout data on stdin and flags as cli args
+
+```bash
+poetry run cli util tlc itf < <TLC_STDOUT_STRING> # Run without flags
+poetry run cli util tlc itf --lists=<bool> --records=<bool> < <TLC_STDOUT_STRING> # Run with flags
+```
+
+### Option 2: provide TLC's stdout data and flags inside a json object
+
+```bash
+poetry run cli util tlc itf --json < <JSON_OBJECT>
+```
+
+### Flag explanation
+
+```bash
+# In TLA+ there is no distinction between some functions and sequences. This means
+# that a sequence may be represented by function with domain 1..n for some n,
+# and vice versa. It is likely convenient to handle such functions as lists. 
+# Default: True
+--lists
+# In TLA+ there is no distinction between some functions and records. This means
+# that a record may be represented by functions with domain all strings, and vice
+# versa. It is likely convenient to handle such functions as records. 
+# Default: True
+--records 
+```
+
+### Examples
+
+The `tests/resource` directory contains convenient example data.
+
+```bash
+cd tests/resource
+```
+
+```bash
+# Provide TLC's stdout data on stdin and flags as cli args
+poetry run cli util tlc itf --lists=False < TlcTraceParse.txt > traces.json
+# Provide TLC's stdout data and flags inside a json object
+poetry run cli util tlc itf --json < HelloWorld_util_tlc_itf.json > traces.json
+```


Test patch:
diff --git a/tests/resource/HelloWorld_util_tlc_itf.json b/tests/resource/HelloWorld_util_tlc_itf.json
new file mode 100644
index 0000000..eb3cec0
--- /dev/null
+++ b/tests/resource/HelloWorld_util_tlc_itf.json
@@ -0,0 +1,5 @@
+{
+    "lists": true,
+    "records": false,
+    "stdout": "TLC2 Version 2.16 of Day Month 20?? (rev: 7d936f2)\nRunning breadth-first search Model-Checking with fp 67 and seed 5767608612270942875 with 8 workers on 8 cores with 10923MB heap and 64MB offheap memory [pid: 50075] (Mac OS X 11.4 aarch64, Homebrew 17.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).\nParsing file /Users/danwt/Documents/work/mbt-python/tests/resource/TlcTraceParse.tla\nParsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/tlc-16867280054817799297/Naturals.tla (jar:file:/Users/danwt/Documents/model-checkers/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)\nParsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/tlc-16867280054817799297/FiniteSets.tla (jar:file:/Users/danwt/Documents/model-checkers/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)\nParsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/tlc-16867280054817799297/Sequences.tla (jar:file:/Users/danwt/Documents/model-checkers/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)\nParsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/tlc-16867280054817799297/TLC.tla (jar:file:/Users/danwt/Documents/model-checkers/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)\nParsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/tlc-16867280054817799297/Reals.tla (jar:file:/Users/danwt/Documents/model-checkers/tla2tools.jar!/tla2sany/StandardModules/Reals.tla)\nParsing file /private/var/folders/9l/fjtclx4d6txfdsj2ynqnrr5c0000gn/T/tlc-16867280054817799297/Integers.tla (jar:file:/Users/danwt/Documents/model-checkers/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)\nSemantic processing of module Naturals\nSemantic processing of module Sequences\nSemantic processing of module FiniteSets\nSemantic processing of module TLC\nSemantic processing of module Integers\nSemantic processing of module Reals\nSemantic processing of module TlcTraceParse\nStarting... (2022-02-09 08:59:37)\nComputing initial states...\nFinished computing initial states: 1 distinct state generated at 2022-02-09 08:59:37.\nError: Invariant Inv is violated.\nError: The behavior up to this point is:\nState 1: <Initial predicate>\n/\\ sequence_indexed_map = (<<\"one\", \"two\">> :> 42)\n/\\ one_indexed_sequential_map = <<42, 42, 42, 42, 42>>\n/\\ string_indexed_map = [two |-> 42, one |-> 42]\n/\\ negative_number = -123456\n/\\ record = [foo |-> 42, bar |-> 43]\n/\\ tuple = <<1, 2>>\n/\\ bool = FALSE\n/\\ map_indexed_map = ([foo |-> 42, bar |-> 42] :> 42)\n/\\ set_indexed_map = ({1, 2, 3} :> 42 @@ {4, 5, 6} :> 42)\n/\\ set = {1, 2, 3}\n/\\ list = <<1, \"two\">>\n/\\ map = ( 0 :> 42 @@\n  1 :> 42 @@\n  2 :> 42 @@\n  3 :> 42 @@\n  4 :> 42 @@\n  5 :> 42 @@\n  6 :> \"forty-two\" @@\n  8 :> \"forty-two\" @@\n  13 :> \"forty-two\" )\n/\\ json_int = 123\n/\\ string_literal = \"hello\"\n/\\ zero_indexed_sequential_map = (0 :> 42 @@ 1 :> 42 @@ 2 :> 42 @@ 3 :> 42 @@ 4 :> 42 @@ 5 :> 42)\n/\\ other_bool = TRUE\n\nState 2: <Next line 42, col 5 to line 57, col 32 of module TlcTraceParse>\n/\\ sequence_indexed_map = (<<\"one\", \"two\">> :> 42)\n/\\ one_indexed_sequential_map = <<42, 42, 42, 42, 42>>\n/\\ string_indexed_map = [two |-> 42, one |-> 42]\n/\\ negative_number = -123456\n/\\ record = [foo |-> 42, bar |-> 43]\n/\\ tuple = <<1, 2>>\n/\\ bool = TRUE\n/\\ map_indexed_map = ([foo |-> 42, bar |-> 42] :> 42)\n/\\ set_indexed_map = ({1, 2, 3} :> 42 @@ {4, 5, 6} :> 42)\n/\\ set = {1, 2, 3}\n/\\ list = <<1, \"two\">>\n/\\ map = ( 0 :> 42 @@\n  1 :> 42 @@\n  2 :> 42 @@\n  3 :> 42 @@\n  4 :> 42 @@\n  5 :> 42 @@\n  6 :> \"forty-two\" @@\n  8 :> \"forty-two\" @@\n  13 :> \"forty-two\" )\n/\\ json_int = 123\n/\\ string_literal = \"hello\"\n/\\ zero_indexed_sequential_map = (0 :> 42 @@ 1 :> 42 @@ 2 :> 42 @@ 3 :> 42 @@ 4 :> 42 @@ 5 :> 42)\n/\\ other_bool = TRUE\n\n2 states generated, 2 distinct states found, 0 states left on queue.\nThe depth of the complete state graph search is 2.\nFinished in 00s at (2022-02-09 08:59:37)\nTrace exploration spec path: ./TlcTraceParse_TTrace_1644397177.tla\n"
+}
\ No newline at end of file