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

_fc-plugins/aorai.md

@@ -40,34 +40,39 @@ 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`
+- `-aorai-verbose`:
   Gives some information during computation, such as used/produced files
   and heuristics applied.
 
-- `-aorai-show-op-spec`
+- `-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`
+- `-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`
+- `-aorai-acceptance`:
   If set, considers acceptation states (Only on finite traces).
   If not, only the safety is verified.
 
-- `-aorai-output-c-file` *file*
+- `-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`
+- `-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 isonly a restriction to the terminating state of the program thathave to be an acceptation state. Hence, if the program terminates, then the liveness property is verified.
+- 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-array or C-structure are not statically evaluated (it's an optimization) but are 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