Commit graph

6 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
bfe0ada634 deprecate spot::acc_cond::format()
* NEWS: Mention it.
* spot/twa/acc.hh (spot::acc_cond::format): Deprecate.
(spot::acc_cond::mark_t::as_string): New function.
* spot/taalgos/dot.cc: Use mark_t::as_string().
* spot/priv/satcommon.cc, spot/priv/satcommon.hh,
spot/twaalgos/dtwasat.cc, spot/twaalgos/emptiness.cc,
tests/core/acc.cc, tests/core/acc.test: Adjust to use << directly.
2019-07-05 22:43:36 +02:00
Alexandre Duret-Lutz
c766f58d5d sat_minimize: improve logs and document Python bindings
* spot/priv/satcommon.cc, spot/priv/satcommon.hh: Make it possible to
set the log file without setting the environment variable.  Adjust
print_log to take the input state and print it as a new column.
* spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc: Adjust all
calls to print_log.  Fix log output for incremental approaches.
Prefer purge_unreachable_states() over stats_reachable().  Do
not call scc_filter() on colored automata.
* spot/twaalgos/dtwasat.hh: Document the new "log" option.
* NEWS: Mention the changes.
* tests/python/satmin.ipynb: New file.
* tests/Makefile.am: Add it.
* doc/org/satmin.org, doc/org/tut.org: Link to it.
* doc/org/satmin.org, bin/man/spot-x.x: Adjust description
of CSV files.
* bench/dtgbasat/gen.py, bench/dtgbasat/tabl.pl,
bench/dtgbasat/tabl1.pl, bench/dtgbasat/tabl2.pl,
bench/dtgbasat/tabl3.pl, bench/dtgbasat/tabl4.pl: Adjust for
the new column.
* spot/misc/satsolver.cc, spot/misc/satsolver.hh (stats): Make it
const.
* python/spot/__init__.py (sat_minimize): Add display_log and
return_log options.
* tests/python/ipnbdoctest.py: Adjust to not compare SAT-minimization
logs as they contain timings.
2018-03-30 18:01:59 +02:00
Alexandre Duret-Lutz
ac6b0c9432 include config.h in all *.cc files
This helps working around missing C functions like strcasecmp that do
not exist everywhere (e.g. on Cygwin), and for which lib/ supplies a
replacement.  Unfortunately we do not have such build in our current
continuous integration suite, so we cannot easily detect files where
such config.h inclusion would be useful.  Therefore this patch simply
makes it mandatory to include config.h in *.cc files.  Including this
in public *.hh file is currently forbidden.

* spot/gen/automata.cc, spot/gen/formulas.cc,
spot/kripke/fairkripke.cc, spot/kripke/kripke.cc,
spot/ltsmin/ltsmin.cc, spot/misc/game.cc, spot/parseaut/fmterror.cc,
spot/parsetl/fmterror.cc, spot/parsetl/parsetl.yy,
spot/priv/bddalloc.cc, spot/priv/freelist.cc, spot/priv/satcommon.cc,
spot/priv/trim.cc, spot/priv/weight.cc, spot/ta/ta.cc,
spot/ta/taexplicit.cc, spot/ta/taproduct.cc, spot/ta/tgtaexplicit.cc,
spot/ta/tgtaproduct.cc, spot/taalgos/dot.cc,
spot/taalgos/emptinessta.cc, spot/taalgos/minimize.cc,
spot/taalgos/reachiter.cc, spot/taalgos/statessetbuilder.cc,
spot/taalgos/stats.cc, spot/taalgos/tgba2ta.cc, spot/tl/apcollect.cc,
spot/tl/contain.cc, spot/tl/declenv.cc, spot/tl/defaultenv.cc,
spot/tl/dot.cc, spot/tl/exclusive.cc, spot/tl/hierarchy.cc,
spot/tl/length.cc, spot/tl/ltlf.cc, spot/tl/mark.cc,
spot/tl/mutation.cc, spot/tl/nenoform.cc, spot/tl/print.cc,
spot/tl/randomltl.cc, spot/tl/relabel.cc, spot/tl/remove_x.cc,
spot/tl/simplify.cc, spot/tl/snf.cc, spot/tl/unabbrev.cc,
spot/twa/acc.cc, spot/twa/bdddict.cc, spot/twa/bddprint.cc,
spot/twa/formula2bdd.cc, spot/twa/taatgba.cc, spot/twa/twa.cc,
spot/twa/twagraph.cc, spot/twa/twaproduct.cc, spot/twaalgos/aiger.cc,
spot/twaalgos/alternation.cc, spot/twaalgos/are_isomorphic.cc,
spot/twaalgos/bfssteps.cc, spot/twaalgos/canonicalize.cc,
spot/twaalgos/cleanacc.cc, spot/twaalgos/cobuchi.cc,
spot/twaalgos/complement.cc, spot/twaalgos/complete.cc,
spot/twaalgos/compsusp.cc, spot/twaalgos/couvreurnew.cc,
spot/twaalgos/cycles.cc, spot/twaalgos/degen.cc,
spot/twaalgos/determinize.cc, spot/twaalgos/dot.cc,
spot/twaalgos/dtbasat.cc, spot/twaalgos/dtwasat.cc,
spot/twaalgos/dualize.cc, spot/twaalgos/emptiness.cc,
spot/twaalgos/gtec/ce.cc, spot/twaalgos/gtec/gtec.cc,
spot/twaalgos/gtec/sccstack.cc, spot/twaalgos/gtec/status.cc,
spot/twaalgos/gv04.cc, spot/twaalgos/hoa.cc,
spot/twaalgos/iscolored.cc, spot/twaalgos/isdet.cc,
spot/twaalgos/isunamb.cc, spot/twaalgos/isweakscc.cc,
spot/twaalgos/langmap.cc, spot/twaalgos/lbtt.cc,
spot/twaalgos/ltl2taa.cc, spot/twaalgos/ltl2tgba_fm.cc,
spot/twaalgos/magic.cc, spot/twaalgos/mask.cc,
spot/twaalgos/minimize.cc, spot/twaalgos/neverclaim.cc,
spot/twaalgos/parity.cc, spot/twaalgos/postproc.cc,
spot/twaalgos/powerset.cc, spot/twaalgos/product.cc,
spot/twaalgos/rabin2parity.cc, spot/twaalgos/randomgraph.cc,
spot/twaalgos/randomize.cc, spot/twaalgos/reachiter.cc,
spot/twaalgos/relabel.cc, spot/twaalgos/remfin.cc,
spot/twaalgos/remprop.cc, spot/twaalgos/sbacc.cc,
spot/twaalgos/sccfilter.cc, spot/twaalgos/sccinfo.cc,
spot/twaalgos/se05.cc, spot/twaalgos/sepsets.cc,
spot/twaalgos/simulation.cc, spot/twaalgos/split.cc,
spot/twaalgos/stats.cc, spot/twaalgos/strength.cc,
spot/twaalgos/stripacc.cc, spot/twaalgos/stutter.cc,
spot/twaalgos/sum.cc, spot/twaalgos/tau03.cc,
spot/twaalgos/tau03opt.cc, spot/twaalgos/totgba.cc,
spot/twaalgos/toweak.cc, spot/twaalgos/translate.cc,
spot/twaalgos/word.cc, tests/core/acc.cc, tests/core/bitvect.cc,
tests/core/checkpsl.cc, tests/core/checkta.cc, tests/core/consterm.cc,
tests/core/emptchk.cc, tests/core/equalsf.cc, tests/core/graph.cc,
tests/core/ikwiad.cc, tests/core/intvcmp2.cc, tests/core/intvcomp.cc,
tests/core/kind.cc, tests/core/kripkecat.cc, tests/core/length.cc,
tests/core/ltlrel.cc, tests/core/ngraph.cc, tests/core/parity.cc,
tests/core/randtgba.cc, tests/core/readltl.cc, tests/core/reduc.cc,
tests/core/safra.cc, tests/core/sccif.cc, tests/core/syntimpl.cc,
tests/core/taatgba.cc, tests/core/tostring.cc, tests/core/trival.cc,
tests/core/twagraph.cc, tests/ltsmin/modelcheck.cc,
spot/parseaut/scanaut.ll, spot/parsetl/scantl.ll: Include config.h.
* spot/gen/Makefile.am, spot/graph/Makefile.am,
spot/kripke/Makefile.am, spot/ltsmin/Makefile.am,
spot/parseaut/Makefile.am, spot/parsetl/Makefile.am,
spot/priv/Makefile.am, spot/ta/Makefile.am, spot/taalgos/Makefile.am,
spot/tl/Makefile.am, spot/twa/Makefile.am, spot/twaalgos/Makefile.am,
spot/twaalgos/gtec/Makefile.am, tests/Makefile.am: Add the -I lib/
flags.
* tests/sanity/includes.test: Catch missing config.h in *.cc, and
diagnose config.h in *.hh.
* tests/sanity/style.test: Better diagnostics.
2018-02-21 17:59:09 +01:00
Alexandre Duret-Lutz
dd5a820863 * spot/priv/satcommon.cc: Fix include. 2017-02-28 17:02:06 +01:00
Alexandre GBAGUIDI AISSE
67e3a4f28e spot: Add 'langmap' option with dichotomy (it helps to choose min val)
* python/spot/__init__.py: Handle 'dicho' option in 'sat_minimize'.
* spot/priv/satcommon.cc: Implement get_number_of_distinct_vals.
* spot/priv/satcommon.hh: Declare get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtbasat.hh: Change dichotomy function's prototype.
* spot/twaalgos/dtwasat.cc: Use get_number_of_distinct_vals.
* spot/twaalgos/dtwasat.hh: Change dichotomy function's prototype.
Handle options.
* spot/twaalgos/postproc.cc: Handle options.
* spot/twaalgos/postproc.hh: Add dicho_langmap_ var for options.
* tests/core/satmin2.test: Add tests for dichotomy.
* tests/core/satmin.test: Add tests for dichotomy.
* tests/python/satmin.py: Replace 'dichotomy' with 'dicho' option.
2017-01-06 19:53:21 +01:00
Alexandre GBAGUIDI AISSE
9acd7370b2 twaalgos: Improve data storage in SAT-minimization
* spot/misc/satsolver.hh: Make solver return vector<bool> instead of
vector<int>.
* spot/misc/satsolver.cc: Update code.
* spot/priv/Makefile.am: Add satcommon.*
* spot/priv/satcommon.hh: Declare helper class and factorize some
duplicate code of dt*asat.cc
* spot/priv/satcommon.cc: Implement helper class and factorize some
duplicate code of dt*asat.cc
* spot/twaalgos/dtbasat.cc: Declare helper, implement some functions
in dict struct and update code.
* spot/twaalgos/dtwasat.cc: Declare helper, implement some functions
in dict struct and update code.
* tests/core/readsat.cc: Update tests.
* tests/core/satmin.test: Typo.
* tests/core/satmin2.test: Update an expected result.
2017-01-06 19:53:21 +01:00