Spinroot

Laurapanizo

Member

Registered: 2011-07-19

Posts: 3

Embedded C code and partial order reduction

Hello everybody,
I would like to know if partial order reduction and statement merging are applied when there are embedded C code in the model.
I have read in "SPIN primer and reference manual" that statement mergin can be applied when there are code that only uses local data.
Does it holds when the local data is defined in c_state?
In addition I have seen that the examples in chapeter 17, the verification of the examples uses partial order reduction but I am not sure
If it is possible to reduce states when there are c_code that modify the value of PROMELA variables or C variables that are tracked.
There is any paper about partial order reduction and embed C code?

Thanks,
Laura

spinroot

forum

Registered: 2010-11-18

Posts: 695

Website

Re: Embedded C code and partial order reduction

yes, partial order reduction is used, but not for c_code fragments, since it is too hard to analyze those fragments for potential global effects on the state
there's no paper on this, because pretty much the above sentence says it all :-)