[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Specify Non deterministic specification
Hi i'm new user of TLA +. Did a small project and now trying to write spec but getting into little trouble. I have written informal spec earlier and would write complete spec before coding.
How to specify spec that uses non deterministic variable which then be used to specify property.
We have a graph. We choose a non deterministic number n, initialize it to represent length of a path.
unsigned int n;
# Constraint it btw 0 and k
assume( n >= 1 && n <= k);
# An array to store the path
unsigned int arry[n];
and then make sure that this array represents a cycle in the graph.
everything is fine but as the number n is non-deterministically chosen i have to write something like :
edge(arry -> arry) && edge(array -> arry ) && ... && edge(arry[n-1] -> arry[n]) && edge(arry[n] -> arry)
My only problem is how to specify "..." ?? Can i state this as ... ??