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

Repeated terms in AndGuard and OrGuard #93

Open
magoorden opened this issue Nov 25, 2022 · 0 comments
Open

Repeated terms in AndGuard and OrGuard #93

magoorden opened this issue Nov 25, 2022 · 0 comments
Labels
enhancement New feature or request

Comments

@magoorden
Copy link
Contributor

In #88, an example of printed guards looked as follows.

Given the query refinement: Adm2 <= HalfAdm1 && HalfAdm2, the new change will log

Picked state pair (L20, L12L14) [ y-x<=0 && x-x<=0 && y-x<=0 && x-y<=0 && x-y<=0 && y-y<=0 && x-x<=0 && y-x<=0 && y-x<=0 && x-y<=0 && y-y<=0 && x-y<=0 ]
Picked state pair (L22, L13L14) [ x<=2 && x<=2 && x-x<=0 && x-y<=0 && x-y<=0 && y-y<=0 && x-x<=0 && x-y<=0 && y-y<=0 && x-y<=0 ]
Picked state pair (L21, L12L15) [ y<=2 && y<=2 && y-x<=0 && x-x<=0 && y-x<=0 && y-y<=0 && x-x<=0 && y-x<=0 && y-x<=0 && y-y<=0 ]
Picked state pair (L20, L12L14) [ x-x<=0 && x-y<=0 && x-y<=0 && y-y<=0 && x-x<=0 && x-y<=0 && y-y<=0 && x-y<=0 ]
Picked state pair (L23, L13L15) [ x<=2 && y<=2 && x<=2 && y<=2 && y-x<=0 && x-x<=0 && y-x<=0 && x-y<=2 && x-y<=2 && y-y<=0 && x-x<=0 && y-x<=0 && y-x<=0 && x-y<=2 && y-y<=0 && x-y<=2 ]
Picked state pair (L20, L12L14) [ y-x<=0 && x-x<=0 && y-x<=0 && y-y<=0 && x-x<=0 && y-x<=0 && y-x<=0 && y-y<=0 ]
Picked state pair (L23, L13L15) [ x<=2 && y<=2 && x<=2 && y<=2 && y-x<=2 && x-x<=0 && y-x<=2 && x-y<=0 && x-y<=0 && y-y<=0 && x-x<=0 && y-x<=2 && y-x<=2 && x-y<=0 && y-y<=0 && x-y<=0 ]
Picked state pair (L22, L13L14) [ x<=2 && y<=2 && x<=2 && y<=2 && y-x<=0 && x-x<=0 && y-x<=0 && x-y<=2 && x-y<=2 && y-y<=0 && x-x<=0 && y-x<=0 && y-x<=0 && x-y<=2 && y-y<=0 && x-y<=2 ]
Picked state pair (L21, L12L15) [ x<=2 && y<=2 && x<=2 && y<=2 && y-x<=2 && x-x<=0 && y-x<=2 && x-y<=0 && x-y<=0 && y-y<=0 && x-x<=0 && y-x<=2 && y-x<=2 && x-y<=0 && y-y<=0 && x-y<=0 ]

It will print the invariant from the CDD. If this is unsatisfactory, please let me know

(...) But what I notice now is that the printed guard contains repeated terms. In this PR you are just printing the content of CDD as a Guard object, so all these terms are present in the AndGuard object. It seems we could do some more cleaning in the Guard class itself to reduce the size of specific instances.

Originally posted by @magoorden in #88 (comment)

@Brandhoej Brandhoej added the enhancement New feature or request label Nov 29, 2022
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

2 participants