Klever

This is an experimental branch for which practical improvements weren't shown yet while theoretically it is known that current automata have quite poor abilities for formalizing rules as well as they are supported by the only verification back-end, namely CPAchecker. Even good testing wasn't performed. In addition this feature request has the priority that is lower than the one of really significant features and bugs at the moment. Taking all this together means that there are no chances for this feature to be even reviewed and evaluated by anybody in near future.

The only thing that is absolutely obvious that changing any existing rule specifications can't be done in this branch. This should be done separately. In particular separate comparison of verification results should be provided.

This is the best option to solve https://forge.ispras.ru/issues/7392.
It has 2 sets of new tests.
Comparison of new rule specification was provided.
It must be used in all experiments already.

Vitaly Mordan wrote:

This is the best option to solve https://forge.ispras.ru/issues/7392.

Read again the topic, the description and comments for #7392.

It has 2 sets of new tests.

Tests usually show that something isn't complete shit. Nothing more. Moreover often hard test cases are missed or even specially excluded.

Comparison of new rule specification was provided.

I don't need comparison of rule specifications. I need comparison of verification results.

It must be used in all experiments already.

You are free to use this in experiments in your free time and on free resources.

After resolving some issues, property automata operate exactly like instrumentation with small reduction of CPU time. Also they allow us to use MPV-strategies to verify multiple rules at once.

Currently there are several also important issues, which require this one, therefore I do not see any reasons to postpone it more and more. Otherwise, it will be very hard to merge it in master in a few weeks and we will lose much more time again (as it already was with MAV branch).

Evgeny Novikov wrote:

We will consider this after really important things will be done.

Is it possible, that there was not a few minutes in about five months to finally merge this branch? After it was thoroughly evaluated and results were presented.

To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5

This is absolutely incorrect (see https://forge.ispras.ru/issues/7617#note-6).

this branch will be merged to master just after it will be totally synced

It was synced already and was not merged before. Why?

very well tested and most likely fixed

It was tested before as well as basic strategy in master. Statement

Tests usually show that something isn't complete shit. Nothing more. Moreover often hard test cases are missed or even specially excluded.

means absolutely the same for any other component in master. For example, is there a test for error trace conversion functions, which operates with ~100Mb traces, in master? No. "Useless" filters from my branch could handle such traces. Can you give sumilar example for my branch?

documented

There is a documentation (about methods, not implementation), I did not change it much since summer. Anyone can comment there, so I could improve it.

*carefully reviewed by several people"

If so, then why this branch was not reviewed for the last few months?
Also this branch includes property automata. Who is going to review them? Or we do not need them, because they are too efficient?

Of course, all orthogonal changes, e.g. fixes and improvements in rule specifications if so, should be considered and merged absolutely separately

I merged a lot of fixes in this branch only because it was not merged in master for like half of the year.
When I prepared it for merge for the first time, it did not contain any orthogonal changes.

Thus, there was none adequate reasons, why it was not merged.

I reduce the priority of this issue in accordance with our plan to deal with really important tasks

Exactly the same was told several months ago (even in this issue). I guess one of such "important tasks" is to break and then to remove efficient and effective methods from VTG instead of fixing and refactoring them.

Vitaly Mordan wrote:

To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5

This is absolutely incorrect (see https://forge.ispras.ru/issues/7617#note-6).

Since your original statement is bad (https://forge.ispras.ru/issues/7617#note-7) all other notes don't need comments. The most of people have to spend their time doing really necessary things.

Evgeny Novikov wrote:

Vitaly Mordan wrote:

To avoid the situation described at https://forge.ispras.ru/issues/7617#note-5

This is absolutely incorrect (see https://forge.ispras.ru/issues/7617#note-6).

Since your original statement is bad (https://forge.ispras.ru/issues/7617#note-7) all other notes don't need comments. The most of people have to spend their time doing really necessary things.

Since statement https://forge.ispras.ru/issues/7617#note-7 is far from being adequate (see https://forge.ispras.ru/issues/7617#note-8), real issues from this discussion are simple ignored.