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

Adapt Apalache CE transformer to new JSON format, and split into multiple files #8

Open
andrey-kuprianov opened this issue Jul 28, 2020 · 0 comments
Open

Adapt Apalache CE transformer to new JSON format, and split into multiple files #8

andrey-kuprianov opened this issue Jul 28, 2020 · 0 comments
Assignees
@andrey-kuprianov
Labels
enhancement New feature or request
Milestone
v0.1-user-friendly

Comments

@andrey-kuprianov
Copy link
Contributor

As the JSON format of Apalache counterexamples has changed (see apalache-mc/apalache#153) we need to adapt the transformer that produces the LightClient test to the new format.

Besides, we need to factor out the reusable parts from this transformer, namely:

  • UNIX commands
  • Apalache counterexample analysis
  • Tendermint testgen transformers
@andrey-kuprianov andrey-kuprianov added the enhancement New feature or request label Jul 28, 2020
@andrey-kuprianov andrey-kuprianov added this to the v0.1-user-friendly milestone Jul 28, 2020
@andrey-kuprianov andrey-kuprianov self-assigned this Jul 28, 2020
andrey-kuprianov added a commit that referenced this issue Jul 29, 2020
@andrey-kuprianov
#8: factor out unix commands
8853528
andrey-kuprianov added a commit that referenced this issue Jul 29, 2020
@andrey-kuprianov
#8: factor out apalache transformers
1504227
andrey-kuprianov added a commit that referenced this issue Jul 29, 2020
@andrey-kuprianov
#8: add input parameter to allow disabling passing STDIN to command
2b055f3
andrey-kuprianov added a commit that referenced this issue Jul 29, 2020
@andrey-kuprianov
#8: reject doubly-defined inputs only if different: allows to include…
36a4a64 
… defs multiple times
andrey-kuprianov added a commit that referenced this issue Jul 29, 2020
@andrey-kuprianov
#8: restructure transformation of Apalache CE into LightClient test; …
dc5ab04 
…factor out common components
andrey-kuprianov added a commit that referenced this issue Jul 29, 2020
@andrey-kuprianov
#8: update README.md
a7f5a60
andrey-kuprianov added a commit that referenced this issue Aug 3, 2020
@andrey-kuprianov
#8: more adaptation to LightClient tests
f5e1335
andrey-kuprianov added a commit that referenced this issue Aug 4, 2020
@andrey-kuprianov
#8: adapt to LightClient model history variables
7b21677
andrey-kuprianov added a commit that referenced this issue Aug 10, 2020
@andrey-kuprianov
#8: make time abstract in LightClient test
e2f3597
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@andrey-kuprianov andrey-kuprianov

Labels
enhancement New feature or request
Projects
None yet
Milestone
v0.1-user-friendly
Development

No branches or pull requests
1 participant
@andrey-kuprianov