Use the lts library for counter-examples in ltscompare

[matifch]

A trc file generated by ltscompare cannot be opened in lpsxsim.

[tneele]

The traces generated by ltscompare are lacking state information. Therefore, it's currently not possible to load these traces in lpsxsim. The best alternative for now it to use the tool tracepp.

[tneele]

After some discussion in the most recent meeting, we agreed that this issue should be addressed with a more general solution. In short: the toolset currently contains various algorithms that construct some kind of evidence (counter-example or witness). This evidence can have different shapes, not just traces. The best solution is therefore to retire the trace library and rely solely on the lts library for evidence.

This may require developing a philosophy on what evidence may look like in its most general form.

[mlaveaux]

We have made various changes to the generation of counter examples as modal formulas in the equivalences, and the trace library has been retired. Therefore, this issue can be closed.