1. 25 Jan, 2023 2 commits
  2. 24 Jan, 2023 1 commit
  3. 23 Jan, 2023 4 commits
  4. 10 Jan, 2023 1 commit
    • Alexandre Duret-Lutz's avatar
      more code smells · 09bbaa1e
      Alexandre Duret-Lutz authored
      * bin/common_file.cc, bin/common_file.hh, bin/common_finput.cc,
      bin/common_finput.hh, bin/common_output.cc, bin/common_setup.cc,
      bin/common_setup.hh, bin/common_trans.cc, bin/common_trans.hh,
      bin/dstar2tgba.cc, bin/genaut.cc, bin/genltl.cc, bin/ltl2tgba.cc,
      bin/ltl2tgta.cc, bin/ltlcross.cc, bin/ltldo.cc, bin/ltlfilt.cc,
      bin/ltlsynt.cc, bin/randltl.cc: Fix minor code issues reported by
      sonarcloud.
      09bbaa1e
  5. 09 Jan, 2023 1 commit
  6. 06 Jan, 2023 1 commit
  7. 05 Jan, 2023 4 commits
  8. 04 Jan, 2023 1 commit
  9. 10 Dec, 2022 3 commits
  10. 09 Dec, 2022 9 commits
    • Philipp Schlehuber's avatar
      lazy eval for sat mealy minimization · 427f667f
      Philipp Schlehuber authored
      Evaluate incomp of player conditions only if necessary
      
      * spot/twaalgos/mealy_machine.cc: Here
      427f667f
    • Philipp Schlehuber's avatar
      Using partitioned_relabel_here · 6e2e7c94
      Philipp Schlehuber authored
      Put the new function to use in order to speed up
      mealy machine minimization
      
      * spot/twaalgos/mealy_machine.cc: Here
      * spot/twaalgos/synthesis.cc
      , spot/twaalgos/synthesis.hh: Helper function to relabel games
      * tests/python/_mealy.ipynb
      , tests/python/except.py
      , tests/python/_partitioned_relabel.ipynb: Adapt/expand tests
      6e2e7c94
    • Philipp Schlehuber's avatar
      introduce partitioned_relabel_here · fb63dfc3
      Philipp Schlehuber authored
      Function taking an automaton and trying to relabel
      it by partitioning the old conditions and encode the
      different subsets of the partition with new variables
      
      * spot/priv/Makefile.am: Add
      * spot/priv/partitioned_relabel.hh
      , spot/priv/partitioned_relabel.cc: try_partition_me,
      computes the partition of a given vector of bdds
      * spot/twaalgos/relabel.hh
      , spot/twaalgos/relabel.cc: Here. Adapt also relabel()
      to cope with the different type of relabeling_maps
      * tests/python/_partitioned_relabel.ipynb
      , tests/python/except.py: Test and Usage
      * tests/Makefile.am: Add test
      fb63dfc3
    • Alexandre Duret-Lutz's avatar
      Merge branch 'master' into next · b02d8328
      Alexandre Duret-Lutz authored
      b02d8328
    • Alexandre Duret-Lutz's avatar
      09e147ee
    • Alexandre Duret-Lutz's avatar
      Release Spot 2.11.3 · d7feeca1
      Alexandre Duret-Lutz authored
      * NEWS, configure.ac, doc/org/setup.org: Bump version to 2.11.3.
      d7feeca1
    • Alexandre Duret-Lutz's avatar
      Work around spurious g++-12 warnings · 1248d326
      Alexandre Duret-Lutz authored
      * spot/twaalgos/ltl2tgba_fm.cc, spot/tl/formula.hh,
      spot/twaalgos/translate.cc: Add SPOT_ASSUME in various places to help
      g++.
      1248d326
    • Alexandre Duret-Lutz's avatar
      formula: new trivial simplifications · 720c3804
      Alexandre Duret-Lutz authored
      Add the following rules:
        - f|[+] = [+] if f rejects [*0]
        - f|[*] = [*] if f accepts [*0]
        - f&&[+] = f if f rejects [*0]
        - b:b[*i..j] = b[*max(i,1)..j]
        - b[*i..j]:b[*k..l] = b[*max(i,1)+max(k,1)-1,1), j+l-1]
      
      * spot/tl/formula.cc: Implement the new rules.
      * doc/tl/tl.tex: Document them.
      * tests/core/equals.test: Test them.
      * NEWS: Add them
      720c3804
    • Alexandre Duret-Lutz's avatar
      formula: introduce one_plus(), and saturate predefined formulas · 8ed9e338
      Alexandre Duret-Lutz authored
      * spot/tl/formula.hh, spot/tl/formula.cc (one_plus): New.
      (fnode): Add a saturated argument.
      (tt_, ff_, eword_, one_plus, one_star): Create saturated node.
      (destroy): Do not check for id() < 3.
      8ed9e338
  11. 07 Dec, 2022 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix semantics of [*i..j] and [:*i..j] · 4629d074
      Alexandre Duret-Lutz authored
      * doc/tl/tl.tex: After a discussion with Antoin, it appears that the
      semantics previously given for f[*0..j] was not considering that f[*0]
      should accept any sequence of one letter.
      4629d074
  12. 06 Dec, 2022 3 commits
  13. 02 Dec, 2022 3 commits
  14. 17 Nov, 2022 1 commit
  15. 15 Nov, 2022 3 commits
  16. 10 Nov, 2022 2 commits