How to explore states with all subset of a set ?

[thisismy...@gmail.com]

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

[thisismy...@gmail.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.

[thisismy...@gmail.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;*)