On 30/03/2019 20:00, Julian Brunner wrote: > > 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.
For now it is sufficient to have some sanity check of the existing material. I will put it into better shape following the hints below ... > On Sat, Mar 30, 2019 at 7:49 PM Mathias Fleury > <[email protected]> wrote: >> >> 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. Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
