Properties should not be part of an automata network
This is a rather philosophical issue, and it is a humble test baloon. On a meta-level, I am posting it to find out how people react to it and whether we care about these kinds of questions at all:
Today I noticed again that in order to construct an automata network, you have to give properties, i.e. the AutomataNetwork class forces you to pass it a set of properties when an automata network is to be created. This in itself is IMHO already bad design because in the mental concept of a network of automata, properties are just absent: It is perfectly natural to think of an automata network without ever bothering about the concept of property at all.
However, I also have two more technical arguments to support my point:
- If you construct an automata network, but don't know the properties to check yet, you will later have to create a copy of the network with those properties as an argument to the constructor. I find this counter-intuitive and - at least in theory - wasteful. I would rather expect the model checker to take two completely separate arguments, i.e. the automata network and then a set of properties that are defined over the set of variables one finds in that network.
- The fact that the type
Property
occurs in the definition of the typeAutomataNetwork
creates a tight coupling between those types. I think that in general one rather strives towards loose coupling because reducing dependencies among different parts of the code makes it easier to maintain and easier to reuse for a new purpose (which people like Michaela, Gregory, or myself are doing as their primary task).
I can imagine that despite the above counter-arguments, this design might have been chosen because it allows an easier interface to the model checker (which thus has to take only one single argument, and not several), but because of those counter-arguments, I would like to overhaul it.
In case the feedback for this suggestion of mine is positive, I intend to do two things:
- Find out whether resolving this issue is indeed worth the gain and then have Sanny resolve it.
- Keep an eye open for and collect more issues of this kind. I have a feeling that they occur in a number of places, but so far I never took care to remember them. However I just realized that often when Gregory or Michaela ask me for help and also when I myself am struggling, problems are at least partly connected to tight coupling (may it be actual or perceived). I therefor consider tight coupling a technical debt that you're sometimes willing to make, but that we're paying quite some interest on. So let's pay back some of it.