alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity
5270 commits 6 branches 0 tags 36 MiB
Commit graph

117 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
0d9cc29b46 tl: eight new simplification rules 
* NEWS, doc/tl/tl.tex: Document the rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
* tests/core/det.test, tests/core/ltl2tgba2.test,
tests/python/stutter-inv.ipynb, tests/core/385.test: Adjust.
 2019-07-09 16:09:15 +02:00
Alexandre Duret-Lutz
caad07cfa4 * doc/tl/tl.tex: Typo. 2019-06-30 19:06:50 +02:00
Alexandre Duret-Lutz
da5d23f0a2 simplify: GF(f)=GF(dnf(f)) FG(f)=FG(cnf(f)) 
These rules come from Delag's paper, and help some cases
in issue #385.

* spot/tl/simplify.cc: Implement the simplification.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/385.test: New file.
* tests/Makefile.am: Add it.
* tests/core/reduccmp.test: More tests.
* tests/core/ltl2tgba2.test: Adjust one improved case.
* tests/python/automata.ipynb, tests/python/twagraph-internals.ipynb:
Adjust expected output, as the cnf/dnf reorder some subformulas.
 2019-06-18 10:03:56 +02:00
Alexandre Duret-Lutz
df326e032b use a bibtex file to collect all references in Doxygen 
* doc/tl/tl.bib: Move ...
* doc/spot.bib: ... here, and augment it with all references that
appeared verbatim in Doxygen comments.
* doc/Makefile.am, doc/tl/Makefile.am
doc/tl/tl.tex: Adjust for the move.
* doc/Doxyfile.in: Point to spot.bib.
* spot/gen/automata.hh, spot/gen/formulas.hh, spot/misc/game.hh,
spot/misc/minato.hh spot/taalgos/emptinessta.hh,
spot/taalgos/minimize.hh, spot/taalgos/tgba2ta.hh, spot/tl/formula.hh,
spot/tl/remove_x.hh, spot/tl/simplify.hh, spot/tl/snf.hh,
spot/twaalgos/cobuchi.hh, spot/twaalgos/cycles.hh,
spot/twaalgos/dualize.hh, spot/twaalgos/gtec/gtec.hh,
spot/twaalgos/gv04.hh, spot/twaalgos/ltl2taa.hh,
spot/twaalgos/ltl2tgba_fm.hh, spot/twaalgos/magic.hh,
spot/twaalgos/minimize.hh, spot/twaalgos/parity.hh,
spot/twaalgos/powerset.hh, spot/twaalgos/randomgraph.hh,
spot/twaalgos/se05.hh, spot/twaalgos/simulation.hh,
spot/twaalgos/strength.hh, spot/twaalgos/stutter.hh,
spot/twaalgos/tau03.hh, spot/twaalgos/totgba.hh,
spot/twaalgos/toweak.hh: Use \cite instead of a verbatim bibtex entry.
 2019-06-14 21:02:27 +02:00
Alexandre Duret-Lutz
58389bdb80 tl: extend F[n:m] and G[n:m] to the case of m=$ 
Suggested by Victor Khomenko.

* spot/tl/formula.cc, spot/tl/formula.hh, spot/parsetl/parsetl.yy:
Implement this.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/sugar.test, tests/python/ltlparse.py: Add some tests.
 2019-06-02 14:39:21 +02:00
Alexandre Duret-Lutz
90a88d0b5a tl: fix handling of f##[0:0]g, and of ##[0:n]g 
The first issue was reported by Victor Khomenko.

* spot/tl/formula.cc: Introduce a single-argument
version of sugar_delay().
* spot/parsetl/parsetl.yy: Use it.
* doc/tl/tl.tex, spot/tl/formula.hh: Adjust doc.
* tests/core/ltlfilt.test, tests/core/sugar.test: More tests.
 2019-05-20 20:59:33 +02:00
Alexandre Duret-Lutz
66a3b6f7cb tl: fix the definition of ##[i:j] 
Reported by Victor Khomenko.

* NEWS, doc/tl/tl.tex, spot/tl/formula.cc: Fix the definition.
* tests/core/ltl2tgba.test: Add some test cases.
 2019-05-19 09:16:42 +02:00
Alexandre Duret-Lutz
f476483f4a tl: add support for ##[+] and ##[*] 
Suggested by Victor Khomenko.

* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Implement them.
* NEWS, doc/tl/tl.tex: Document them.
* tests/core/sugar.test: Add a couple of tests.
 2019-05-18 12:06:35 +02:00
Alexandre Duret-Lutz
b726d78cbd tl: new simplification rules 
Related to issue #385.

* doc/tl/tl.tex, NEWS: Document the rules.
* spot/tl/simplify.cc: Implement the rules.
* tests/core/reduccmp.test, tests/core/ltl2tgba2.test: Add tests.
* tests/core/degenscc.test: Adjust.
 2019-05-18 11:39:09 +02:00
Alexandre Duret-Lutz
e325289a12 simplify: more rules for first_match 
* spot/tl/simplify.cc: Implement the rules.
* tests/core/reduccmp.test: Test them.
* doc/tl/tl.tex: Document them.
 2019-05-11 14:10:57 +02:00
Alexandre Duret-Lutz
c6605e951d tl: add some simplifications for first_match 
Following a discussion with Victor Khomenko.

* doc/tl/tl.tex: Document those rules.
* spot/tl/simplify.cc: Implement them.
* tests/core/reduccmp.test: Test them.
 2019-05-08 15:08:31 +02:00
Alexandre Duret-Lutz
6fac026454 implement SVA's first_match operator 
* NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document it.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* spot/tl/formula.cc, spot/tl/formula.hh, spot/tl/dot.cc,
spot/tl/mutation.cc, spot/tl/print.cc, spot/tl/randomltl.cc,
spot/twaalgos/ltl2tgba_fm.cc: Adjust to support first_match.
* spot/tl/mark.cc, spot/tl/simplify.cc, spot/tl/snf.cc,
spot/tl/unabbrev.cc, spot/twa/formula2bdd.cc,
spot/twaalgos/ltl2taa.cc: Ignore it.
* tests/core/acc_word.test, tests/core/randpsl.test: Add more tests.
* tests/core/rand.test, tests/core/unambig.test,
tests/python/randltl.ipynb: Adjust.
* tests/python/formulas.ipynb: Show first_match.
 2019-05-06 15:11:30 +02:00
Alexandre Duret-Lutz
caf1eaa4ce tl.pdf: add missing precedence and grammar rules 
* doc/tl/tl.tex: Here.
 2019-05-05 14:26:10 +02:00
Alexandre Duret-Lutz
60d488b30c tl: add support for ##n and ##[i:j] from SVA 
* spot/tl/formula.cc, spot/tl/formula.hh (formula::sugar_delay): New
function to implement this operator as syntactic sugar.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse it.
* doc/tl/tl.tex: Document the syntactic sugar rules and precedence.
* tests/core/sugar.test: Add tests.
* NEWS: Mention this new feature.
 2019-05-04 22:03:13 +02:00
Alexandre Duret-Lutz
82a152c38a unabbreviate: add new rules based on eventual/universal arguments 
Based on a report by Simon Jantsch.  Fixes #362.

* NEWS, doc/tl/tl.tex: Mention the new rules.
* spot/tl/unabbrev.cc: Implement them.
* tests/core/unabbrevwm.test: Test them.
* tests/python/randltl.ipynb: Adjust.
 2018-10-01 17:53:05 +02:00
Alexandre Duret-Lutz
4ce0d92896 tl: add some implication-based rewritings for "<->", "->", and "xor" 
This prevents an exception from being raised if NNF is not performed
on Boolean properties and implication-based checks are used.

* NEWS: Mention the issue.
* spot/tl/simplify.cc, doc/tl/tl.tex: Add some rules.
* tests/python/ltlsimple.py: Test them.
 2018-08-01 17:17:09 +02:00
Alexandre Duret-Lutz
9b8af36527 * doc/tl/tl.tex: Convert to utf-8. 2018-07-06 21:53:14 +02:00
Alexandre Duret-Lutz
e7aa334a71 tl: add support for X[n], F[n:m] and G[n:m] 
* NEWS, doc/tl/tl.tex, doc/tl/tl.bib: Document these new operators.
* spot/parsetl/parsetl.yy, spot/parsetl/scantl.ll: Parse those.
* spot/tl/formula.cc, spot/tl/formula.hh: Add constructors.
* spot/gen/formulas.cc: Use it.
* tests/core/sugar.test: New file.
* tests/Makefile.am: Add it.
 2018-07-06 21:53:10 +02:00
Alexandre Duret-Lutz
ca1c67a73d simplifier: add two new rules 
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.
 2018-06-05 08:48:40 +02:00
Alexandre Duret-Lutz
cfcc18e680 simplify: reduce {r;1} to {r} or {1} 
Fixes #3.

* spot/tl/simplify.cc: Implement this new rule.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
 2018-03-15 07:59:25 +01:00
Florian Perlié-Long
206b1ee287 * doc/tl/tl.tex: Typos 2018-01-19 08:17:44 +01:00
Alexandre Duret-Lutz
308415f88a document the recent changes to implication rules 
* doc/tl/tl.tex: This adds the rules implemented in 0a2bca137
for #293.
 2017-10-17 17:58:59 +02:00
Florian Perlié-Long
0f023bd0fe * HACKING, doc/tl/tl.tex, spot/tl/formula.hh: Typos 2017-10-03 15:54:48 +02:00
Alexandre Duret-Lutz
e8527d5ae9 Improve simplification of expr[*0..1] 
Fixes #108.

* spot/tl/simplify.cc: Implement the reduction.
* doc/tl/tl.tex, NEWS: Document it.
* tests/core/reduccmp.test: Test it.
 2017-09-02 16:35:18 +02:00
Alexandre Duret-Lutz
646c5170ed simplify: some new simplification rules 
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áš.
 2017-09-02 11:27:04 +02:00
Alexandre Duret-Lutz
d134c09f1c tl.pdf: adjust syntactic hierarchy class to match code 
Fixes #243.

* doc/tl/tl.tex: Here.
 2017-03-14 14:38:19 +01:00
Alexandre Duret-Lutz
a0d9bab566 tl: fix incorrect comment about {r} vs. cl(r) 
Fixes #242.

* doc/tl/tl.tex: Remove incorrect claim that {r} does not match the
PSL semantics.
 2017-03-13 18:09:44 +01:00
Alexandre Duret-Lutz
fe1f754d2e * doc/tl/tl.tex: Typo. 2016-11-05 12:11:00 +01:00
Alexandre Duret-Lutz
6528d75339 simplify: rewrite GF(a & GFb) as G(Fa & Fb) 
Fixes #185.

* spot/tl/simplify.cc: Implement the new rule.
* NEWS, doc/tl/tl.tex: Document it.
* tests/core/reduccmp.test: Test it.
 2016-09-22 17:37:55 +02:00
Alexandre Duret-Lutz
abff7eba8e simplifier: new PSL simplifications 
{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.
 2016-07-19 17:57:16 +02:00
Alexandre Duret-Lutz
d5b2de7fa8 simplifier: new LTL simplifications 
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.
 2016-07-19 16:02:19 +02:00
Alexandre Duret-Lutz
176c9e2e17 tl: rename ltl_simplifier to tl_simplifier 
* 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.
 2015-10-18 13:35:23 +02:00
Alexandre Duret-Lutz
cb39210166 kill the ltl namespace 
* 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.
 2015-09-28 16:20:53 +02:00
Alexandre Duret-Lutz
6ded5e75c4 merge ltlvisit/ ltlast/ ltlenv/ into a single tl/ directory 
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.
 2015-09-28 15:36:48 +02:00
Alexandre Duret-Lutz
767e0522c9 tl: fix two typo in the bibliography 
* doc/tl/tl.bib (babiak.12.tacas): Typos in authors.
Reported by Jan Strejček.
 2015-09-06 16:38:19 +02:00
Alexandre Duret-Lutz
308833788b unabbreviate: enable removal of R 
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.
 2015-08-21 16:02:52 +02:00
Alexandre Duret-Lutz
8a3a07d8a4 * doc/tl/tl.tex: Refine note about {r} vs. r in PSL. 2015-08-19 14:20:17 +02:00
Alexandre Duret-Lutz
5f76f34607 * doc/tl/tl.bib: Properly quote PSL. 2015-08-19 10:59:09 +02:00
Alexandre Duret-Lutz
47824bead6 tl: reorganize section 5 
* doc/tl/tl.tex: Here.
 2015-08-18 11:15:28 +02:00
Alexandre Duret-Lutz
d1f915c748 merge tunnabrev/lunnabrev/wmunabbrev into a single function 
* 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.
 2015-08-17 17:38:47 +02:00
Alexandre Duret-Lutz
813c3799c0 ltl: remove is_eltl_formula() 
* 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.
 2015-06-20 15:21:31 +02:00
Alexandre Duret-Lutz
28c8666cf8 doc: make clean should not need latexmk 
Report from Joachim Klein.

* doc/tl/Makefile.am (mostlyclean-local): Rename as...
(maintainer-clean-local): ... this.
 2015-06-19 17:08:26 +02:00
Alexandre Duret-Lutz
7f8aad05e8 tl: add grammar info for [:*] 
Fixes #92.

* doc/tl/tl.tex: Complete grammar rules and operator precedence.
 2015-06-08 23:53:25 +02:00
Alexandre Duret-Lutz
a79db4eefe psl: add support for the [:*i..j] operator 
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.
 2015-01-19 14:39:41 +01:00
Alexandre Duret-Lutz
eebbcac281 tl: formul\ae -> formulas 
* doc/tl/tl.tex: Use "formulas" everywhere in this file.
 2015-01-19 14:39:41 +01:00
Alexandre Duret-Lutz
3b7b52027c More files to ignore. 2015-01-03 19:01:44 +01:00
Alexandre Duret-Lutz
1156866630 simplify: remove an incorect SERE simplification 
* src/ltlvisit/simplify.cc, doc/tl/tl.tex: Remove the rule.
* src/ltltest/reduc0.test: Add a regression test.
* src/ltltest/reduccmp.test: Adjust test cases for its removal.
* NEWS: Mention it.
 2014-12-05 11:06:21 +01:00
Alexandre Duret-Lutz
05ed3def00 snf: Fix the handling of bounded repetition. 
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.
 2014-05-16 09:39:45 +02:00
Alexandre Duret-Lutz
d741d9266d simplify: remove an incorrect simplification rule 
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.
 2014-05-13 17:31:51 +02:00
Alexandre Duret-Lutz
48471b5114 simplify: fix 3 incorrect simplification rules 
* 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.
 2014-05-13 16:59:51 +02:00