Daniel Szekeres

Generalization of CegarChecker and related classes

2

Currently, the CegarChecker class, the SafetyResult class, and indirectly the SafetyChecker interface depend on the ARG and Trace classes. Only ARG can be used as abstraction, and only a Trace...

Theta seems to handle urgent/commited initial locations incorrectly. Urgentness is generally handled by the transfunc through optionally applying a delay _after_ all other modifications have been done, based on whether...

Currently, ExprUtil.simplify(expr, valuation) accepts PrimeExprs, which leads to unintuitive behavior and potential bugs. For example, `x'=x+1` with a valuation` x->2` becomes `2'=2+1`, which does not make much sense. Although I...