This paper deals with two relevant aspects of Supervisory Control Theory (SCT) of Discrete Event Systems: the difficulty faced to model specifications to be fulfilled by the system under control, and the computational cost to synthesize supervisors. These aspects are addressed by Extended Finite-state Machines (EFSMs), a version of ordinary finite-state machines, extended with variables. EFSMs have been used in SCT to facilitate modeling tasks, but they are not directly advantageous in synthesis. This paper shows that some variables can nevertheless be abstracted from an EFSM to compute a supervisor. The proposed approach has the modeling benefits of EFSMs while preserving controllability and least restrictiveness of control solutions, and the synthesis procedure can be conducted with computational gains. An algorithm to compute supervisors from abstractions is also proposed. A way to construct abstractions that always lead to optimal synthesis complements the contributions, which are illustrated by two examples of manufacturing systems.