AVERIST
Algorithmic Verifier of Stability
Home
About AVERIST
Software
Download
Run AVERIST
Input syntax
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.
n
linearexp
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.