Spinroot

A forum for Spin users

You are not logged in.

#1 2015-09-08 12:20:17

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Confusion about %X parameters within test harness (modex)

Greetings to everyone,

After working with Modex and SPIN for a while, I discovered a strange behaviour when it comes to using the %X command within a test harness.
I want to extract some functions from the C code and turn them into different type of processes within the resulting PROMELA model.

A simple version of my intended use would be the following:

My c-code:

void foo_a () {
	printf("I want to be an active proctype\n");
}

void foo_p () {
	printf("I want to be a passive proctype!\n");
}

void foo_n () {
	printf("I want to be a proctpye without capsulation!\n");
}

My test harness:

%X -p foo_p	// Turn into passive proctype
%X -a foo_a	// Turn into active proctype
%X -n foo_n	// Don't encapsulate into proctype
%L
printf(...	keep
%%
%P
	active proctype p_foo_n () 
	{
		//Some model-based PROMELA code...
		#include "_modex_foo_n.pml"	//Manually wrap into active proctype
	}	
%%

My expectation is that all functions appear as proctypes in the model file: "foo_p" just as an ordinary proctype, "foo_a" as an active proctype and "foo_n" also as an active one, but manually transfered into the proctype "p_foo_n" through the %P command.

After running modex over the test harness (without errors), the model file looks like this:

// Generated by MODEX Version 2.8 - 1 September 2015
// Tue Sep  8 13:08:54 CEST 2015 from test.prx

 active proctype p_foo_n ()
 {
       printf("I want to be a proctpye without capsulation!\n");
;
 }

When I replace the "-n" flag with a "-p" or a "-a" just like the other two functions, everything looks dandy (although not as originally planed):

// Generated by MODEX Version 2.8 - 1 September 2015
// Tue Sep  8 13:04:20 CEST 2015 from test.prx

 active proctype p_foo_n ()
 {
proctype p_foo_n()
{
       printf("I want to be a proctpye without capsulation!\n");
}
 }
proctype p_foo_n()
{
       printf("I want to be a proctpye without capsulation!\n");
}
active proctype p_foo_a()
{
       printf("I want to be an active proctype\n");
}
proctype p_foo_p()
{
       printf("I want to be a passive proctype!\n");
}

I now have a double-capsulation that won't work when I try to use this model as input for SPIN; but all the functions have been turned into proctypes as planed.
So I am wondering why modex ignores the other %X commands when I use the -n flag for this one process?
Is there more to know about this particular flag or is this just a bug within Modex?

Maybe someone here has some ideas or suggestions regarding this. For the meantime, I will try to find a work-around without the use of uncapsulated proctypes.


So long,
Max

Offline

#2 2015-09-09 21:04:30

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

Re: Confusion about %X parameters within test harness (modex)

If you include an explicit %P fragment in the test-harness, then
modex will assume that this is the model template. So if you
want to include the generated pieces -- you have to choose the
place for it.  You can do so by adding, for instance,

#include "_modex_foo_a.pml"

at the start of the %P fragment.
If you want to see the filenames that correspond to the extracted
proctypes or proctype fragments:

$ modex -v foo.prx
$ ls -l *_modex*.pml

Offline

#3 2015-09-15 10:52:23

Schachtschabel
Member
Registered: 2015-08-28
Posts: 15

Re: Confusion about %X parameters within test harness (modex)

I think I got it now...

So defining a %P means describing the model in total; everything you want to include has to go there. So if you want to wrap some processes with a custom enviroment (like foo_p in my case), then that goes into the %P-section with an "#include". If I do that, I have to include the other proctypes as well, since they will be translated, but not included in the final model.

Looks like I could have guessed this on my own...

Anyway, big thanks from my side (again) for the support big_smile 


So long,
Max

Offline

Board footer

Powered by FluxBB