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

5 commits

Author SHA1 Message Date
Alexandre Duret-Lutz
496c449fa4 Update the intro of tl.tex, and add a reference to VECOS'11. 
* doc/tl/tl.tex, doc/tl/tl.bib: Here.
 2012-04-30 11:57:55 +02:00
Alexandre Duret-Lutz
6eb830c8ae Implement star-normal-form rewriting. 
* src/ltlvisit/snf.cc, src/ltlvisit/snf.hh: New files.
* src/ltlvisit/Makefile.am: Distribute them.
* src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh: Call snf(f) for
all f[*].
* src/ltltest/reduccmp.test: Test it.
* doc/tl/tl.tex, doc/tl/tl.bib: Document it.
 2012-04-28 09:34:46 +02:00
Alexandre Duret-Lutz
212c7ebdd7 Add implication-based rewritings from Babiak et al. (TACAS'12) 
* src/ltlvisit/simplify.cc: Implement them here, and augment them
to support M, and W operators.
* src/ltltest/reduccmp.test: Add some tests.
* doc/tl/tl.tex (Simplifications Based on Implications): Document
these rules.
* doc/tl/tl.bib (babiak.12.tacas): New entry.
 2012-04-28 09:34:44 +02:00
Alexandre Duret-Lutz
fef1547bc3 Use `SERE' consistently. Add more references. 
* doc/tl/tl.tex: Replace all occurrences of ``rational
[expression]'' by SERE.  Add a couple of more notes and
bibliographic references.
* doc/tl/tl.bib: More entries.
 2012-04-28 09:34:44 +02:00
Alexandre Duret-Lutz
c483053a85 Add documentation for temporal logic operators. 
* doc/tl/Makefile.am, doc/tl/tl.tex, doc/tl/tl.bib: New files.
* doc/Makefile.am (SUBDIRS): Recurse into tl/.
* configure.ac: Output doc/tl/Makefile
* README: Describe doc/tl/.
 2012-04-28 09:34:43 +02:00