Revision 7 as of 2015-07-28 16:45:29

Clear message

Bismulation based shrink strategy

This shrink strategy implements the algorithm described in the paper:

shrink_bisimulation(max_states=-1, max_states_before_merge=-1, threshold=-1, greedy=false, at_limit=RETURN)

shrink_bisimulation(max_states=infinity, threshold=1, greedy=true): Greedy bisimulation without size bound (called M&S-gop in the IJCAI 2011 paper).Combine this with the linear merge strategy REVERSE_LEVEL to match the heuristic in the paper. When we last ran experiments on interaction of shrink strategies with label reduction, this strategy performed best when used with label reduction before shrinking (and no label reduction before merging).

shrink_bisimulation(max_states=N, greedy=false): Exact bisimulation with a size limit (called DFP-bop in the IJCAI 2011 paper), where N is a numerical parameter for which sensible values include 1000, 10000, 50000, 100000 and 200000. Combine this with the linear merge strategy REVERSE_LEVEL to match the heuristic in the paper. When we last ran experiments on interaction of shrink strategies with label reduction, this strategy performed best when used with label reduction before shrinking (and no label reduction before merging).

f-preserving shrink strategy

This shrink strategy implements the algorithm described in the paper:

shrink_fh(max_states=-1, max_states_before_merge=-1, threshold=-1, shrink_f=HIGH, shrink_h=LOW)

shrink_fh(max_states=N): f-preserving shrinking of transition systems (called HHH in the IJCAI 2011 paper, see shrink_bisimulation). Here, N is a numerical parameter for which sensible values include 1000, 10000, 50000, 100000 and 200000. Combine this with the linear merge strategy CG_GOAL_LEVEL to match the heuristic in the paper. When we last ran experiments on interaction of shrink strategies with label reduction, this strategy performed best when used with label reduction before merging (and no label reduction before shrinking).

Random

shrink_random(max_states=-1, max_states_before_merge=-1, threshold=-1)