specless.automaton.mps.should_use_BMPS_exact

specless.automaton.mps.should_use_BMPS_exact(num_strings_to_find: int, try_to_use_greedy: bool, is_deterministic: bool) → bool[source]

Determine if we should use BMPS_exact based on the type of automaton we have and what we actually want to solve for

Parameters:

  • num_strings_to_find – The number of viable strings to return. only BMPS_exact can acutually sample strings, so setting this > 1 guarantees the use of BMPS_exact.

  • try_to_use_greedy – whether to try using the MUCH faster greedy search algorithm. only possible if the automaton has deterministic transitions.

  • is_deterministic – if the automaton is deterministic. SWDFA_MPS only works on deterministic automata.

Returns:

whether to use the BMPS_exact solver or the SWDFA_MPS solver