No location pointers for automata with single location.
Original issue text:
Currently, when introducing location pointers, we don't have a special case for automata with a single location. For such automata however, the introduced location pointer variable can only ever have one value, and is thus superfluous.
We should not introduce a location pointer for such automata, during linearization, and for the CIF to CIF transformation to eliminate location references. Both share the same code.
Obviously, if the location pointer is not introduced, we can't create 'lp = loc' kind of predicates, and we have to ensure we don't create them. In such cases, 'true' could be a substitute. If we combine this with other predicates, we get non-optimal predicates, but for the current uses, this is already the case.
Notice that we have special case dummy updates that use location pointers.
Related to this, are dummy updates, which are added to ensure that the correct updates are taken. For instance, the following specification:
automaton p: event e; disc int x = 0; location: edge e when x >= 3; edge e when x < 3 do x := x + 1; end
is transformed to the following specification:
enum E = X; automaton M: alphabet p_e; event p_e; disc int p_x = 0; disc E p in any; initial p = X and false; marked p = X and false; location L: initial; marked; edge p_e when p = X and (p_x >= 3 or p_x < 3) do if p = X and p_x >= 3: p := X elif p = X and p_x < 3: p_x := p_x + 1 end; end
In the case there is no location pointer, the dummy update should be p_x := p_x
, instead of p := X