Spinroot

A forum for Spin users

You are not logged in.

#1 2011-01-11 07:24:47

crazyHorse
Member
Registered: 2011-01-10
Posts: 6

basic help with modex/feaver

Hi, i'm trying to use modex/feaver to generate my model to be used in spin, but i keep getting an undeclared error or parse error in pan.m . After using these commmands

$ modex main.prx
and
$ sh _modex_.run
In file included from pan.c:5320:
pan.m: In function `do_transit':
pan.m:23: error: `gate' undeclared (first use in this function)
pan.m:23: error: (Each undeclared identifier is reported only on
pan.m:23: error: for each function it appears in.)
pan.m:66: error: `gC' undeclared (first use in this function)
pan.m:78: error: `n' undeclared (first use in this function)
pan.m:116: error: `gS' undeclared (first use in this function)

Here are my source files
// main.c
#include "gate.h"
#define MAX 2

int main()
{
    int x;
    int y;
    int z;
    struct GATE_CONTROL gate;
   
    gate.numberOfEntries = 22;
    gate.maxNumber = 23;
    gate.state = OPEN;
    printf("%d",gate.state);
return 0;
}
// end main.c


// Gate.H
#ifndef GATE_H
#define GATE_H

int n;

typedef enum
{
   OPEN = 1,
   CLOSE = 0
}GATE_STATE;

struct GATE_CONTROL
{
  int numberOfEntries;
  int maxNumber;
  GATE_STATE state;
} ;

void setState(struct GATE_CONTROL gC, GATE_STATE gS);
int getState(struct GATE_CONTROL gC);
void Init(struct GATE_CONTROL gC, int n);

void setState(struct GATE_CONTROL gC, GATE_STATE gS)
{
    gC.state = gS;
}

int getState(struct GATE_CONTROL gC)
{
    return gC.state;
}

void Init(struct GATE_CONTROL gC, int n)
{
   
        gC.numberOfEntries = 0;
        gC.maxNumber = n;
        gC.state = OPEN;

}

#endif
//end Gate.H

//My test harnes file main.prx
%F main.c
%X -x
%L
import _all_
%%
//end main.prx

I'm sure something is missing in my test harness file, any help would be sincerely appreciated.

Offline

#2 2011-01-12 04:34:56

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

Re: basic help with modex/feaver

There are some limitations to how modex works, and I think you're being bitten by a few of these.
First, the complaint about 'gate' not being defined -- this is because gate is a local variable in main,
and I think the import _all_ statement in the .prx file only gives globals (I could be wrong).
You can add it by explicitly adding it with a c_decl statement in the .prc file
The second complaint is similar, 'gC' is this time a parameter to a function, which doesn't get extracted,
but you can again add it explicitly in the .prx file.
It is a bit of a black art to get modex extraction to work right -- usually one goes through lots of iterations of the .prx file before things are right.
All this is about a decade old and no longer maintained -- although the basic methodology is quite promising.
There has to be a simpler way to setup these runs though.

Typically the way to figure out what went wrong is to look at the 'model' file that is generated (after you execute the .run script) and see where it is lacking...

Offline

#3 2011-01-12 13:54:39

crazyHorse
Member
Registered: 2011-01-10
Posts: 6

Re: basic help with modex/feaver

Thanks for your prompt reply
I tried what you suggested and with a little tweaking of the "model" file it compiles now although Its still not clear to me how the model is extracted.
I am now trying to use modex with another program.
My state machine has a main.c where inputs are fed into the state machine, then there is another source file with functions that initialize the state machine,update its state and check whether inputs are vaild.

My question now is, do i extract the functions that make up the state machine or the main.c that inputs into my state machine.   

You said that modex is no longer maintained, has something replaced it? you also mentioned that modex has some limitations could you please elaborate on that.

Offline

#4 2011-01-12 16:48:19

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

Re: basic help with modex/feaver

I hope you found the user guide in the Doc/ directory from the distribution (i think it's called feaver.pdf) useful -- and the examples in the Examples/ directory.
Once the test harness is correctly setup, this tends to work amazingly well, and will allow you to prove both safety and liveness properties.
The biggest problem is often figuring out precisely what data must be tracked by the model checker. If you omit something essential, you can get very strange behavior...

If you have function calls, you can just leave them as such in the model (when they occur inside c_code { ... } fragments. The only downside of that is that the function calls will then be executed atomically. This very often is still sufficient to catch the errors though.

Most of the limitations are described in the documentation.
There is no successor tool yet, but we've mostly switched to a different approach that we've called "model-driven" verification (see for instance this paper: [url]http://spinroot.com/gerard/pdf/spin04.pdf[/url] or this one: [url]http://spinroot.com/gerard/pdf/ASE_J_2008.pdf[/url]  (both listed on [url]http://spinroot.com/gerard/pubs.html)[/url].
This is a lot easier to setup -- allows you to easily define abstractions -- and can also prove safety and liveness -- but it is not as fine-grained as modex.

Offline

#5 2011-01-18 07:33:53

crazyHorse
Member
Registered: 2011-01-10
Posts: 6

Re: basic help with modex/feaver

Thanks again for your help, I had a look at those papers. The way i understood what was going on in there was that you need to rewrite the source code in promela with the ability to include c code, I was trying to avoid coding in promela by using modex. So i guess i do not have a choice but to code the state machine in promela.

Offline

#6 2011-01-19 06:01:36

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

Re: basic help with modex/feaver

You'd have to write a driver only in Promela, but should be able to call the functions in the original source code as is. You do have to bypass the 'main' in the application though, and make sure the 'main' from spin (pan.c) is used when you compile, but it shouldn't be needed to rewrite the code other than these few things.
The hard part is in setting up the c_track statements correctly -- no easy way around that I'm afraid.

Offline

#7 2011-01-19 12:46:31

crazyHorse
Member
Registered: 2011-01-10
Posts: 6

Re: basic help with modex/feaver

Ok, i seem to be getting a better understanding now! I do have one question though, the promela driver would basically become the 'main', how do i include a .c file that has my functions in promela?

Offline

#8 2011-01-19 16:15:45

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

Re: basic help with modex/feaver

you call the C functions from within the driver, which is in Promela, by using embedded c_code or c_expr statements.
to get them to be part of the model, you simply compile the pan.c with the C source from your application: cc -o pan pan.c yourcode.c
you can use c_decl statements at the top of the spin model to add extern declarations where needed -- check out some of the examples in the example directory from the distribution, or the description in the user guide, for more detail?

Offline

#9 2011-01-20 14:57:00

crazyHorse
Member
Registered: 2011-01-10
Posts: 6

Re: basic help with modex/feaver

Hi again, Am i suppose to include header files of my source code in promela driver or pan.c? Reason im asking is coz when i compile gcc -o pan pan.c mycode.c i get parse errors for myFunc and  " data definition has no storage type or class " warnings for the struct instance it seems the compiler doesnt seem to know about my struct.

im doing something like this
promela driver
c_decl
{
extern void myFunc(myStruct *strInst);
extern myStruct mst;
}

init{
blah blah..
}

myCode.c

void myFunc(myStruct *st)
{

blah blah
}

myCode.h

typedef struct
{
int name;
}myStruct;

Offline

#10 2011-01-20 16:53:28

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

Re: basic help with modex/feaver

yes, if you use a datastructure that is unknown to spin (such as myStruct, which appears in the c_decl), then you also have to include a headerfile with the definition of that type.
you can do that by saying
c_decl {
\#include "header.h"
extern void myFunc(myStruct *strInst);
extern myStruct mst;
};

(remember the backslash in front of the c_decl -- it defers expansion to the pan.c file)

Also, you will probably want to track the contents of mst:

c_track "&mst" "sizeof(myStruct)";

if you get compiler errors -- you can also look at the generated code and figure out what's missing -- or maybe if things appear in the wrong place in the source.
it takes a bit of effort to get it all right. once it works it's great of course....

Offline

#11 2011-01-25 14:45:06

crazyHorse
Member
Registered: 2011-01-10
Posts: 6

Re: basic help with modex/feaver

Hi again!, What im trying to do now is use the test driver to read from a .PRN file and input those values into the state machine. I inserted an array bounds error in the update method to see if spin will pick it up, after running pan.exe spin doesnt seem to find the error. My question is: does it look like my test driver correctly driving my code through its states?
one more thing would it be incorrect to use a large c_code{} statement to do the file input? doing it that way picks up the array bounds error.


c_decl{
\#include "header.h"
\#include <stdio.h>
\#include <stdlib.h>
extern void myFuncInitialize(myStr *inst)
extern void myFunc2Update(myStr *inst, int num)
extern void myFunc3(myStr *inst)
extern myStr structure;
extern myStr1 str
int inputValue;
int ig;
char inputValuesArray [2];
FILE *inputFile;
};
c_track "&structure" "sizeof(myStr)";
c_track "&str" "sizeof(myStr1)";
init
{        //READS IN VALUES FROM A .PRN FILE AND INPUTS THEM TO THE STATE MAHCINE
    c_code
        {               
        inputFile = fopen("input.prn","r");
        myFunc1Initialize(&structure); //INITIALIZES THE STATE MACHINE WITH DEFAULTS           
        };
        if
        :: c_expr { (inputFile != NULL)} -> do::c_expr{(!feof(inputFile))} ->  c_code  {
                                                                                fgets(inputValuesArray,20,inputFile);
                                                                                ig = 0;
                                                                                        };
            do::c_expr{ig <=2} -> c_code {
                inputValue = inputValuesArray[ig];                   
                    switch (ig)
                {                   
                    break;                                   
                    case 1:   
                    structure.amount = (int)inputValue;
                    break;
                    case 2:    
                    structure.value = (int)inputValue;
                    break;               
                }   
                    ig++;
                myFunc2Update(structure,120);// UPDATES THE STATE MACHINE
                };
                :: else -> break
                od;
       
            c_code {
                    fclose(inputFile);
                   };   
        :: else ->  break
        od;
        ::else printf("cannot open file")
        fi;   
}

Offline

#12 2011-01-26 02:57:45

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

Re: basic help with modex/feaver

Remember that the model you're building and analyzing has to be closed: it must contain all information.
Here you're reading data from an external source (a file), and that defeats the model checking process because there is now state information beyond its reach (e.g., the file seek pointer).
If it is essential to read the data from some source, that source should become part of the model. You could do that by putting it incore in a static table that you're then reading -- with the read pointer being c_tracked.
Note that the DFS search engine must be able to go both forwards and backwards through the execution, so it needs to be able to backup and restore a previous state accurately. With external data the model checker wont be able to do so....

Offline

#13 2011-06-13 08:51:17

milon_mi7
Member
Registered: 2011-06-10
Posts: 13

Re: basic help with modex/feaver

HI, i am having some problem in spin. I have successfully install modex and can generate a model from a c file. but when i try to use spin command, it said command not found. is there any tutorial to show how to install modex and spin? i am using ubuntu 11.04. tutorial in windows is also appreciable.

Offline

#14 2011-06-13 16:44:46

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

Re: basic help with modex/feaver

have you looked at these instructions:
[url]http://spinroot.com/spin/Man/README.html#S1[/url]

Offline

#15 2011-10-01 20:45:35

BillKx
Member
Registered: 2011-10-01
Posts: 1
Website

Re: basic help with modex/feaver

The feaver.pdf file was very helpful in getting modex/feaver to generate a model to be used in spin. It really helps to look at the instructions. lol
Thanks.

Offline

Board footer

Powered by FluxBB