A forum for Spin users
You are not logged in.
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
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
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
So long,
Max
Offline