diff --git a/doc/Doxyfile.in b/doc/Doxyfile.in index 52ee00eaa..25f3ec580 100644 --- a/doc/Doxyfile.in +++ b/doc/Doxyfile.in @@ -688,7 +688,7 @@ LAYOUT_FILE = # LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the # search path. See also \cite for info how to create references. -CITE_BIB_FILES = +CITE_BIB_FILES = @srcdir@/spot.bib #--------------------------------------------------------------------------- # Configuration options related to warning and progress messages diff --git a/doc/Makefile.am b/doc/Makefile.am index cfbd13c73..79d437a28 100644 --- a/doc/Makefile.am +++ b/doc/Makefile.am @@ -152,6 +152,7 @@ $(srcdir)/userdoc: $(srcdir)/org-stamp EXTRA_DIST = \ footer.html \ mainpage.dox \ + spot.bib \ $(ORG_FILES) \ $(PICTURES_EXTRA) \ $(srcdir)/org-stamp \ diff --git a/doc/spot.bib b/doc/spot.bib new file mode 100644 index 000000000..23d56681f --- /dev/null +++ b/doc/spot.bib @@ -0,0 +1,751 @@ +@InProceedings{ babiak.12.tacas, + author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r + K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k + and Jan Strej{\v c}ek}, + title = {{LTL} to {B\"u}chi Automata Translation: Fast and More + Deterministic}, + year = 2012, + booktitle = {Proceedings of the 18th International Conference on Tools + and Algorithms for the Construction and Analysis of Systems + (TACAS'12)}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {7214}, + pages = {95--109} +} + +@InProceedings{ babiak.13.spin, + author = {Tom{\'a}{\v{s}} Babiak and Thomas Badie and Alexandre + Duret-Lutz and Mojm{\'i}r K{\v{r}}et{\'i}nsk{\'y} and Jan + Strej{\v{c}}ek}, + title = {Compositional Approach to Suspension and Other + Improvements to {LTL} Translation}, + booktitle = {Proceedings of the 20th International SPIN Symposium on + Model Checking of Software (SPIN'13)}, + year = 2013, + volume = {7976}, + series = {Lecture Notes in Computer Science}, + pages = {81--98}, + month = jul, + publisher = {Springer}, + doi = {10.1007/978-3-642-39176-7_6} +} + +@InProceedings{ beer.01.cav, + author = {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana + Fisman and Anna Gringauze and Yoav Rodeh}, + title = {The Temporal Logic {S}ugar}, + booktitle = {Proceedings of the 13th international conferance on + Computer Aided Verification (CAV'01)}, + series = {Lecture Notes in Computer Science}, + editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain}, + publisher = {Springer}, + isbn = {978-3-540-42345-4}, + pages = {363--367}, + volume = {2102}, + year = {2001}, + month = jul +} + +@InProceedings{ benedikt.13.tacas, + author = {Michael Benedikt and Rastislav Lenhardt and James + Worrell}, + title = {{LTL} Model Checking of Interval Markov Chains}, + booktitle = {19th International Conference on Tools and Algorithms for + the Construction and Analysis of Systems (TACAS'13)}, + year = {2013}, + pages = {32--46}, + series = {Lecture Notes in Computer Science}, + volume = {7795}, + editor = {Nir Piterman and Scott A. Smolka}, + publisher = {Springer} +} + +@Article{ boker.2011.fossacs, + author = {Udi Boker and Orna Kupferman}, + title = {Co-Büching Them All}, + booktitle = {Foundations of Software Science and Computational + Structures - 14th International Conference, FOSSACS 2011}, + year = {2011}, + pages = {184--198}, + url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} +} + +@Article{ bruggeman.96.tcs, + author = {Anne Br{\"u}ggemann-Klein}, + title = {Regular Expressions into Finite Automata}, + journal = {Theoretical Computer Science}, + year = {1996}, + volume = {120}, + pages = {87--98} +} + +@Article{ carton.99.ita, + author = {Olivier Carton and Ram{\'o}n Maceiras}, + title = {Computing the {R}abin index of a parity automaton}, + journal = {Informatique théorique et applications}, + year = {1999}, + volume = {33}, + number = {6}, + pages = {495--505} +} + +@InProceedings{ cerna.03.mfcs, + author = {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek}, + title = {Relating Hierarchy of Temporal Properties to Model + Checking}, + booktitle = {Proceedings of the 28th International Symposium on + Mathematical Foundations of Computer Science (MFCS'03)}, + pages = {318--327}, + year = {2003}, + editor = {Branislav Rovan and Peter Vojt{\'a}{\v{a}}}, + volume = {2747}, + series = {Lecture Notes in Computer Science}, + address = {Bratislava, Slovak Republic}, + month = aug, + publisher = {Springer-Verlag} +} + +@InProceedings{ chang.92.icalp, + author = {Edward Y. Chang and Zohar Manna and Amir Pnueli}, + title = {Characterization of Temporal Property Classes}, + booktitle = {Proceedings of the 19th International Colloquium on + Automata, Languages and Programming (ICALP'92)}, + year = {1992}, + pages = {474--486}, + publisher = {Springer-Verlag}, + address = {London, UK} +} + +@InProceedings{ cichon.09.depcos, + author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski}, + title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} + Formulas}, + booktitle = {Proceedings of the Fourth International Conference on + Dependability of Computer Systems}, + pages = {17--24}, + year = 2009, + publisher = {IEEE Computer Society} +} + +@Article{ cimatti.08.tcad, + author = {Alessandro Cimatti and Marco Roveri and Stefano Tonetta}, + journal = {IEEE Transactions on Computer Aided Design of Integrated + Circuits and Systems}, + number = 10, + pages = {1737--1750}, + title = {Symbolic Compilation of {PSL}}, + volume = 27, + year = 2008, + date = {2009-03-20}, + note = {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}} +} + +@Article{ courcoubetis.92.fmsd, + author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre Wolper + and Mihalis Yannakakis}, + title = {Memory-Efficient Algorithm for the Verification of + Temporal Properties}, + journal = {Formal Methods in System Design}, + pages = {275--288}, + year = {1992}, + volume = {1} +} + +@InProceedings{ couvreur.99.fm, + author = {Jean-Michel Couvreur}, + title = {On-the-fly Verification of Temporal Logic}, + pages = {253--271}, + editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, + booktitle = {Proceedings of the World Congress on Formal Methods in the + Development of Computing Systems (FM'99)}, + publisher = {Springer-Verlag}, + series = {Lecture Notes in Computer Science}, + volume = {1708}, + year = {1999}, + month = sep, + isbn = {3-540-66587-0} +} + +@InProceedings{ dax.07.atva, + author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, + title = {Mechanizing the Powerset Construction for Restricted + Classes of {$\omega$}-Automata}, + year = 2007, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag}, + volume = 4762, + booktitle = {Proceedings of the 5th International Symposium on + Automated Technology for Verification and Analysis + (ATVA'07)}, + editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino + and Yoshio Okamura}, + month = oct +} + +@InProceedings{ dax.09.atva, + author = {Christian Dax and Felix Klaedtke and Stefan Leue}, + title = {Specification Languages for Stutter-Invariant Regular + Properties}, + booktitle = {Proceedings of the 7th International Symposium on + Automated Technology for Verification and Analysis + (ATVA'09)}, + pages = {244--254}, + year = {2009}, + volume = {5799}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag} +} + +@InProceedings{ duret.11.vecos, + author = {Alexandre Duret-Lutz}, + title = {{LTL} Translation Improvements in {Spot}}, + booktitle = {Proceedings of the 5th International Workshop on + Verification and Evaluation of Computer and Communication + Systems (VECoS'11)}, + year = {2011}, + series = {Electronic Workshops in Computing}, + address = {Tunis, Tunisia}, + month = sep, + publisher = {British Computer Society}, + abstract = {Spot is a library of model-checking algorithms. This paper + focuses on the module translating LTL formul{\ae} into + automata. We discuss improvements that have been + implemented in the last four years, we show how Spot's + translation competes on various benchmarks, and we give + some insight into its implementation.}, + url = {http://ewic.bcs.org/category/15853} +} + +@Article{ duret.14.ijccbs, + author = {Alexandre Duret-Lutz}, + title = {{LTL} Translation Improvements in {S}pot 1.0}, + journal = {International Journal on Critical Computer-Based Systems}, + year = {2014}, + volume = {5}, + number = {1/2}, + pages = {31--54}, + month = mar, + doi = {10.1504/IJCCBS.2014.059594} +} + +@InProceedings{ dwyer.98.fmsp, + author = {Matthew B. Dwyer and George S. Avrunin and James C. + Corbett}, + title = {Property Specification Patterns for Finite-state + Verification}, + booktitle = {Proceedings of the 2nd Workshop on Formal Methods in + Software Practice (FMSP'98)}, + publisher = {ACM Press}, + editor = {Mark Ardis}, + month = mar, + year = 1998, + pages = {7--15} +} + +@Book{ eisner.06.psl, + author = {Cindy Eisner and Dana Fisman}, + title = {A Practical Introduction to {PSL}}, + publisher = {Springer}, + year = {2006}, + series = {Series on Integrated Circuits and Systems} +} + +@InCollection{ eisner.08.hvc, + author = {Cindy Eisner and Dana Fisman}, + title = {Structural Contradictions}, + booktitle = {Proceedings of the 4th International Haifa Verification + Conference (HVC'2008)}, + series = {Lecture Notes in Computer Science}, + editor = {Hana Chockler and Alan Hu}, + publisher = {Springer}, + isbn = {978-3-642-01701-8}, + pages = {164--178}, + volume = {5394}, + year = {2009}, + month = oct +} + +@InProceedings{ etessami.00.concur, + author = {Kousha Etessami and Gerard J. Holzmann}, + title = {Optimizing {B\"u}chi Automata}, + booktitle = {Proceedings of the 11th International Conference on + Concurrency Theory (Concur'00)}, + pages = {153--167}, + year = {2000}, + editor = {C. Palamidessi}, + volume = {1877}, + series = {Lecture Notes in Computer Science}, + address = {Pennsylvania, USA}, + publisher = {Springer-Verlag}, + note = {Beware of a typo in the version from the proceedings: $f + \U g$ is purely eventual if both operands are purely + eventual. The revision of the paper available at + \url{http://www.bell-labs.com/project/TMP/} is fixed. We + fixed the bug in Spot in 2005, thanks to LBTT. See also + \url{http://arxiv.org/abs/1011.4214v2} for a discussion + about this problem.} +} + +@Article{ etessami.00.ipl, + author = {Kousha Etessami}, + title = {A note on a question of {P}eled and {W}ilke regarding + stutter-invariant {LTL}}, + journal = {Information Processing Letters}, + volume = {75}, + number = {6}, + year = {2000}, + pages = {261--263} +} + +@InProceedings{ gastin.01.cav, + author = {Paul Gastin and Denis Oddoux}, + title = {Fast {LTL} to {B\"u}chi Automata Translation}, + booktitle = {Proceedings of the 13th International Conference on + Computer Aided Verification (CAV'01)}, + pages = {53--65}, + year = 2001, + editor = {G. Berry and H. Comon and A. Finkel}, + volume = {2102}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag} +} + +@InProceedings{ geldenhuys.04.tacas, + author = {Jaco Geldenhuys and Antti Valmari}, + title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification + More Efficient}, + booktitle = {Proceedings of the 10th International Conference on Tools + and Algorithms for the Construction and Analysis of Systems + (TACAS'04)}, + editor = {Kurt Jensen and Andreas Podelski}, + pages = {205--219}, + year = {2004}, + publisher = {Springer-Verlag}, + series = {Lecture Notes in Computer Science}, + volume = {2988}, + isbn = {3-540-21299-X} +} + +@InProceedings{ geldenhuys.06.spin, + author = {Jaco Geldenhuys and Henri Hansen}, + title = {Larger Automata and Less Work for {LTL} Model Checking}, + booktitle = {Proceedings of the 13th International SPIN Workshop + (SPIN'06)}, + year = {2006}, + pages = {53--70}, + series = {Lecture Notes in Computer Science}, + volume = {3925}, + publisher = {Springer} +} + +@TechReport{ holevek.04.tr, + title = {Verification Results in {Liberouter} Project}, + author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak and + D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek}, + month = {September}, + year = 2004, + number = 03, + institution = {CESNET} +} + +@Book{ holzmann.91.book, + author = {Gerard J. Holzmann}, + title = {Design and Validation of Computer Protocols}, + publisher = {Prentice-Hall}, + address = {Englewood Cliffs, New Jersey}, + year = {1991} +} + +@InProceedings{ jacobs.16.synt, + author = {Swen Jacobs and Felix Klein and Sebastian Schirmer}, + title = {A High-Level {LTL} Synthesis Format: {TLSF} v1.1}, + booktitle = {Proceedings Fifth Workshop on Synthesis (SYNT@CAV'16)}, + pages = {112--132}, + year = {2016}, + series = {Electronic Proceedings in Theoretical Computer Science}, + volume = {229}, + doi = {10.4204/EPTCS.229.10} +} + +@InProceedings{ kretisnky.12.cav, + author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza}, + title = {Deterministic Automata for the {(F,G)}-Fragment of {LTL}}, + booktitle = {24th International Conference on Computer Aided + Verification (CAV'12)}, + year = 2012, + pages = {7--22}, + doi = {10.1007/978-3-642-31424-7_7}, + url = {https://doi.org/10.1007/978-3-642-31424-7_7}, + isbn = {978-3-642-31424-7}, + publisher = {Springer} +} + +@InProceedings{ kuperberg.15.icalp, + author = {Denis Kuperberg and Micha{\l} Skrzypczak }, + title = {On Determinisation of Good-for-Games Automata}, + booktitle = {Proceedings of the 42nd International Colloquium on + Automata, Languages, and Programming (ICALP'15)}, + pages = {299--310}, + year = {2015}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = 9135, + doi = {10.1007/978-3-662-47666-6_24} +} + +@Article{ kupferman.01.tocl, + author = {Orna Kupferman and Moshe Y. Vardi}, + title = {Weak alternating automata are not that weak}, + journal = {ACM Transactions on Computational Logic (TOCL)}, + month = {July}, + year = 2001, + pages = {408--429}, + volume = {2}, + number = {3}, + publisher = {ACM New York, NY, USA} +} + +@Article{ kupferman.05.tcl, + author = {Orna Kupferman and Moshe Y. Vardi}, + title = {From Linear Time to Branching Time}, + journal = {ACM Transactions on Computational Logic}, + volume = {6}, + number = {2}, + month = apr, + year = {2005}, + pages = {273--294}, + doi = {10.1145/1055686.1055689}, + acmid = {1055689}, + publisher = {ACM} +} + +@Article{ kupferman.05.tcs, + author = {Orna Kupferman and Moshe Y. Vardi}, + title = {From complementation to certification}, + journal = {Theoretical Computer Science}, + month = {November}, + year = 2005, + pages = {83--100}, + volume = {345}, + number = {1}, + publisher = {Elsevier} +} + +@InProceedings{ kupferman.10.mochart, + author = {Orna Kupferman and Adin Rosenberg}, + title = {The Blow-Up in Translating {LTL} do Deterministic + Automata}, + booktitle = {Proceedings of the 6th International Workshop on Model + Checking and Artificial Intelligence (MoChArt 2010)}, + pages = {85--94}, + year = 2011, + volume = {6572}, + series = {Lecture Notes in Artificial Intelligence}, + month = nov, + publisher = {Springer}, + note = {See also + \url{https://www.lrde.epita.fr/dload/spot/mochart10-fixes.pdf}} +} + +@MastersThesis{ loding.98.msc, + author = {Christof Löding}, + title = {Methods for the Transformation of ω-Automata: Complexity + and Connection to Second Order Logic}, + school = {Institute of Computer Science and Applied Mathematics + Christian-Albrechts-University of Kiel}, + year = {1998} +} + +@InProceedings{ loding.99.fstts, + author = {Christof L{\"o}ding}, + title = {Optimal Bounds for Transformations of {$\omega$}-Automata}, + booktitle = {Proceedings of the 19th Conference on Foundations of + Software Technology and Theoretical Computer Science + (FSTTCS'99)}, + year = 1999, + publisher = {Springer}, + pages = {97--109}, + series = {Lecture Notes in Computer Science}, + volume = 1738, + doi = {10.1007/3-540-46691-6_8} +} + +@Article{ loizou.82.is, + author = {George Loizou and Peter Thanisch}, + title = {Enumerating the Cycles of a Digraph: A New Preprocessing + Strategy}, + journal = {Information Sciences}, + year = {1982}, + volume = {27}, + number = {3}, + pages = {163--182}, + month = aug +} + +@InProceedings{ manna.87.podc, + author = {Zohar Manna and Amir Pnueli}, + title = {A hierarchy of temporal properties}, + booktitle = {Proceedings of the sixth annual ACM Symposium on + Principles of distributed computing (PODC'90)}, + year = {1990}, + location = {Quebec City, Canada}, + pages = {377--410}, + publisher = {ACM}, + address = {New York, NY, USA} +} + +@InProceedings{ michaud.15.spin, + author = {Thibaud Michaud and Alexandre Duret-Lutz}, + title = {Practical Stutter-Invariance Checks for {$\omega$}-Regular + Languages}, + booktitle = {Proceedings of the 22th International SPIN Symposium on + Model Checking of Software (SPIN'15)}, + year = 2015, + pages = {84--101}, + series = {Lecture Notes in Computer Science}, + volume = 9232, + publisher = {Springer}, + month = aug +} + +@InProceedings{ minato.92.sasimi, + author = {Shin-ichi Minato}, + title = {Fast Generation of Irredundant Sum-of-Products Forms from + Binary Decision Diagrams}, + booktitle = {Proceedings of the third Synthesis and Simulation and + Meeting International Interchange workshop (SASIMI'92)}, + pages = {64--73}, + year = {1992}, + address = {Kobe, Japan}, + month = {April} +} + +@InProceedings{ muller.17.gandalf, + author = {David M\"uller and Salomon Sickert}, + title = {{LTL} to Deterministic {E}merson-{L}ei Automata}, + booktitle = {Proceedings of the 8th International Sumposium on Games, + Automata, Logics and Formal Verification (GandALF'17)}, + year = 2017, + publisher = {Open Publishing Association}, + series = {Electronic Proceedings in Theoretical Computer Science}, + volume = {256}, + pages = {180--194}, + doi = {10.4204/EPTCS.256.13} +} + +@InProceedings{ pelanek.07.spin, + author = {Radek Pel\'{a}nek}, + title = {{BEEM}: benchmarks for explicit model checkers}, + booktitle = {Proceedings of the 14th international SPIN conference on + Model checking software}, + year = 2007, + pages = {263--267}, + numpages = {5}, + volume = {4595}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag} +} + +@Book{ psl.04.lrm, + title = {Property Specification Language Reference Manual v1.1}, + publisher = {Accellera}, + year = {2004}, + month = jun, + note = {\url{http://www.eda.org/vfv/}} +} + +@InProceedings{ renault.13.tacas, + author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice + Kordon and Denis Poitrenaud}, + title = {Strength-Based Decomposition of the Property {B\"u}chi + Automaton for Faster Model Checking}, + booktitle = {Proceedings of the 19th International Conference on Tools + and Algorithms for the Construction and Analysis of Systems + (TACAS'13)}, + year = {2013}, + pages = {580--593}, + publisher = {Springer}, + series = {Lecture Notes in Computer Science}, + volume = {7795}, + doi = {10.1007/978-3-642-36742-7_42} +} + +@InProceedings{ rozier.07.spin, + author = {Kristin Y. Rozier and Moshe Y. Vardi}, + title = {LTL Satisfiability Checking}, + booktitle = {Proceedings of the 12th International SPIN Workshop on + Model Checking of Software (SPIN'07)}, + pages = {149--167}, + year = 2007, + volume = {4595}, + series = {Lecture Notes in Computer Science}, + publisher = {Springer-Verlag} +} + +@InProceedings{ schneider.01.lpar, + author = {Klaus Schneider}, + title = {Improving Automata Generation for Linear Temporal Logic by + Considering the Automaton Hierarchy}, + booktitle = {Proceedings of the 8th International Conference on Logic + for Programming, Artificial Intelligence and Reasoning}, + pages = {39--54}, + year = {2001}, + volume = {2250}, + series = {Lecture Notes in Artificial Intelligence}, + address = {Havana, Cuba}, + publisher = {Springer-Verlag} +} + +@TechReport{ schwoon.04.tr, + author = {Stefan Schwoon and Javier Esparza}, + institution = {Universit{\"a}t Stuttgart, Fakult\"at Informatik, + Elektrotechnik und Informationstechnik}, + month = {November}, + number = {2004/06}, + title = {A Note on On-The-Fly Verification Algorithms}, + year = {2004}, + url = {http://www.fmi.uni-stuttgart.de/szs/publications/info/schwoosn.SE04.shtml} +} + +@InProceedings{ sebastiani.03.charme, + author = {Roberto Sebastiani and Stefano Tonetta}, + title = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for + Efficient LTL Model Checking}, + booktitle = {Proceedings for the 12th Advanced Research Working + Conference on Correct Hardware Design and Verification + Methods (CHARME'03)}, + pages = {126--140}, + year = {2003}, + editor = {G. Goos and J. Hartmanis and J. van Leeuwen}, + volume = {2860}, + series = {Lectures Notes in Computer Science}, + month = {October}, + publisher = {Springer-Verlag} +} + +@InProceedings{ sickert.16.cav, + author = {Salomon Sickert and Javier Esparza and Stefaan Jaax and + Jan K{\v{r}}et{\'i}nsk{\'y}}, + title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal + Logic}, + booktitle = {Proceedings of the 28th International Conference on + Computer Aided Verification (CAV'16)}, + year = 2016, + publisher = {Springer-Verlag}, + series = {Lecture Notes in Computer Science}, + volume = {9780}, + pages = {312--332}, + doi = {10.1007/978-3-319-41540-6_17} +} + +@InProceedings{ somenzi.00.cav, + author = {Fabio Somenzi and Roderick Bloem}, + title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, + booktitle = {Proceedings of the 12th International Conference on + Computer Aided Verification (CAV'00)}, + pages = {247--263}, + year = {2000}, + volume = {1855}, + series = {Lecture Notes in Computer Science}, + address = {Chicago, Illinois, USA}, + publisher = {Springer-Verlag} +} + +@Book{ systemverilog.18.std, + title = {1800-2017 - IEEE Standard for SystemVerilog--Unified + Hardware Design, Specification, and Verification Language}, + publisher = {IEEE}, + year = {2018}, + month = feb, + doi = {10.1109/IEEESTD.2018.8299595} +} + +@InProceedings{ tabakov.10.rv, + author = {Deian Tabakov and Moshe Y. Vardi}, + title = {Optimized Temporal Monitors for {SystemC}}, + booktitle = {Proceedings of the 1st International Conference on Runtime + Verification (RV'10)}, + pages = {436--451}, + year = 2010, + volume = {6418}, + series = {Lecture Notes in Computer Science}, + month = nov, + publisher = {Springer} +} + +@TechReport{ tauriainen.00.tr, + author = {Heikki Tauriainen}, + title = {Automated Testing of {B\"u}chi Automata Translators for + {L}inear {T}emporal {L}ogic}, + address = {Espoo, Finland}, + institution = {Helsinki University of Technology, Laboratory for + Theoretical Computer Science}, + number = {A66}, + year = {2000}, + type = {Research Report}, + note = {Reprint of Master's thesis} +} + +@TechReport{ tauriainen.03.tr, + address = {Espoo, Finland}, + author = {Heikki Tauriainen}, + institution = {Helsinki University of Technology, Laboratory for + Theoretical Computer Science}, + month = {December}, + number = {A83}, + pages = {132}, + title = {On Translating Linear Temporal Logic into Alternating and + Nondeterministic Automata}, + type = {Research Report}, + year = {2003}, + note = {Reprint of Licentiate's thesis} +} + +@TechReport{ tauriainen.06.tr, + address = {Espoo, Finland}, + author = {Heikki Tauriainen}, + month = {September}, + note = {Doctoral dissertation}, + number = {A104}, + title = {Automata and Linear Temporal Logic: Translations with + Transition-Based Acceptance}, + type = {Research Report}, + year = {2006} +} + +@InProceedings{ thirioux.02.fmics, + author = {Xavier Thirioux}, + title = {Simple and Efficient Translation from {LTL} Formulas to + {B\"u}chi Automata}, + booktitle = {Proceedings of the 7th International ERCIM Workshop in + Formal Methods for Industrial Critical Systems (FMICS'02)}, + series = {Electronic Notes in Theoretical Computer Science}, + volume = {66(2)}, + publisher = {Elsevier}, + editor = {Rance Cleaveland and Hubert Garavel}, + year = {2002}, + month = jul, + address = {M{\'a}laga, Spain} +} + +@InBook{ thomas.97.chapter, + author = {Wolfgang Thomas}, + title = {Languages, Automata, and Logic}, + booktitle = {Handbook of Formal Languages --- Volume 3 Beyond Words}, + editor = {Grzegorz Rozenberg and Arto Salomaa}, + chapter = 7, + publisher = {Springer-Verlag}, + year = {1997} +} + +@Article{ zielonka.98.tcs, + author = {Wieslaw Zielonka}, + title = {Infinite games on finitely coloured graphs with + applications to automata on infinite trees}, + journal = {Theoretical Computer Science}, + volume = {200}, + number = {1}, + pages = {135--183}, + year = {1998} +} diff --git a/doc/tl/Makefile.am b/doc/tl/Makefile.am index 941615da9..e4a840aee 100644 --- a/doc/tl/Makefile.am +++ b/doc/tl/Makefile.am @@ -1,5 +1,5 @@ ## -*- coding: utf-8 -*- -## Copyright (C) 2011, 2012, 2013, 2015 Laboratoire de Recherche et +## Copyright (C) 2011, 2012, 2013, 2015, 2019 Laboratoire de Recherche et ## Développement de l'Epita (LRDE). ## ## This file is part of Spot, a model checking library. @@ -24,12 +24,12 @@ all: $(srcdir)/tl.pdf # recent version of latexmk; but version 4.13a, installed on some # of our hosts, does not support it. Add -pvc- because some people # turn pvc on in their config file. -LATEXMK = BIBINPUTS='$(srcdir)' latexmk -pdf -ps- -dvi- -pvc- \ +LATEXMK = BIBINPUTS='$(srcdir)/..' latexmk -pdf -ps- -dvi- -pvc- \ -e '$$bibtex_use=2' \ -e '$$pdflatex="pdflatex %O \"\\def\\SpotVersion{$(VERSION)}\\input{%S}\""' dist_pdf_DATA = $(srcdir)/tl.pdf -EXTRA_DIST = tl.tex tl.bib spotltl.sty +EXTRA_DIST = tl.tex spotltl.sty # latexmk produces its output in the current directory, and may not # update its timestamp when no rebuild was necessary. This can cause @@ -38,7 +38,7 @@ EXTRA_DIST = tl.tex tl.bib spotltl.sty # people that do not change the documentation). Hence the "touch" # below. In case of a VPATH build, we always copy the file, so the # timestamp is updated anyway. -$(srcdir)/tl.pdf: $(srcdir)/tl.tex $(srcdir)/tl.bib +$(srcdir)/tl.pdf: $(srcdir)/tl.tex $(srcdir)/../spot.bib $(LATEXMK) $(srcdir)/tl.tex if test '$(srcdir)' = '.'; then touch $@; else cp tl.pdf $@; fi diff --git a/doc/tl/tl.bib b/doc/tl/tl.bib deleted file mode 100644 index 8a855f59b..000000000 --- a/doc/tl/tl.bib +++ /dev/null @@ -1,241 +0,0 @@ - -@InProceedings{ babiak.12.tacas, - author = {Tom{\'a}{\v{s}} Babiak and Mojm{\'i}r - K{\v{r}}et{\'i}nsk{\'y} and Vojt{\v{e}}ch {\v{R}}eh{\'a}k - and Jan Strej{\v c}ek}, - title = {{LTL} to {B\"u}chi Automata Translation: Fast and More - Deterministic}, - year = 2012, - booktitle = {Proceedings of the 18th International Conference on Tools - and Algorithms for the Construction and Analysis of Systems - (TACAS'12)}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {7214}, - pages = {95--109} -} - -@InProceedings{ beer.01.cav, - author = {Ilan Beer and Shoham Ben-David and Cindy Eisner and Dana - Fisman and Anna Gringauze and Yoav Rodeh}, - title = {The Temporal Logic {S}ugar}, - booktitle = {Proceedings of the 13th international conferance on - Computer Aided Verification (CAV'01)}, - series = {Lecture Notes in Computer Science}, - editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain}, - publisher = {Springer}, - isbn = {978-3-540-42345-4}, - pages = {363--367}, - volume = {2102}, - year = {2001}, - month = jul -} - -@Article{ bruggeman.96.tcs, - author = {Anne Br{\"u}ggemann-Klein}, - title = {Regular Expressions into Finite Automata}, - journal = {Theoretical Computer Science}, - year = {1996}, - volume = {120}, - pages = {87--98} -} - -@InProceedings{ cerna.03.mfcs, - author = {Ivana {\v{C}}ern{\'a} and Radek Pel{\'a}nek}, - title = {Relating Hierarchy of Temporal Properties to Model - Checking}, - booktitle = {Proceedings of the 28th International Symposium on - Mathematical Foundations of Computer Science (MFCS'03)}, - pages = {318--327}, - year = {2003}, - editor = {Branislav Rovan and Peter Vojt{\'a}{\v{a}}}, - volume = {2747}, - series = {Lecture Notes in Computer Science}, - address = {Bratislava, Slovak Republic}, - month = aug, - publisher = {Springer-Verlag} -} - -@InProceedings{ chang.92.icalp, - author = {Edward Y. Chang and Zohar Manna and Amir Pnueli}, - title = {Characterization of Temporal Property Classes}, - booktitle = {Proceedings of the 19th International Colloquium on - Automata, Languages and Programming (ICALP'92)}, - year = {1992}, - pages = {474--486}, - publisher = {Springer-Verlag}, - address = {London, UK} -} - -@Article{ cimatti.08.tcad, - author = {Alessandro Cimatti and Marco Roveri and Stefano Tonetta}, - journal = {IEEE Transactions on Computer Aided Design of Integrated - Circuits and Systems}, - number = 10, - pages = {1737--1750}, - title = {Symbolic Compilation of {PSL}}, - volume = 27, - year = 2008, - date = {2009-03-20}, - note = {\url{https://es.fbk.eu/people/tonetta/tests/tcad07/}} -} - -@InProceedings{ dax.09.atva, - author = {Christian Dax and Felix Klaedtke and Stefan Leue}, - title = {Specification Languages for Stutter-Invariant Regular - Properties}, - booktitle = {Proceedings of the 7th International Symposium on - Automated Technology for Verification and Analysis - (ATVA'09)}, - pages = {244--254}, - year = {2009}, - volume = {5799}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} -} - -@InProceedings{ duret.11.vecos, - author = {Alexandre Duret-Lutz}, - title = {{LTL} Translation Improvements in {Spot}}, - booktitle = {Proceedings of the 5th International Workshop on - Verification and Evaluation of Computer and Communication - Systems (VECoS'11)}, - year = {2011}, - series = {Electronic Workshops in Computing}, - address = {Tunis, Tunisia}, - month = sep, - publisher = {British Computer Society}, - abstract = {Spot is a library of model-checking algorithms. This paper - focuses on the module translating LTL formul{\ae} into - automata. We discuss improvements that have been - implemented in the last four years, we show how Spot's - translation competes on various benchmarks, and we give - some insight into its implementation.}, - url = {http://ewic.bcs.org/category/15853} -} - -@Book{ eisner.06.psl, - author = {Cindy Eisner and Dana Fisman}, - title = {A Practical Introduction to {PSL}}, - publisher = {Springer}, - year = {2006}, - series = {Series on Integrated Circuits and Systems} -} - -@InCollection{ eisner.08.hvc, - author = {Cindy Eisner and Dana Fisman}, - title = {Structural Contradictions}, - booktitle = {Proceedings of the 4th International Haifa Verification - Conference (HVC'2008)}, - series = {Lecture Notes in Computer Science}, - editor = {Hana Chockler and Alan Hu}, - publisher = {Springer}, - isbn = {978-3-642-01701-8}, - pages = {164--178}, - volume = {5394}, - year = {2009}, - month = oct -} - -@InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'00)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - address = {Pennsylvania, USA}, - publisher = {Springer-Verlag}, - note = {Beware of a typo in the version from the proceedings: $f - \U g$ is purely eventual if both operands are purely - eventual. The revision of the paper available at - \url{http://www.bell-labs.com/project/TMP/} is fixed. We - fixed the bug in Spot in 2005, thanks to LBTT. See also - \url{http://arxiv.org/abs/1011.4214v2} for a discussion - about this problem.} -} - -@InProceedings{ jacobs.16.synt, - author = {Swen Jacobs and Felix Klein and Sebastian Schirmer}, - title = {A High-Level {LTL} Synthesis Format: {TLSF} v1.1}, - booktitle = {Proceedings Fifth Workshop on Synthesis (SYNT@CAV'16)}, - pages = {112--132}, - year = {2016}, - series = {Electronic Proceedings in Theoretical Computer Science}, - volume = {229}, - doi = {10.4204/EPTCS.229.10} -} - -@InProceedings{ manna.87.podc, - author = {Zohar Manna and Amir Pnueli}, - title = {A hierarchy of temporal properties}, - booktitle = {Proceedings of the sixth annual ACM Symposium on - Principles of distributed computing (PODC'90)}, - year = {1990}, - location = {Quebec City, Canada}, - pages = {377--410}, - publisher = {ACM}, - address = {New York, NY, USA} -} - -@Book{ psl.04.lrm, - title = {Property Specification Language Reference Manual v1.1}, - publisher = {Accellera}, - year = {2004}, - month = jun, - note = {\url{http://www.eda.org/vfv/}} -} - -@InProceedings{ schneider.01.lpar, - author = {Klaus Schneider}, - title = {Improving Automata Generation for Linear Temporal Logic by - Considering the Automaton Hierarchy}, - booktitle = {Proceedings of the 8th International Conference on Logic - for Programming, Artificial Intelligence and Reasoning}, - pages = {39--54}, - year = {2001}, - volume = {2250}, - series = {Lecture Notes in Artificial Intelligence}, - address = {Havana, Cuba}, - publisher = {Springer-Verlag} -} - -@InProceedings{ somenzi.00.cav, - author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, - booktitle = {Proceedings of the 12th International Conference on - Computer Aided Verification (CAV'00)}, - pages = {247--263}, - year = {2000}, - volume = {1855}, - series = {Lecture Notes in Computer Science}, - address = {Chicago, Illinois, USA}, - publisher = {Springer-Verlag} -} - -@Book{ systemverilog.04.lrm, - title = {SystemVerilog 3.1a Language Reference Manual: - Accellera’s Extensions to Ver- ilog}, - publisher = {Accellera}, - year = {2004}, - month = may, - note = {\url{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.366.6206}} -} - -@TechReport{ tauriainen.03.a83, - author = {Heikki Tauriainen}, - title = {On Translating Linear Temporal Logic into Alternating and - Nondeterministic Automata}, - institution = {Helsinki University of Technology, Laboratory for - Theoretical Computer Science}, - address = {Espoo, Finland}, - month = dec, - number = {A83}, - pages = {132}, - type = {Research Report}, - year = {2003}, - note = {Reprint of Licentiate's thesis} -} diff --git a/doc/tl/tl.tex b/doc/tl/tl.tex index 9598aaa33..38c19da92 100644 --- a/doc/tl/tl.tex +++ b/doc/tl/tl.tex @@ -722,7 +722,7 @@ operands are Boolean formulas. to define a subset of PSL that expresses exactly the stutter-invariant $\omega$-regular languages. \item The $\FIRSTMATCH$ operator does not exist in PSL. It comes - from SystemVerilog Assertions (SVA)~\cite{systemverilog.04.lrm}. + from SystemVerilog Assertions (SVA)~\cite{systemverilog.18.std}. One intuition behind $\FIRSTMATCH\code(f\code)$ is that the DFA for $\FIRSTMATCH\code(f\code)$ can be obtained from the DFA for $f$ by removing all transitions leaving accepting states. @@ -1805,7 +1805,7 @@ implication can be done in two ways: we implement are described in Appendix~\ref{ann:syntimpl}. \item[Language Containment Checks] were initially proposed - by~\citet{tauriainen.03.a83}. This detection is enabled by the + by~\citet{tauriainen.03.tr}. This detection is enabled by the ``\verb|tl_simplifier_options::containment_checks|'' option. \end{description} @@ -1888,7 +1888,7 @@ are counted as one. \endgroup Many of the above rules were collected from the -literature~\cite{somenzi.00.cav,tauriainen.03.a83,babiak.12.tacas} and +literature~\cite{somenzi.00.cav,tauriainen.03.tr,babiak.12.tacas} and sometimes generalized to support operators such as $\M$ and $\W$. \appendix @@ -2043,7 +2043,7 @@ $f_1\AND f_2$ & \bor{f_1}{g}{f_2}{g} & & & \phantomsection % fix hyperlinks \addcontentsline{toc}{chapter}{\bibname} \bibliographystyle{plainnat} -\bibliography{tl} +\bibliography{spot} \end{document} %%% Local Variables: diff --git a/spot/gen/automata.hh b/spot/gen/automata.hh index 242620745..d0c43d5f5 100644 --- a/spot/gen/automata.hh +++ b/spot/gen/automata.hh @@ -27,6 +27,12 @@ namespace spot { namespace gen { + /// \defgroup gen Hard-coded families of formulas or automata. + /// @{ + /// \defgroup genaut Hard-coded families of automata. + /// @{ + + /// \brief Identifiers for automaton patterns enum aut_pattern_id { AUT_BEGIN = 256, /// \brief A family of co-Büchi automata. @@ -34,23 +40,9 @@ namespace spot /// Builds a co-Büchi automaton of size 2n+1 that is /// good-for-games and that has no equivalent deterministic /// co-Büchi automaton with less than 2^n / (2n+1) states. + /// \cite kuperberg.15.icalp /// /// Only defined for n>0. - /// - /** \verbatim - @InProceedings{ kuperberg.15.icalp, - author = {Denis Kuperberg and Micha{\l} Skrzypczak }, - title = {On Determinisation of Good-for-Games Automata}, - booktitle = {Proceedings of the 42nd International Colloquium on - Automata, Languages, and Programming (ICALP'15)}, - pages = {299--310}, - year = {2015}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = 9135, - doi = {10.1007/978-3-662-47666-6_24} - } - \endverbatim */ AUT_KS_NCA = AUT_BEGIN, /// \brief Hard-to-complement non-deterministic Büchi automata /// @@ -59,27 +51,10 @@ namespace spot /// at least n! states if Streett acceptance is used. /// /// Only defined for n>0. The automaton constructed corresponds - /// to the right part of Fig.1 in the following paper, except + /// to the right part of Fig.1 of \cite loding.99.fstts , except /// that only state q_1 is initial. (The fact that states q_2, /// q_3, ..., and q_n are not initial as in the paper does not /// change the recognized language.) - /// - /** \verbatim - @InProceedings{loding.99.fstts, - author = {Christof L{\"o}ding}, - title = {Optimal Bounds for Transformations of - $\omega$-Automata}, - booktitle = {Proceedings of the 19th Conference on Foundations of - Software Technology and Theoretical Computer Science - (FSTTCS'99)}, - year = 1999, - publisher = {Springer}, - pages = {97--109}, - series = {Lecture Notes in Computer Science}, - volume = 1738, - doi = {10.1007/3-540-46691-6_8} - } - \endverbatim */ AUT_L_NBA, /// \brief DSA hard to convert to DRA. /// @@ -90,43 +65,15 @@ namespace spot /// Only defined for 1 - -// Families defined here come from the following papers: -// -// @InProceedings{cichon.09.depcos, -// author = {Jacek Cicho{\'n} and Adam Czubak and Andrzej Jasi{\'n}ski}, -// title = {Minimal {B\"uchi} Automata for Certain Classes of {LTL} Formulas}, -// booktitle = {Proceedings of the Fourth International Conference on -// Dependability of Computer Systems}, -// pages = {17--24}, -// year = 2009, -// publisher = {IEEE Computer Society}, -// } -// -// @InProceedings{geldenhuys.06.spin, -// author = {Jaco Geldenhuys and Henri Hansen}, -// title = {Larger Automata and Less Work for LTL Model Checking}, -// booktitle = {Proceedings of the 13th International SPIN Workshop}, -// year = {2006}, -// pages = {53--70}, -// series = {Lecture Notes in Computer Science}, -// volume = {3925}, -// publisher = {Springer} -// } -// -// @InProceedings{gastin.01.cav, -// author = {Paul Gastin and Denis Oddoux}, -// title = {Fast {LTL} to {B\"u}chi Automata Translation}, -// booktitle = {Proceedings of the 13th International Conference on -// Computer Aided Verification (CAV'01)}, -// pages = {53--65}, -// year = 2001, -// editor = {G. Berry and H. Comon and A. Finkel}, -// volume = {2102}, -// series = {Lecture Notes in Computer Science}, -// address = {Paris, France}, -// publisher = {Springer-Verlag} -// } -// -// @InProceedings{rozier.07.spin, -// author = {Kristin Y. Rozier and Moshe Y. Vardi}, -// title = {LTL Satisfiability Checking}, -// booktitle = {Proceedings of the 12th International SPIN Workshop on -// Model Checking of Software (SPIN'07)}, -// pages = {149--167}, -// year = {2007}, -// volume = {4595}, -// series = {Lecture Notes in Computer Science}, -// publisher = {Springer-Verlag} -// } -// -// @InProceedings{dwyer.98.fmsp, -// author = {Matthew B. Dwyer and George S. Avrunin and James C. Corbett}, -// title = {Property Specification Patterns for Finite-state -// Verification}, -// booktitle = {Proceedings of the 2nd Workshop on Formal Methods in -// Software Practice (FMSP'98)}, -// publisher = {ACM Press}, -// address = {New York}, -// editor = {Mark Ardis}, -// month = mar, -// year = {1998}, -// pages = {7--15} -// } -// -// @InProceedings{etessami.00.concur, -// author = {Kousha Etessami and Gerard J. Holzmann}, -// title = {Optimizing {B\"u}chi Automata}, -// booktitle = {Proceedings of the 11th International Conference on -// Concurrency Theory (Concur'00)}, -// pages = {153--167}, -// year = {2000}, -// editor = {C. Palamidessi}, -// volume = {1877}, -// series = {Lecture Notes in Computer Science}, -// address = {Pennsylvania, USA}, -// publisher = {Springer-Verlag} -// } -// -// @InProceedings{somenzi.00.cav, -// author = {Fabio Somenzi and Roderick Bloem}, -// title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, -// booktitle = {Proceedings of the 12th International Conference on -// Computer Aided Verification (CAV'00)}, -// pages = {247--263}, -// year = {2000}, -// volume = {1855}, -// series = {Lecture Notes in Computer Science}, -// address = {Chicago, Illinois, USA}, -// publisher = {Springer-Verlag} -// } -// -// @InProceedings{tabakov.10.rv, -// author = {Deian Tabakov and Moshe Y. Vardi}, -// title = {Optimized Temporal Monitors for {SystemC}}, -// booktitle = {Proceedings of the 1st International Conference on Runtime -// Verification (RV'10)}, -// pages = {436--451}, -// year = 2010, -// volume = {6418}, -// series = {Lecture Notes in Computer Science}, -// month = nov, -// publisher = {Springer} -// } -// -// @InProceedings{kupferman.10.mochart, -// author = {Orna Kupferman and And Rosenberg}, -// title = {The Blow-Up in Translating LTL do Deterministic Automata}, -// booktitle = {Proceedings of the 6th International Workshop on Model -// Checking and Artificial Intelligence (MoChArt 2010)}, -// pages = {85--94}, -// year = 2011, -// volume = {6572}, -// series = {Lecture Notes in Artificial Intelligence}, -// month = nov, -// publisher = {Springer} -// } -// -// @techreport{holevek.04.tr, -// title = {Verification Results in {Liberouter} Project}, -// author = {J. Hole\v{c}ek and T. Kratochv\'ila and V. \v{R}eh\'ak -// and D. \v{S}afr\'anek and P. \v{S}ime\v{c}ek}, -// month = {September}, -// year = 2004, -// number = 03, -// institution = {CESNET} -// } -// -// @InProceedings{pelanek.07.spin, -// author = {Radek Pel\'{a}nek}, -// title = {{BEEM}: benchmarks for explicit model checkers}, -// booktitle = {Proceedings of the 14th international SPIN conference on -// Model checking software}, -// year = 2007, -// pages = {263--267}, -// numpages = {5}, -// volume = {4595}, -// series = {Lecture Notes in Computer Science}, -// publisher = {Springer-Verlag} -// } -// -// @InProceedings{muller.17.gandalf, -// author = {David M\"uller and Salomon Sickert}, -// title = {{LTL} to Deterministic {E}merson-{L}ei Automata}, -// booktitle = {Proceedings of the 8th International Sumposium on Games, -// Automata, Logics and Formal Verification (GandALF'17)}, -// year = 2017, -// publisher = {Springer-Verlag} -// series = {Electronic Proceedings in Theoretical Computer Science}, -// volume = {256}, -// publisher = {Open Publishing Association}, -// pages = {180--194}, -// doi = {10.4204/EPTCS.256.13} -// } -// -// @InProceedings{sickert.16.cav, -// author = {Salomon Sickert and Javier Esparza and Stefaan Jaax -// and Jan K{\v{r}}et{\'i}nsk{\'y}}, -// title = {Limit-Deterministic {B\"u}chi Automata for Linear Temporal Logic} -// booktitle = {Proceedings of the 28th International Conference on -// Computer Aided Verification (CAV'16)}, -// year = 2016, -// publisher = {Springer-Verlag} -// series = {Lecture Notes in Computer Science}, -// volume = {9780}, -// pages = {312--332}, -// doi = {10.1007/978-3-319-41540-6_17} -// } -// -// @InProceedings{kretisnky.12.cav, -// author = {Jan K{\v{r}}et{\'i}nsk{\'y} and Javier Esparza}, -// title = {Deterministic Automata for the {(F,G)}-Fragment of -// {LTL}}, -// booktitle = {24th International Conference on Computer Aided -// Verification (CAV'12)}, -// year = 2012, -// pages = {7--22}, -// doi = {10.1007/978-3-642-31424-7_7}, -// url = {https://doi.org/10.1007/978-3-642-31424-7_7}, -// isbn = {978-3-642-31424-7}, -// publisher = {Springer}, -// } - - namespace spot { namespace gen { + /// \ingroup gen + /// \defgroup genltl Hard-coded families of formulas. + /// @{ + + /// \brief Identifiers for formula patterns enum ltl_pattern_id { LTL_BEGIN = 256, + /// `F(p1)&F(p2)&...&F(pn)` + /// \cite geldenhuys.06.spin LTL_AND_F = LTL_BEGIN, + /// `FG(p1)&FG(p2)&...&FG(pn)` LTL_AND_FG, + /// `GF(p1)&GF(p2)&...&GF(pn)` + /// \cite cichon.09.depcos , + /// \cite geldenhuys.06.spin . LTL_AND_GF, + /// `F(p1&F(p2&F(p3&...F(pn)))) & F(q1&F(q2&F(q3&...F(qn))))` + /// \cite cichon.09.depcos LTL_CCJ_ALPHA, + /// `F(p&X(p&X(p&...X(p)))) & F(q&X(q&X(q&...X(q))))` + /// \cite cichon.09.depcos LTL_CCJ_BETA, + /// `F(p&(Xp)&(XXp)&...(X...X(p))) & F(q&(Xq)&(XXq)&...(X...X(q)))` + /// \cite cichon.09.depcos LTL_CCJ_BETA_PRIME, + /// 55 specification patterns from Dwyer et al. + /// \cite dwyer.98.fmsp LTL_DAC_PATTERNS, + /// 12 formulas from Etessami and Holzmann. + /// \cite etessami.00.concur LTL_EH_PATTERNS, + /// `F(p0 | XG(p1 | XG(p2 | ... XG(pn))))` LTL_FXG_OR, + /// `(GFa1 & GFa2 & ... & GFan) <-> GFz` LTL_GF_EQUIV, + /// `GF(a <-> X[n](a))` LTL_GF_EQUIV_XN, + /// `(GFa1 & GFa2 & ... & GFan) -> GFz` LTL_GF_IMPLIES, + /// `GF(a -> X[n](a))` LTL_GF_IMPLIES_XN, + /// `(F(p1)|G(p2))&(F(p2)|G(p3))&...&(F(pn)|G(p{n+1}))` + /// \cite geldenhuys.06.spin LTL_GH_Q, + /// `(GF(p1)|FG(p2))&(GF(p2)|FG(p3))&... &(GF(pn)|FG(p{n+1}))` + /// \cite geldenhuys.06.spin LTL_GH_R, + /// `!((GF(p1)&GF(p2)&...&GF(pn)) -> G(q->F(r)))` + /// \cite gastin.01.cav LTL_GO_THETA, + /// `G(p0 & XF(p1 & XF(p2 & ... XF(pn))))` LTL_GXF_AND, + /// 55 patterns from the Liberouter project. + /// \cite holevek.04.tr LTL_HKRSS_PATTERNS, + /// Linear formula with doubly exponential DBA. + /// \cite kupferman.10.mochart LTL_KR_N, + /// Quasilinear formula with doubly exponential DBA. + /// \cite kupferman.10.mochart LTL_KR_NLOGN, + /// Quadratic formula with doubly exponential DBA. + /// \cite kupferman.10.mochart , + /// \cite kupferman.05.tcl . LTL_KV_PSI, + /// `GF(a1&X(a2&X(a3&...Xan)))&F(b1&F(b2&F(b3&...&Xbm)))` + /// \cite muller.17.gandalf LTL_MS_EXAMPLE, + /// `FG(a|b)|FG(!a|Xb)|FG(a|XXb)|FG(!a|XXXb)|...` + /// \cite muller.17.gandalf LTL_MS_PHI_H, + /// `(FGa{n}&GFb{n})|((FGa{n-1}|GFb{n-1})&(...))` + /// \cite muller.17.gandalf LTL_MS_PHI_R, + /// `(FGa{n}|GFb{n})&((FGa{n-1}&GFb{n-1})|(...))` + /// \cite muller.17.gandalf LTL_MS_PHI_S, + /// `FG(p1)|FG(p2)|...|FG(pn)` + /// \cite cichon.09.depcos LTL_OR_FG, + /// `G(p1)|G(p2)|...|G(pn)` + /// \cite geldenhuys.06.spin LTL_OR_G, + /// `GF(p1)|GF(p2)|...|GF(pn)` + /// \cite geldenhuys.06.spin LTL_OR_GF, + /// 20 formulas from BEEM. + /// \cite pelanek.07.spin LTL_P_PATTERNS, + /// `(((p1 R p2) R p3) ... R pn)` LTL_R_LEFT, + /// `(p1 R (p2 R (... R pn)))` LTL_R_RIGHT, + /// n-bit counter + /// \cite rozier.07.spin LTL_RV_COUNTER, + /// n-bit counter with carry + /// \cite rozier.07.spin LTL_RV_COUNTER_CARRY, + /// linear-size formular for an n-bit counter with carry + /// \cite rozier.07.spin LTL_RV_COUNTER_CARRY_LINEAR, + /// linear-size formular for an n-bit counter + /// \cite rozier.07.spin LTL_RV_COUNTER_LINEAR, + /// 27 formulas from Somenzi and Bloem + /// \cite somenzi.00.cav LTL_SB_PATTERNS, + /// `f(0,j)=(GFa0 U X^j(b))`, `f(i,j)=(GFai U G(f(i-1,j)))` + /// \cite sickert.16.cav LTL_SEJK_F, + /// `(GFa1&...&GFan) -> (GFb1&...&GFbn)` + /// \cite sickert.16.cav LTL_SEJK_J, + /// `(GFa1|FGb1)&...&(GFan|FGbn)` + /// \cite sickert.16.cav LTL_SEJK_K, + /// 3 formulas from Sikert et al. + /// \cite sickert.16.cav LTL_SEJK_PATTERNS, + /// `G(p -> (q | Xq | ... | XX...Xq)` + /// \cite tabakov.10.rv LTL_TV_F1, + /// `G(p -> (q | X(q | X(... | Xq)))` + /// \cite tabakov.10.rv LTL_TV_F2, + /// `G(p -> (q & Xq & ... & XX...Xq)` + /// \cite tabakov.10.rv LTL_TV_G1, + /// `G(p -> (q & X(q & X(... & Xq)))` + /// \cite tabakov.10.rv LTL_TV_G2, + /// `G(p1 -> (p1 U (p2 & (p2 U (p3 & (p3 U ...))))))` + /// \cite tabakov.10.rv LTL_TV_UU, + /// `(((p1 U p2) U p3) ... U pn)` + /// \cite geldenhuys.06.spin LTL_U_LEFT, + /// `(p1 U (p2 U (... U pn)))` + /// \cite geldenhuys.06.spin , + /// \cite gastin.01.cav . LTL_U_RIGHT, LTL_END }; @@ -283,5 +193,6 @@ namespace spot /// /// Return the number of arguments expected by an LTL pattern. SPOT_API int ltl_pattern_argc(ltl_pattern_id pattern); + /// @} } } diff --git a/spot/misc/game.hh b/spot/misc/game.hh index 64a155ece..aad248404 100644 --- a/spot/misc/game.hh +++ b/spot/misc/game.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -93,19 +93,7 @@ public: typedef std::unordered_map strategy_t; /// Compute the winning strategy and winning region of this game for player - /// 1 using Zielonka's recursive algorithm. - /** \verbatim - @article{ zielonka.98.tcs - title = "Infinite games on finitely coloured graphs with applications to - automata on infinite trees", - journal = "Theoretical Computer Science", - volume = "200", - number = "1", - pages = "135 - 183", - year = "1998", - author = "Wieslaw Zielonka", - } - \endverbatim */ + /// 1 using Zielonka's recursive algorithm. \cite zielonka.98.tcs void solve(region_t (&w)[2], strategy_t (&s)[2]) const; private: diff --git a/spot/misc/minato.hh b/spot/misc/minato.hh index 6d5b2864a..ff1e1f8b1 100644 --- a/spot/misc/minato.hh +++ b/spot/misc/minato.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2009, 2013-2015, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -33,21 +33,7 @@ namespace spot /// BDD function. /// /// This algorithm implements a derecursived version the Minato-Morreale - /// algorithm presented in the following paper. - /** \verbatim - @InProceedings{ minato.92.sasimi, - author = {Shin-ichi Minato}, - title = {Fast Generation of Irredundant Sum-of-Products Forms - from Binary Decision Diagrams}, - booktitle = {Proceedings of the third Synthesis and Simulation - and Meeting International Interchange workshop - (SASIMI'92)}, - pages = {64--73}, - year = {1992}, - address = {Kobe, Japan}, - month = {April} - } - \endverbatim */ + /// algorithm. \cite minato.92.sasimi class SPOT_API minato_isop { public: diff --git a/spot/taalgos/emptinessta.hh b/spot/taalgos/emptinessta.hh index ff3abd6f3..46a5fc64e 100644 --- a/spot/taalgos/emptinessta.hh +++ b/spot/taalgos/emptinessta.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012-2014, 2016, 2018 Laboratoire de Recherche +// Copyright (C) 2012-2014, 2016, 2018, 2019 Laboratoire de Recherche // et Dévelopment de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -46,20 +46,7 @@ namespace spot /// If spot::ta_check::check() returns false, then the product automaton /// was found empty. Otherwise the automaton accepts some run. /// - /// This is based on the following paper. - /** \verbatim - @InProceedings{ geldenhuys.06.spin, - author = {Jaco Geldenhuys and Henri Hansen}, - title = {Larger Automata and Less Work for {LTL} Model Checking}, - booktitle = {Proceedings of the 13th International SPIN Workshop - (SPIN'06)}, - year = {2006}, - pages = {53--70}, - series = {Lecture Notes in Computer Science}, - volume = {3925}, - publisher = {Springer} - } - \endverbatim */ + /// This is based on \cite geldenhuys.06.spin . /// /// the implementation of spot::ta_check::check() is inspired from the /// two-pass algorithm of the paper above: diff --git a/spot/taalgos/minimize.hh b/spot/taalgos/minimize.hh index f844baa96..2d7af4741 100644 --- a/spot/taalgos/minimize.hh +++ b/spot/taalgos/minimize.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de +// Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014, 2019 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -36,24 +36,6 @@ namespace spot /// same executions starting for either of these states. This can be /// achieved using any algorithm based on partition refinement /// - /// For more detail about this type of algorithm, see the following paper: - /** \verbatim - @InProceedings{valmari.09.icatpn, - author = {Antti Valmari}, - title = {Bisimilarity Minimization in in O(m logn) Time}, - booktitle = {Proceedings of the 30th International Conference on - the Applications and Theory of Petri Nets - (ICATPN'09)}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer}, - isbn = {978-3-642-02423-8}, - pages = {123--142}, - volume = 5606, - url = {http://dx.doi.org/10.1007/978-3-642-02424-5_9}, - year = {2009} - } - \endverbatim */ - /// /// \param ta_ the TA automaton to convert into a simplified TA SPOT_API ta_explicit_ptr minimize_ta(const const_ta_ptr& ta_); diff --git a/spot/taalgos/tgba2ta.hh b/spot/taalgos/tgba2ta.hh index 90112a42f..50b06ff8c 100644 --- a/spot/taalgos/tgba2ta.hh +++ b/spot/taalgos/tgba2ta.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2012-2015, 2017 Laboratoire de Recherche et -// Développement de l'Epita (LRDE). +// Copyright (C) 2010, 2012-2015, 2017, 2019 Laboratoire de Recherche +// et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -28,20 +28,7 @@ namespace spot /// \ingroup tgba_ta /// \brief Build a spot::ta_explicit* (TA) from an LTL formula. /// - /// This is based on the following paper. - /** \verbatim - @InProceedings{ geldenhuys.06.spin, - author = {Jaco Geldenhuys and Henri Hansen}, - title = {Larger Automata and Less Work for {LTL} Model Checking}, - booktitle = {Proceedings of the 13th International SPIN Workshop - (SPIN'06)}, - year = {2006}, - pages = {53--70}, - series = {Lecture Notes in Computer Science}, - volume = {3925}, - publisher = {Springer} - } - \endverbatim */ + /// This is based on \cite geldenhuys.06.spin . /// /// \param tgba_to_convert The TGBA automaton to convert into a TA automaton /// diff --git a/spot/tl/formula.hh b/spot/tl/formula.hh index 7a70a9d97..4c4fb0007 100644 --- a/spot/tl/formula.hh +++ b/spot/tl/formula.hh @@ -1191,22 +1191,7 @@ namespace spot /// \brief Create SERE for f[:*min..max] /// /// This operator is a generalization of the (+) operator - /// defined in the following paper. - /** \verbatim - @InProceedings{ dax.09.atva, - author = {Christian Dax and Felix Klaedtke and Stefan Leue}, - title = {Specification Languages for Stutter-Invariant Regular - Properties}, - booktitle = {Proceedings of the 7th International Symposium on - Automated Technology for Verification and Analysis - (ATVA'09)}, - pages = {244--254}, - year = {2009}, - volume = {5799}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} - } - \endverbatim */ + /// defined by Dax et al. \cite dax.09.atva /// @{ SPOT_DEF_BUNOP(FStar); /// @} @@ -1617,44 +1602,18 @@ namespace spot /// \brief Whether the formula is purely eventual. /// /// Pure eventuality formulae are defined in - /** \verbatim - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'2000)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} - } - \endverbatim */ /// /// A word that satisfies a pure eventuality can be prefixed by /// anything and still satisfies the formula. + /// \cite etessami.00.concur SPOT_DEF_PROP(is_eventual); /// \brief Whether a formula is purely universal. /// /// Purely universal formulae are defined in - /** \verbatim - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'2000)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} - } - \endverbatim */ /// /// Any (non-empty) suffix of a word that satisfies a purely /// universal formula also satisfies the formula. + /// \cite etessami.00.concur SPOT_DEF_PROP(is_universal); /// Whether a PSL/LTL formula is syntactic safety property. SPOT_DEF_PROP(is_syntactic_safety); diff --git a/spot/tl/remove_x.hh b/spot/tl/remove_x.hh index 0a3961607..2171077a7 100644 --- a/spot/tl/remove_x.hh +++ b/spot/tl/remove_x.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2015 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2015, 2019 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. // @@ -23,24 +23,14 @@ namespace spot { + /// \ingroup tl_rewriting /// \brief Rewrite a stutter-insensitive formula \a f without /// using the X operator. /// /// This function may also be applied to stutter-sensitive formulas, /// but in that case the resulting formula is not equivalent. /// - /** \verbatim - @Article{ etessami.00.ipl, - author = {Kousha Etessami}, - title = {A note on a question of {P}eled and {W}ilke regarding - stutter-invariant {LTL}}, - journal = {Information Processing Letters}, - volume = {75}, - number = {6}, - year = {2000}, - pages = {261--263} - } - \endverbatim */ + /// \see \cite etessami.00.ipl SPOT_API formula remove_x(formula f); } diff --git a/spot/tl/simplify.hh b/spot/tl/simplify.hh index d06a3d5c7..725255745 100644 --- a/spot/tl/simplify.hh +++ b/spot/tl/simplify.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011-2017 Laboratoire de Recherche et Developpement +// Copyright (C) 2011-2017, 2019 Laboratoire de Recherche et Developpement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -121,21 +121,8 @@ namespace spot /// /// Returns whether \a f syntactically implies \a g. /// - /// This is adapted from - /** \verbatim - @InProceedings{ somenzi.00.cav, - author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formulae}, - booktitle = {Proceedings of the 12th International Conference on - Computer Aided Verification (CAV'00)}, - pages = {247--263}, - year = {2000}, - volume = {1855}, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag} - } - \endverbatim */ - /// + /// This is adapted from the rules of Somenzi and + /// Bloem. \cite somenzi.00.cav bool syntactic_implication(formula f, formula g); /// \brief Syntactic implication with one negated argument. /// diff --git a/spot/tl/snf.hh b/spot/tl/snf.hh index 43d22218e..839b0496b 100644 --- a/spot/tl/snf.hh +++ b/spot/tl/snf.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2019 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -26,29 +26,20 @@ namespace spot { typedef std::unordered_map snf_cache; - /// Helper to rewrite a sere in Star Normal Form. + /// \ingroup tl_rewriting + /// \brief Helper to rewrite a sere in Star Normal Form. /// /// This should only be called on children of a Star operator. It - /// corresponds to the E° operation defined in the following - /// paper. - /// - /** \verbatim - @Article{ bruggeman.96.tcs, - author = {Anne Br{\"u}ggemann-Klein}, - title = {Regular Expressions into Finite Automata}, - journal = {Theoretical Computer Science}, - year = {1996}, - volume = {120}, - pages = {87--98} - } - \endverbatim */ + /// corresponds to the E° operation defined by Brüggemann-Klein. + /// \cite bruggeman.96.tcs /// /// \param sere the SERE to rewrite /// \param cache an optional cache SPOT_API formula star_normal_form(formula sere, snf_cache* cache = nullptr); - /// A variant of star_normal_form() for r[*0..j] where j < ω. + /// \ingroup tl_rewriting + /// \brief A variant of star_normal_form() for `r[*0..j]` where `j < ω`. SPOT_API formula star_normal_form_bounded(formula sere, snf_cache* cache = nullptr); } diff --git a/spot/twaalgos/cobuchi.hh b/spot/twaalgos/cobuchi.hh index 166c1a530..5c8d85e59 100644 --- a/spot/twaalgos/cobuchi.hh +++ b/spot/twaalgos/cobuchi.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -58,18 +58,8 @@ namespace spot /// \brief Converts a nondet Streett-like aut. to a nondet. co-Büchi aut. /// /// This function works in top of the augmented subset construction algorithm - /// and is described in section 3.1 of: - /** \verbatim - @Article{boker.2011.fossacs, - author = {Udi Boker and Orna Kupferman}, - title = {Co-Büching Them All}, - booktitle = {Foundations of Software Science and Computational - Structures - 14th International Conference, FOSSACS 2011} - year = {2011}, - pages = {184--198}, - url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} - } - \endverbatim */ + /// and is described in section 3.1 of \cite boker.2011.fossacs . + /// /// This implementation is quite different from the described algorithm. It /// is made to work with automaton with Street-like acceptance (including /// Büchi). @@ -86,18 +76,7 @@ namespace spot /// /// This function converts the Rabin-like automaton into a Strett-like /// automaton and then calls nsa_to_nca() on it. It is described in section - /// 3.2 of: - /** \verbatim - @Article{boker.2011.fossacs, - author = {Udi Boker and Orna Kupferman}, - title = {Co-Büching Them All}, - booktitle = {Foundations of Software Science and Computational - Structures - 14th International Conference, FOSSACS 2011} - year = {2011}, - pages = {184--198}, - url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} - } - \endverbatim */ + /// 3.2 of \cite boker.2011.fossacs . /// /// \a aut The automaton to convert. /// \a named_states name each state for easier debugging. @@ -122,18 +101,7 @@ namespace spot /// /// This function calls first nsa_to_nca() in order to retrieve som /// information and then runs a breakpoint construction. The algorithm is - /// described in section 4 of: - /** \verbatim - @Article{boker.2011.fossacs, - author = {Udi Boker and Orna Kupferman}, - title = {Co-Büching Them All}, - booktitle = {Foundations of Software Science and Computational - Structures - 14th International Conference, FOSSACS 2011} - year = {2011}, - pages = {184--198}, - url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} - } - \endverbatim */ + /// described in section 4 of \cite boker.2011.fossacs . /// /// \a aut The automaton to convert. /// \a named_states name each state for easier debugging. @@ -144,18 +112,7 @@ namespace spot /// /// This function calls first nra_to_nca() in order to retrieve som /// information and then runs a breakpoint construction. The algorithm is - /// described in section 4 of: - /** \verbatim - @Article{boker.2011.fossacs, - author = {Udi Boker and Orna Kupferman}, - title = {Co-Büching Them All}, - booktitle = {Foundations of Software Science and Computational - Structures - 14th International Conference, FOSSACS 2011} - year = {2011}, - pages = {184--198}, - url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} - } - \endverbatim */ + /// described in section 4 of \cite boker.2011.fossacs . /// /// \a aut The automaton to convert. /// \a named_states name each state for easier debugging. diff --git a/spot/twaalgos/cycles.hh b/spot/twaalgos/cycles.hh index fa8fbd1bc..47c8d5ad4 100644 --- a/spot/twaalgos/cycles.hh +++ b/spot/twaalgos/cycles.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2018 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2018-2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -28,20 +28,7 @@ namespace spot /// \brief Enumerate elementary cycles in a SCC. /// /// This class implements a non-recursive version of the algorithm - /// on page 170 of: - /** \verbatim - @Article{loizou.82.is, - author = {George Loizou and Peter Thanisch}, - title = {Enumerating the Cycles of a Digraph: A New - Preprocessing Strategy}, - journal = {Information Sciences}, - year = {1982}, - volume = {27}, - number = {3}, - pages = {163--182}, - month = aug - } - \endverbatim */ + /// on page 170 of \cite loizou.82.is . /// (the additional preprocessings described later in that paper are /// not implemented). /// diff --git a/spot/twaalgos/dualize.hh b/spot/twaalgos/dualize.hh index f5f5cb7af..53c600dab 100644 --- a/spot/twaalgos/dualize.hh +++ b/spot/twaalgos/dualize.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017, 2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017, 2018, 2019 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -43,17 +43,7 @@ namespace spot /// If the input automaton is existential, the output will be universal. /// If the input automaton is universal, the output will be existential. /// Finally, if the input automaton is alternating, the result is alternating. - /// More can be found on page 22 (Definition 1.6) of: - /** \verbatim - @mastersthesis{loding.98.methodsfor - author = {Christof Löding} - title = {Methods for the Transformation of ω-Automata: Complexity - and Connection to Second Order Logic} - school = {Institute of Computer Science and Applied Mathematics - Christian-Albrechts-University of Kiel} - year = {1998} - } - \endverbatim */ + /// More can be found on page 22 (Definition 1.6) of \cite loding.98.msc . SPOT_API twa_graph_ptr dualize(const const_twa_graph_ptr& aut); } diff --git a/spot/twaalgos/gtec/gtec.hh b/spot/twaalgos/gtec/gtec.hh index b0a2e5188..c601ca0d1 100644 --- a/spot/twaalgos/gtec/gtec.hh +++ b/spot/twaalgos/gtec/gtec.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2008, 2013, 2014, 2015, 2016, 2018 Laboratoire de Recherche +// Copyright (C) 2008, 2013-2016, 2018-2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -34,24 +34,7 @@ namespace spot /// \brief Check whether the language of an automate is empty. /// - /// This is based on the following paper. - /** \verbatim - @InProceedings{couvreur.99.fm, - author = {Jean-Michel Couvreur}, - title = {On-the-fly Verification of Temporal Logic}, - pages = {253--271}, - editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, - booktitle = {Proceedings of the World Congress on Formal Methods in - the Development of Computing Systems (FM'99)}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {1708}, - year = {1999}, - address = {Toulouse, France}, - month = {September}, - isbn = {3-540-66587-0} - } - \endverbatim */ + /// This is based on \cite couvreur.99.fm . /// /// A recursive definition of the algorithm would look as follows, /// but the implementation is of course not recursive. diff --git a/spot/twaalgos/gv04.hh b/spot/twaalgos/gv04.hh index 3dea3b920..4bef9bff1 100644 --- a/spot/twaalgos/gv04.hh +++ b/spot/twaalgos/gv04.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -33,25 +33,9 @@ namespace spot /// \ingroup emptiness_check_algorithms /// \pre The automaton \a a must have at most one acceptance condition. /// - /// The original algorithm, coming from the following paper, has only - /// been slightly modified to work on transition-based automata. - /** \verbatim - @InProceedings{geldenhuys.04.tacas, - author = {Jaco Geldenhuys and Antti Valmari}, - title = {Tarjan's Algorithm Makes On-the-Fly {LTL} Verification - More Efficient}, - booktitle = {Proceedings of the 10th International Conference on Tools - and Algorithms for the Construction and Analysis of Systems - (TACAS'04)}, - editor = {Kurt Jensen and Andreas Podelski}, - pages = {205--219}, - year = {2004}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {2988}, - isbn = {3-540-21299-X} - } - \endverbatim */ + /// The original algorithm, coming from \cite geldenhuys.04.tacas , + /// has only been slightly modified to work on transition-based + /// automata. SPOT_API emptiness_check_ptr explicit_gv04_check(const const_twa_ptr& a, option_map o = option_map()); } diff --git a/spot/twaalgos/ltl2taa.hh b/spot/twaalgos/ltl2taa.hh index f688127d1..755490334 100644 --- a/spot/twaalgos/ltl2taa.hh +++ b/spot/twaalgos/ltl2taa.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009, 2010, 2013, 2014, 2015 Laboratoire de Recherche +// Copyright (C) 2009, 2010, 2013-2015, 2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -27,21 +27,7 @@ namespace spot /// \ingroup twa_ltl /// \brief Build a spot::taa* from an LTL formula. /// - /// This is based on the following. - /** \verbatim - @techreport{HUT-TCS-A104, - address = {Espoo, Finland}, - author = {Heikki Tauriainen}, - month = {September}, - note = {Doctoral dissertation}, - number = {A104}, - pages = {xii+229}, - title = {Automata and Linear Temporal Logic: Translations - with Transition-Based Acceptance}, - type = {Research Report}, - year = {2006} - } - \endverbatim */ + /// This is based on \cite tauriainen.06.tr . /// /// \param f The formula to translate into an automaton. /// \param dict The spot::bdd_dict the constructed automata should use. diff --git a/spot/twaalgos/ltl2tgba_fm.hh b/spot/twaalgos/ltl2tgba_fm.hh index 6a1d2be2a..76a5a15b9 100644 --- a/spot/twaalgos/ltl2tgba_fm.hh +++ b/spot/twaalgos/ltl2tgba_fm.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017 Laboratoire de +// Copyright (C) 2010, 2011, 2012, 2013, 2014, 2015, 2017, 2019 Laboratoire de // Recherche et Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004, 2005, 2006 Laboratoire d'Informatique de // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), @@ -30,26 +30,11 @@ namespace spot { /// \ingroup twa_ltl - /// \brief Build a spot::twa_graph_ptr from an LTL formula. + /// \brief Build a spot::twa_graph_ptr from an LTL or PSL formula. /// - /// This is based on the following paper. - /** \verbatim - @InProceedings{couvreur.99.fm, - author = {Jean-Michel Couvreur}, - title = {On-the-fly Verification of Temporal Logic}, - pages = {253--271}, - editor = {Jeannette M. Wing and Jim Woodcock and Jim Davies}, - booktitle = {Proceedings of the World Congress on Formal Methods in the - Development of Computing Systems (FM'99)}, - publisher = {Springer-Verlag}, - series = {Lecture Notes in Computer Science}, - volume = {1708}, - year = {1999}, - address = {Toulouse, France}, - month = {September}, - isbn = {3-540-66587-0} - } - \endverbatim */ + /// This originally derived from an algorithm by Couvreur + /// \cite couvreur.99.fm , but it has been improved in many + /// ways \cite duret.14.ijccbs . /// /// \param f The formula to translate into an automaton. /// @@ -68,25 +53,7 @@ namespace spot /// /// \param branching_postponement When set, several transitions leaving /// from the same state with the same label (i.e., condition + acceptance - /// conditions) will be merged. This corresponds to an optimization - /// described in the following paper. - /** \verbatim - @InProceedings{ sebastiani.03.charme, - author = {Roberto Sebastiani and Stefano Tonetta}, - title = {"More Deterministic" vs. "Smaller" B{\"u}chi Automata for - Efficient LTL Model Checking}, - booktitle = {Proceedings for the 12th Advanced Research Working - Conference on Correct Hardware Design and Verification - Methods (CHARME'03)}, - pages = {126--140}, - year = {2003}, - editor = {G. Goos and J. Hartmanis and J. van Leeuwen}, - volume = {2860}, - series = {Lectures Notes in Computer Science}, - month = {October}, - publisher = {Springer-Verlag} - } - \endverbatim */ + /// conditions) will be merged. \cite sebastiani.03.charme /// /// \param fair_loop_approx When set, a really simple characterization of /// unstable state is used to suppress all acceptance conditions from @@ -100,43 +67,11 @@ namespace spot /// \param simplifier If this parameter is set, the LTL formulae /// representing each state of the automaton will be simplified /// before computing the successor. \a simpl should be configured - /// for the type of reduction you want, see - /// spot::tl_simplifier. This idea is taken from the - /// following paper. - /** \verbatim - @InProceedings{ thirioux.02.fmics, - author = {Xavier Thirioux}, - title = {Simple and Efficient Translation from {LTL} Formulas to - {B\"u}chi Automata}, - booktitle = {Proceedings of the 7th International ERCIM Workshop in - Formal Methods for Industrial Critical Systems (FMICS'02)}, - series = {Electronic Notes in Theoretical Computer Science}, - volume = {66(2)}, - publisher = {Elsevier}, - editor = {Rance Cleaveland and Hubert Garavel}, - year = {2002}, - month = jul, - address = {M{\'a}laga, Spain} - } - \endverbatim */ + /// for the type of reduction you want, see spot::tl_simplifier. + /// This idea is taken from \cite thirioux.02.fmics . /// - /// \param unambiguous When true, unambigous TGBA will be produced using - /// the trick described in the following paper. - /** \verbatim - @InProceedings{ benedikt.13.tacas, - author = {Michael Benedikt and Rastislav Lenhardt and James - Worrell}, - title = {{LTL} Model Checking of Interval Markov Chains}, - booktitle = {19th International Conference on Tools and Algorithms for - the Construction and Analysis of Systems (TACAS'13)}, - year = {2013}, - pages = {32--46}, - series = {Lecture Notes in Computer Science}, - volume = {7795}, - editor = {Nir Piterman and Scott A. Smolka}, - publisher = {Springer} - } - \endverbatim */ + /// \param unambiguous When true, unambigous TGBA will be produced + /// using the trick described in \cite benedikt.13.tacas . /// /// \return A spot::twa_graph that recognizes the language of \a f. SPOT_API twa_graph_ptr diff --git a/spot/twaalgos/magic.hh b/spot/twaalgos/magic.hh index 15bf9b750..744c81669 100644 --- a/spot/twaalgos/magic.hh +++ b/spot/twaalgos/magic.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre // et Marie Curie. @@ -79,19 +79,7 @@ namespace spot /// /// This algorithm is an adaptation to TBA of the one /// (which deals with accepting states) presented in - /// - /** \verbatim - Article{ courcoubetis.92.fmsd, - author = {Costas Courcoubetis and Moshe Y. Vardi and Pierre - Wolper and Mihalis Yannakakis}, - title = {Memory-Efficient Algorithm for the Verification of - Temporal Properties}, - journal = {Formal Methods in System Design}, - pages = {275--288}, - year = {1992}, - volume = {1} - } - \endverbatim */ + /// \cite courcoubetis.92.fmsd . /// /// \bug The name is misleading. Magic-search is the algorithm /// from \c godefroid.93.pstv, not \c courcoubetis.92.fmsd. @@ -106,16 +94,7 @@ namespace spot /// /// During the visit of \a a, the returned checker does not store explicitely /// the traversed states but uses the bit-state hashing technic presented in: - /// - /** \verbatim - @book{Holzmann91, - author = {G.J. Holzmann}, - title = {Design and Validation of Computer Protocols}, - publisher = {Prentice-Hall}, - address = {Englewood Cliffs, New Jersey}, - year = {1991} - } - \endverbatim */ + /// \cite Holzmann.91.book. /// /// Consequently, the detection of an acceptence cycle is not ensured. /// diff --git a/spot/twaalgos/minimize.hh b/spot/twaalgos/minimize.hh index 98a161ab1..9bf1f796b 100644 --- a/spot/twaalgos/minimize.hh +++ b/spot/twaalgos/minimize.hh @@ -36,21 +36,7 @@ namespace spot /// determinized and minimized using the standard DFA construction /// as if all states were accepting states. /// - /// For more detail about monitors, see the following paper: - /** \verbatim - @InProceedings{ tabakov.10.rv, - author = {Deian Tabakov and Moshe Y. Vardi}, - title = {Optimized Temporal Monitors for SystemC{$^*$}}, - booktitle = {Proceedings of the 10th International Conferance - on Runtime Verification}, - pages = {436--451}, - year = 2010, - volume = {6418}, - series = {Lecture Notes in Computer Science}, - month = nov, - publisher = {Spring-Verlag} - } - \endverbatim */ + /// For more detail about monitors, see \cite tabakov.10.rv . /// (Note: although the above paper uses Spot, this function did not /// exist in Spot at that time.) /// @@ -75,24 +61,7 @@ namespace spot /// /// The construction is inspired by the following paper, however we /// guarantee that the output language is a subsets of the original - /// language while they don't. - /** \verbatim - @InProceedings{ dax.07.atva, - author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, - title = {Mechanizing the Powerset Construction for Restricted - Classes of {$\omega$}-Automata}, - year = 2007, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag}, - volume = 4762, - booktitle = {Proceedings of the 5th International Symposium on - Automated Technology for Verification and Analysis - (ATVA'07)}, - editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino - and Yoshio Okamura}, - month = oct - } - \endverbatim */ + /// language while they don't. \cite dax.07.atva /// /// If an \a output_aborter is given, the determinization is aborted /// whenever it would produce an automaton that is too large. In @@ -104,25 +73,7 @@ namespace spot /// /// This function attempts to minimize the automaton \a aut_f using the /// algorithm implemented in the minimize_wdba() function, and presented - /// by the following paper: - /// - /** \verbatim - @InProceedings{ dax.07.atva, - author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, - title = {Mechanizing the Powerset Construction for Restricted - Classes of {$\omega$}-Automata}, - year = 2007, - series = {Lecture Notes in Computer Science}, - publisher = {Springer-Verlag}, - volume = 4762, - booktitle = {Proceedings of the 5th International Symposium on - Automated Technology for Verification and Analysis - (ATVA'07)}, - editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino - and Yoshio Okamura}, - month = oct - } - \endverbatim */ + /// by \cite dax.07.atva . /// /// Because it is hard to determine if an automaton corresponds /// to an obligation property, you should supply either the formula diff --git a/spot/twaalgos/parity.hh b/spot/twaalgos/parity.hh index 11b48b6e5..167c6b2d8 100644 --- a/spot/twaalgos/parity.hh +++ b/spot/twaalgos/parity.hh @@ -140,17 +140,7 @@ namespace spot /// /// This implements an algorithm derived from the following article, /// but generalized to all types of parity acceptance. - /** \verbatim - @Article{carton.99.ita, - author = {Olivier Carton and Ram{\'o}n Maceiras}, - title = {Computing the {R}abin index of a parity automaton}, - journal = {Informatique théorique et applications}, - year = {1999}, - volume = {33}, - number = {6}, - pages = {495--505} - } - \endverbatim */ + /// \cite carton.99.ita /// /// The kind of parity (min/max) is preserved, but the style /// (odd/even) may be altered to reduce the number of colors used. diff --git a/spot/twaalgos/powerset.hh b/spot/twaalgos/powerset.hh index d1d601c05..a0d41eeb7 100644 --- a/spot/twaalgos/powerset.hh +++ b/spot/twaalgos/powerset.hh @@ -112,24 +112,8 @@ namespace spot /// determinized, and this procedure does not ensure that the /// produced automaton is equivalent to \a aut. /// - /// The construction is adapted from Section 3.2 of: - /// \verbatim - /// @InProceedings{ dax.07.atva, - /// author = {Christian Dax and Jochen Eisinger and Felix Klaedtke}, - /// title = {Mechanizing the Powerset Construction for Restricted - /// Classes of {$\omega$}-Automata}, - /// year = 2007, - /// series = {Lecture Notes in Computer Science}, - /// publisher = {Springer-Verlag}, - /// volume = 4762, - /// booktitle = {Proceedings of the 5th International Symposium on - /// Automated Technology for Verification and Analysis - /// (ATVA'07)}, - /// editor = {Kedar S. Namjoshi and Tomohiro Yoneda and Teruo Higashino - /// and Yoshio Okamura}, - /// month = oct - /// } - /// \endverbatim + /// The construction is adapted from Section 3.2 of + /// \cite dax.07.atva /// only adapted to work on TBA rather than BA. /// /// If \a threshold_states is non null, abort the construction diff --git a/spot/twaalgos/randomgraph.hh b/spot/twaalgos/randomgraph.hh index 7eed91e7c..8e8a5dd08 100644 --- a/spot/twaalgos/randomgraph.hh +++ b/spot/twaalgos/randomgraph.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2011, 2013, 2014, 2015 Laboratoire de Recherche et +// Copyright (C) 2011, 2013-2015, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -55,21 +55,7 @@ namespace spot /// belongs to a single acceptance set. /// /// This algorithms is adapted from the one in Fig 6.2 page 48 of - /** \verbatim - @TechReport{ tauriainen.00.a66, - author = {Heikki Tauriainen}, - title = {Automated Testing of {B\"u}chi Automata Translators for - {L}inear {T}emporal {L}ogic}, - address = {Espoo, Finland}, - institution = {Helsinki University of Technology, Laboratory for - Theoretical Computer Science}, - number = {A66}, - year = {2000}, - url = {http://citeseer.nj.nec.com/tauriainen00automated.html}, - type = {Research Report}, - note = {Reprint of Master's thesis} - } - \endverbatim */ + /// \cite tauriainen.00.tr . /// /// Although the intent is similar, there are some differences /// between the above published algorithm and this implementation. diff --git a/spot/twaalgos/se05.hh b/spot/twaalgos/se05.hh index b9c2f69d0..268762f38 100644 --- a/spot/twaalgos/se05.hh +++ b/spot/twaalgos/se05.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Developpement -// de l'Epita (LRDE). +// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et +// Developpement de l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 // (LIP6), département Systèmes Répartis Coopératifs (SRC), Université // Pierre et Marie Curie. @@ -84,19 +84,7 @@ namespace spot \endverbatim */ /// /// It is an adaptation to TBA of the one presented in - /** \verbatim - @techreport{SE04, - author = {Stefan Schwoon and Javier Esparza}, - institution = {Universit{\"a}t Stuttgart, Fakult\"at Informatik, - Elektrotechnik und Informationstechnik}, - month = {November}, - number = {2004/06}, - title = {A Note on On-The-Fly Verification Algorithms}, - year = {2004}, - url = - {http://www.fmi.uni-stuttgart.de/szs/publications/info/schwoosn.SE04.shtml} - } - \endverbatim */ + /// \cite schwoon.04.tr . /// /// \sa spot::explicit_magic_search /// @@ -109,17 +97,8 @@ namespace spot /// it is a TBA). /// /// During the visit of \a a, the returned checker does not store explicitely - /// the traversed states but uses the bit-state hashing technic presented in: - /// - /** \verbatim - @book{Holzmann91, - author = {G.J. Holzmann}, - title = {Design and Validation of Computer Protocols}, - publisher = {Prentice-Hall}, - address = {Englewood Cliffs, New Jersey}, - year = {1991} - } - \endverbatim */ + /// the traversed states but uses the bit-state hashing technic presented in + /// \cite holzmann.91.book /// /// Consequently, the detection of an acceptence cycle is not ensured. /// diff --git a/spot/twaalgos/simulation.hh b/spot/twaalgos/simulation.hh index 241b7fd15..2721a6893 100644 --- a/spot/twaalgos/simulation.hh +++ b/spot/twaalgos/simulation.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2012, 2013, 2014, 2015, 2017 Laboratoire de Recherche et +// Copyright (C) 2012-2015, 2017, 2019 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -33,24 +33,7 @@ namespace spot /// When the suffixes (letter and acceptance conditions) reachable /// from one state are included in the suffixes seen by another one, /// the former state can be merged into the latter. The algorithm is - /// based on the following paper, but generalized to handle TωA - /// directly. - /// - /** \verbatim - @InProceedings{ etessami.00.concur, - author = {Kousha Etessami and Gerard J. Holzmann}, - title = {Optimizing {B\"u}chi Automata}, - booktitle = {Proceedings of the 11th International Conference on - Concurrency Theory (Concur'00)}, - pages = {153--167}, - year = {2000}, - editor = {C. Palamidessi}, - volume = {1877}, - series = {Lecture Notes in Computer Science}, - address = {Pennsylvania, USA}, - publisher = {Springer-Verlag} - } - \endverbatim */ + /// described in \cite babiak.13.spin . /// /// Our reconstruction of the quotient automaton based on this /// suffix-inclusion relation will also improve determinism. @@ -87,24 +70,7 @@ namespace spot /// /// When the prefixes (letter and acceptance conditions) leading to /// one state are included in the prefixes leading to one, the former - /// state can be merged into the latter. - /// - /// Reverse simulation is discussed in the following paper, - /// but generalized to handle TωA directly. - /** \verbatim - @InProceedings{ somenzi.00.cav, - author = {Fabio Somenzi and Roderick Bloem}, - title = {Efficient {B\"u}chi Automata for {LTL} Formul{\ae}}, - booktitle = {Proceedings of the 12th International Conference on - Computer Aided Verification (CAV'00)}, - pages = {247--263}, - year = {2000}, - volume = {1855}, - series = {Lecture Notes in Computer Science}, - address = {Chicago, Illinois, USA}, - publisher = {Springer-Verlag} - } - \endverbatim */ + /// state can be merged into the latter. \cite babiak.13.spin . /// /// Our reconstruction of the quotient automaton based on this /// prefix-inclusion relation will also improve codeterminism. diff --git a/spot/twaalgos/strength.hh b/spot/twaalgos/strength.hh index ec2cad656..809fdc1d9 100644 --- a/spot/twaalgos/strength.hh +++ b/spot/twaalgos/strength.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2010, 2011, 2013, 2014, 2015, 2016, 2017, 2018 Laboratoire -// de Recherche et Développement de l'Epita (LRDE) +// Copyright (C) 2010-2011, 2013-2019 Laboratoire de Recherche et +// Développement de l'Epita (LRDE) // // This file is part of Spot, a model checking library. // @@ -156,29 +156,10 @@ namespace spot /// an incorrect SCC number is supplied. /// /// The definition are basically those used in the following paper, - /// except that we extra the "inherently weak" part instead of the + /// except that we extract the "inherently weak" part instead of the /// weak part because we can now test for inherent weakness /// efficiently enough (not enumerating all cycles as suggested in - /// the paper). - /** \verbatim - @inproceedings{renault.13.tacas, - author = {Etienne Renault and Alexandre Duret-Lutz and Fabrice - Kordon and Denis Poitrenaud}, - title = {Strength-Based Decomposition of the Property {B\"u}chi - Automaton for Faster Model Checking}, - booktitle = {Proceedings of the 19th International Conference on Tools - and Algorithms for the Construction and Analysis of Systems - (TACAS'13)}, - editor = {Nir Piterman and Scott A. Smolka}, - year = {2013}, - month = mar, - pages = {580--593}, - publisher = {Springer}, - series = {Lecture Notes in Computer Science}, - volume = {7795}, - doi = {10.1007/978-3-642-36742-7_42} - } - \endverbatim */ + /// the paper). \cite renault.13.tacas /// /// \param aut the automaton to decompose /// \param keep a string specifying the strengths/SCCs to keep diff --git a/spot/twaalgos/stutter.hh b/spot/twaalgos/stutter.hh index cbb40c6b6..47faceafb 100644 --- a/spot/twaalgos/stutter.hh +++ b/spot/twaalgos/stutter.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2017 Laboratoire de Recherche +// Copyright (C) 2014-2017, 2019 Laboratoire de Recherche // et Développement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -30,22 +30,7 @@ namespace spot /// /// Any letter that enters a state will spawn a copy of this state /// with a self-loop using the same letter. For more details - /// about this function, see - /** \verbatim - @InProceedings{ michaud.15.spin, - author = {Thibaud Michaud and Alexandre Duret-Lutz}, - title = {Practical Stutter-Invariance Checks for - {$\omega$}-Regular Languages}, - booktitle = {Proceedings of the 22th International SPIN - Symposium on Model Checking of Software (SPIN'15)}, - year = 2015, - pages = {84--101}, - series = {Lecture Notes in Computer Science}, - volume = 9232, - publisher = {Springer}, - month = aug - } - \endverbatim */ + /// about this function, see \cite michaud.15.spin . SPOT_API twa_graph_ptr sl(const_twa_graph_ptr aut); @@ -55,22 +40,7 @@ namespace spot /// /// For any transition (s,d) labeled by a letter ℓ, we add a state x /// and three transitions (s,x), (x,x), (x,d) all labeled by ℓ. - /// For more details about this function, see - /** \verbatim - @InProceedings{ michaud.15.spin, - author = {Thibaud Michaud and Alexandre Duret-Lutz}, - title = {Practical Stutter-Invariance Checks for - {$\omega$}-Regular Languages}, - booktitle = {Proceedings of the 22th International SPIN - Symposium on Model Checking of Software (SPIN'15)}, - year = 2015, - pages = {84--101}, - series = {Lecture Notes in Computer Science}, - volume = 9232, - publisher = {Springer}, - month = aug - } - \endverbatim */ + /// For more details about this function, see \cite michaud.15.spin . /// /// The inplace version of the function modifies the input /// automaton. @@ -89,23 +59,7 @@ namespace spot /// a transition labeled by B, and (y,z) is a transition labeled by C, /// we add a transition (x,z) labeled by B∧C. /// - /// For more details about this function, see - /** \verbatim - @InProceedings{ michaud.15.spin, - author = {Thibaud Michaud and Alexandre Duret-Lutz}, - title = {Practical Stutter-Invariance Checks for - {$\omega$}-Regular Languages}, - booktitle = {Proceedings of the 22th International SPIN - Symposium on Model Checking of Software (SPIN'15)}, - year = 2015, - pages = {84--101}, - series = {Lecture Notes in Computer Science}, - volume = 9232, - publisher = {Springer}, - month = aug - } - \endverbatim */ - /// + /// For more details about this function, see \cite michaud.15.spin . /// /// The inplace version of the function modifies the input /// automaton. @@ -133,22 +87,7 @@ namespace spot /// The prop_stutter_invariant() property of \a aut_f is set as a /// side-effect. /// - /// For more details about this function, see - /** \verbatim - @InProceedings{ michaud.15.spin, - author = {Thibaud Michaud and Alexandre Duret-Lutz}, - title = {Practical Stutter-Invariance Checks for - {$\omega$}-Regular Languages}, - booktitle = {Proceedings of the 22th International SPIN - Symposium on Model Checking of Software (SPIN'15)}, - year = 2015, - pages = {84--101}, - series = {Lecture Notes in Computer Science}, - volume = 9232, - publisher = {Springer}, - month = aug - } - \endverbatim */ + /// For more details about this function, see \cite michaud.15.spin . SPOT_API bool is_stutter_invariant(formula f, twa_graph_ptr aut_f = nullptr); @@ -164,22 +103,7 @@ namespace spot /// The prop_stutter_invariant() property of \a aut_f is set as a /// side-effect. /// - /// For more details about this function, see - /** \verbatim - @InProceedings{ michaud.15.spin, - author = {Thibaud Michaud and Alexandre Duret-Lutz}, - title = {Practical Stutter-Invariance Checks for - {$\omega$}-Regular Languages}, - booktitle = {Proceedings of the 22th International SPIN - Symposium on Model Checking of Software (SPIN'15)}, - year = 2015, - pages = {84--101}, - series = {Lecture Notes in Computer Science}, - volume = 9232, - publisher = {Springer}, - month = aug - } - \endverbatim */ + /// For more details about this function, see \cite michaud.15.spin . SPOT_API bool is_stutter_invariant(twa_graph_ptr aut_f, const_twa_graph_ptr aut_nf = nullptr, diff --git a/spot/twaalgos/tau03.hh b/spot/twaalgos/tau03.hh index f4f870aa6..324379af0 100644 --- a/spot/twaalgos/tau03.hh +++ b/spot/twaalgos/tau03.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013, 2014 Laboratoire de Recherche et Développement de +// Copyright (C) 2013, 2014, 2019 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // Copyright (C) 2004, 2005 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -75,25 +75,7 @@ namespace spot end; \endverbatim */ /// - /// This algorithm is the one presented in - /// - /** \verbatim - @techreport{HUT-TCS-A83, - address = {Espoo, Finland}, - author = {Heikki Tauriainen}, - institution = {Helsinki University of Technology, Laboratory for - Theoretical Computer Science}, - month = {December}, - number = {A83}, - pages = {132}, - title = {On Translating Linear Temporal Logic into Alternating and - Nondeterministic Automata}, - type = {Research Report}, - year = {2003}, - url = {http://www.tcs.hut.fi/Publications/info/bibdb.HUT-TCS-A83.shtml} - } - \endverbatim */ - /// + /// This algorithm is the one presented in \cite tauriainen.03.tr . SPOT_API emptiness_check_ptr explicit_tau03_search(const const_twa_ptr& a, option_map o = option_map()); diff --git a/spot/twaalgos/totgba.hh b/spot/twaalgos/totgba.hh index e888891ec..a011b920a 100644 --- a/spot/twaalgos/totgba.hh +++ b/spot/twaalgos/totgba.hh @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015, 2016, 2018 Laboratoire de Recherche et Développement -// de l'Epita. +// Copyright (C) 2015-2016, 2018-2019 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -87,18 +87,7 @@ namespace spot /// \brief Converts any DNF acceptance condition into Streett-like. /// /// This function is an optimized version of the construction described - /// by Lemma 4 and 5 of the paper below. - /** \verbatim - @Article{boker.2011.fossacs, - author = {Udi Boker and Orna Kupferman}, - title = {Co-Büching Them All}, - booktitle = {Foundations of Software Science and Computational - Structures - 14th International Conference, FOSSACS 2011} - year = {2011}, - pages = {184--198}, - url = {\url{www.cs.huji.ac.il/~ornak/publications/fossacs11b.pdf}} - } - \endverbatim */ + /// by Lemma 4 and 5 of \cite boker.2011.fossacs . /// /// In the described construction, as many copies as there are minterms in /// the acceptance condition are made and the union of all those copies is diff --git a/spot/twaalgos/toweak.hh b/spot/twaalgos/toweak.hh index 0b77749af..27661cb56 100644 --- a/spot/twaalgos/toweak.hh +++ b/spot/twaalgos/toweak.hh @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017 Laboratoire de Recherche et Développement de +// Copyright (C) 2017, 2019 Laboratoire de Recherche et Développement de // l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -31,30 +31,9 @@ namespace spot /// automaton is already weak, it will simply be copied. /// /// For details about the algorithm used, see the following papers: - /** \verbatim - @article{kupferman.01.tocl, - author = {Orna Kupferman and Moshe Y. Vardi}, - title = {Weak alternating automata are not that weak}, - journal = {ACM Transactions on Computational Logic (TOCL)}, - month = {July}, - year = 2001, - pages = {408--429}, - volume = {2}, - number = {3}, - publisher = {ACM New York, NY, USA} - } - @article{kupferman.05.tcs, - author = {Orna Kupferman and Moshe Y. Vardi}, - title = {From complementation to certification}, - journal = {Theoretical Computer Science}, - month = {November}, - year = 2005, - pages = {83--100}, - volume = {345}, - number = {1}, - publisher = {Elsevier} - } - \endverbatim */ + /// \cite kupferman.01.tocl , + /// \cite kupferman.05.tcs . + /// /// Although at the end of the above paper there is a hint at an optimization /// that greatly reduces the number of transition in the resulting automaton, /// but in return makes the run of remove_alternation algorithm way slower.