问题描述
我和 PROMELA 真的很挣扎。当我在模拟模式下运行我的文件时,我有一个断言冲突(这是正确的)。但是,当我在验证模式下运行相同的文件时,不会监视断言冲突。
这是我的代码:
/*****************************************************/
/*INPUT*/
/*****************************************************/
#define N 4
#define N_Types 2
#define MODE 0 /*No Failures mode*/
#define N_Failures 1
#define N_Messages 30
int process_broadcasting = 2
/*****************************************************/
/*GLOBAL VARIABLES*/
/*****************************************************/
#define NO_FAILURE 0
#define CRASH_FAILURE 1
#define BYZANTINE_FAILURE 2
typedef content {
int m[N_Messages]
}
typedef types {
content t[N_Types]
}
typedef bool_types {
bool bt[N_Types]
}
typedef sender {
types s[N]
}
int message_brodcasted = 1;
chan inputChannel[N] = [50] of { int,int,int};
bool executing[N] = true;
int state[N] = NO_FAILURE;
content messages_delivered[N];
/*****************************************************/
/*PROCESS*/
/*****************************************************/
/* Process */
active[N] proctype Proc() {
int ID = _pid;
int type,msg = message_brodcasted,from,process_neighbours[N];
types mr;
sender pr;
/*****************************************************/
/*LOCAL VARIABLES*/
/*****************************************************/
atomic{
if
:: ID == 0->
process_neighbours[0] = 0;
process_neighbours[1] = 1;
process_neighbours[2] = 3;
process_neighbours[3] = 2;
:: ID == 1->
process_neighbours[0] = 1;
process_neighbours[1] = 2;
process_neighbours[2] = 3;
process_neighbours[3] = 0;
:: ID == 2->
process_neighbours[0] = 2;
process_neighbours[1] = 3;
process_neighbours[2] = 1;
process_neighbours[3] = 0;
:: ID == 3->
process_neighbours[0] = 3;
process_neighbours[1] = 2;
process_neighbours[2] = 0;
process_neighbours[3] = 1;
:: else ->
skip;
fi;
}
/*****************************************************/
/*DECISION PATH*/
/*****************************************************/
atomic
{
if
:: process_broadcasting == ID ->
goto step0;
:: else ->
goto step1;
fi;
}
/*****************************************************/
/*ALGORITHM*/
/*****************************************************/
/******************************/
/*STEP 0*/
/******************************/
step0:
atomic
{
if
::(state[ID] == NO_FAILURE) ->
/*SEND(<0,msg>,N1*/
inputChannel[process_neighbours[1]]!0,msg,ID;
::(state[ID] == CRASH_FAILURE) ->
goto final_step;
::(state[ID] == BYZANTINE_FAILURE ) ->
if
:: true ->
skip;
fi;
fi;
}
atomic
{
if
::(state[ID] == NO_FAILURE) ->
/*SEND(<0,N0*/
inputChannel[process_neighbours[0]]!0,N3*/
inputChannel[process_neighbours[3]]!0,N2*/
inputChannel[process_neighbours[2]]!0,ID;
::(state[ID] == CRASH_FAILURE) ->
goto final_step;
::(state[ID] == BYZANTINE_FAILURE ) ->
if
:: true ->
skip;
fi;
fi;
}
/******************************/
/*STEP 1*/
/******************************/
step1:
executing[ID]=false;
atomic
{
do
/**************************/
/* VALIDATE CONDITIONS */
/**************************/
:: mr.t[0].m[0] >= 1->
msg=0;executing[ID]=true;break;
:: mr.t[0].m[1] >= 1->
msg=1;executing[ID]=true;break;
:: mr.t[0].m[2] >= 1->
msg=2;executing[ID]=true;break;
:: mr.t[0].m[3] >= 1->
msg=3;executing[ID]=true;break;
:: mr.t[0].m[4] >= 1->
msg=4;executing[ID]=true;break;
:: mr.t[1].m[0] >= 3->
msg=0;executing[ID]=true;break;
:: mr.t[1].m[1] >= 3->
msg=1;executing[ID]=true;break;
:: mr.t[1].m[2] >= 3->
msg=2;executing[ID]=true;break;
:: mr.t[1].m[3] >= 3->
msg=3;executing[ID]=true;break;
:: mr.t[1].m[4] >= 3->
msg=4;executing[ID]=true;break;
:: else ->
do
::inputChannel[ID]?type,from ->
if
::pr.s[from].t[type].m[msg]==0->
mr.t[type].m[msg]++;
pr.s[from].t[type].m[msg]=1;
break;
::else->
break;
fi;
od;
od;
}
step1_content:
atomic
{
if
::(state[ID] == NO_FAILURE) ->
/*SEND(<1,N0*/
inputChannel[process_neighbours[0]]!1,ID;
::(state[ID] == CRASH_FAILURE) ->
goto final_step;
::(state[ID] == BYZANTINE_FAILURE ) ->
if
:: true ->
skip;
fi;
fi;
}
/******************************/
/*STEP 2*/
/******************************/
step2:
executing[ID]=false;
atomic
{
do
/**************************/
/* VALIDATE CONDITIONS */
/**************************/
:: mr.t[0].m[0] >= 1->
msg=0;executing[ID]=true;break;
:: mr.t[0].m[1] >= 1->
msg=1;executing[ID]=true;break;
:: mr.t[0].m[2] >= 1->
msg=2;executing[ID]=true;break;
:: mr.t[0].m[3] >= 1->
msg=3;executing[ID]=true;break;
:: mr.t[0].m[4] >= 1->
msg=4;executing[ID]=true;break;
:: mr.t[1].m[0] >= 1->
msg=0;executing[ID]=true;break;
:: mr.t[1].m[1] >= 1->
msg=1;executing[ID]=true;break;
:: mr.t[1].m[2] >= 1->
msg=2;executing[ID]=true;break;
:: mr.t[1].m[3] >= 1->
msg=3;executing[ID]=true;break;
:: mr.t[1].m[4] >= 1->
msg=4;executing[ID]=true;break;
:: else ->
do
::inputChannel[ID]?type,from ->
if
::pr.s[from].t[type].m[msg]==0->
mr.t[type].m[msg]++;
pr.s[from].t[type].m[msg]=1;
break;
::else->
break;
fi;
od;
od;
}
step2_content:
atomic
{
if
::(state[ID] == NO_FAILURE) ->
/*SEND(<1,N2*/
inputChannel[process_neighbours[2]]!1,ID;
::(state[ID] == CRASH_FAILURE) ->
goto final_step;
::(state[ID] == BYZANTINE_FAILURE ) ->
if
:: true ->
skip;
fi;
fi;
}
atomic
{
if
::(state[ID] == NO_FAILURE) ->
/*SEND(<1,N1*/
inputChannel[process_neighbours[1]]!1,N3*/
inputChannel[process_neighbours[3]]!1,ID;
::(state[ID] == CRASH_FAILURE) ->
goto final_step;
::(state[ID] == BYZANTINE_FAILURE ) ->
if
:: true ->
skip;
fi;
fi;
}
/*****************************************************/
/*END STATE*/
/*****************************************************/
final_step:
executing[ID]=false;
do
:: inputChannel[ID]?type,from -> skip;
od;
}
/*****************************************************/
/*MONITOR*/
/*****************************************************/
active proctype Monitor() {
if
:: executing[0]==false && len(inputChannel[0])==0 && executing[1]==false && len(inputChannel[1])==0 && executing[2]==false && len(inputChannel[2])==0 && executing[3]==false && len(inputChannel[3])==0 -> //executing == 0 && traffic == 0 ->
assert(false)
atomic
{
/*****************************************************/
/* VALIDITY */
/*****************************************************/
int a,b,c;
if
:: state[process_broadcasting] == NO_FAILURE ->
if
:: messages_delivered[process_broadcasting].m[message_brodcasted] == 0 ->
assert(false);
:: else ->
skip
fi;
:: else ->
skip;
fi;
/*****************************************************/
/* INTEGRITY */
/*****************************************************/
a=0;
do
:: a < N ->
if
:: state[a] == NO_FAILURE ->
b=0;
do
:: b < N_Messages ->
if
:: messages_delivered[a].m[b] > 1 || (state[a] == NO_FAILURE && messages_delivered[a].m[b] > 0 && b!=message_brodcasted) ->
assert(false)
:: else
fi;
b++;
:: break;
od;
:: else;
fi;
a++;
:: break;
od;
/*****************************************************/
/* AGREEMENT */
/*****************************************************/
a=0;
do
:: a < N ->
if
:: state[a] == NO_FAILURE ->
b=0;
do
:: b < N ->
if
:: state[b] == NO_FAILURE ->
c=0
do
:: c < N_Messages ->
if
:: messages_delivered[a].m[c] > 0 ->
if
:: messages_delivered[b].m[c] > 0 ->
skip;
:: else ->
assert(false);
fi;
:: else
fi;
c++;
:: break;
od;
:: else
fi;
b++;
:: break;
od;
:: else
fi;
a++;
:: break
od;
}
fi;
}
基本上,我正在运行 4 个 Proc 进程,并且监视器正在等待执行结束以验证系统。在模拟模式下运行时,监视器进行验证,但是,在验证模式下运行时,监视器永远不会进入它的 if,反过来,也永远不会验证系统。
有人可以帮我吗? 谢谢你的时间
解决方法
暂无找到可以解决该程序问题的有效方法,小编努力寻找整理中!
如果你已经找到好的解决方法,欢迎将解决方案带上本链接一起发送给小编。
小编邮箱:dio#foxmail.com (将#修改为@)