Implement choicepoint restrictions / "configurators" into the language

[sprocter]

Creating part of the large, synthetic model I'd like to use for an experiment requires changing multiple choicepoints to the same value. This is supported in ATSV using configurators, but it's not currently specifiable in the language.

Here's a MWE model:

package configurator_mwe
public

    bus sandboxbus
    end sandboxbus;

    bus implementation sandboxbus.i
    end sandboxbus.i;

    bus implementation sandboxbus.ext1 extends sandboxbus.i
    end sandboxbus.ext1;

    bus implementation sandboxbus.ext2 extends sandboxbus.i
    end sandboxbus.ext2;

    device prov_dev
        features
            feat : provides bus access sandboxbus.i;
    end prov_dev;

    device req_dev
        features
            feat : requires bus access sandboxbus.i;
    end req_dev;

    system sys
    end sys;

    system implementation sys.i
        subcomponents
            a : device prov_dev;
            b : device req_dev;
        connections
            c : bus access  a.feat <-> b.feat;
    end sys.i;

end configurator_mwe;

What I'd like to be able to do is somehow specify that whatever extension of sanboxbus.i (ie, either sandboxbus.ext1 or sandboxbus.ext2) gets picked for one device must be selected for the other.

Potentially useful, and also immediately encodable in ATSV's configurators, would be inequality (aka uniqueness).

[sprocter]

FYI: There's now proposed syntax for the configurator specification in the .properties file in #11

[sprocter]

• Configurator syntax:
  • Current specification:

    ## Configurator specification
    ## Choicepoints can be uniquely identified by their type and instance-model path, so that's what we 
    # 1. Type of Configurator (Currently supported: EqConfigurator, NeqConfigurator)
    # 2. Name of the choicepoint (SubcompChoice: Just the instance path. PropertyValues: Path-Qualified Property Name)
    # = 
    # 3. Name of the choicepoint (SubcompChoice: Just the instance path. PropertyValues: Path-Qualified Property Name)
    EqConfigurator-scs.dev1=scs.dev2

[sprocter]

All the restrictions I can come up with are basically tests of set membership -- ie, if choicepoint X has value a, then choicepoint Y should or should not have value b.

By building varying levels of syntactic sugar on top of this, there are six kinds of restrictions I think we should support. All examples assume two choicepoints, X and Y, each with a type of ℕ:

1. Equality -- Choosing one value means another choicepoint has to have the same value
   • X = 7 → Y = 7
   • X = 3 → Y = 3.
2. Inequality -- Choosing one value means another choicepoint can't take that same value
   • X = 7 → Y ≠ 7
   • X = 3 → Y ≠ 3
3. Requires -- Choosing one value means another choicepoint has to have a specific value that is not equal to the first value
   • X = 7 → Y = 9
   • X = 2 → Y = 4
4. Forbids -- Choosing one value means another choicepoint can't take a specific value that is not equal to the first value
   • X = 7 → Y ≠ 9
   • X = 2 → Y ≠ 4
5. Set Membership -- Choosing one value means another choicepoint's choices are restricted to the specified set.
   • X = 7 → Y ∈ {1,3,9}
   • X = 5 → Y ∈ {2,4,7}
6. Set Exclusion -- Choosing one value means another choicepoint's choices cannot be any of the specified set.
   • X = 7 → Y ∉ {1,3,9}
   • X = 5 → Y ∉ {2,4,7}

One thing to think about is sets on the left hand side -- it's possible that users would want this functionality. We'll probably want to "flatten" it to only allow single elements on the LHS (so enforcement can be done using a map) but we can still expose the sugared syntax to the user.