From mboxrd@z Thu Jan 1 00:00:00 1970 Message-Id: <200412011102.iB1B2rd14890@zamenhof.cs.utwente.nl> To: Fans of the OS Plan 9 from Bell Labs <9fans@cse.psu.edu> Subject: Re: [9fans] spin models In-reply-to: Your message of "Wed, 17 Nov 2004 00:07:51." References: From: Axel Belinfante Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii Date: Wed, 1 Dec 2004 12:02:53 +0100 Topicbox-Message-UUID: 0fdcf704-eace-11e9-9e20-41e7f4b1d025 > i think a version of spin newer than that in plan 9 (ca. 2000) > supports channel passing and dynamic processes. > a glance at spinroot.com suggests that might be right. not that I'm much of a spin expert (we have one/some here, don't know if he/they will be available during twente9con), but running xspin (4.2.0) in simulation and/or verification mode on slave2.spin brings me further than rog suggested in his mail. wr.r.t. automatic transformation: (disclaimer as above) there has been work on extracting promela models from C code, http://spinroot.com/spin/News/news36.html so maybe doing something from limbo could be interesting/possible too. Axel.