Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[FEATURE] JSON importer #121

Closed
konnov opened this issue Apr 8, 2020 · 1 comment
Closed

[FEATURE] JSON importer #121

konnov opened this issue Apr 8, 2020 · 1 comment
Assignees
@andrey-kuprianov
Labels
new New issue to be triaged.
Milestone
v0.7-dev-integration

Comments

@konnov
Copy link
Collaborator

konnov commented Apr 8, 2020 •
edited
Loading

Similar to #77, we should introduce an importer from Apalache IR in the JSON format into Apalache IR. Optionally, we could invoke semantic checks by SANY as follows: JSON import -> IR -> pretty printing in TLA+ -> SANY -> SanyImporter -> IR.

This feature will be useful for testing frameworks and other tools, e.g., see this Reddit post.
@konnov konnov added the new New issue to be triaged. label Apr 8, 2020
@konnov konnov added this to the v0.7-dev-integration milestone Apr 8, 2020
This was referenced Apr 10, 2020
Closed
Open
@andrey-kuprianov andrey-kuprianov self-assigned this Apr 24, 2020
andrey-kuprianov added a commit that referenced this issue May 15, 2020
@andrey-kuprianov
JsonReader: started on #121, reading JSON input
41a41a1
andrey-kuprianov added a commit that referenced this issue May 15, 2020
@andrey-kuprianov
#121 TestJson: refactor JSON tests to use common testset for both rea…
ec014e3 
…der and writer
andrey-kuprianov added a commit that referenced this issue May 15, 2020
@andrey-kuprianov
#121 JsonReader: extending coverage
76909da
andrey-kuprianov added a commit that referenced this issue May 18, 2020
@andrey-kuprianov
#121 JsonWriter merge binary and nary ops into the same case
fb2ee03
andrey-kuprianov added a commit that referenced this issue May 18, 2020
@andrey-kuprianov
#121 JsonReader: extending coverage (added functional and predicate ops)
8beb1ed
andrey-kuprianov added a commit that referenced this issue May 18, 2020
@andrey-kuprianov
#121 JsonWriter: always specify args for operator calls
36e3b00
andrey-kuprianov added a commit that referenced this issue May 18, 2020
@andrey-kuprianov
#121 JsonReader: add function and operator applications
eb3f101
andrey-kuprianov added a commit that referenced this issue May 18, 2020
@andrey-kuprianov
#121 JsonReader: add IF, CASE, stutter, fairness
bd57c12
andrey-kuprianov added a commit that referenced this issue May 18, 2020
@andrey-kuprianov
#121 JsonReader: add labels
5f3d635
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonWriter: make params in operator decl non-optional
eeef4a1
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonReader: add LET-IN expressions; current unit tests pass
59b3ac0
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonReader: add reading of modules + some module tests
9cada27
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonReader: integrate JSON input into parse and check commands
dd5a8e5
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonReader/Writer: add --output option to parse command
23c433a
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonReader/Writer: bump up version of ujson library
9f14720
andrey-kuprianov added a commit that referenced this issue May 19, 2020
@andrey-kuprianov
#121 JsonReader: update TestCounterexampleWriter
067e659
andrey-kuprianov added a commit that referenced this issue May 25, 2020
@andrey-kuprianov
#121 ParseCmd: simplify handling of parse --output
6ff0c7a
andrey-kuprianov added a commit that referenced this issue Jun 30, 2020
@andrey-kuprianov
Ak/jsoninput (#146)
e25ea0f 
* JsonReader: started on #121, reading JSON input

* #121 TestJson: refactor JSON tests to use common testset for both reader and writer

* #121 JsonReader: extending coverage

* * join together functional ops into a common pattern
* make json name mappings public for usage in JsonReader
* make unique names for bounded set operators

* #121 JsonWriter merge binary and nary ops into the same case

* #121 JsonReader: extending coverage (added functional and predicate ops)

* #121 JsonWriter: always specify args for operator calls

* #121 JsonReader: add function and operator applications

* #121 JsonReader: add IF, CASE, stutter, fairness

* #121 JsonReader: add labels

* #121 JsonWriter: make params in operator decl non-optional

* #121 JsonReader: add LET-IN expressions; current unit tests pass

* #121 JsonReader: add reading of modules + some module tests

* #121 JsonReader: integrate JSON input into parse and check commands

* #121 JsonReader/Writer: add --output option to parse command

* #121 JsonReader/Writer: bump up version of ujson library

* merge 'unstable' into 'ak/jsoninput'

* #121 JsonReader: update TestCounterexampleWriter

* #121 ParseCmd: simplify handling of parse --output
@andrey-kuprianov
Copy link
Contributor

Closing this issue for now; the JSON encoding works fine, but NB! will need to be changed in the near future: see #153

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andrey-kuprianov andrey-kuprianov

Labels
new New issue to be triaged.
Projects
None yet
Milestone
v0.7-dev-integration
Development

No branches or pull requests
2 participants
@konnov @andrey-kuprianov