Spinroot

A forum for Spin users

You are not logged in.

#1 2013-05-17 14:08:56

pratikdesai12
Member
Registered: 2013-05-16
Posts: 7

inline text too long near 'BankClient.pml'

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();
  }
}

Offline

#2 2013-05-19 01:05:40

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

Re: inline text too long near 'BankClient.pml'

It looks like a number of macros are defined in the include files, which aren't visible here.
If the length of any of he inlines exceeds the maximum, try splitting it up into smaller pieces?

Offline

#3 2013-05-23 15:05:55

pratikdesai12
Member
Registered: 2013-05-16
Posts: 7

Re: inline text too long near 'BankClient.pml'

Thank you i have got it now....

Offline

Board footer

Powered by FluxBB