Danwt/tlc 2.16 stdout to informal trace format correct lexing #21 - Githubissues

informalsystems / modelator-py

Utilities for the TLA+ ecoystem and model-based testing using TLA+.

Apache License 2.0

28 stars 2 forks source link

Danwt/tlc 2.16 stdout to informal trace format correct lexing #21 #28

Closed danwt closed 2 years ago

danwt commented 2 years ago

Tackles https://github.com/informalsystems/mbt-python/issues/21

[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]+" }.
[ ] A list of the form [ , ..., ].
[ ] A record of the form { "field1": , ..., "fieldN": }.
[ ] ~A tuple of the form { "#tup": [ , ..., ] }.~ Will never be supported.
[x] A set of the form { "#set": [ , ..., ] }.
[x] A map of the form { "#map": [ [ , ], ..., [ , ] ] }.
[x] Multiple traces
[ ] Lasso traces
[ ] Ergonomic cli exposure

Missing features will be subject of another PR

danwt commented 2 years ago

Merged manually at https://github.com/informalsystems/mbt-python/commit/9bfbe4c5209147f7787ea983a25226abc1973b81