search

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

[Feature request] Adding division operation to the parser #337

Closed jgraeb closed 12 months ago

jgraeb commented 12 months ago

I am trying to use "/" in the contracts and the parser instead of declaring a variable separately. This would be a nice functionality for the parser to have.

Code: c = PolyhedralContract.from_string( input_vars=["a"], output_vars=["b"], assumptions=["a >= 0"], guarantees=["b <= 1/15"] )

Error message: PolyhedralSyntaxException: pacti.terms.polyhedra.PolyhedralTerm syntax error. b <= 1/15 ^ Expected end of text, found '/' (at char 6), (line:1, col:7)

NicolasRouquette commented 12 months ago

See this commit: https://github.com/pacti-org/pacti/pull/336/commits/f902115a32fd6ab6414bf58e9cc081f3fbdbd3c6

NicolasRouquette commented 12 months ago

See this example:

https://github.com/pacti-org/pacti/blob/6cb8444c22f898f219577175a9c9279cb626f675/tests/test_polyhedral_contract_syntax.py#L29