Spinroot

jllang

Member

From: Finland

Registered: 2021-05-05

Posts: 29

Obtaining the true model that goes to pan

Macro expansion and/or preprocessing seems to change the line numbers of my PROMELA models. Is there any way to see the exact PROMELA source code that goes to pan when I compile my model using `spin -a`? I'm planning to write a debugger-like trace analyzer tool. I need to be able to connect the line numbers occurring in traces reported by pan to those occurring in the true model. In the future, I might also want to be able to expand d_steps.

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: Obtaining the true model that goes to pan

yes, you can run the preprocessor manually (call gcc -E -x c model.pml)
just like spin does internally (main.c line 106)