Different result when adding a constant to another constant

[tobixdev]

I think we encountered a bug in the StlDenseTimeSpecification.
Namely, we have two specifications that should be semantically equivalent (from our perspective) but have a different outcome when updating the specification.

Here is a minimal reproduction:

from rtamt import StlDenseTimeSpecification

spec1 = StlDenseTimeSpecification()
spec1.spec = "signal > (50 + 0)"
spec1.declare_var("signal", "float")
spec1.parse()

spec2 = StlDenseTimeSpecification()
spec2.spec = "signal > 50"
spec2.declare_var("signal", "float")
spec2.parse()

rob1 = spec1.update(['signal', [(0, 25), (10, 75), (20, 100)]])
print('spec1: ' + str(rob1))

rob2 = spec2.update(['signal', [(0, 25), (10, 75), (20, 100)]])
print('spec2: ' + str(rob2))

Output:

./.venv/bin/python3 rtamt_bug.py 
spec1: []
spec2: [[0, -25.0], [10, 25.0]]

The same thing also happens when we use the formula signal > (50 + 1).
Tested with rtamt 0.3.5, Python 3.10.12

Do you have any pointers on what could be the issue here or are we missing something obvious?
Unfortunately, as we generate these specifications automatically, we cannot simply fold the constants manually.

P.S. Thanks for the library! :)

[nickovic]

In the latest version of RTAMT (in the master branch), this issue does not manifest itself. I added nevertheless a new test based on your example. I suggest to use the version of RTAMT from the master branch, since it also fixes some other previously encountered issues.

[tobixdev]

Thanks for taking your time to test the issue. I'll use the master branch.

[tobixdev]

I have a follow-up question:

I see that you've version 0.4.6 in this repository.
However, in PyPI the most recent version is 0.3.5.
Is there a reason for this discrepancy?