Spinroot

A forum for Spin users

You are not logged in.

#1 2011-07-23 14:31:57

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

Use the indices in formulas LTL

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

#2 2011-07-23 18:43:56

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

Re: Use the indices in formulas LTL

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

#3 2011-07-23 18:46:32

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

Re: Use the indices in formulas LTL

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

Board footer

Powered by FluxBB