TAPAAL Trunk Search Strategy

Asked by Kenneth Yrke Jørgensen on 2011-06-24

In the new version the Search Strategy allowes something called Heuristic Search, even for the UPAAAL reduction. Does it use the UPPAAL Closes to Target for this search. If so this is a problem as this is only a experimental feature in UPPAAL and some times returns a wrong answer. See bug (https://bugs.launchpad.net/tapaal/+bug/769875)

Also is Heuristic Search chosen as default by some special reason? Or is there a better default?

Question information

Kenneth Yrke Jørgensen (yrke) said : #1

It seems this is not the case, read the manual.

Jiri Srba (srba) said : #2

At the moment, the Heuristic Search uses BFS for all engines expect for the TAPAAL engine verifytapn with discrete inclusion
enabled, where the candidates from the waiting list are picked in the order so that they maximize the number of tokens
in the inclusion places.

It is the default option as it is often the choice that provides the fastest verification.