AVERIST Algorithmic Verifier of Stability

Instructions

Install sage: www.sagemath.org

---

• Construct a folder with the name you want for your experiment.
• Inside such folder construct a folder called input.
• Inside input folder store the input file with the automaton definition of the hybrid system, called input.dat.
• The structure of input.dat is described at input syntax.
• Inside input folder it is optional to store a file with linear expressions to use for partitioning the continuous state space, called linearexp.dat.

---

To run AVERIST: ./sage sage: cd averist/ sage: attach ('Main.py')

---

When running AVERIST the next variables need to be set:

• Name folder of the experiment.
• le/nle in case you constructed a linearexp.dat file or not.
• le: given linear expressions file.
• nle: no given linear expressions file.
• exle/nexle for extracting or not the linear expressions from the input automaton.
• exle: extract linear expressions.
• nexle: not extract linear expressions.
• Indicate the maximum number of iterations for creating uniform linear expressions.

---

The output:

• output is a folder into the experiment folder.
• Into the output folder the file graph_automaton.dat contains the automaton in the input.dat as a graph.
• nlinearexp is a folder with n as the number of linear expressions used in the partition and is into the experiment folder. Inside this folder there are:
• linear_expressions.dat, a file with all the linear expressions used in the state space partition.
• stable.dat, a file which contains the final answer, 'stable', 'unstable' or 'do not know'. 'do not know' answer implies the existence of a counterexample.
• counterexample.dat, a file containing the counterexample.
• time.dat, a file with a time table.
• weighted_graph.dat, a file with the data of the abstract weighted graph.
• weighted_graph.png, a file with a picture of the abstract weighted graph.