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

*From*: bongiovanni francesco <bongi...@xxxxxxxxx>*Date*: Thu, 3 Mar 2016 04:51:31 -0800 (PST)*References*: <890b8393-0a71-46dc-9fc3-d2abb8680090@googlegroups.com> <2A528B14-A8E1-49C7-B2D0-FECE2655B3A8@gmail.com> <c1a20ea1-15f3-47bc-a7fd-b6005343aff6@googlegroups.com> <5AD58E34-0168-443B-AB94-BE9C52433140@gmail.com>

Yes exactly, rookie mistake :D

Thanks again for your insights !

On Thursday, 3 March 2016 13:31:17 UTC+1, Stephan Merz wrote:

Thanks again for your insights !

On Thursday, 3 March 2016 13:31:17 UTC+1, Stephan Merz wrote:

SumSet({<<1,2,3>>, <<1,2,3>>, <<1,2,3>>}) = <<1,2,3>>, actually the good result should be : <<3,6,9>>That shows that you don't want the input given as a set:{<<1,2,3>>, <<1,2,3>>, <<1,2,3>>} = {<<1,2,3>>}It's easy to adapt the function so that it takes a sequence of sequences as input.Cheers,StephanOn Thursday, 3 March 2016 12:06:12 UTC+1, Stephan Merz wrote:Hi Francesco,as far as I can tell, your function is not well specified for an empty set of sequences, so I'll assume that the function need produce the correct result only when the input set is non-empty. I'll also assume that all sequences have the same length. Then you can write something like the following(* Auxiliary function to sum the i-th components of all sequences in S *)sumi(i,S) ==LET s[T \in SUBSET S] ==IF T = {} THEN 0ELSE LET x == CHOOSE x \in T : TRUEIN x[i] + s[T \ {x}]IN s[S]SumSet(S) ==LET l == Len(CHOOSE x \in S : TRUE)IN [i \in 1 .. l |-> sumi(i,S)](Of course, you can put the definition of sumi inside the LET in the definition of SumSet if you don't want that operator to be visible on the top level.)I used TLC to check thatSumSet({<<1,2,3>>, <<3,4,6>>) = <<4,6,9>> andSumSet({<<1,2,3>>, <<1,2,3>>, <<1,2,3>>}) = <<1,2,3>>Best,StephanHello,

I was wondering how one would specify in an elegant way the sum of finite sequences of integer in a set S.

Example:

Let S = { << 1,2,3 >>, << 3,4,6 >> }

The result of the function would be : << 1+3, 2+4, 3+6>> that the finite sequence <<4,6,9>>

The function has to work for an arbitrary number of finite sequences, provided they have the same length obviously.

Could someone guide towards this spec please ?

Thanks in advance !

- Francesco--

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...@googlegroups.com.

Visit this group at https://groups.google.com/group/tlaplus .

For more options, visit https://groups.google.com/d/optout .--

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**:**Element-wise sum of a set of finite sequences***From:*bongiovanni francesco

**Re: [tlaplus] Element-wise sum of a set of finite sequences***From:*Stephan Merz

**Re: [tlaplus] Element-wise sum of a set of finite sequences***From:*bongiovanni francesco

**Re: [tlaplus] Element-wise sum of a set of finite sequences***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Element-wise sum of a set of finite sequences** - Next by Date:
**Announcing Sbuilder - a tool to generate TLA+ model for business IT systems** - Previous by thread:
**Re: [tlaplus] Element-wise sum of a set of finite sequences** - Next by thread:
**Announcing Sbuilder - a tool to generate TLA+ model for business IT systems** - Index(es):