writing tests and fixing problems in LTL evaluation for
nested until