henkele

- Jenkins: [history](https://monteverdi.informatik.uni-freiburg.de/ci/job/Ultimate%20Nightly/de.uni_freiburg.informatik.ultimate$de.uni_freiburg.informatik.ultimate.regressiontest/2665/testReport/de.uni_freiburg.informatik.ultimate.regressiontest.generic/ReqCheckerRegressionTestSuite/I_Requirements_regression_rtinconsistency_rtinconsistency_test5_req_S_Requirements_regression_ReqCheck_SmtInterpol_epf_T_Requirements_regression_ReqCheck_xml/history/) - Hanfor: [req1](https://ultimate-pa.github.io/hanfor/references/patterns.html#mindurationpattern), [req2](https://ultimate-pa.github.io/hanfor/references/patterns.html#bnddelayedresponsepatternut) ### Result - Expected: rt-inconsistent:req1+req2; vacuous:; inconsistent:; - Actual: rt-inconsistent:; vacuous:; inconsistent:; ### Test (.req file) ``` CONST MAX_TIME is 50.0 CONST time_at_least...

I implemented the following two patterns in a2b5588fde3feb43bc2b021a659c9925bb29fe42 and updated the documentation. Right now, only scope type `globally` is supported. Let me know if you need the others right away,...

Yes it's the first one. By "keywords" I mean e.g. Bnd, Triggered, Delayed,... and even the "keyletters" UT. Ideally one should at least get an idea of what a pattern...

Currently we support the following 24 patterns: - BndDelayedResponsePatternTU - BndDelayedResponsePatternUT - BndEdgeResponsePattern - BndEdgeResponsePatternDelayed - BndEntryConditionPattern - BndExistencePattern - BndInvariancePattern - BndRecurrencePattern - BndResponsePatternTT - BndResponsePatternTU - BndResponsePatternUT -...

Some remarks on what we currently call "BndEntryConditionPattern": `, it is always the case that after "R" holds for at least "t" time units, then "Q" holds` We also have...

I would further suggest to rename the following patterns - "InstAbsPattern" to "AbsencePattern" - "InvariantPattern" to "InvariancePattern" (as we also have "BndInvariancePattern")

Concerning a naming convention, is there any reason not to use a pattern like ` + "Pattern" + + ... ` , where the keywords are arranged alphabetically. So for...

In summary, I would apply the following changes (if you confirm @danieldietsch @Langenfeld ) - [ ] Remove "BndEntryConditionPattern" - [ ] Rename "EntryConditionPattern" to "ResponsePattern" - [ ] Rename...

But I think you're right about the `Delayed` keyword, using it together with the `Bnd` keyword is not very consistent: - The short version is rather cryptic: `ResponsePattern-BndUT-Dlyd` - The...

Looks good, except for the UTD part, but I guess thats the lesser evil ;)