1. 17 Sep, 2021 3 commits
    • Florian Renkin's avatar
      synthesis: aps_of uses a local cache · 82960792
      Florian Renkin authored
      * spot/twaalgos/synthesis.cc: here.
      82960792
    • Alexandre Duret-Lutz's avatar
      ltlsynt: fix syntax error handling · cb3a833a
      Alexandre Duret-Lutz authored
      Fixes #477.
      
      * bin/common_finput.cc (job_processor::process_string): Fix return
      value.
      * bin/ltlsynt.cc: Fix handling of syntax errors.  While we are here,
      make sure game_info is destroyed before Spot's globals.
      * tests/core/ltlsynt.test: Add a test case.
      cb3a833a
    • Alexandre Duret-Lutz's avatar
      build: fix multiple GCC warnings · 4710577d
      Alexandre Duret-Lutz authored
      These occur when Spot is compiled with --enable-optimizations and
      --disable-assert.
      
      * spot/mc/unionfind.cc, spot/twaalgos/mealy_machine.cc,
      spot/twaalgos/aiger.cc: Work around warnings about variables that are
      only used in assert.
      * spot/misc/common.hh [NDEBUG] (SPOT_ASSUME): Do not define
      as assert() when it is disabled.
      * spot/twaalgos/alternation.cc: Use insert instead of emplace
      to work around a spurious possible nullptr dereference.
      * spot/twaalgos/ltl2taa.cc, spot/twaalgos/ndfs_result.hxx,
      spot/twaalgos/tau03.cc, spot/twaalgos/tau03opt.cc:
      Work around spurious possible nullptr dereference.
      * spot/twaalgos/sbacc.cc: Work around spurious "maybe uninitialized"
      warning.
      4710577d
  2. 16 Sep, 2021 16 commits
    • Philipp Schlehuber's avatar
      Improving handling of unused proposition for aig · c973fcdf
      Philipp Schlehuber authored
      By default only propositions appearing in the strategy are
      treated. By handing over propositions explicitly one
      can force their appearance in the aig circuit.
      
      * spot/twaalgos/aiger.cc: Here
      * spot/twaalgos/aiger.hh: New doc
      * tests/python/games.ipynb: New test
      c973fcdf
    • Florian Renkin's avatar
      synthesis: fix decomposition · 7c1230b4
      Florian Renkin authored
      It is wrong to decompose an implication that is not at the top of
      the formula.
      
      * spot/twaalgos/synthesis.cc: don't always split implication
      7c1230b4
    • Florian Renkin's avatar
      synthesis: Fix segfault when there is no output · ad5203e7
      Florian Renkin authored
      * spot/twaalgos/synthesis.cc: here
      * tests/python/synthesis.py: create a test
      * tests/Makefile.am: add synthesis.py to the tests
      ad5203e7
    • Florian Renkin's avatar
      Aiger: Add a way to evaluate an input sequence (Python) · 306a45f2
      Florian Renkin authored
      Add a method to the class aig (Python) that produces a sequence of
      outputs for a given sequence of inputs.
      
      * python/spot/__init__.py: here
      306a45f2
    • Florian Renkin's avatar
      Typos · b9ec16f9
      Florian Renkin authored
      * bin/ltlsynt.cc, spot/twaalgos/game.hh,
      spot/twaalgos/synthesis.cc: here
      b9ec16f9
    • Philipp Schlehuber's avatar
      ltlsynt rewrite · 7d908b93
      Philipp Schlehuber authored
      Introducing the new game interface
      to ltlsynt.
      ltlsynt now also uses direct strategy deduction
      and formula decomposition.
      
      * bin/ltlsynt.cc: Here
      * spot/twaalgos/aiger.cc
      , spot/twaalgos/aiger.hh: Use strategy_like
      * spot/twaalgos/game.hh: Minor adaption
      * spot/twaalgos/mealy_machine.cc: Use new interface
      * spot/twaalgos/synthesis.cc
      , spot/twaalgos/synthesis.hh: Spezialised split
      * tests/core/ltlsynt.test
      , tests/python/games.ipynb: Adapting
      7d908b93
    • Philipp Schlehuber's avatar
      Use new minterm enumeration in split_2step · a5185c21
      Philipp Schlehuber authored
      Also remove self-loop for sink and make it work for any
      acceptance condition.
      
      * spot/twaalgos/synthesis.cc: Here
      * tests/core/ltlsynt.test: Adjust tests
      * tests/python/split.py: Adjust tests
      a5185c21
    • Florian Renkin's avatar
      Introducing formula split · 98ab8262
      Florian Renkin authored
      Split a LTL formula to a set of formula that don't share
      output proposition. It allows to create multiple
      strategies in ltlsynt.
      
      * spot/twaalgos/synthesis.cc,
        spot/twaalgos/synthesis.hh: here
      * doc/spot.bib: Add reference
      98ab8262
    • Philipp Schlehuber's avatar
      New game api · 4260b17f
      Philipp Schlehuber authored
      Introduce a new, uniform way to create and solve
      games.
      Games can now be created directly from specification
      using creat_game, uniformly solved using
      solve_game and transformed into a strategy
      using create_strategy.
      Strategy are mealy machines, which can be minimized.
      
      * bin/ltlsynt.cc: Minor adaption
      * spot/twaalgos/game.cc: solve_game, setters and getters
      for named properties
      * spot/twaalgos/game.hh: Here too
      * spot/twaalgos/mealy_machine.cc: Minor adaption
      * spot/twaalgos/synthesis.cc: create_game, create_strategy and
      minimize_strategy
      * spot/twaalgos/synthesis.hh: Here too
      * tests/core/ltlsynt.test: Adapting
      * tests/python/aiger.py
      , tests/python/games.ipynb
      , tests/python/mealy.py
      , tests/python/parity.py
      , tests/python/split.py: Adapting
      4260b17f
    • Philipp Schlehuber's avatar
      Adding selective edge sorting and state merging · 786599ed
      Philipp Schlehuber authored
      The merging is (possibly) more expensive but also
      merges more states when applied to all states.
      
      * spot/graph/graph.hh: edge sorting
      * spot/twa/twagraph.cc,
      spot/twa/twagraph.hh: selective state merging
      * tests/core/twagraph.cc: Adjusting tests
      786599ed
    • Philipp Schlehuber's avatar
      Adding dot suppport for aiger class · 2c267dd8
      Philipp Schlehuber authored
      * spot/twaalgos/aiger.cc: Useless assert
      * spot/twaalgos/dot.hh,
      spot/twaalgos/dot.cc: aig to dot
      * python/spot/__init__.py: Adapting
      * tests/python/games.ipynb: Additional tests
      2c267dd8
    • Philipp Schlehuber's avatar
      Making aiger a class · 17db5823
      Philipp Schlehuber authored
      Aiger circuits noew have their own class.
      Monitors can be translated to and obtained
      from aiger circuits.
      Moreover a step by step evaluation method
      is provided.
      
      * spot/twaalgos/aiger.hh,
      spot/twaalgos/aiger.cc: Here
      * bin/ltlsynt.cc: Adopt new modes
      * tests/core/ltlsynt.test: Adapt tests
      * python/spot/impl.i: Add python support
      * tests/Makefile.am,
      tests/python/aiger.py: New test cases
      17db5823
    • Philipp Schlehuber's avatar
      Adding bdd_is_cube for python · 18948a96
      Philipp Schlehuber authored
      * python/buddy.i: Here
      18948a96
    • Philipp Schlehuber's avatar
      [buddy] Adding bdd_is_cube · 3aef5f31
      Philipp Schlehuber authored
      bdd_is_cube determines whether or not a given bdd
      represents a cube.
      
      * src/bddop.c: Here
      * src/bddx.h: And here
      3aef5f31
    • Alexandre Duret-Lutz's avatar
      [buddy] introduce a bdd_satoneshortest() function · 5a0fbf6c
      Alexandre Duret-Lutz authored
      * src/bddop.c, src/bddx.h: Introduce this function.
      * src/bddtest.cxx: Add some short tests.
      5a0fbf6c
    • Alexandre Duret-Lutz's avatar
      robin_hood: Update to version 3.11.3 · 830f68b3
      Alexandre Duret-Lutz authored
      The only difference with upstream is that we keep std::malloc() as
      malloc() to avoid issues with gnulib that sometimes redefine malloc to
      rpl_malloc with a macro without defining std::rpl_malloc.
      
      * spot/priv/robin_hood.hh, debian/copyright: Update.
      * spot/priv/Makefile.am (update): Rename std::malloc to malloc.
      830f68b3
  3. 15 Sep, 2021 2 commits
  4. 13 Sep, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      parseaut: improve parsing of HOA labels · ce1cf550
      Alexandre Duret-Lutz authored
      On a debug build with the automaton from #476, the gain seems to be
      about 33% of the parsing time.
      
      * spot/parseaut/parseaut.yy, spot/parseaut/parsedecl.hh,
      spot/parseaut/scanaut.ll: Share a hash map of string->BDD
      between the scanner and parser so that [labels] can be looked
      up by the scanner if they have already been parsed once.
      * NEWS: Mention it.
      ce1cf550
  5. 11 Sep, 2021 5 commits
    • Alexandre Duret-Lutz's avatar
      genem: implement the logic from the future journal version of ATVA19 · 9539fbcf
      Alexandre Duret-Lutz authored
      This version of the generic emptiness-check, using smart selection and
      extraction of the Fin (implemented here via fin_one_extract), was
      suggested by Jan Strejček on 2020-06-26.
      
      * spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Add the spot210
      variant.  Also use it for the ACD use-case.
      * spot/twaalgos/zlktree.cc (zielonka_tree): Also use the same logic
      here.
      * tests/python/genem.py: Test the new version as well.
      9539fbcf
    • Alexandre Duret-Lutz's avatar
      acc: introduce fin_one_extract() · 7fedb3dc
      Alexandre Duret-Lutz authored
      * spot/twa/acc.cc, spot/twa/acc.hh (acc_cond::fin_one_extract,
      acc_code::acc_cond::fin_one_extract): New methods.
      * python/spot/impl.i: Add support for the return type.
      * tests/python/acc_cond.ipynb: Test them.
      7fedb3dc
    • Alexandre Duret-Lutz's avatar
      zlktree: replace std::vector<bool> by bitvect in ACD · 2d1cb0dd
      Alexandre Duret-Lutz authored
      On the example from previous patch, the number of instruction fetches
      goes from 18490399159 down to 18248898077.
      
      * spot/twaalgos/zlktree.cc, spot/twaalgos/zlktree.hh (acd): Use
      bitvect instead of std::vector<bool> in nodes.  This make is easier to
      update an edge of a bitvector shared by multiple nodes set after
      pruning non-maximal sets from an SCC.  Also compute the set of states
      hit by the edges at the very end, once all nodes are known.
      * spot/twaalgos/sccinfo.cc, spot/twaalgos/sccinfo.hh,
      spot/twaalgos/genem.cc, spot/twaalgos/genem.hh: Adjust to work with
      bitvect as filter.
      2d1cb0dd
    • Alexandre Duret-Lutz's avatar
      zlktree: speedup the construction of ACD nodes · 6aa20790
      Alexandre Duret-Lutz authored
      This uses the foreach_set_index() method introduced in the previous
      patch to speed up the copy bitvectors in ACD nodes, as pointed in
      issue #476.
      
      Running
      PREFIXCMD='valgrind --tool=callgrind' ./run python3 -c \
      "import spot; spot.acd_transform(spot.automaton('syntcomp_91.hoa'))"
      went from 65139436227 instruction fetches down to 18490399159.
      
      * spot/twaalgos/zlktree.cc (acd::build_): Use foreach_set_index().
      6aa20790
    • Alexandre Duret-Lutz's avatar
      bitvect: add a foreach_set_index(callback) function · b6df1f8f
      Alexandre Duret-Lutz authored
      Related to #476, where that is needed.
      
      * spot/misc/bitvect.hh: Here.
      * tests/core/bitvect.cc, tests/core/bitvect.test: Add some tests.
      b6df1f8f
  6. 08 Sep, 2021 3 commits
  7. 07 Sep, 2021 1 commit
  8. 05 Sep, 2021 1 commit
    • Alexandre Duret-Lutz's avatar
      acd: remove redundant nodes · 170d839c
      Alexandre Duret-Lutz authored
      Reported by Florian Renkin.
      
      * spot/twaalgos/zlktree.cc (acd::_build): Use a sorted list to remove
      redundant children, has done in zielonka_tree.
      * tests/python/zlktree.ipynb: Add Florian's test case.
      * tests/python/toparity.py: Adjust, and revert some tests
      uncommented by mistake in a previous patch.
      170d839c
  9. 04 Sep, 2021 3 commits
  10. 03 Sep, 2021 2 commits
  11. 01 Sep, 2021 3 commits