pacti-org / pacti

A package for compositional system analysis and design
https://www.pacti.org
BSD 3-Clause "New" or "Revised" License
19 stars 5 forks source link

[BUG] Format strings error in creating contracts #347

Open ayush9pandey opened 2 months ago

ayush9pandey commented 2 months ago

Describe the bug Bug when using format strings in contract creation from strings. Two negatives should become a positive (i.e. -1 * -1 = 1).

To Reproduce Steps to reproduce the behavior:

code
a = 2
b = 100
c = 1
d = -10

my_contract = PolyhedralIoContract.from_strings(
    input_vars=["x"],
    output_vars=["y"],
    assumptions=[],
    guarantees=[f"y >= {a}x + {b} - {c*d}"]
)

Expected behavior Contract should be created without problems.

Screenshots

PolyhedralSyntaxException: pacti.terms.polyhedra.PolyhedralTerm syntax error.
y >= -2 x + 100  - - 10
                            ^
Expected end of text, found '-'  (at char 56), (line:1, col:57)

System (please complete the following information):