Defining the set of all bags

[Dan Plyukhin]

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

[Felipe Oliveira Carvalho]

When modeling the process for Bounded Model Checking (the kind of checking TLC performs), your sets have to be bounded.

I usually solve this by defining a CONSTANT and then finding the biggest value I can use that still makes model checking run in reasonable time.

Something like `MaxNumMessages`.

—

Felipe

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/f25aa067-57b9-4907-9d8c-22bf9c5505cfn%40googlegroups.com.