Spinroot

A forum for Spin users

You are not logged in.

#1 2016-12-28 10:42:31

abet
Member
Registered: 2014-02-28
Posts: 14

How to control choices of executable clauses through Promela codes

Hello,

I am Tatsuya, a Spin user.  I am wondering if there exists a way
to control choices of executable clauses through Promela codes.

The following (named as foo.pml):

active proctype main() {
int i=0;
int x=0;
do
:: atomic { i<1 -> i++; x=1; }
:: atomic { i<2 -> i++; }
:: else -> break;
od;
assert(x==1);
}

has two executions:
the first clause; the second clause; break; ... , and
the second clause; the second clause; break; ... .
since there exist two executable clauses at first.

The assertion is violated.  Actually,
$ spin -a foo.pml; gcc -O0 -w -g -DSAFETY pan.c; ./a.out -c1

pan:1: assertion violated (x==1) (at depth 3)
pan: wrote foo.pml.trail

(Spin Version 6.4.6 -- 2 December 2016)
Warning: Search not completed
    + Partial Order Reduction

Full statespace search for:
    never claim             - (none specified)
    assertion violations    +
    cycle checks           - (disabled by -DSAFETY)
    invalid end states    +

State-vector 20 byte, depth reached 5, errors: 1
        9 states, stored
        0 states, matched
        9 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

The latter execution is a counterexample.  Next, I modify the
Promela code by exchanging the first and second clauses.  Of
course, Spin returns the same counterexample.  However, the
number of states is reduced as follows:

State-vector 20 byte, depth reached 3, errors: 1
        4 states, stored
        0 states, matched
        4 transitions (= stored+matched)
        0 atomic steps
hash conflicts:         0 (resolved)

I guess that the exploration strategy in the current version is
to choose the first clause if there exist multiple executable
clauses.  In this sense, I can control explorations of executions
by Spin through Promela codes.  However, this method depends on
implementation of Spin.

Could you tell me if there exists a way to control choices of
executable clauses through Promela codes?  For example,

do
#pragma priority(2)
:: atomic { i<1 -> i++; x=1; }
#pragma priority(1)
:: atomic { i<2 -> i++; }
:: else -> break;
od;

This looks useful for me because I often model algorithms while
expecting specific counterexamples.  Of course, if there is a
better way, could you tell me that?

Thank you in advance.

Tatsuya

# Although I have searched similar questions at this forum by
# using ``executable'', ``exploration'', ``clause'', etc., I
# could not find that.  If a similar question was asked, could
# you direct me to the thread?
#
# I also referred to some papers at SPIN workshops which proposed
# new partial order reductions, e.g.,
# D. Bosnacki and G.J. Holzmann ``Improving Spin's Partial-Order Reduction for Breadth-First Search''.
# However, they modify Spin itself, and are beyond my skill.

Offline

#2 2016-12-29 00:07:55

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

Re: How to control choices of executable clauses through Promela codes

Tatsuya,
The only way to enforce an order of evaluation is to do just that, but explicitly.
For instance, first test for the priority 1 case and only if that fails test for the priority 2 case.

Offline

#3 2016-12-29 04:15:58

abet
Member
Registered: 2014-02-28
Posts: 14

Re: How to control choices of executable clauses through Promela codes

Dear Professor Gerard J. Holzmann,
Thank you so much for the quick response.

I got it.  I manually lift up a clause according to a
counterexample which I expect, as follows:

do
:: atomic { i<2 -> i++; }
:: atomic { i<1 -> i++; x=1; }
:: else -> break;
od;
assert(x==1);

>>However, this method depends on implementation of Spin.
I am wondering if I was wrong.
>For instance, first test for the priority 1 case and only if that fails test for the priority 2 case.
This is defined by the Promela specification, isn't it?

Tatsuya

Offline

#4 2016-12-29 05:56:43

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

Re: How to control choices of executable clauses through Promela codes

yes it is

Offline

#5 2016-12-29 06:41:04

abet
Member
Registered: 2014-02-28
Posts: 14

Re: How to control choices of executable clauses through Promela codes

Thank you!  My questions have been completely resolved.

Offline

#6 2017-01-25 11:30:05

abet
Member
Registered: 2014-02-28
Posts: 14

Re: How to control choices of executable clauses through Promela codes

Dear Professor Gerard J. Holzmann,

May I ask one additional question?

>>>For instance, first test for the priority 1 case and only if that fails test for the priority 2 case.
>>This is defined by the Promela specification, isn't it?
>yes it is
You told me that SPIN chooses the first executable clause on a do
loop, and explores the execution trace first (The others are
postponed).  This is not an implementation-matter but defined by
a specification.

Could you tell me how I should cite the fact in my paper?  I
appreciate if you would tell me some literature/document.  I am
writing a paper about developing a software which uses SPIN as
backend engine.

# If no document is published (confidential), I would like to
# cite the SPIN forum, that is, to write ``I have confirmed the
# specification by the developer at the SPIN forum'' in my paper.

Tatsuya

Offline

#7 2017-01-25 16:45:32

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

Re: How to control choices of executable clauses through Promela codes

In a do-loop all executable options (determined by the first statement in each option sequence) are equally likely to be selected.
(you can check the semantics on the manual pages).
So, no, there's no special significance of the order in which options are listed.
The best reference to cite in a paper is the 2004 Spin textbook, where you can find all of this documented in detail.

Offline

#8 2017-01-26 02:21:45

abet
Member
Registered: 2014-02-28
Posts: 14

Re: How to control choices of executable clauses through Promela codes

Thank you so much for the quick response and information.
I immediately read your book!

Offline

Board footer

Powered by FluxBB