Algorithmic Verifier of Stability
with the name you want for your
construct a folder called
Inside input folder store the input file with the automaton definition of the hybrid system, called
The structure of input.dat is described at
Inside input folder it is optional to store a file with linear expressions to use for partitioning the continuous state space, called
the next variables need to be set:
of the experiment.
in case you constructed a linearexp.dat file or not.
le: given linear expressions file.
nle: no given linear expressions file.
for extracting or not the linear expressions from the input automaton.
exle: extract linear expressions.
nexle: not extract linear expressions.
for creating uniform linear expressions.
is a folder into the experiment folder.
Into the output folder the file
contains the automaton in the input.dat as a graph.
is a folder with
as the number of linear expressions used in the partition and is into the experiment folder. Inside this folder there are:
, a file with all the linear expressions used in the state space partition.
, a file which contains the final answer, 'stable', 'unstable' or 'do not know'. 'do not know' answer implies the existence of a counterexample.
, a file containing the counterexample.
, a file with a time table.
, a file with the data of the abstract weighted graph.
, a file with a picture of the abstract weighted graph.