[4diac-dev] Detecting self-cycles in ECC

[Sándor Bácsi <bacsi.sandor93@xxxxxxxxx>]

Hi,

As a first step, I started to implement OCL constraints to detect inconsistencies in ECC. Such an inconsistency can be, for example, if we create self-cycles in the ECC. A self-cycle exists when there is a transition from an EC state back to itself. If there is no event associated with such a transition, it can happen that the executor may enter an infinite loop. Therefore, I think we should warn users about self-cycles gated by "1" or "[None]". I created an OCL invariant which can detect self-cycles, which are gated by "1" or "[None]".

Gated by "[None]":

   Gated by "1":

Since I am a newbie to ECC, I would like to ask your opinion on this constraint. What do you think is this the right direction for detecting self-cycles? What previous experiences do you have with self-cycles in ECC? 

Cheers,
Sándor