Approach 3: Test sequence Generation from Controllable EFSM
Controllable EFSM-- identify controllable predicates (i.e. predicates involving input parameters)-- split states with uncontrollable predicates
Non-exhaustive Test Property (e.g. Counter)-- do not fully expand certain regular structure, e.g. counter-- number of state is saved dramatically.