Epispin (in the Promela and Spin editor option screen) will not allow filenames such as def.h.pml whereas such filenames are accepted in spin.
Without the .pml (of course) the filename still contains a point, which seems to be not allowed.

Also, when the user, by accident, types in the .pml extension, the filename is rejected.
This could be made somewhat friendlier.

Submitted by Kees Pronk on 23 August 2011 at 12:44

I’ve changed this. When a filename ends in .OPT or .PML, it is rejected with the error message “Enter the filename without extensions”. All other filenames are allowed.