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

*From*: Maneet Bansal <maneet...@xxxxxxxxx>*Date*: Thu, 2 Aug 2018 19:14:51 -0700*References*: <0d952da0-3e9c-4d8a-85e2-bfeb743e9b03@googlegroups.com> <3a937bed-fb95-4566-a774-b26938b27426@googlegroups.com>

Hi Hillel,

Here is the definition of Max operator

Max(s) == {x \in s : \A y \in s : x >= y}

On Thu, Aug 2, 2018 at 3:13 PM, Hillel Wayne <hwa...@xxxxxxxxx> wrote:

Hi,I need to find all subsets of an integer range which are continuous. For example forInput:- 1..4output:- {1}, {2}, {3}, {4}, {1,2}, {2,3}, {3,4}, {1,2,3}, {2,3,4}, {1,2,3,4}I wrote the following operator and check with "Evaluate Constant _expression_ in TLC". It is giving me an unexpected output{s \in SUBSET {1,2,3,4}: /\ s # {}

/\ \A x \in s : IF x = Max(s) THEN TRUE \* if x is maximum of the range than TRUE ELSE (x+1) \in s} \* other wise x+1 should be there in the set

The output I am getting is

{s \in {{}, {1}, {2}, {3}, {4}, {1, 2}, {1, 3}, {1, 4}, {2, 3}, {2, 4}, {3, 4}, {1, 2, 3}, {1, 2, 4}, {1, 3, 4}, {2, 3, 4}, {1, 2, 3, 4}} : <_expression_ line 11, col 27 to line 12, col 428 of module MC> }

Question:-

1. What are these charcaters I am getting in the output? Is this some error?

I tried it on 1.5.7 and am getting the correct result. Could you share your definition of the Max operator?2. Is there a better/easier way of doing this?

In this case, instead of filtering out all of the sets that don't match your criteria, I think it's easier to generate all of the sets that do match your criteria. This would use a set map instead of a set filter:>>> {a..b: a, b \in {1,2,3,4}}{{}, 1..1, 2..2, 3..3, 4..4, 1..2, 2..3, 3..4, 1..3, 2..4, 1..4}We get the empty set because if a > b, then a..b is empty.Thanks

Maneet

Hillel--

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

Regards

Maneet Bansal

Maneet Bansal

**Follow-Ups**:**Re: [tlaplus] Re: Continuous subset of integer range***From:*Hillel Wayne

**References**:**Continuous subset of integer range***From:*Maneet Bansal

**Re: Continuous subset of integer range***From:*Hillel Wayne

- Prev by Date:
**Re: Continuous subset of integer range** - Next by Date:
**Re: [tlaplus] Re: Continuous subset of integer range** - Previous by thread:
**Re: Continuous subset of integer range** - Next by thread:
**Re: [tlaplus] Re: Continuous subset of integer range** - Index(es):