From 88a6bd82a34fc6a7c02609827f995b8b836d6b3e Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Thu, 24 May 2018 17:53:37 +0200 Subject: [PATCH] document --enable-max-accsets * README, doc/org/hoa.org: Here. --- README | 8 ++++++++ doc/org/hoa.org | 15 ++++++++------- 2 files changed, 16 insertions(+), 7 deletions(-) diff --git a/README b/README index 796e7b7ce..c130e2f98 100644 --- a/README +++ b/README @@ -115,6 +115,14 @@ flags specific to Spot: do not have a working Python 3.2+ installation or if you are attempting some cross-compilation. + --enable-max-accsets=N + Compile Spot so that it supports up to N acceptance sets. The + default is 32, so that the membership of each transition to + any of the 32 acceptance sets can be represented by an + "unsigned int" (interpreted as a bit-vector). Using a larger + N (it still has to be a multiple of 32) will consume more + unsigned ints per transitions, costing both time and space. + --enable-doxygen Generate the Doxygen documentation for the code as part of the build. This requires Doxygen to be installed. Even if diff --git a/doc/org/hoa.org b/doc/org/hoa.org index f3a8c1aea..12c28e489 100644 --- a/doc/org/hoa.org +++ b/doc/org/hoa.org @@ -58,14 +58,15 @@ the HOA format, the output may not be exactly the same as the input. - Automata using explicit alphabet (introduced in version 1.1 of the format via =Alphabet:=) are not supported. -- The maximum number of acceptance sets used is (currently) limited - to 32. +- The maximum number of acceptance sets used is limited to 32. - This limit is not very hard to increase in the source code, - however we want to keep it until it becomes an actual problem. So - please report to us if you suffer from it. In the past, this - limitation has forced us to improve some of our algorithms to be - less wasteful and not introduce useless acceptance sets. + In the past, this limitation has forced us to improve some of our + algorithms to be less wasteful and not introduce useless acceptance + sets. + + This hard-coded limit can be augmented at configure time + using option `--enable-max-accsets=N`, but doing so will consume + more memory and time. - Multiple (or missing) initial states are emulated.