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

Handle state variables without next-function as inputs #73

Open
lonsing opened this issue Aug 26, 2020 · 0 comments
Open

Handle state variables without next-function as inputs #73

lonsing opened this issue Aug 26, 2020 · 0 comments
Labels
enhancement New feature or request

Comments

@lonsing
Copy link
Collaborator

lonsing commented Aug 26, 2020

Issue refers to BTOR2 inputs and Pono master 5b6af14.

Excerpt from the BTOR2 paper (https://link.springer.com/content/pdf/10.1007%2F978-3-319-96145-3_32.pdf):

"A state variable without associated next function is treated as a primary input, i.e., it has the same behaviour as inputs defined via keyword input."

Pono properly handles inputs that are explicitly declared using the keyword input. Such inputs are added to the set inputvars_ of a transition system.

However, state variables declared using the keyword state and for which no next-function is given are added to the set statevars_ of a transition system although according to the BTOR2 standard they should appear in inputvars_.

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

No branches or pull requests

1 participant