Re: New Book: CONCURRENCY

[Oyvind Teig <Oyvind.Teig@xxxxxxxxxxxx>]

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/.

-- 

|=======================================|==========================|
| Oyvind Teig                           | oyvind.teig@xxxxxxxxxxxx |
| Navia Maritime AS, division Autronica | oyvind.teig@xxxxxxxxxxxx |
| 7005 Trondhem     |    http://www.navia.no | Tel:+47 73 58 12 68 |
| Norway            |http://www.autronica.no | Fax:+47 73 91 93 20 |
|===================|========================|=====================|