Spinroot

i keep trying to run my code when is run with
$spin -a + .pml file its works properly and does not give me any error but when i try compiling it with
$ cc -o pan pan.c it gives me the above mentioned error.
i dont have clue what does it mean and i am stuck here
please help.

I am working on validation a contract for which i use spin. when i ask spin to validate it gives me the error "inline text too long near 'BankClient.pml'" . i know the length of inline definition is 64k, but i dont know how to remove this error. please help.
here is the code of the promela file.

#include "setting.h"      /* macro definition */
#include "BizOperation.h" /* macro definition */
#include "rule.h"        /* Transfer rule code */

#define TRUE  1
#define FALSE 0
#define YES   1
#define NO    0

#define AbnContractEnd (abncoend==TRUE)

/* var for recording occurrences of executions
* with S and BF outcomes                     
*/
bool abncoend=FALSE;
bool DebitAFailBefore=NO;
bool CreditBFailBefore=NO;
bool CreditAFailBefore=NO;

/* declaration of the 3 role players involved */
RolePlayer(BANKA,BANKB,CLIENT);

/* account for S,F,TO execution outcome,
* in this ex, we use only S and F */
RuleMessage(S,F,TO);

/* 5 operations are involved in the contract */
BIS_OP(DEBITA);
BIS_OP(CANCEL);
BIS_OP(CREDITB);
BIS_OP(CREDITA);
BIS_OP(CANCEL);

/* Event Generator */
proctype EG()
{
BEGIN_INIT:
{
/* Define the initial state of the rights (R),
  * obligations (O) and prohibitions (P) of the 2
  * role players following:
  * INIT(OperName, RolePlayerName, R,O,P)
  * 1 means granted, 0 means not granted 
  * In initial state buyer has been granted the
  * right to execute DEBITA. No other R,O,P are
  * granted to CLIENT */
  DONE(BANKA);
  DONE(BANKB);
  DONE(CLIENT);

  INIT(DEBITA,  CLIENT, 1,0,0);
  INIT(CANCEL,  BANKA, 0,0,0);
  INIT(CREDITB, BANKB, 0,0,0);
  INIT(CANCEL,  BANKB, 0,0,0);
  INIT(CREDITA, BANKA, 0,0,0);
}
END_INIT:

/* generation of events.
  * For each of the 5 operations, 2 possible exec
  * are modelled: exec with S and exec with F */
end:do
:: B_E(CLIENT, DEBITA,  S); 
:: B_E(CLIENT, DEBITA,  F);

:: B_E(CANCEL, BANKA,  S);
:: B_E(CANCEL, BANKA,  F);

:: B_E(CREDITB, BANKB, S);
:: B_E(CREDITB, BANKB, F);

:: B_E(CANCEL, BANKB,  S);           
:: B_E(CANCEL, BANKB,  F);             

:: B_E(CREDITA, BANKA, S);           
:: B_E(CREDITA, BANKA, F);
od;
}

/* contract rule manager: it uses the rule.h
* file declared in the inline definition.
* It retrieves and includes the rule (one at a
* time) needed to respond to the event under
* process                                   
*/
proctype CRM()
{
printf("CONTRACT RULE MANAGER");
end:do
  :: CONTRACT(DEBITA);  /* include RULE(DEbITA) */
  :: CONTRACT(CANCEL);  /* include RULE(CANCEL) */
  :: CONTRACT(CREDITB);
  :: CONTRACT(CANCEL);
  :: CONTRACT(CREDITA);
od;
}

init
{
  atomic /* start exec of EG and CRM */
  {
   run EG();
   run CRM();
  }
}