[plugins] Convert to Markdown, normalize section names and URLs

_fc-plugins/aorai.md

+---
+layout: plugin
+title: Aoraï
+description: Verify specifications expressed as LTL (Linear Temporal Logic) formulas.
+key: specifications
+distrib_mode: main
+manual_pdf: /download/frama-c-aorai-manual.pdf
+---
+
+## Overview
+
+The **Aoraï** plug-in provides a method to automatically annotate a C program
+according to an LTL formula *F* such that, if the annotations are verified,
+then we ensure that the program respects *F*.
+The classical method to validate annotations is to use the [Wp](wp.html) or
+[Eva](eva.html) plug-ins.
+
+## Installation Dependencies
+
+Aoraï is available in the main Frama-C distribution. It used to be
+available from http://amazones.gforge.inria.fr/aorai, but the version
+currently hosted there is obsolete and won't compile with newer versions of
+Frama-C.
+
+If you want to use LTL syntax for properties, you have to install the
+[ltl2ba](http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php) tool in your
+path. This tool is distributed by its author, Paul Gastin (ENS Cachan),
+under the GPL licence and converts an LTL formula into a Büchi automaton.
+
+## Usage
+
+The plug-in is activated with one of the following command lines:
+
+    frama-c file.c -aorai-ltl file.ltl
+
+    frama-c file.c -aorai-automata file.ya
+
+These two commands differ only by the syntax used to express the
+property to be verified: *.ltl* files are described in an ltl-like syntax,
+while *.ya* are description of automata in an yacc-like syntax.
+Options are:
+
+- `-aorai-verbose`:
+  Gives some information during computation, such as used/produced files
+  and heuristics applied.
+
+- `-aorai-show-op-spec`:
+  Displays, at the end of the process, the computed specification
+  of each operation, in terms of Büchi states and transitions.
+
+- `-aorai-dot`:
+  Generates a dot file of the Büchi automaton. Dot is a graph
+  format used by the [GraphViz](http://www.graphviz.org) tool.
+
+- `-aorai-acceptance`:
+  If set, considers acceptation states (Only on finite traces).
+  If not, only the safety is verified.
+
+- `-aorai-output-c-file`: *file*
+  Outputs the annotated program in *file* (the default is to
+  derive a name from the one of the first input file).
+
+- `-aorai-help`:
+  Gives the whole list of options.
+
+## Installation Dependencies
+
+- Only the safety part of properties is checked. The liveness part is not truly
+  considered. Currently, a liveness property is only a restriction that the
+  terminating state of the program has to be an accepting state.
+  Hence, if the program terminates, then the liveness property is verified.
+- Currently, function pointers are not supported.
+- In the init state from the automaton, conditions on C arrays and C structures
+  are not statically evaluated (which would be an optimization)
+  but are supported.
+
+## Contact
+
+Aoraï has been originally written by
+[Nicolas Stouls]( mailto:nicolas.stouls@insa-lyon.fr?subject=[Plug-in Aorai]),
+[CITI Labs](http://www.citi-lab.fr), [AMAZONES team](http://amazones.gforge.inria.fr).
+It is currently maintained by CEA LIST as part of the main Frama-C distribution.
+See our [contact](contact.html) page for more information.
+
+**End Note:** to the question "*Why this name: Aoraï?*" my answer is: why not?
+Aoraï is the name of the tallest reachable mount in the Tahiti island and its
+reachability is not always obvious.
+
+## Further Reading
+
+- [Short Documentation]({{page.manual_pdf}})
+- [A few simple examples](/download/frama-c-aorai-example.tgz)
+
+Other resources can be found at
+[the official web page of Aoraï](http://amazones.gforge.inria.fr/aorai/).