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

*From*: Dan Plyukhin <dplyukhin@xxxxxxxxx>*Date*: Sat, 27 May 2023 11:45:34 -0700 (PDT)

I'm trying to specify the type of an _expression_ that ranges over bags of messages. I'd like to write something like this:

TypeOK == myVar \in [NodeID -> [delivered: BagOf(Msg), dropped: BagOf(Msg)]]

...which would have the following meaning:

IsABag(myVar[node].delivered) /\ BagToSet(myVar[node].delivered) \subseteq Msg /\

IsABag(myVar[node].dropped) /\ BagToSet(myVar[node].dropped) \subseteq Msg

How do you define BagOf(_) in a way that TLC can check efficiently? I see in the Bags module that IsABag(_) is defined as follows:

IsABag(B) ==

(************************************************************************)

(* True iff B is a bag. *)

(************************************************************************)

B \in [DOMAIN B -> {n \in Nat : n > 0}]

(************************************************************************)

(* True iff B is a bag. *)

(************************************************************************)

B \in [DOMAIN B -> {n \in Nat : n > 0}]

So my first guess was to define:

BagOf(S) == UNION { [B -> {n \in Nat : n > 0}] : B \in SUBSET S }

But TLC can't compute this if S is infinite. Any hints?

Dan

-- 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/f25aa067-57b9-4907-9d8c-22bf9c5505cfn%40googlegroups.com.

**Follow-Ups**:**Re: [tlaplus] Defining the set of all bags***From:*Felipe Oliveira Carvalho

- Prev by Date:
**Re: [tlaplus] Question about SYMMETRY optimization** - Next by Date:
**Re: [tlaplus] Defining the set of all bags** - Previous by thread:
**[tlaplus] review request: TLA+ model of Katzenpost/tor dirauth protocol** - Next by thread:
**Re: [tlaplus] Defining the set of all bags** - Index(es):