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

Parser grammar update #164

Closed seblund closed 1 year ago

seblund commented 1 year ago

This PR updates the grammar to a newer version and cleans up the code base by refactoring QueryExpression. Changes:

The refactor is very nice because we can now rely on the type system with exhaustive match statements: If we add a new query type or composition type, we will get a compile error until we handle it in all match cases instead of getting runtime errors. And in general we won't miss match cases during development.

Also now simplifies the edge parser and deduplicates code and grammar by combining the edge and invariant parser. This works because invariants are equivalent to edge guards.

seblund commented 1 year ago

Made all the changes that were requested :)