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

Interpreter hangs while running a function #23

Open
pt7k opened this issue Feb 24, 2025 · 0 comments
Open

Interpreter hangs while running a function #23

pt7k opened this issue Feb 24, 2025 · 0 comments
Labels
bug Something isn't working

Comments

@pt7k
Copy link
Contributor

pt7k commented Feb 24, 2025

  1. Summary

    • Description: Bug Summary in 2 to 3 sentences.
    • While this specification provided to the interpreter is very similar to the example in issue Interpreter returns the unsat error for a function that runs fine and has a fp through rr #22 this time the program is hanging in an endless loop without any warnings or messages.
    • One can see the program continuously iterating by setting severity to debug.
    • It is also possible to get the same outcome as in the previously mentioned issue by shortening the specification to just o1[n] = g(o1[n-1]) that is by skipping the explicit assignment of 0 to the initial timeline.
  2. Environment

    • Tau Version: for now "v0.7-alpha"
    • Build Number or Date: 90db47a
    • Operating System: Ubuntu
  3. Steps to Reproduce
    Step 1: What input did you first provide?

sbf o1 = console
f(0) := {b}:sbf
f({a b}:sbf) := {a b}:sbf
g(x) := {a}:sbf f(x)
h[0]() := 0
h[n]() := g(h[n-1]())
n h()
# g(x) has a fixed point when being run through rr but hangs in a loop with the interpreter
r o1[0] = 0 && o1[n] = g(o1[n-1])

Step 2: Any additional input to Tau?

Expected Result
Same result from the interpreter as from the equivalent test through a recurrence relation h:

h[0]() = 0
h[1]() = { a b } : sbf
...

Actual Result
Program hanging

  1. Additional Information
    • Error Messages or Logs:
    • Screenshots:

Image

Partial debug output:

Image

  1. Severity and Impact

    • Severity Level: Minor
    • Impact on Work: Program Hanging
  2. Workaround (if applicable)

    • Tell us if you found a way around this problem:
    • It's possible to prevent this particular example from going to an endless loop by not explicitly assigning 0 to o1[0] in the specification, but then the interpreter yields the unsat error:

Image

  1. Contact Information
    • Name: pt7k
    • Email: Telegram @ksdjfskfh
    • Additional Notes: Any other message for the Tau Team

Submission Instructions

  • Make sure to attach any input files to this bug report.
@pt7k pt7k added the bug Something isn't working label Feb 24, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working
Projects
None yet
Development

No branches or pull requests

1 participant