Does SPIN support CTL for expressing constraints now?
I googled for a while and I found out some papers proposed CTL or CTL* Model checking for SPIN. However, according to Promela manual page, there is no way how to express CTL in Promela model. Is it just in a proposal level now?
I just used it a few months ago, but checked back to make sure. After skimming through their recent release notes, I have to say no. It still only supports checking of LTL properties, unless you have access to certain research projects.
Yes, proposal/promice. Nevetheless you might be able to validate CTL on Promela by compiling it to NuSVM https://code.google.com/archive/p/s2n/