Type-checking for required variables

[pefribeiro]

While investigating how variables should be resolved via required interfaces, I have seen that it is possible to require variables of the wrong type. Unless I am wrong, I think that variable references are resolved based on name, and the type checker does not check that they indeed are of the correct type.

For example:

type sim

interface IVars {
    var rate : nat
}

interface RVars {
    var rate : sim
}

robotic platform RP {
    provides RVars
}

module Mod {
    rref rp=RP
    cref c1=C1
    ...
}

controller C1 {
    requires RVars
    sref stm1=STM1
    ...
}

stm STM1 {
    requires IVars
    ...
}

There are no errors reported, as indeed the variable rate is required by STM1, C1 and provided by RP. However, note that RVars is declaring a variable of name rate, but type sim, whereas IVars declares a variable of the same name but nat.

I'm not sure if this needs to be resolved, but it would be useful to fully understand what is the notion of equality when comparing variables and their references. If it indeed should just based on names, then the type checker should ensure that at least they are of the correct type.

[pefribeiro]

There is another related issue, which is regarding the uniqueness of variable names in a context, such as controller.

Currently, it is possible to modify the above example to define the following .rct:

...
controller C1 {
    requires RVars
    sref stm1=STM1
    var rate : int
    ...
}

So we have in the context of C1 two variables of name rate, one required via RVars and another defined in the controller C1. Again they are of different type, but I suppose they do have a unique name following the qualified name provider? Ie. C1::rate vs RVars::rate.

It could be argued that at this point it is the users' fault, and the implementation just resolves the reference rate in the state machine STM1 to one of them. So, the user could in theory specialise the use of rate in STM1 as follows:

stm STM1 {
    requires IVars
    transition T0 { from I to F action C1::rate = 1 }
    ...
}

But specifying C1::rate here breaks the modular paradigm, because now we have a state machine referring to the name of a controller. I think we agree that this is bad practice. If this is not allowed, then I doubt there is a good reason to allow the ambiguity in C1? If we follow the well-formedness condition C5 in the manual, then it isn't clear if this scenario should be allowed.

I looked into the implementation of checkUniqueness and see that the qualified name provider is involved. I think this warrants some discussion of how to proceed.