Revision 5 as of 2015-07-28 15:10:45

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. This strategy performs 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. This strategy performs 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. This strategy performs 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)