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

*From*: "thisismy...@xxxxxxxxx" <thisismyidashish@xxxxxxxxx>*Date*: Thu, 26 Oct 2023 14:12:11 -0700 (PDT)

Hi

I have a set `Files`. I want TLC to explore next steps of my `process` with all subset combinations of `Files`.

E.g.

process DeleteX \in DeleteWorkers

process DeleteOp:

someFiles := CHOOSE x \in SUBSET {p \in Files: p.size < TargetSize}: TRUE;

await Cardinatlity(someFiles) > 0;

... next steps ...

end process;

But i see that next steps are disabled with Total/Distinct states as 0/0.

I think it is because CHOOSE always takes `{}`.

How can i tell TLC to explore all `someFiles` where it is a subset of `Files with my predicate` applied ?

Thanks

Ashish

-- 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/e54b8176-d180-47db-b4e8-c73fe2290e07n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: How to explore states with all subset of a set ?***From:*thisismy...@xxxxxxxxx

- Prev by Date:
**Re: [tlaplus] Set vs Functions for modelling** - Next by Date:
**[tlaplus] Re: How to explore states with all subset of a set ?** - Previous by thread:
**Re: [tlaplus] Why vars is defined as tuples instead of set** - Next by thread:
**[tlaplus] Re: How to explore states with all subset of a set ?** - Index(es):