Spinroot
A forum for Spin users
You are not logged in.
- Topics: Active | Unanswered
Pages: 1
#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
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
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
Pages: 1