We present a virtual machine architecture designed to provide an executional interpretation for a major subset of the Generalised Substitution Language and its probabilistic extension _p GSL, including bounded non-determinism and infeasible operations. The virtual machine techniques we use to support abstract program execution are reversible execution and execution cloning. The architecture we propose will also allow the efficient execution of concrete programs, and a free mixture of abstract and concrete components, so it is possible to envisage a blurring of the distinction between the animation of a specification and the execution of its implementation.