Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-27 14:54:44

blackhorse
Member
Registered: 2011-06-22
Posts: 3

Source code for asynchronous xxx automata

For the research purpose, I need to understand how to compute the asynchronous xxx automata from each instantiated process. Would you please tell me which source file(pangen?.c file or generated pan.? file) contains the function for computing such xxx?  Thank you very much!

Last edited by blackhorse (2011-11-27 14:54:57)

Offline

#2 2011-11-27 17:00:21

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: Source code for asynchronous xxx automata

you'll find a full description of the algorithm in the book 'the spin model checker - primer and reference manual'
the imementation in spin is an optimized version of this that is tuned very specifically to promela specifications
it's pretty much all the code in pan.c that is generated from pangen.h
(but that's a bad place to start looking - first understand the algorithms for synchronous and asynchronous xxx given in the book)

Offline

Board footer

Powered by FluxBB