Ecdar / Reveaal

A model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems) written in rust.
5 stars 7 forks source link

Support constraints of the format "x-y < c" in reachability query #141

Open Mati-AAU opened 1 year ago

Mati-AAU commented 1 year ago

Currently the reachability query only supports clock constraints such as "x < 2", "z >= 1", etc.

However those of format "x-y < c" should also be supported, by supporting the "-" operator.

This is currently missing from both the query parser and invariant parser (#96).

The reachability query parser uses the invariant parser, so that must be solved first. After solving the invariant parser issue, making it work for reachability should be trivial.