Differences between revisions 12 and 13
Revision 12 as of 2016-05-13 13:18:07
Size: 2743
Editor: XmlRpcBot
Comment:
Revision 13 as of 2016-05-13 13:59:41
Size: 2742
Editor: XmlRpcBot
Comment:
Deletions are marked like this. Additions are marked like this.
Line 26: Line 26:
 * ''randomized_order'' (bool): If true, use a 'globally'' randomized order, i.e. all transition systems are considered in an arbitrary order. This renders all other ordering options void.  * ''randomized_order'' (bool): If true, use a 'globally' randomized order, i.e. all transition systems are considered in an arbitrary order. This renders all other ordering options void.

This page describes the various merge strategies supported by the planner.

Merge strategy DFP

This merge strategy implements the algorithm originally described in the paper "Directed model checking with distance-preserving abstractions" by Draeger, Finkbeiner and Podelski (SPIN 2006), adapted to planning in the following paper:

merge_dfp(atomic_ts_order=regular, product_ts_order=new_to_old, atomic_before_product=false, randomized_order=false, random_seed=-1)
  • atomic_ts_order ({regular, inverse, random}): The order in which atomic transition systems are considered when considering pairs of potential merges.

    • regular: the variable order of Fast Downward

    • inverse: opposite of regular

    • random: a randomized order

  • product_ts_order ({old_to_new, new_to_old, random}): The order in which product transition systems are considered when considering pairs of potential merges.

    • old_to_new: consider composite transition systems from most recent to oldest, that is in decreasing index order

    • new_to_old: opposite of old_to_new

    • random: a randomized order

  • atomic_before_product (bool): Consider atomic transition systems before composite ones iff true.

  • randomized_order (bool): If true, use a 'globally' randomized order, i.e. all transition systems are considered in an arbitrary order. This renders all other ordering options void.

  • random_seed (int [-1, infinity]): Set to -1 (default) to use the global random number generator. Set to any other value to use a local random number generator with the given seed.

Linear merge strategies

This merge strategy implements several linear merge orders, which are described in the paper:

merge_linear(variable_order=CG_GOAL_LEVEL)
  • variable_order ({CG_GOAL_LEVEL, CG_GOAL_RANDOM, GOAL_CG_LEVEL, RANDOM, LEVEL, REVERSE_LEVEL}): the order in which atomic transition systems are merged

FastDownward: Doc/MergeStrategy (last edited 2024-01-11 22:26:37 by XmlRpcBot)