Set comprehension in VDM++

I've defined 2 types:

public string = seq1 of char;
public config = map string to bool;

I've also defined a test set: dcl subFeatures : set of string := {"test1", "test2", "test3"}.

And I'm trying to generate a set of valid configs by:

{ elem | elem : config & dom elem = subFeatures and {true} subset rng elem }

A config is called "valid" when it has at least one true range value.

Overture is launching an error Error 4: Cannot get bind values for type config. After an investigation I found that Overture by default cannot handle type binds for infinite types, but this is not the case, I'm restricting the map domain.

Can anyone with some more experience check what I am doing wrong?

Solution

Although what you've written is valid VDM++, the interpreter can only enumerate a type bind (ie. "elem : config") if it is a finite type, as you say. However, the interpreter also cannot determine that you have reduced the infinite type to a finite number of elements. So this fails at runtime.

For the interpreter to work, you would need to use a set bind over the subFeatures and create "elem |-> true" for each.

EDIT:

After some deliberation and help, I think we can conclude that this either isn't possible with a non-type-bind comprehension, or it would be horribly complicated. The functions below will implement what you require though, I think:

PossibleMappings: set of seq1 of char * map seq1 of char to bool -> set of map seq1 of char to bool
PossibleMappings(s,m) ==
    if s = dom m
    then {m}
    else let e in set s be st e not in set dom m in
        dunion {PossibleMappings(s, m munion {e |-> true}),
                PossibleMappings(s, m munion {e |-> false})};

ValidMappings: set of seq1 of char -> set of map seq1 of char to bool
ValidMappings(s) ==
    { m | m in set PossibleMappings(s, {|->}) & true in set rng m };

For example:

> p ValidMappings({"a", "b"})
= {
{"a" |-> false, "b" |-> true},
{"a" |-> true, "b" |-> false},
{"a" |-> true, "b" |-> true}
}
Executed in 0.027 secs.