Spinroot

A forum for Spin users

You are not logged in.

#1 2021-08-22 09:15:31

jllang
Member
From: Finland
Registered: 2021-05-05
Posts: 27

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.

Offline

#2 2022-03-01 19:10:04

spinroot
forum
Registered: 2010-11-18
Posts: 691
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)

Offline

Board footer

Powered by FluxBB