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

*From*: Felipe Oliveira Carvalho <felipekde@xxxxxxxxx>*Date*: Sat, 27 May 2023 20:49:20 -0300*References*: <f25aa067-57b9-4907-9d8c-22bf9c5505cfn@googlegroups.com>

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

On Sat, 27 May 2023 at 16:07 Dan Plyukhin <dplyukhin@xxxxxxxxx> wrote:

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

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/CAOC8YXZTvGKsGvh5CwPiudiDLNDZ1m%3DpJP6uNUD2gteKSrO0sg%40mail.gmail.com.

**References**:**[tlaplus] Defining the set of all bags***From:*Dan Plyukhin

- Prev by Date:
**[tlaplus] Defining the set of all bags** - Next by Date:
**Re: [tlaplus] Question about SYMMETRY optimization** - Previous by thread:
**[tlaplus] Defining the set of all bags** - Next by thread:
**[tlaplus] Installation on Ubuntu 22.04** - Index(es):