Static simplification of HPL AST

git-afsantos / haros

H(igh) A(ssurance) ROS - Static analysis of ROS application code.

MIT License

190 stars 37 forks source link

Closed git-afsantos closed 3 years ago

git-afsantos commented 4 years ago

Reminder to implement static simplification of expressions in HPL predicates.

resolve static arithmetic expressions
resolve tautologies and contradictions
reduce boolean operators to simpler equivalent expressions (e.g., p implies false to not p)