Revision 13 as of 2016-05-13 13:59:41

Clear message

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)

Linear merge strategies

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

merge_linear(variable_order=CG_GOAL_LEVEL)