modex on a C source file in a large project?

awesan · 2012-01-01 05:22:26

I see that the shell script "_modex_.run" that gets created by modex is hard-coded to use "spin4". Well, I can fix that to use "spin" (which is the latest SPIN tool). However, I am wondering whether it is up-to-date in being compatible with the latest SPIN.

Also, can I run "modex" on a C source file in a large project and will modex simply ignore the functions that are called which are found in other source files? The interesting aspect of the C source file is that the actual state machine that I would expect to be extracted is self-contained in that single file. The reason I am asking is that I have to do quite some work to actually compile that single source file and I wanted to know the scope of modex, if possible, before delving into this much. Thanks in advance.

spinroot · 2012-01-02 20:27:25

it should work with the current version of spin -- so yes, replacing spin4 with spin would work
(originally modex assumed spin version 4 as opposed to older versions of spin which did not support embedded c code)
any function not extracted is simply called atomically from within a c_code fragment. it just means that you have to link the code with the other functions to the pan executable, so that they are accessible for those calls.
if you have the full state machine in a single file then it shouldn't be too hard to make this work
the hardest part is always to make sure that all relevant data is tracked by the model checker, i.e., figuring out which c_track statements are missing when things don't seem to work right
the typical signature of things not seeming to work right is getting strange counter-examples that cannot be replayed later -- it means that c_track statements are missing. the trick is then to look at the first statement that cannot be replayed -- which is typically a conditional test -- and add c_track statements for the data that is part of that conditional test
it can be frustration, but there is documentation, and when it all works it's very powerful

awesan · 2012-01-04 23:22:11

Interesting and thanks. I will check this out, when I get a chance.

khemchicken · 2012-01-22 12:07:49

Thank you for this article. That’s all I can say. You most definitely have made this post into something special. You clearly know what you are doing, you’ve covered so many bases.Thanks!

________________________________

Last edited by khemchicken (2012-01-26 11:21:00)

Spinroot

#1 2012-01-01 05:22:26

modex on a C source file in a large project?

#2 2012-01-02 20:27:25

Re: modex on a C source file in a large project?

#3 2012-01-04 23:22:11

Re: modex on a C source file in a large project?

#4 2012-01-22 12:07:49

Re: modex on a C source file in a large project?

Board footer