A forum for Spin users

You are not logged in.

- Topics: Active | Unanswered

Pages: **1**

**Antony****Member**- Registered: 2011-07-20
- Posts: 3

Hello,

I have a problem with the use of indices in a formula ltl, that is, if I define a formula in which need to vary an index, e.g []<>occupied[ i ] for 0<=i<n, how can I do? In Spin is possible do this,how?, or you must list them ? that is :

[]<>occupied [ 0 ] && []<>occupied [ i ]&& ...&& []<>occupied [ n-1 ] ???

*Last edited by Antony (2011-07-23 14:33:02)*

Offline

seems to work as it should

for instance, try the following model, which works as it should:

byte occupied[5];

int i;

int n;

ltl p0 { []<>occupied [ 0 ] && []<>occupied [ i ]&& []<>occupied [ n-1 ] }

active proctype antony()

{

occupied[0] = 1;

}

Offline

maybe i misunderstood your question

do you mean: ls there a way to specify a quantified formula such as:

ltl p0 { forall i, []<>occupied [ i ] }

unfortunately, for that the answer is no..... you do have to expand the 'forall' manually alas

Offline

Pages: **1**