This attachment contains a development version of Isabelle together with
compatible theories for the Reachability Analysis tool described at ARCH 2015:
"Isabelle/HOL for Reachability Analysis of Continuous Systems" (Fabian Immler).

The current setup is quite involved, if you experience difficulties in running
any of the systems, please contact me <immler@in.tum.de> and I will try my best
to assist you in experimenting with the tool.

The easiest (still quite involved) way to experiment with the tool is the
following:

1.) build Isabelle:
  a) download required components:
    $ isabelle-8535cfcfa493/bin/isabelle components -a
  b) build the logic images and open the example theory file in Isabelle/jEdit:
    $ isabelle-8535cfcfa493/bin/isabelle jedit -d \
        afp/thys/Ordinary_Differential_Equations -l \
        HOL-Multivariate_Analysis-Collections \
        afp/thys/Ordinary_Differential_Equations/Ex/Example_van_der_Pol.thy
  d) run the example in Isabelle/jEdit:
    - The previous command should have opened Isabelle's IDE, Isabelle/jEdit and
      display the content of the file 'Example_van_der_Pol.thy' (with light red
      background color, meaning that the dependencies are still loading)

    - it will take some time until all the dependencies are loaded (the
      background turns from light red to white/light gray)

    - open the "Raw output" panel (this will display the output of the
    reachability analysis): in the menu-bar, choose
      "Plugins -> Isabelle -> Raw Output panel"

    - scroll down to the line with "value [code] vanderpol_limit'"

    - the system will start evaluating that line as soon at is visible.
      (Evaluation is indicated by purple color)

    - Some tracing output should start appearing in the "Raw output" panel

    - You can copy this output to some file, say trace.log

    - The output (with interval enclosures) can be visualized with
      $ ./plot_ivls.py 2 0 1 trace.log

    - The output (with zonotopes) can be visualized with
      $ ./plot_aforms_2d.py i 0 1 < trace.log | gnuplot

    - The output (with zonotopes at discretization points) can be visualized with
      $ ./plot_aforms_2d.py d 0 1 < trace.log | gnuplot

From within Isabelle/jEdit, you can also open other examples, like
afp/thys/Ex/Lorenz/Lorenz_Approxmation.thy, where you can also run the tool
(e.g. by uncommenting (removing "(*" and "*)") the line
"(* value [code] "lorenz_irects 8 8 373 588 *)"
then you can plot a projection by
  $ ./plot_ivls.py 3 0 2 trace.log
or
  $ ./plot_aforms_2d.py i 0 2 trace.log

In general, "./plot_ivls.py d x y filename" expects output of d-dimensional sets
in the file given by filename and projects to the coordinates given by x and y.

In general, "./plot_aforms_2d.py b x y" reads zonotopes from stdin and plots the
sets at discretization points (if b=d), in between (if b=i), or all (if b=a),
projecting the zonotopes to the coordinates given by x and y.
