Incorrect LTL Property Generation for Universality and Absence Before Patterns
In Temporal Specifications the properties generated for following patterns do not match the mathematical definitions:
1. For Absence Before generated property is “<>P ->(!P U R)”
whereas mathematical property is “<>R ->(!P U R)”
2. For Universality Before generated property is “<>P ->(P U
R)” whereas mathematical property is “<>R ->(P U R)”
LTL patterns are described here: http://patterns.projects.cs.ksu.edu/documentation/patterns/ltl.shtml
(from redmine: issue id 3610, created on 2019-01-10, closed on 2019-02-12)