Hello, At the moment, the executable merely complements a hardcoded automaton and writes it to a file for testing and benchmarking purposes. It will not stay like this. Once a parser for the Hanoi Omega Automata format has been written, this will become a generic command-line complementation tool. I am not sure what sort of test should be run on such a tool as part of the regular AFP build.
Julian On Sat, Mar 30, 2019 at 7:49 PM Mathias Fleury <[email protected]> wrote: > > Hi all, > > > I had a look at that: > > > > Current examples are in AFP/09ea4594dc4e: > > > > * Diophantine_Eqns_Lin_Hom for Haskell (with GHC) > > * Buchi_Complementation for SML (with MLton) > > > > The latter was actually untested before, and is presently broken: > > "unhandled exception: Empty". Either this is natural bit-rot, or I've > > got something wrong with the setup in > > AFP/thys/Buchi_Complementation/Complementation_Build.thy > > > The programs expects as first argument a path where the complemented > automaton can be written (i.e., ./Completion /tmp/automaton). The path is > extracted with hd and if you don't pass an argument, then an error is raised > because the list of arguments is empty. > > Now I am not certain if the correct fix is to: > - add an argument in the Isabelle theory > - remove the part writing the file in Completion.sml, > - change Completion.sml to either print the automaton to stdout if there is > no argument, or to print it to a file if there is an argument > > > Best, > Mathias > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
