Jeremy Martin and S.A.Jassim did a state-implosion(?) in their "A Tool for Proving Deadlock Freedom" at WoTUG-20. Jeremy mentioned at the presentation that it might be done on occam, or a subset of it. What's the state? The psychology that Denis mentioned is important. I'm SO POSITIVE to these things, but I am a real programmer in the worst sense, and can't find a place to start filling up the semantics/syntactic gap. I WANT ONE LANGUAGE FOR MODELING AND IMPLEMENTATION no matter if things are 10exp8. I don't hear what your're saying. The SPoC occam->smv, what state is it in? = Could I download (like) the free The SMV Model Checker from = http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/ and start off with occam NOW? Will it accept my 20000 lines of occam, or will I have to write a "model"-occam? Could this community make an occam->FSP translation (FSP is the language they have defined in the CONCURRENCY book) - or is that a waste if we have occam->smv? Where does SPIN come into this picture? (Extract from my html data-base:) Reliable design of concurrent software, Holzmann, = Dr.Dobb's Journal, October 1997, SPIN, XSPIN and PROLEMA,Chan-of-protocol metalanguage for analyzing = deadlocks etc. http://netlib.bell-labs.com/netlib/spin/. -- = |=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D|=3D=3D=3D=3D=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D| | Oyvind Teig | oyvind.teig@autronica.no | | Navia Maritime AS, division Autronica | oyvind.teig@computer.org | | 7005 Trondhem | http://www.navia.no | Tel:+47 73 58 12 68 | | Norway |http://www.autronica.no | Fax:+47 73 91 93 20 | |=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D|=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D|=3D=3D=3D=3D=3D= =3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D=3D|