Spinroot

A forum for Spin users

You are not logged in.

#1 2011-10-11 16:20:38

mgarcia
Member
Registered: 2011-01-25
Posts: 2

LTL error

I have installed the latest Spin version. Spin detects a syntax error everytime I add a ltl formula. I attach here an example but the error occurs in every ltl formula and model.
Thank you so much


$ spin -a dekker.pml
spin: line   6 "dekker.pml", Error: syntax error    saw 'an identifier' near 'ltl'


/* Dekker's algorithm */
bool    wantp = false, wantq = false;
byte    turn = 1;
bool csp = false, csq = false;

ltl { []<>csp && []<>csq }

active proctype p() {
    do
    ::  wantp = true;
        do
        :: !wantq -> break;
        :: else ->
            if
            :: (turn == 1)
            :: (turn == 2) ->
                wantp = false;
                (turn == 1);
                wantp = true
            fi
        od;
        csp = true;
        assert (!(csp && csq));
        csp = false;
        wantp = false;
        turn = 2
    od
}

active proctype q() {
    do
    ::  wantq = true;
        do
        :: !wantp -> break;
        :: else ->
            if
            :: (turn == 2)
            :: (turn == 1) ->
                wantq = false;
                (turn == 2);
                wantq = true
            fi
        od;
        csq = true;
        assert (!(csp && csq));
        csq = false;
        wantq = false;
        turn = 1
    od
}

Offline

#2 2011-10-11 21:26:47

theo.ruys
Administrator
Registered: 2010-11-18
Posts: 11

Re: LTL error

What version of SPIN are you using?
(use "spin -v" to find out the version of SPIN)

At my side, SPIN 6.1.0 parses the above model without any problems.
I used the following (standard) commands to verify the example:

spin -a dekker.prom
gcc -o pan pan.c
./pan -a

And pan reports that the LTL property is not valid.

Offline

#3 2011-10-13 09:57:05

mgarcia
Member
Registered: 2011-01-25
Posts: 2

Re: LTL error

My mistake, I had the latest version of jspin that uses the spin version 5. I have installed the new version of spin and it works fine.
Thank you very much.

Offline

Board footer

Powered by FluxBB