微信公众号搜"智元新知"关注
微信扫一扫可直接关注哦！

为什么，在验证模式下，我的代码不会引发违反断言？普罗美拉

分类：编程问答

如何解决为什么，在验证模式下，我的代码不会引发违反断言？普罗美拉

我和 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 举报，一经查实，本站将立刻删除。

苹果市值2025年有望达4万亿美元
pythonJavaScriptjavaHTMLPHPreactjsC#AndroidCSSNode.jssqlrpython-3.xMysqLjQueryc++pandasFlutterangularIOSdjangolinuxswifttypescript路由器JSON路由器设置无线路由器h3c华三华三路由器设置华三路由器电脑软件教程arraysdocker软件图文教程Cvue.jslaravelspring-boot