[tlaplus] Defining the set of all bags

[Dan Plyukhin <dplyukhin@xxxxxxxxx>]

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}]

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.