assertion violation but values in trail suggest assertion was not viol

abhinavatul · 2012-03-23 22:55:22

I am getting the following on running the verifier
pan:1: assertion violated (blockdurationofprocess[ID]<=mymaxwaitpredictedbyprotocol[ID]) (at depth 2172)
pan: wrote m.pml.trail

On doing spin -t m.pml
mymaxwaitpredictedbyprotocol[0] = 4
mymaxwaitpredictedbyprotocol[1] = 4
mymaxwaitpredictedbyprotocol[2] = 0
numberofprocess = 3
queue 3 (blockedprocess):
blockdurationofprocess[0] = 0
blockdurationofprocess[1] = 0
blockdurationofprocess[2] = 0

I don't get how this is happening as all blocking duration <= corresponding maxwait in the trail

The code is below

#define MAX 3
#define MAX_PROCESS MAX
#define MAX_SEM 3
#define MAX_SEM_1 4
#define _2_MAX_SEM 6
#define _4_MAX_SEM 12
#define _1_4_MAX_SEM 12
#define _4_MAX_SEM_plus_1_4_MAX_SEM 24
#define MAX_CONTIGUOUS_SIMPLE_INSTRUCTION 3
typedef VECTOR
{
bool vector[MAX_SEM];
}
hidden VECTOR sema_set[MAX_PROCESS];
hidden byte random_sem[_2_MAX_SEM];
byte random_sem_counter;
byte program_counters[MAX_PROCESS];
typedef INSTRUCTION
{
byte sem[_4_MAX_SEM_plus_1_4_MAX_SEM];
bool p_or_v[_4_MAX_SEM_plus_1_4_MAX_SEM];
}
hidden INSTRUCTION p_execution_replacement[MAX_PROCESS];
inline generate_random_sem_sequence()
{

j = 0;
label1:
do
::random_sem_counter == 2*MAX_SEM -> break;
::else->
j = 0;
do
::j < MAX_SEM - 1 -> j = j + 1;
::j < MAX_SEM->break;
od;
random_sem[random_sem_counter] = j;
random_sem_counter = random_sem_counter + 1;
od;
}
inline insert_simple_instruction(i)
{
if
::true->p_execution_replacement[i].sem[program_counters[i]] = MAX_SEM;
p_execution_replacement[i].p_or_v[program_counters[i]] = 0;
program_counters[i] = program_counters[i] + 1;
::true->skip;
fi;
}
hidden byte maxPeriod;
bool p_created;
chan queue = [MAX] of { byte };
chan semaq = [MAX_SEM] of {byte,byte};
bool clockavailable = 0;
hidden byte semaceiling[MAX_SEM];
hidden byte mymaxwaitpredictedbyprotocol[MAX];
hidden byte numberofprocess;
chan blockedprocess = [MAX] of { byte};
hidden byte blockdurationofprocess[MAX] ;
chan blockedprocess_swap = [MAX] of { byte } ;
inline updateblocktimeofprocesses(ID)
{
do
:: nempty(blockedprocess)->
blockedprocess ? bp;
blockedprocess_swap !! bp;
if
::bp < ID ->
blockdurationofprocess[bp] = blockdurationofprocess[bp] + 1;
::else->break;
fi;
::empty(blockedprocess)->break;
od;
do
::nempty(blockedprocess_swap)->
blockedprocess_swap ? bp;
blockedprocess !! bp;
::empty(blockedprocess_swap)->break;
od;

}
inline release_blocked_processes(sema_ac)
{
if
::empty(semaq)->
   do
   ::nempty(blockedprocess)->
   blockedprocess ? bp;
   queue !! bp;
   ::empty(blockedprocess)->break;
   od;
::nempty(semaq)->
semaq?[prioriticeiling,_];
do
::nempty(blockedprocess)->
   blockedprocess ? bp;
   if
   ::bp >= prioriticeiling ->
   blockedprocess !! bp;
   break;
   ::else->
      queue !! bp;
   fi;
::empty(blockedprocess)->break;
od;
fi;
}
byte prioriticeiling;
byte owner;
byte ownerprioriti;
byte bp ;

proctype T(byte ID)
{
do
::
d_step
{
( queue ? [eval(ID)] ) && clockavailable ->
if
:: program_counters[ID] == _4_MAX_SEM_plus_1_4_MAX_SEM ->
queue ?? eval(ID);
numberofprocess = numberofprocess - 1;
program_counters[ID] = program_counters[ID] + 1;
:: else->
clockavailable = 0;
queue ? _;
if
::p_execution_replacement[ID].sem[program_counters[ID]] == MAX_SEM ->
program_counters[ID] = program_counters[ID] + 1;
queue !! ID;
updateblocktimeofprocesses(ID);
::p_execution_replacement[ID].sem[program_counters[ID]]!= MAX_SEM && p_execution_replacement[ID].p_or_v[program_counters[ID]] == 1->
if
::nempty(semaq)->semaq ? <prioriticeiling,owner>;

if
::prioriticeiling <= ID && owner != ID ->
blockedprocess !! ID;
:: prioriticeiling > ID || owner == ID ->
semaq !! semaceiling[p_execution_replacement[ID].sem[program_counters[ID]]],ID;
program_counters[ID] = program_counters[ID] + 1;
queue !! ID;
fi;
::empty(semaq)->
semaq !! semaceiling[p_execution_replacement[ID].sem[program_counters[ID]]],ID;
program_counters[ID] = program_counters[ID] + 1;
queue !! ID;
fi;
::p_execution_replacement[ID].sem[program_counters[ID]]!= MAX_SEM && p_execution_replacement[ID].p_or_v[program_counters[ID]] == 0 ->
queue !! ID;
semaq ?? eval(semaceiling[p_execution_replacement[ID].sem[program_counters[ID]]]),eval(ID);
release_blocked_processes(p_execution_replacement[ID].sem[program_counters[ID]]);
program_counters[ID] = program_counters[ID] + 1;

fi;
fi;
}
::program_counters[ID] == _4_MAX_SEM_plus_1_4_MAX_SEM + 1 ->break;

od;
assert(blockdurationofprocess[ID] <= mymaxwaitpredictedbyprotocol[ID]);
}

proctype clockworking()
{
do
::
d_step
{
!clockavailable ->
clockavailable = 1;
assert(nempty(queue) || (_nr_pr == 2));
}
::_nr_pr == 2 && p_created -> break;
od
}
typedef semcritic
{
byte firstmax;
byte secondmax;
}
inline initialise_upperblock_duration()
{
i = 0;
do
:: i == MAX_PROCESS -> break;
:: else ->
i1 = 0;
do
::i1 == MAX_SEM -> break;
::else->
semacritic[i1].firstmax = 0;
semacritic[i1].secondmax = 0;
semacritic_on[i1] = false;
i1 = i1 + 1;
od;
do
::program_counters[i] == _4_MAX_SEM_plus_1_4_MAX_SEM->break;
::else->
semap = p_execution_replacement[i].sem[program_counters[i]];
p_or_v = p_execution_replacement[i].p_or_v[program_counters[i]];
program_counters[i] = program_counters[i] + 1;
if
::semap == MAX_SEM ->
i1 = 0;
do
:: i1 == MAX_SEM ->break;
:: else->
if
::semacritic_on[i1] && semacritic[i1].secondmax == 0 ->
semacritic[i1].firstmax = semacritic[i1].firstmax + 1;
::semacritic_on[i1] && semacritic[i1].secondmax != 0 ->
semacritic[i1].secondmax = semacritic[i1].secondmax + 1;
::else->skip;
fi;
i1 = i1 + 1;

od;

::semap != MAX_SEM && p_or_v == 1 ->
   semacritic_on[semap] = true;
   if
   ::semacritic[semap].firstmax!=0->semacritic[semap].secondmax = 1;
   ::else -> semacritic[semap].firstmax = 1;
   fi;

::semap != MAX_SEM && p_or_v == 0 ->
   semacritic_on[semap] = false;
   if
   ::semacritic[semap].secondmax!=0->semacritic[semap].secondmax = semacritic[semap].secondmax + 1;
semacritic[semap].firstmax = (semacritic[semap].firstmax < semacritic[semap].secondmax -> semacritic[semap].secondmax : semacritic[semap].firstmax);
semacritic[semap].secondmax = 0;
   ::else->
      semacritic[semap].firstmax = semacritic[semap].firstmax + 1;
   fi;
::else->skip;
fi;
od;
{
   i1 = 0;
   do
   :: i1 == MAX_SEM -> break;
   :: else->
   if
::semacritic[i1].firstmax > 0 ->
process_index = 0;
   do
   ::process_index >= i -> break;
   ::else->
      if
::sema_set[process_index].vector[i1]==true && mymaxwaitpredictedbyprotocol[process_index] < semacritic[i1].firstmax ->
mymaxwaitpredictedbyprotocol[process_index] = semacritic[i1].firstmax;
process_index = process_index + 1;
::process_index > semaceiling[i1] && mymaxwaitpredictedbyprotocol[process_index] < semacritic[i1].firstmax ->
mymaxwaitpredictedbyprotocol[process_index] = semacritic[i1].firstmax;
process_index = process_index + 1;
::else->process_index = process_index + 1;

fi;
od;
::else->skip
fi;
i1 = i1 + 1;
od;
}

program_counters[i] = 0;
i = i + 1;
od;
}
byte i;
byte i1;
hidden byte semaphore;

hidden semcritic semacritic[MAX_SEM] ;
bool semacritic_on[MAX_SEM];
hidden byte semap;
hidden byte p_or_v;
byte process_index ;
init
{
bool sem[MAX_SEM] ;
i = 0;
i1 = 0;
do
:: i == MAX_SEM -> break;
:: else ->
sem[i] = false;
semaceiling[i] = MAX_PROCESS;
i = i + 1;
od;
i = 0;
byte j;
do
::i == MAX_PROCESS ->break;
::else->
j = 0 ;
program_counters[i] = 0;
do
:: j == MAX_SEM ->break;
::else ->
sema_set[i].vector[j] = false;
j = j + 1;
od;
i = i + 1;
od;
i = 0;
do
:: i == MAX_PROCESS -> break;
:: else->
   random_sem_counter = 0;
   generate_random_sem_sequence();
   random_sem_counter = 0;
   do
   ::random_sem_counter == 2*MAX_SEM ->break;
   ::else->
      semaphore = random_sem[random_sem_counter];
random_sem_counter = random_sem_counter + 1;
sema_set[i].vector[semaphore] = true;
if
::semaceiling[semaphore] > i -> semaceiling[semaphore] = i;
::else->skip;
fi;

if
::sem[semaphore] == true->
insert_simple_instruction(i);
p_execution_replacement[i].sem[program_counters[i]] = semaphore;
p_execution_replacement[i].p_or_v[program_counters[i]] = 0;
program_counters[i] = program_counters[i] + 1;
sem[semaphore] = false;
::else->
   sem[semaphore] = true;
   p_execution_replacement[i].sem[program_counters[i]] = semaphore;
   p_execution_replacement[i].p_or_v[program_counters[i]] = 1;
   program_counters[i] = program_counters[i] + 1;
   insert_simple_instruction(i);
fi;
   od;
   i1 = 0;
   do
   ::i1 == MAX_SEM -> break
   ::else->
      if
::sem[i1] == true->
insert_simple_instruction(i);
p_execution_replacement[i].sem[program_counters[i]] = i1;
p_execution_replacement[i].p_or_v[program_counters[i]] = 0;
program_counters[i] = program_counters[i] + 1;
sem[i1] = false;
::else-> skip;
fi;
i1 = i1 + 1;
   od;
   i1 = 0;
   do
   ::program_counters[i] == _4_MAX_SEM_plus_1_4_MAX_SEM -> break;
   ::else->
      p_execution_replacement[i].sem[program_counters[i]] = MAX_SEM;
p_execution_replacement[i].p_or_v[program_counters[i]] = 0;
program_counters[i] = program_counters[i] + 1;
   od;
   program_counters[i] = 0;
   i = i + 1;
od;
i = 0 ;
do
::i == MAX_PROCESS -> break;
::else->
mymaxwaitpredictedbyprotocol[i] = 0;
i = i + 1;
od;
i = 0;
initialise_upperblock_duration();
p_created = 0;
i = 0;
do
::i < MAX ->
blockdurationofprocess[i] = 0;
i++;
::i == MAX -> break;
od;
numberofprocess = MAX + 2;
i = 0;

bool flag[MAX_PROCESS];
i = 0;
do
:: i == MAX_PROCESS -> break;
:: else ->
flag[i] = true;
i = i + 1;
od;

i = 0;
clockavailable = 0;
run clockworking();
do
::i == MAX_PROCESS + 1 -> break;
::else->
i1 = 0;
do
::i1 < MAX_PROCESS -1 -> i1 = i1 + 1;
::true -> break;
od;
atomic
{
if
::flag[i1]-> queue!!i1;
flag[i1] = false;
run T(i1);
::else -> skip;
fi;
}
i = i + 1;
od;
p_created = 1;
do
::_nr_pr == 1 -> break;
od
}

spinroot · 2012-03-24 03:16:09

I would suggest removing all the 'hidden' keywords and see if it still happens.
The cause is likely in an unjustified use of hidden.

Spinroot

#1 2012-03-23 22:55:22

assertion violation but values in trail suggest assertion was not viol

#2 2012-03-24 03:16:09

Re: assertion violation but values in trail suggest assertion was not viol

Board footer