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

*From*: p.tollot@xxxxxxxxxxxxxxxxx*Date*: Sun, 15 Dec 2019 02:43:39 -0800 (PST)

Hi, i want to write a function that given a sequence will return a sequence as the one passed but without one element at random, this is my solution but it is wrong, someone can tell me why? And what would be a correct solution? Thanks

-- EXTENDS Integers, Sequences

Remove(i, seq) ==

[j \in 1..(Len(seq)-1) |-> IF j < i THEN seq[j]

ELSE seq[j+1]]

Random(S) == CHOOSE x \in S : TRUE

Err(seq) ==

Remove(Random({1..Len(seq)}), seq)

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+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2b6263b2-50cc-4591-b748-ea66d0b23bd8%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Eliminate random element from seq***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Command-line tool options** - Next by Date:
**Re: [tlaplus] Eliminate random element from seq** - Previous by thread:
**Re: [tlaplus] Command-line tool options** - Next by thread:
**Re: [tlaplus] Eliminate random element from seq** - Index(es):