Edit of traces in hyper-LTL query dialog

[Jiri Srba]

Open the attached net and open the query dialog. Then click on

T2.comp1.haveA <= 1

and the dropdown boxes will automatically find comp1 and haveA, however, they will not
update the trace to T2 and instead show T1.

The correct behaviour is that the dropdown menu for a trace should be setup to T2 as it
is in the proposition.

[Jiri Srba (srba)]

Also, it is possible to remove a trace that is used in the query (hyper-LTL). This should not be possible.

[Jiri Srba (srba)]

Finally, in a manual edit, I can add a new trace name to the query, the query will be parsed correctly but the new name does not appear in the list of traces and will not be possible to select it in the dropdown menu.

[Jiri Srba (srba)]

In the predefined trace names, maybe add both T1 and T2 as the two default names, so that one does not have to add T2 manually every time - the logic with just one trace name does not make any sense anyway.

[Jiri Srba (srba)]

Also, the simulator show traces (after query verification) which do not appear in the formula. Maybe this is a smaller problem, but if possible, these traces do not have to be shown at all.

[Jiri Srba (srba)]

Also, the query results for hyper-LTL should allow to display the raw output.

[Jiri Srba (srba)]

E T1 (E T1 ( ...)) should not be allowed (every trace can be quantified only once)

E T1 ( T2.a=3) should not be allowed (the atomic proposition a refers to trace T2 that is not decleared.