Skip to content

Repeated terms in AndGuard and OrGuard #93

@magoorden

Description

@magoorden

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)

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions