Giter Site home page Giter Site logo

Support for KISS format about strix HOT 4 OPEN

santolucito avatar santolucito commented on June 16, 2024
Support for KISS format

from strix.

Comments (4)

meyerphi avatar meyerphi commented on June 16, 2024

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.

from strix.

santolucito avatar santolucito commented on June 16, 2024

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.

from strix.

lazkany avatar lazkany commented on June 16, 2024

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.

from strix.

santolucito avatar santolucito commented on June 16, 2024

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.

from strix.

Related Issues (4)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.