Support for KISS format

[santolucito]

Are there any plans to add back support for KISS output? This was a breaking change for me and I am hoping to not have to rewrite my code. Or do you know of any tools that would convert HOAF to KISS?

Thanks for making such an awesome tool!

[meyerphi]

There are no plans to add back KISS support. The main reasons for switching from KISS to HOA were:

• Full support for the possible successor and output non-determinism possible in controllers in Strix.
• Better tool support e.g. by Owl and Spot to verify and further manipulate controllers.
• Using the same format as ltlsynt to compare controllers and make switching between tools easy.

Still, I am not against adding back support for KISS as an additional output format, but I don't plan to do so myself. If that is restricted to fully determinized controllers (as with the current --determinize flag), it should not be too hard to do. So if want to initiate a pull request, I would be happy to review it and integrate it into Strix.

[santolucito]

Thanks for the response, this makes lots of sense. Actually, after looking into HOA more, it is so much nicer than KISS that I realized I am probably better off rewriting my side of things in the long run anyway.

[lazkany]

Just to let you know, many of my colleagues and myself are still using the old version of Strix because you guys stopped supporting kiss format. Some people are interested in compact representation of the controllers. HOA is too verbos if I only want to work on the generated controller which is a simple mealy machine.

Moreover, the old kiss format with binary labelling was very much readable. Now unfortunately with all this added information, the controller is not readable at all.

Readability is key for many of us. Assume that my atomic proportions are words, just imagine how ugly is the presentation.

[santolucito]

In case it is helpful to you @lazkany , I am now using https://github.com/reactive-systems/hanoi to get a useful representation out of HOA. I also only care about simple mealy machine representations as well. Here is a snippet where we parse HOA to get the states and atomic propositions - https://github.com/Barnard-PL-Labs/tsltools/blob/6107ae55ccb7f9293cd57977602b5d7b805f441a/src/lib/TSL/Writer/HOA/Codegen.hs#L80

Unfortunately, this code is pretty much useless unless you know Haskell (and even then, it still doesn't make much sense if I'm honest), but at least it works. Maybe it helps.