This paper proposes an approach for automatically generating model-based tests from a symbolic transition system built as an abstraction of a textual model description written using a pre/postcondition formalism. The abstraction gathers into equivalence classes states from which the same set of operation behaviors can be activated, computed using constraint solving techniques. This abstraction is then used to generate model-based tests using an online test generation technique in which the model animation is guided by the exploration of the abstraction. We apply this approach on the B abstract machines formalism, and compare with a commercial tool, named Leirios Test Generator. We show that our approach makes it possible to achieve a wider variety of test cases, by exploiting the knowledge of the model topology, resulting in an improved fault detection capability.