HyLaGI

Overview

  • HyLaGI is an implementation of HydLa.
  • HyLaGI features
    • error-free simulation
    • symbolic execution
    • automatic case analysis

How to use HyLaGI

  1. HyLaGI requires Mathematica (the latest version is recommended, at least above Mathematica 9.0)
    • HyLaGI can be used if Mathematica can be located.
    • That is, if Mathematica is invoked by the "math" command, HyLaGI will work.
      • If a command name other than "math" is used, change the command name after the linkname in the "--mathlink" option.
  2. Please download HyLaGI from Download Page.
  3. Extract the downloaded archive to any place where you want to locate HyLaGI and change your current directory to it.
  4. Execute a HydLa program by typing the following command:

    ./hylagi <program_path> [<options>]

    • For example, you can simulate examples/bouncing_particle.hydla (included by the HyLaGI archive) like below:

      ./hylagi examples/bouncing_particle.hydla -t 10 -p 20 --nd

    • "-t" stands for the time limit.
    • "-p" stands for the number of phases to simulate.
    • "--nd" stands for the nondeterministic mode.

      If you want to simulate only one case, you can remove this option.

      (In fact, the option has no effect for this example program)

  • If you want to know more options of HyLaGI, please type

    ./hylagi -h

ASSERT statement

  • HyLaGI features bounded model checking of HydLa programs.
  • We can specify the condition to be checked by adding a line of an $\texttt{ASSERT}$ statement to a HydLa program.
    • An $\texttt{ASSERT}$ statement should be in the following form.

      $\texttt{ASSERT}(condition).$

    • The $condition$ part allows a constraint that is available as a guard, like $x = y$.
Last-modified: 2017-03-23 (Thu) 05:52:17 (147d)