1. 06 Jul, 2018 2 commits
  2. 05 Jun, 2018 1 commit
    • Alexandre Duret-Lutz's avatar
      simplifier: add two new rules · ca1c67a7
      Alexandre Duret-Lutz authored
      Fixes #354.
      
      * spot/tl/simplify.cc: Implement the rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test: Add tests.
      * tests/core/det.test, tests/core/satmin.test: Adjust.
      ca1c67a7
  3. 15 Mar, 2018 1 commit
  4. 19 Jan, 2018 1 commit
  5. 18 Oct, 2017 1 commit
  6. 17 Oct, 2017 1 commit
  7. 03 Oct, 2017 2 commits
  8. 02 Sep, 2017 2 commits
    • Alexandre Duret-Lutz's avatar
      Improve simplification of expr[*0..1] · e8527d5a
      Alexandre Duret-Lutz authored
      Fixes #108.
      
      * spot/tl/simplify.cc: Implement the reduction.
      * doc/tl/tl.tex, NEWS: Document it.
      * tests/core/reduccmp.test: Test it.
      e8527d5a
    • Alexandre Duret-Lutz's avatar
      simplify: some new simplification rules · 646c5170
      Alexandre Duret-Lutz authored
      For #263, reported by Mikuláš Klokočka.
      
      G(a & Xe1 & F(b & e2)) = G(a & e1 & Fb & e2)
      F(a | Xu1 | G(b | u2)) = F(a | u1 | Gb | u2)
      
      * spot/tl/simplify.cc: Implement the rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test, tests/core/eventuniv.test: Add test cases.
      * tests/core/det.test, tests/core/ltl2tgba2.test: Adjust to expect
      smaller automata.
      * THANKS: Add Mikuláš.
      646c5170
  9. 14 Mar, 2017 3 commits
  10. 13 Mar, 2017 1 commit
  11. 05 Nov, 2016 1 commit
  12. 22 Sep, 2016 1 commit
  13. 19 Jul, 2016 2 commits
    • Alexandre Duret-Lutz's avatar
      simplifier: new PSL simplifications · abff7eba
      Alexandre Duret-Lutz authored
      {e[*0..j]}<>->f = {e[*1..j]}<>->f
      {e[*0..j]}[]->f = {e[*1..j]}[]->f
      
      Fixes #81.
      
      This required a small change to the bounded-star-normal-form to prevent
      infinite recursion.
      
      * spot/tl/simplify.cc: Implement these rules.
      * doc/tl/tl.tex, NEWS: Document them.
      * tests/core/reduccmp.test: Add tests, and adjust others.
      * tests/core/unambig.test: Replace formula that used to generated an
      ambiguous automaton, but now generates a deterministic one.
      abff7eba
    • Alexandre Duret-Lutz's avatar
      simplifier: new LTL simplifications · d5b2de7f
      Alexandre Duret-Lutz authored
      if e is pure eventuality and g => e, then e U g = Fg
      if u is purely universal and u => g, then u R g = Gg
      
      Fixes #93.
      
      * doc/tl/tl.tex, NEWS: Document the rules.
      * spot/tl/simplify.cc: Implement them.
      * tests/core/reduccmp.test: Test them.
      * tests/core/det.test: Adjust.
      d5b2de7f
  14. 18 Oct, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      tl: rename ltl_simplifier to tl_simplifier · 176c9e2e
      Alexandre Duret-Lutz authored
      * doc/org/tut01.org, doc/tl/tl.tex, src/bin/common_r.hh,
      src/bin/ltlfilt.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
      src/tests/randtgba.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
      src/tl/nenoform.cc, src/tl/randomltl.cc, src/tl/randomltl.hh,
      src/tl/simplify.cc, src/tl/simplify.hh, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/stutter.cc,
      src/twaalgos/translate.cc, src/twaalgos/translate.hh,
      wrap/python/ajax/spotcgi.in, wrap/python/spot.py,
      wrap/python/tests/interdep.py: Rename ltl_simplifier to tl_simplifier.
      * NEWS: Mention it.
      176c9e2e
  15. 28 Sep, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      kill the ltl namespace · cb392101
      Alexandre Duret-Lutz authored
      * NEWS: Mention it.
      * bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc, doc/mainpage.dox,
      doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
      iface/ltsmin/ltsmin.cc, iface/ltsmin/ltsmin.hh,
      iface/ltsmin/modelcheck.cc, src/bin/autfilt.cc,
      src/bin/common_aoutput.cc, src/bin/common_aoutput.hh,
      src/bin/common_finput.cc, src/bin/common_finput.hh,
      src/bin/common_output.cc, src/bin/common_output.hh, src/bin/common_r.hh,
      src/bin/common_trans.cc, src/bin/common_trans.hh, src/bin/dstar2tgba.cc,
      src/bin/genltl.cc, src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc,
      src/bin/ltlcross.cc, src/bin/ltldo.cc, src/bin/ltlfilt.cc,
      src/bin/ltlgrind.cc, src/bin/randaut.cc, src/bin/randltl.cc,
      src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh,
      src/kripkeparse/kripkeparse.yy, src/kripkeparse/public.hh,
      src/ltlparse/fmterror.cc, src/ltlparse/ltlparse.yy,
      src/ltlparse/ltlscan.ll, src/ltlparse/parsedecl.hh,
      src/ltlparse/public.hh, src/parseaut/parseaut.yy,
      src/parseaut/public.hh, src/tests/checkpsl.cc, src/tests/checkta.cc,
      src/tests/complementation.cc, src/tests/consterm.cc,
      src/tests/emptchk.cc, src/tests/equalsf.cc, src/tests/ikwiad.cc,
      src/tests/kind.cc, src/tests/length.cc, src/tests/ltlprod.cc,
      src/tests/ltlrel.cc, src/tests/parse.test,
      src/tests/parse_print_test.cc, src/tests/randtgba.cc,
      src/tests/readltl.cc, src/tests/reduc.cc, src/tests/syntimpl.cc,
      src/tests/taatgba.cc, src/tests/tostring.cc, src/tests/tostring.test,
      src/tl/apcollect.cc, src/tl/apcollect.hh, src/tl/contain.cc,
      src/tl/contain.hh, src/tl/declenv.cc, src/tl/declenv.hh,
      src/tl/defaultenv.cc, src/tl/defaultenv.hh, src/tl/dot.cc,
      src/tl/dot.hh, src/tl/environment.hh, src/tl/exclusive.cc,
      src/tl/exclusive.hh, src/tl/formula.cc, src/tl/formula.hh,
      src/tl/length.cc, src/tl/length.hh, src/tl/mark.cc, src/tl/mark.hh,
      src/tl/mutation.cc, src/tl/mutation.hh, src/tl/nenoform.cc,
      src/tl/nenoform.hh, src/tl/print.cc, src/tl/print.hh,
      src/tl/randomltl.cc, src/tl/randomltl.hh, src/tl/relabel.cc,
      src/tl/relabel.hh, src/tl/remove_x.cc, src/tl/remove_x.hh,
      src/tl/simpfg.cc, src/tl/simpfg.hh, src/tl/simplify.cc,
      src/tl/simplify.hh, src/tl/snf.cc, src/tl/snf.hh, src/tl/unabbrev.cc,
      src/tl/unabbrev.hh, src/twa/bdddict.cc, src/twa/bdddict.hh,
      src/twa/bddprint.cc, src/twa/formula2bdd.cc, src/twa/formula2bdd.hh,
      src/twa/taatgba.cc, src/twa/taatgba.hh, src/twa/twa.hh,
      src/twa/twagraph.cc, src/twa/twagraph.hh, src/twaalgos/compsusp.cc,
      src/twaalgos/compsusp.hh, src/twaalgos/ltl2taa.cc,
      src/twaalgos/ltl2taa.hh, src/twaalgos/ltl2tgba_fm.cc,
      src/twaalgos/ltl2tgba_fm.hh, src/twaalgos/minimize.cc,
      src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
      src/twaalgos/postproc.cc, src/twaalgos/postproc.hh,
      src/twaalgos/powerset.cc, src/twaalgos/powerset.hh,
      src/twaalgos/randomgraph.cc, src/twaalgos/randomgraph.hh,
      src/twaalgos/relabel.cc, src/twaalgos/relabel.hh,
      src/twaalgos/remprop.cc, src/twaalgos/remprop.hh, src/twaalgos/stats.cc,
      src/twaalgos/stats.hh, src/twaalgos/stutter.cc, src/twaalgos/stutter.hh,
      src/twaalgos/translate.cc, src/twaalgos/translate.hh,
      wrap/python/spot_impl.i: Remove the ltl namespace.
      cb392101
    • Alexandre Duret-Lutz's avatar
      merge ltlvisit/ ltlast/ ltlenv/ into a single tl/ directory · 6ded5e75
      Alexandre Duret-Lutz authored
      The ltl prefix does not make a lot of sens anymore (since we
      support psl as well).  ltlast/ and ltlenv/ were almost empty.
      And ltlvisit/ did not contain any visitor anymore.
      
      * src/ltlvisit/, src/ltlast/, src/ltlenv/: Merge into...
      * src/tl/: ...this.
      * NEWS: Mention the change.
      * README, bench/stutter/stutter_invariance_formulas.cc,
      bench/stutter/stutter_invariance_randomgraph.cc, configure.ac,
      doc/org/tut01.org, doc/org/tut02.org, doc/org/tut10.org, doc/tl/tl.tex,
      iface/ltsmin/ltsmin.hh, iface/ltsmin/modelcheck.cc, src/Makefile.am,
      src/bin/autfilt.cc, src/bin/common_output.cc, src/bin/common_output.hh,
      src/bin/common_r.hh, src/bin/common_trans.cc, src/bin/genltl.cc,
      src/bin/ltl2tgba.cc, src/bin/ltl2tgta.cc, src/bin/ltlcross.cc,
      src/bin/ltldo.cc, src/bin/ltlfilt.cc, src/bin/ltlgrind.cc,
      src/bin/randltl.cc, src/kripke/kripkeexplicit.hh,
      src/kripkeparse/public.hh, src/parseaut/public.hh, src/priv/accmap.hh,
      src/ta/taexplicit.hh, src/ta/tgtaexplicit.hh, src/tests/equalsf.cc,
      src/tests/ikwiad.cc, src/tests/length.cc, src/tests/ltlrel.cc,
      src/tests/randtgba.cc, src/tests/readltl.cc, src/tests/reduc.cc,
      src/tests/syntimpl.cc, src/tests/taatgba.cc, src/tests/tostring.cc,
      src/tests/twagraph.cc, src/twa/acc.hh, src/twa/bdddict.cc,
      src/twa/bdddict.hh, src/twa/bddprint.cc, src/twa/taatgba.cc,
      src/twa/taatgba.hh, src/twa/twa.hh, src/twa/twagraph.cc,
      src/twa/twagraph.hh, src/twa/twasafracomplement.cc,
      src/twaalgos/compsusp.cc, src/twaalgos/compsusp.hh,
      src/twaalgos/dtgbasat.cc, src/twaalgos/hoa.cc,
      src/twaalgos/isweakscc.cc, src/twaalgos/lbtt.cc,
      src/twaalgos/ltl2taa.cc, src/twaalgos/ltl2taa.hh,
      src/twaalgos/ltl2tgba_fm.cc, src/twaalgos/ltl2tgba_fm.hh,
      src/twaalgos/minimize.hh, src/twaalgos/neverclaim.cc,
      src/twaalgos/randomgraph.hh, src/twaalgos/relabel.hh,
      src/twaalgos/remprop.hh, src/twaalgos/stats.cc, src/twaalgos/stutter.cc,
      src/twaalgos/translate.hh, wrap/python/spot_impl.i,
      src/ltlparse/ltlparse.yy, src/ltlparse/public.hh: Adjust.
      6ded5e75
  16. 21 Aug, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      unabbreviate: enable removal of R · 30883378
      Alexandre Duret-Lutz authored
      This implies learning alternative rules for G, and W as well, since
      those would use R.
      
      Fixes #103.  Suggested by Joachim Klein.
      
      * src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: Implement the
      new rules.
      * doc/tl/tl.tex: Document the rules.
      * src/tests/unabbrevwm.test: Test them.
      * src/bin/ltlfilt.cc, NEWS: Mention that --unabbreviate accepts R.
      30883378
  17. 19 Aug, 2015 1 commit
  18. 18 Aug, 2015 1 commit
  19. 17 Aug, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      merge tunnabrev/lunnabrev/wmunabbrev into a single function · d1f915c7
      Alexandre Duret-Lutz authored
      * src/ltlvisit/lunabbrev.cc, src/ltlvisit/lunabbrev.hh,
      src/ltlvisit/tunabbrev.cc, src/ltlvisit/tunabbrev.hh,
      src/ltlvisit/wmunabbrev.cc, src/ltlvisit/wmunabbrev.hh: Delete.
      * src/ltlvisit/unabbrev.cc, src/ltlvisit/unabbrev.hh: New files.
      * src/ltlvisit/Makefile.am: Adjust.
      * src/ltlvisit/print.cc, src/tests/equalsf.cc, src/tests/Makefile.am,
      src/twaalgos/ltl2taa.cc, wrap/python/spot_impl.i, src/bin/ltlfilt.cc:
      Adjust callers.
      * src/ltlvisit/contain.cc, src/tests/syntimpl.cc: Remove useless
      include.
      * wrap/python/tests/formulas.ipynb: New test cases.
      * doc/tl/tl.tex: Group all rules in a single section.
      * NEWS: Mention it.
      d1f915c7
  20. 20 Jun, 2015 1 commit
    • Alexandre Duret-Lutz's avatar
      ltl: remove is_eltl_formula() · 813c3799
      Alexandre Duret-Lutz authored
      * doc/tl/tl.tex, src/ltlast/atomic_prop.cc, src/ltlast/binop.cc,
      src/ltlast/bunop.cc, src/ltlast/constant.cc, src/ltlast/formula.cc,
      src/ltlast/formula.hh, src/ltlast/multop.cc, src/ltlast/unop.cc:
      Remove is_eltl_formula().
      * src/tests/kind.test: Adjust.
      813c3799
  21. 08 Jun, 2015 1 commit
  22. 19 Jan, 2015 2 commits
    • Alexandre Duret-Lutz's avatar
      psl: add support for the [:*i..j] operator · a79db4ee
      Alexandre Duret-Lutz authored
      This operator is to ':' what [*i..j] is to ';'.
      
      Part of issue #51.
      
      * doc/tl/tl.tex: Document syntax, semantic, and trivial
      simplifications.
      * doc/tl/spotltl.sty: Add macros for new operators.
      * src/ltlast/bunop.cc, src/ltlast/bunop.hh: Implement it.
      * src/ltlast/multop.cc: Add some trivial simplifications.
      * src/ltlparse/ltlparse.yy, src/ltlparse/ltlscan.ll: Parse it.
      * src/ltltest/equals.test, src/ltltest/latex.test,
      src/tgbatest/ltl2tgba.test: Add more tests.
      * src/ltlvisit/randomltl.cc: Output this operator in
      random PSL formulas.
      * src/ltltest/rand.test: Adjust.
      * src/tgbaalgos/ltl2tgba_fm.cc: Add translation rules.
      * src/ltlvisit/tostring.cc: Add pretty printing code.
      * src/ltlvisit/simplify.cc, src/ltlvisit/snf.cc: Adjust
      switches.
      * NEWS: Mention the new operator.
      a79db4ee
    • Alexandre Duret-Lutz's avatar
      tl: formul\ae -> formulas · eebbcac2
      Alexandre Duret-Lutz authored
      * doc/tl/tl.tex: Use "formulas" everywhere in this file.
      eebbcac2
  23. 05 Dec, 2014 2 commits
  24. 17 May, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      snf: Fix the handling of bounded repetition. · 139f7b49
      Alexandre Duret-Lutz authored
      star_normal_form() used to be called under bounded
      repetitions like [*0..4], but some of these rewritings
      are only correct for [*0..].  For instance
           (a*|1)[*]      can be rewritten to    1[*]
      but  (a*|1)[*0..1]  cannot be rewritten to 1[*0..1]
      it would be correct to rewrite the latter as (a[+]|1)[*0..1],
      canceling the empty word in a*.
      
      Also (a*;b*)[*]     can be rewritten to    (a|b)[*]
      but  (a*;b*)[*0..1]  cannot be rewritten to (a|b)[*0..1]
      and it cannot either be rewritten to (a[+]|b[+])[*0..1].
      
      This patch introduces a new function to implement
      rewritings under bounded repetition.
      
      * src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
      New function.
      * src/ltlvisit/simplify.cc: Use it.
      * src/ltltest/reduccmp.test: Add tests.
      * doc/tl/tl.tex: Document the rewritings implemented.
      139f7b49
  25. 16 May, 2014 1 commit
    • Alexandre Duret-Lutz's avatar
      snf: Fix the handling of bounded repetition. · 05ed3def
      Alexandre Duret-Lutz authored
      star_normal_form() used to be called under bounded
      repetitions like [*0..4], but some of these rewritings
      are only correct for [*0..].  For instance
           (a*|1)[*]      can be rewritten to    1[*]
      but  (a*|1)[*0..1]  cannot be rewritten to 1[*0..1]
      it would be correct to rewrite the latter as (a[+]|1)[*0..1],
      canceling the empty word in a*.
      
      Also (a*;b*)[*]     can be rewritten to    (a|b)[*]
      but  (a*;b*)[*0..1]  cannot be rewritten to (a|b)[*0..1]
      and it cannot either be rewritten to (a[+]|b[+])[*0..1].
      
      This patch introduces a new function to implement
      rewritings under bounded repetition.
      
      * src/ltlvisit/snf.hh, src/ltlvisit/snf.cc (star_normal_form_unbounded):
      New function.
      * src/ltlvisit/simplify.cc: Use it.
      * src/ltltest/reduccmp.test: Add tests.
      * doc/tl/tl.tex: Document the rewritings implemented.
      05ed3def
  26. 13 May, 2014 2 commits
    • Alexandre Duret-Lutz's avatar
      simplify: remove an incorrect simplification rule · d741d926
      Alexandre Duret-Lutz authored
      Fortunately was only enabled with the
      ltl_simplifier_options::favor_event_univ option, which cannot yet be
      turned on from the command-line tools.
      
      * src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
      * src/ltltest/eventuniv.test: Adjust.
      * NEWS: Mention the bug.
      d741d926
    • Alexandre Duret-Lutz's avatar
      simplify: fix 3 incorrect simplification rules · 48471b51
      Alexandre Duret-Lutz authored
      * src/ltlvisit/simplify.cc: Remove two incorrect rules, and
      partially disable another one.
      * doc/tl/tl.tex: Reflect the change.
      * src/ltltest/reduccmp.test: Likewise.
      * src/ltltest/equals.cc: Add safety checks to catch such errors in the
      future.
      * NEWS: Mention the bug.
      48471b51
  27. 17 Oct, 2013 1 commit
  28. 29 Jul, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Fix interpretation of {e[*]} and !{e[*]}. · cb7bdf8c
      Alexandre Duret-Lutz authored
      This follows from a discussion with Ernesto Posse.
      
      The semantics for the {...} operator we use in Spot comes from the
      cl(...) operator defined by Dax et al. (ATVA'09).  This is slightly
      different from the the way the PSL spec interprets a SERE used in the
      context of a temporal formula (appendix B.3.1.1.2, item 7).
      
      cl({a;b}[*]) would match any infinite word that starts with a;b, while
      in PSL {a;b}[*] would match any infinite word that alternates a and b.
      
      Spot documents that {SERE} in a temporal formula is interpreted like
      cl(SERE) however it failed to ignore the empty prefix of SERE.  So
      {{a;b}[*]} would match anything, because the empty word is a prefix of
      any word, and is also accepted by {a;b}[*].  Some trivial identities
      and basic rewritings were also wrongly considering these empty
      prefixes as well.
      
      This patch therefore fixes the translation and syntactic
      simplification rules, to really ignore these empty prefixes.
      
      In some future version it should probably be wise to rename this {...}
      operator as cl(...), and use {...} for the semantics given in appendix
      B.3.1.1.2 (item 7) of the PSL specs.
      
      * src/ltlast/unop.cc: Fix trivial identities.  We have
      {[*0]} = 0 and !{[*0]} = 1.
      * src/ltlvisit/simplify.cc: Fix basic rewriting rules.
      {e[*]} = {e} and !{e[*]} = !{e}.
      * doc/tl/tl.tex: Adjust documentation.
      * doc/tl/tl.bib (dax.09.atva): New entry.
      * src/tgbaalgos/ltl2tgba_fm.cc: Do not accept any
      infinite word for {e[*]} just because the empty
      prefix is matched by e[*].
      * src/tgbatest/ltl2tgba.test: Add a test case.
      * NEWS: Mention it.
      * THANKS: Add Ernesto.
      cb7bdf8c
  29. 27 Apr, 2013 1 commit
    • Alexandre Duret-Lutz's avatar
      Implement a favor_even_univ option in the rewriting rules. · 9caa9ad1
      Alexandre Duret-Lutz authored
      The set of rules enabled by favor_even_univ try to "lift" the
      subformulae that are both eventual and universal, so they appear
      higher in the AST.  This is contrary to what we used to do (and still
      do when the option is unset), were we try to postpone such subformulae
      (by moving them down the AST).  It is still a bit experimental.
      
      * src/ltlvisit/simplify.hh: Add option favor_event_univ.
      * src/ltlvisit/simplify.cc: Implement new rewriting rules.
      * doc/tl/tl.tex: Document them.
      * src/tgbatest/ltl2tgba.cc: Add option -ra to enable them.
      * src/tgbatest/spotlbtt.test: Test the translation with this option.
      * src/ltltest/reduc.cc, src/ltltest/equals.cc: Add option
      to enable the new rules.
      * src/ltltest/eventuniv.test: New file to test them.
      * src/ltltest/Makefile.am: Add it.
      9caa9ad1
  30. 11 Jan, 2013 1 commit