A forum for Spin users
You are not logged in.
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
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
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