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

*From*: "'Ashish Negi' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Thu, 26 Oct 2023 16:37:03 -0700 (PDT)*References*: <e54b8176-d180-47db-b4e8-c73fe2290e07n@googlegroups.com> <4a762633-dfdb-4ace-b892-dc66bfb171f3n@googlegroups.com>

Below works: I need to use `with`. https://old.learntla.com/pluscal/behaviors/ is great.

(*--algorithm dls

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

process DeleteFile = "DeleteFile"

variable someFiles

begin DeleteOp:

with subset \in SUBSET { f \in Files : f < 5 } do

someFiles := subset

end with;

await Cardinality(someFiles) > 0;

NextWork:

print someFiles

end process;

end algorithm;*)

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

process DeleteFile = "DeleteFile"

variable someFiles

begin DeleteOp:

with subset \in SUBSET { f \in Files : f < 5 } do

someFiles := subset

end with;

await Cardinality(someFiles) > 0;

NextWork:

print someFiles

end process;

end algorithm;*)

On Thursday, October 26, 2023 at 6:22:52 PM UTC-5 thisismy...@xxxxxxxxx wrote:

Here is a concrete example:----------------- MODULE test -----------------EXTENDS Sequences, TLC, Integers, FiniteSets(*--algorithm dlsvariables Files = {1, 2, 3, 4, 5}process DeleteFile = "DeleteFile"variable someFilesbegin DeleteOp:someFiles := CHOOSE x \in SUBSET { f \in Files : f < 5 } : TRUE;print someFiles;NextStep:Files := Files \ someFilesend processend algorithm;*)Changing CHOOSE line tosomeFiles := \E x \in SUBSET { f \in Files : f < 5 } : TRUE;fails as someFiles now is assigned TRUE,andsomeFiles := \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/3209f3a4-5ace-4726-b5d3-f014a366e7abn%40googlegroups.com.

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

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

- Prev by Date:
**[tlaplus] Re: How to explore states with all subset of a set ?** - Next by Date:
**[tlaplus] Writing temporal formula predicated on step not being taken** - Previous by thread:
**[tlaplus] Re: How to explore states with all subset of a set ?** - Next by thread:
**[tlaplus] Writing temporal formula predicated on step not being taken** - Index(es):