[tlaplus] Re: How to explore states with all subset of a set ?

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;*)

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