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.

Sign up for GitHub

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

Jump to bottom

Instantiating global variables should be done consistently #1743

Closed
mlaveaux opened this issue Feb 23, 2024 · 1 comment
Closed

Instantiating global variables should be done consistently #1743

mlaveaux opened this issue Feb 23, 2024 · 1 comment
Assignees
@jgroote
Labels
bug Something isn't working
Milestone
release 202406

Comments

@mlaveaux
Copy link
Member

Currently the instantiation is done based on the ATerm ordering using pointer addresses, this causes issues with loading traces in lpxsim since the instantiation can be different between restarts. As a result the trace might no longer be reachable.
@mlaveaux mlaveaux added the bug Something isn't working label Feb 23, 2024
@mlaveaux mlaveaux added this to the release 202406 milestone Jul 2, 2024
jgroote added a commit that referenced this issue Aug 9, 2024
@jgroote
Adapted the representative_generator to yield a deterministic result.
86f7961 
Using a representative generator it is possible to generate a term
of some given sort. Up till now this term was generated based on
how terms were stored in memory. This meant that in different runs
of the tools different terms could be generated. This was annoying,
as various runs of the simulator could have different terms, which
would mean that generated traces were not always exchangeable between
different runs.

This has now been mended. When there is a choice the lexicographically
minimal function symbol is chosen. Note that there is still a preference
for constants over more complex expressions, and a preference of
mapping constants over constructor constants.

All tests succeed.

This addresses issue #1743.
@jgroote
Copy link
Member

jgroote commented Aug 9, 2024

With the above commit this issue should be resolved.

@jgroote jgroote closed this as completed Aug 9, 2024
mlaveaux pushed a commit that referenced this issue Aug 12, 2024
@jgroote @mlaveaux
Adapted the representative_generator to yield a deterministic result.
257f8c3 
Using a representative generator it is possible to generate a term
of some given sort. Up till now this term was generated based on
how terms were stored in memory. This meant that in different runs
of the tools different terms could be generated. This was annoying,
as various runs of the simulator could have different terms, which
would mean that generated traces were not always exchangeable between
different runs.

This has now been mended. When there is a choice the lexicographically
minimal function symbol is chosen. Note that there is still a preference
for constants over more complex expressions, and a preference of
mapping constants over constructor constants.

All tests succeed.

This addresses issue #1743.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jgroote jgroote

Labels
bug Something isn't working
Projects
mCRL2 Planning
Status: Done
Milestone
release 202406
Development

No branches or pull requests
2 participants
@mlaveaux @jgroote