Simulation and Test-Case Generation for PVS Specifications of Control Logics