Spinroot

A forum for Spin users

You are not logged in.

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

abhinavatul
Member
Registered: 2012-03-23
Posts: 2

assertion violation but values in trail suggest assertion was not viol

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
}

Offline

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

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

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

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

Offline

Board footer

Powered by FluxBB