A forum for Spin users
You are not logged in.
Pages: 1
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
Offline
Thank you i have got it now....
Offline
Pages: 1