Klever

Global VTG strategy should present an infrastructure beyond current strategies, which is able to choose the needed strategy dynamically in optimal way. Global strategy will be default one for users, which do not know much about strategies. More advanced users could use it or the usual strategies.

The first Global strategy, which should become default for us, will unite strengths of MAV and MPV and will minimize the influence of their drawbacks. I suggest the following algorithm, which is based on the latest experiments (the first version):
1. Launch the first iteration of MAV for all rules. About 90% of cases will be solved in more optimized way (since MAV is more optimized). If some rule did not get a verdict Safe/Unsafe, then go to the next step.
2. If only a few rules did not get a verdict (due to heuristic time limit in MAV), launch MPV strategy Sep for them (for reuse of caches of verifier). If there was only one such rule, launch SBT-SA strategy for it. If MAV could not prove Safe for some rules, and most of them did not get any verdict, launch MPV strategy Relevance (as more powerful), but without those rules, which violated MAV internal limits – they should be checked separately by means of MPV-Sep/SBT-SA.

The suggested Global strategy has the following advantages:
1. optimizations of MAV for most of the tasks;
2. dynamic decomposition of MPV for complex tasks;
3. results of the first iteration of MAV will be reused;
4. much more powerful and flexible instrument in a contradiction to static decomposition (#7392).

In order to implement the Global strategy we need:
1. Add automata for all rules (at least from basic set) – this is almost done in #7448.
2. Add support of several verifiers to be able to switch on-the-fly between MAV and MPV (#7435).
3. Automatically change strategy in case of 1 rule (#7466).

This feature also can be viewed as a new method of dynamic specification decomposition.