Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Support for KISS format #4

Open
santolucito opened this issue Jan 4, 2022 · 4 comments
Open

Support for KISS format #4

santolucito opened this issue Jan 4, 2022 · 4 comments
Labels
enhancement New feature or request

Comments

@santolucito
Copy link

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
Copy link
Owner

meyerphi commented Jan 5, 2022

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.

@meyerphi meyerphi added the enhancement New feature or request label Jan 5, 2022
@santolucito
Copy link
Author

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
Copy link

lazkany commented Oct 22, 2023

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
Copy link
Author

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

3 participants