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.

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

pgcl2heyvl annotation support update #66

Open
wants to merge 4 commits into
base: main
Choose a base branch
from

Conversation

umutdural
Copy link
Collaborator

This PR adds annotation support to pgcl2heyvl.

The encodings are generated with corresponding annotations and the transformation of these encodings are done by Caesar.

By changing the _direct global flag in the cmd.py, the tool can be used to generate the transformation directly without using annotations which was the old functionality before this PR.

The examples in the pgcl/examples-heyvl directory are regenerated with the new annotated encodings.

@Philipp15b
Copy link
Collaborator

This is a beautiful diffstat with 1600 lines removed!

@Philipp15b
Copy link
Collaborator

A minor bug: for the refutation examples, the @unroll's second parameter should be zero for wp - just like documented here: https://www.caesarverifier.org/docs/proof-rules/unrolling/#bounded-model-checking.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants