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

*From*: "thisismy...@xxxxxxxxx" <thisismyidashish@xxxxxxxxx>*Date*: Thu, 26 Oct 2023 16:38:51 -0700 (PDT)*References*: <e54b8176-d180-47db-b4e8-c73fe2290e07n@googlegroups.com> <4a762633-dfdb-4ace-b892-dc66bfb171f3n@googlegroups.com>

Learned to use `with` here from https://old.learntla.com/pluscal/behaviors/

(*--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, 26 October 2023 at 18:22:52 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/fe39c3db-79ed-465a-b849-07ffdb4d7009n%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] Re: How to explore states with all subset of a set ?** - Previous by thread:
**[tlaplus] Re: 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):