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

*From*: "Mr. Gogo" <ashle...@xxxxxxxxx>*Date*: Sun, 30 Oct 2016 14:01:07 -0700 (PDT)*References*: <e27cada5-9848-43df-a982-1c5848e6b56a@googlegroups.com> <727AEDB0-C2C2-4F65-9D5F-2A7E620FD130@gmail.com>

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:

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

Hello,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.EXTENDS IntegerCONSTANT edgeASSUME edge \subseteq Int \X IntIt 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 likeIsCycle(p) ==/\ \A n \in 1 .. Len(p)-1 : << p[n], p[n+1] >> \in edge/\ << p[Len(p)], p[1] >> \in edgeIt is not clear to me what you use the array for.Hope this gives you some ideas.Best regards,StephanOn 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 ... ??

Thanks

--

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 .

**References**:**Specify Non deterministic specification***From:*Mr. Gogo

**Re: [tlaplus] Specify Non deterministic specification***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Specify Non deterministic specification** - Next by Date:
**operator `\sim_x' as defined in erratum differs from TOPLAS** - Previous by thread:
**Re: [tlaplus] Specify Non deterministic specification** - Next by thread:
**operator `\sim_x' as defined in erratum differs from TOPLAS** - Index(es):