TAPAAL

TAPAAL Trunk Search Strategy

Asked by Kenneth Yrke Jørgensen

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

Language:
English Edit question
Status:
Solved
For:
TAPAAL Edit question
Assignee:
Jiri Srba Edit question
Solved by:
Kenneth Yrke Jørgensen
Solved:
Last query:
Last reply:
Revision history for this message
Kenneth Yrke Jørgensen (yrke) said : 		#1

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

Revision history for this message
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.