Spinroot

A forum for Spin users

You are not logged in.

#1 2012-06-05 10:24:51

lz
Member
Registered: 2012-05-14
Posts: 9

Priorities and verification

Hello,

Is this a mistake or I misconfigured the verifier?
Normally the process M should not be executed before the end of H.
Do you have a comment...

With my thanks.

byte cnt;
active proctype M() priority 5 {
   int temp;
   ...
   set_priority(0, get_priority(1));   
   temp = cnt; temp++; cnt = temp;
}
active proctype H() priority 10 {
   int temp;
   temp = cnt; temp++; cnt = temp;
}
active proctype B() priority 1 {
   assert(_priority == 1 && cnt == 2);
}

spin -a  priorite1.pml
gcc -DMEMLIM=1024 -O2 -DXUSAFE -DSAFETY -DNOCLAIM -DNOREDUCE -w -o pan pan.c
./pan -m10000  -E
Pid: 4584
pan:1: assertion violated ((_priority==1)&&(cnt==2)) (at depth 10)
pan: wrote priorite1.pml.trail

(Spin Version 6.2.1 -- 14 May 2012)

Offline

#2 2012-06-05 17:28:09

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

Re: Priorities and verification

yes, this is a bug -- thanks.
a new version (6.2.2.) will be made available shortly

Offline

#3 2012-06-06 10:49:14

feng_lei_76
Member
Registered: 2011-05-13
Posts: 43

Re: Priorities and verification

I might find another bug from this example.  If I add a useless statement in process M before set_priority, then verification results with DFS and BFS searches are different.  DFS search finds the error, but BFS doesn't.

This is my Promela modle.

/******************************************************/
byte cnt;

active proctype M() priority 5
{
    int temp;
   
    temp = 0;
    set_priority(0, get_priority(1));   
    temp = cnt; temp++; cnt = temp
}

active proctype H() priority 10
{
   int temp;

   temp = cnt; temp++; cnt = temp
}

active proctype B() priority 1
{
   assert(_priority == 1 && cnt == 2)
}

Offline

#4 2012-06-09 18:46:23

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

Re: Priorities and verification

Will be fixed in Spin Version 6.2.2 -- you're right that this is a bug.

Offline

#5 2012-06-10 21:12:48

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

Re: Priorities and verification

The new version 6.2.2, with the fix, is now available.

Offline

Board footer

Powered by FluxBB