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

Re: [tlaplus] How to set a default for CHOOSE?



Hello,

your approach is correct. Instead of checking emptiness via cardinality, I’d rather use a direct set comparison. Also, you can avoid some repetition using a LET definition, like so:

get_element(key) ==
  LET matches == { x \in some_set : x.key = key }
  IN IF matches = {} THEN [ key |-> 0 ]
     ELSE CHOOSE m \in matches : TRUE

Regards,
Stephan

> On 8 Aug 2018, at 12:42, wangq...@xxxxxxxxx wrote:
> 
> I'm using CHOOSE, but it will catch error when no element is satisfied by p.
> 
> In my situation, I want to choose one element from a set or get a default element.
> 
> Like this:
> 
> ```
> some_set == {[key |-> 1, x |-> 1], [key |-> 2, x |-> 3], ...}
> 
> get_element(key) == 
>  IF Cardinality({x \in some_set : x.key = key}) /= 0 
>  THEN CHOOSE x \in some_set : x.key = key 
>  ELSE [x |-> 0]
> 
> val == get_element(9).x
> ```
> 
> Is there a shorter way to represent `get_element`?
> 
> -- 
> 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...@xxxxxxxxxxxxxxxx.
> 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.