spot/doc/mainpage.dox
Alexandre Duret-Lutz 750d352fb6 Fix many dead links.
Also change http:// to https:// for url that would automatically
redirect to the later.

* doc/mainpage.dox, doc/org/dstar2tgba.org, doc/org/ltl2tgba.org,
doc/org/ltlcross.org, doc/org/satmin.org, doc/org/tools.org,
src/ltlvisit/dot.hh, src/misc/hashfunc.hh, wrap/python/ajax/trans.html:
Here.
2015-07-17 17:55:15 +02:00

32 lines
1.4 KiB
Text

/// \mainpage Spot Library Documentation
///
/// \section overview The Spot Library
///
/// Spot is a model-checking library. It provides algorithms and data
/// structures to manipulate omega-automata, and implement the
/// automata-theoretic approach to model-checking.
///
/// See <a href="https://spot.lrde.epita.fr/">spot.lrde.epita.fr</a>
/// for more information about this project.
///
/// \section thisdoc This Document
///
/// This document describes all the public data structures and functions
/// of Spot. This aims to be a reference manual, not a tutorial.
///
/// If you are new to this manual, start with <a href="modules.html">the
/// module page</a>. This is what looks the closest to a table of contents.
///
/// \section pointers Handy starting points
///
/// \li spot::ltl::formula Base class for an LTL or PSL formula.
/// \li spot::ltl::parse_infix_psl Parsing a text string into a
/// spot::ltl::formula.
/// \li spot::twa Base class for Transition-based
/// ω-Automata.
/// \li spot::translator Convert a spot::ltl::formula into a
/// spot::tgba.
/// \li spot::kripke Base class for Kripke structures.
/// \li spot::twa_product On-the-fly product of two spot::twa.
/// \li spot::emptiness_check Base class for all emptiness-check algorithms
/// (see also module \ref emptiness_check)