[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [tlaplus] Specify Non deterministic specification

Thanks, I got the idea and i used book stated at TLA+ webpage, Named hyperbook (i think) ...  Sorry for not stating what i already represented as TLA+ spec. Actually i was only thinking of representing and as i have written informal spec i was wondering how i should specify it. Thanks .. 

On Monday, October 31, 2016 at 1:54:32 AM UTC+5:30, Stephan Merz wrote:

what material did you use for learning TLA+? Since you state your problem in terms of programming notation, it is not so obvious what parts of your problem you have already expressed in TLA+, and indeed what your objective is.

I am assuming that the graph is a constant, represented by the edge relation.


ASSUME edge \subseteq Int \X Int

It looks to me that you wish to define cycles in your graph. Paths can be represented as sequences of integers, so you could define something like

IsCycle(p) ==
  /\ \A n \in 1 .. Len(p)-1 : << p[n], p[n+1] >> \in edge
  /\ << p[Len(p)], p[1] >> \in edge

It is not clear to me what you use the array for.

Hope this gives you some ideas.

Best regards,

On 30 Oct 2016, at 21:07, Mr. Gogo <ashl...@xxxxxxxxx> wrote:

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.

For eg.

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[0] -> arry[1]) && edge(array[1] -> arry [2]) && ... && edge(arry[n-1] -> arry[n])  && edge(arry[n] -> arry[0])

My only problem is how to specify "..." ?? Can i state this as ... ??


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.