We discussed as part of #319 (closed) how it can be useful to have named invariants. This allows them to be referred to, for instance to 'select' invariants. It would also allow for traceability to requirement documents.
We could just allow an optional <identifier>: prefix for invariants in the textual syntax, and add a String-typed name field to the Invariant class.
Obviously, as for any language change/extension, we would need to carefully consider all implications.
Designs
Child items
...
Linked items
0
Link issues together to show that they're related or that one is blocking others.
Learn more.
I actually implemented this locally sometime ago to try how it would look. I think it is a very nice extension. You can use it for requirement traceability (at RWS all requirements have a code/name).
We could also show in the simulation state output whether an invariant evaluates to true or false.
You can use it for requirement traceability (at RWS all requirements have a code/name).
That is common at various companies, I think.
We could also show in the simulation state output whether an invariant evaluates to true or false.
For state invariants that would likely not be very useful, as you can only be in states where they hold. For state/event exclusion invariants, that could be possible.
I assumed that we want invariant names to be unique.
If the goal is to individually identify them, then that would indeed be a requirement. While we probably can't refer to them from the model itself for now, I would put them in the scope with all other names, and ensure they don't clash with that. Who knows whether we'll want to refer to them within the CIF specification at some point as well.
I propose to change InvariantDecls as follows.
I like that e.g. requirement <something>: ;` reads really nicely.
I'd probably align the similar tokens vertically for improved readability.
That would still allow to have things like: [...]
I see several options here:
Disallow this, as you propose. Would be the most restrictive form.
Allow this, and give them all the same name. Would not allow unique identification, so doesn't satisfy our requirements.
Allow this, and give them unique names. For your example, it could for instance be SYS-005-1, SYS-005-2, SYS-005-3. This would be a bit more magic for users. It would be less direct, and you'd probably have to read the documentation to understand what is happening here.
It makes sense to start with the most restrictive form. Then we can always relax it later and go one of the other forms, or a form we've yet to invent. But once you allow a more relaxed variant, there will be people making models that have that, and changing/restricting it later would be backward incompatible. That is something one ideally prevents.
What also needs to be thought about is the impact on the rest of the language. Will it be a scope? Where else do names play a role and how to incorporate named invariants there? Etc. It is probably not too complex though.
It makes sense to start with the most restrictive form.
I'm doing this right now.
Will it be a scope
I think it makes sense to handle them as declarations?
Where else do names play a role and how to incorporate named invariants there
So I got the type checker to check whether the names are unique and don't overlap with other declarations or child scopes. The only question I have right now is how to handle named invariants in locations (for checking unique names and for generating absolute names). Locations are not scopes (I think?), so in what scope will the named invariants be? Will they be in the automaton scope, or should I handle locations as a scope? The first option is probably the easiest, but the second might make more sense. I'm not sure.
I think it makes sense to handle them as declarations?
Seems logical indeed.
Locations are not scopes (I think?)
Probably not indeed, as you could previously not declare anything with a name in locations.
Will they be in the automaton scope, or should I handle locations as a scope? The first option is probably the easiest, but the second might make more sense. I'm not sure.
The same question can be asked about invariants with the same name in different automata etc. Do we want the names to be globally unique? Or locally unique? I can image that a single requirement could be implemented using multiple invariants, so one could argue it is not a problem if they overlap. On the other hand, that doesn't allow them to be uniquely identified, which was also a goal. So maybe they should then be named REQ1-1 and REQ1-2 or so, for a REQ1 implemented through multiple invariants. In different scopes, their absolute names then need to be unique to allow uniquely identifying them.
For invariants in locations, it depends on whether we want invariants with the same name in different locations, or not. By the argument that you can also put an extra number after them, maybe they can just share the automaton scope? However, if we foresee that they would then always be postfixed with the name of the location, then maybe a location scope would be more logical?
Also, what if you have two invariants named 'X' in different locations of the same automaton, and you for instance linearize it? What would happen then? I suppose they will be postfixed with the location name or so? And if they overlap with other names in the automaton they will get a unique name somehow?
I can image that a single requirement could be implemented using multiple invariants, so one could argue it is not a problem if they overlap.
The same could be said for requirement automaton, yet we require unique names for them. I think we should require unique local names and (as a result) unique global absolute names. As you said, users can simply name them REQ1-1 and REQ1-2
By the argument that you can also put an extra number after them, maybe they can just share the automaton scope? However, if we foresee that they would then always be postfixed with the name of the location, then maybe a location scope would be more logical?
Exactly what I was thinking. I'll see whether it is difficult to check location scopes.
Also, what if you have two invariants named 'X' in different locations of the same automaton, and you for instance linearize it? What would happen then? I suppose they will be postfixed with the location name or so?
I think prefixed similar how we now have group_group_group_automaton_name, you'll get group_group_group_automaton_location_name, or so. Might have to check what happens for locations without names.
And if they overlap with other names in the automaton they will get a unique name somehow?
Yeah, we do similar things already for other named objects when linearized names clash.