Self-loop in TS

[RBinsonB]

Self-loop on TS nodes seems to be critical to trap detection (see issue here).

For now, those self-loop are defined at the TS config file level. Should they always be included in the TS build process? That would only make sense to leave them in the config files if there are specific configurations where we want to avoid it.

[PVarnai]

I think it should be part of the TS. A self-loop on the TS essentially says that it is possible to stay here from one time step to another. I.e., it's possible to generate a sequence of LTL propositions (r1 r1 r1 r1 r1 ...). If this is indeed physically possible in the scenario, then yeah the self-loop should imply that the system this type of behavior.

Whether a 'stay' action is something that we always expect to be possible is a different question. Perhaps a good choice is allow a config-option for automatically including a 'stay' action, which generates the required self-loops for the TS as well.

Imagine a hard task of never r2, and a TS where you can only go back and forth between r1 and r2. Without the possibility to stay at r1 (having a self-loop), r1 is a trap. This is either the case for the physical system, or not, and we should let the user config this as needed.

[RBinsonB]

I like the config-option idea. Maybe it should not be included in the code itself but in the script that will generate the TS config file.

[xiaotan-git]

I think having a self-loop in TS should be the default because for the uavs and ground vehicles in a 2-D scenario, they can stay. Just for a note here that for general dynamics, we don't have this self-loop in TS.

[RBinsonB]

The 2D scenario is what we use here but the code should be general enough to be adapted for other use, so I would not put it as a hard-coded default but part of the TS config file.