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

*From*: "thisismy...@xxxxxxxxx" <thisismyidashish@xxxxxxxxx>*Date*: Thu, 26 Oct 2023 16:22:52 -0700 (PDT)*References*: <e54b8176-d180-47db-b4e8-c73fe2290e07n@googlegroups.com>

Here is a concrete example:

----------------- MODULE test -----------------

EXTENDS Sequences, TLC, Integers, FiniteSets

(*--algorithm dls

variables Files = {1, 2, 3, 4, 5}

process DeleteFile = "DeleteFile"

variable someFiles

begin DeleteOp:

someFiles := CHOOSE x \in SUBSET { f \in Files : f < 5 } : TRUE;

print someFiles;

NextStep:

Files := Files \ someFiles

end process

end algorithm;*)

Changing CHOOSE line to

someFiles := \E x \in SUBSET { f \in Files : f < 5 } : TRUE;

fails as someFiles now is assigned TRUE,

and

someFiles := \E x \in SUBSET { f \in Files : f < 5 } : x;

fails as we need to return boolean instead of x.

On Thursday, 26 October 2023 at 16:12:11 UTC-5 thisismy...@xxxxxxxxx wrote:

HiI 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 DeleteWorkersprocess 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 ?ThanksAshish

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/4a762633-dfdb-4ace-b892-dc66bfb171f3n%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: How to explore states with all subset of a set ?***From:*'Ashish Negi' via tlaplus

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

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

- Prev by Date:
**[tlaplus] How to explore states with all subset of a set ?** - Next by Date:
**[tlaplus] Re: How to explore states with all subset of a set ?** - Previous by thread:
**[tlaplus] How to explore states with all subset of a set ?** - Next by thread:
**[tlaplus] Re: How to explore states with all subset of a set ?** - Index(es):