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

Range maps printing #806

Open
mariaKt opened this issue Jul 18, 2023 · 0 comments
Open

Range maps printing #806

mariaKt opened this issue Jul 18, 2023 · 0 comments

Comments

@mariaKt
Copy link
Contributor

mariaKt commented Jul 18, 2023

There seems to be an issue with pretty printing range maps. This kore output file is the output of an execution whose final configuration includes the following range map:

M: [0 , 1) -> 0  [1 , 2) -> 1  [2 , 3) -> 2  [3 , 4) -> 3  [4 , 6) -> 4

Printing it with kprint results in a parenthesis that includes only the last range of the range map, instead of all its ranges.

$ kprint ./imp-with-rangemaps-kompiled pp.out.kore true true
<T>
  <k>
    .
  </k>
  <state>
    M |-> [ 0 , 1 ) r|-> 0
    [ 1 , 2 ) r|-> 1
    [ 2 , 3 ) r|-> 2
    [ 3 , 4 ) r|-> 3
    ( [ 4 , 6 ) r|-> 4 )
    i |-> 5
  </state>
</T>

The kore output to be printed appears to be correct. I have observed this to be the case with any range map size.

I attach the language definition (imp-with-ranemaps.k) and kore output file (pp.out.kore) needed to recreate the issue, as well as the test's K source (pp.test) that was used to create the kore output file.

imp-with-rangemaps.k.txt
pp.out.kore.txt
pp.test.txt

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

No branches or pull requests

1 participant