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

AGREE counterexample views do not display signal values for event data ports #75

Closed
kfhoech opened this Issue Feb 14, 2018 · 4 comments

Comments

Projects
None yet
1 participant
@kfhoech
Contributor

kfhoech commented Feb 14, 2018

When retrieving counterexamples for disproven statements, the various AGREE viewers (console, spreadsheet and eclipse tree viewer) somehow skip output of the values on event data ports. Investigation has shown that JKind does output the event data port values, but AGREE fails to render them.

@kfhoech kfhoech added bug AGREE labels Feb 21, 2018

@kfhoech kfhoech self-assigned this Feb 23, 2018

@kfhoech

This comment has been minimized.

Contributor

kfhoech commented Feb 23, 2018

Cannot duplicate after restarting OSATE/AGREE.

@kfhoech kfhoech closed this Feb 23, 2018

@kfhoech kfhoech reopened this Feb 23, 2018

@kfhoech

This comment has been minimized.

Contributor

kfhoech commented Feb 23, 2018

Duplicated it. This occurs for multilevel analyses ('Verify All Layers', not monolithic) and in the layers under the top-level layer.

That means this is likely something wrong with the renaming maps are handled on the retrieval of results from the JKindResult structures.

@kfhoech

This comment has been minimized.

Contributor

kfhoech commented Mar 1, 2018

This is a larger problem affecting all variable declarations in layers other than the root layer of a multi-layer (recursive) analysis. The root of the problem is fortunately simple. When the category for signals is calculated in the renaming visitor, it needs to know the instance path of that signal relative to the component instance that is the top of that layer of analysis. The present mechanism does not do this in a truly relative manner; it simply assumes that the path is only one segment deep. This works only for the highest level of a multi-layer analysis. Accordingly, the categories and reference maps for layers other than the top are incorrect, leading to signals being dropped in the counterexamples rather than being mapped to their originating AGREE element.

The fix will require passing in the root instance at each layer of the analysis. This requires changing the interface of the RenamingVisitor which affects AGREE's VerifyHandler, the TcgLinkerFactory, and the AADLSimulator AgreeProgramToSimulationProgram. Fortunately, the appropriate root instance is immediately available in those contexts making the required interface changes simple.

kfhoech added a commit that referenced this issue Mar 19, 2018

Merge pull request #85 from smaccm/develop_issue75
Fix Issue #75: missing variables in counter example views
@kfhoech

This comment has been minimized.

Contributor

kfhoech commented Mar 19, 2018

Resolved by Pull Request.

@kfhoech kfhoech closed this Mar 19, 2018

@kfhoech kfhoech added the v2.3.3 label Jul 11, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment