Alexandre Duret-Lutz ec51f976f8 gen: introduce a new automaton family

* spot/gen/automata.cc, spot/gen/automata.hh: Define AUT_L_NBA.
* bin/genaut.cc (--l-nba): New option.
* bin/man/genaut.x, doc/org/genaut.org, NEWS: Document it.
* tests/python/gen.py, tests/core/genaut.test: Test it.

2017-04-28 13:32:42 +02:00

1.7 KiB

Raw Blame History

`genaut`

This tool outputs ω-automata generated from scalable patterns.

These patterns are usually taken from the literature (see the genaut(1) man page for references).

      --ks-cobuchi=RANGE     A co-Büchi automaton with 2N+1 states for which
                             any equivalent deterministic co-Büchi automaton
                             has at least 2^N/(2N+1) states.
      --l-nba=RANGE          A Büchi automaton with 3N+1 states whose
                             complementary Streett automaton needs at least n!
                             states.

By default, the output format is HOA, but this can be controlled using the common output options for automata.

For instance:

genaut --ks-cobuchi=2 --dot

/alarsyo/spot/media/commit/e041db6101644e8092975cdadb964371946f6826/doc/org/kscobuchi2.png

The patterns can be specified using a range of the form N (a single value), N..M (all values between N and M included), or ..M (all values between 1 and M included).

genaut --ks-cobuchi=..5 --stats='%F=%L has %s states'

1.7 KiB Raw Blame History

genaut

1.7 KiB

Raw Blame History

`genaut`