Documentation

Documentation

Format of XML inputs

The input language supported by VeriLHys is an extension of the modeling language employed by SpaceEx (see here for details).

The input format is defined by a grammar expressed in Compact RelaxNG format; the grammar can be found here.

Usage

  • Install the wheel of VeriLHYs as described in Download page

  • Check that the package has been properly installed by running pip list.

1
2
3
4
5
6
$> pip list
Package         Version
--------------- --------
...
VeriLHyS        1.0.0
...
  • The package can be used in a standard python environment
1
2
$> python
import hybrid_ltl

  • Alternatively, the following two scripts can be used in the shell:

    1
2
    + verilhys_parse_file
+ verilhys_LTL_C_4HS

  • We report here the usage of the two scripts:

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
$> verilhys_parse_file --help
usage: verilhys_parse_file [-h] [--verbose] --xml-file XML_FILE [--sx-grammar-version {1,2,3,4}] 
       [--additional-regions-file ADDITIONAL_REGIONS_FILE]

options:
  -h, --help            show this help message and exit
  --verbose, -v         Enable verbose output
  --xml-file XML_FILE   Path to xml file (SX format)
  --sx-grammar-version {1,2,3,4}
                        Version of the SX grammar (default: 3)
  --additional-regions-file ADDITIONAL_REGIONS_FILE
                        Path to the xml file containing additional regions

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
$> verilhys_LTL_C_4HS --help
usage: verilhys_LTL_C_4HS [-h] [--verbose] [--options-file OPTIONS_FILE] [--time_step TIME_STEP]
       [--final_time_simulations FINAL_TIME_SIMULATIONS] [--folder_output FOLDER_OUTPUT]
       [--additional-regions-fname ADDITIONAL_REGIONS_FNAME] xml_file

Run LTLConstraints4HS from XML file

positional arguments:
  xml_file              Path to the XML file defining the hybrid system

options:
  -h, --help            show this help message and exit
  --verbose, -v         Enable verbose output
  --options-file OPTIONS_FILE
                        Path to the JSON file with options for the run
  --time_step TIME_STEP
                        Time-step to be used in CORA reachability analysis
  --final_time_simulations FINAL_TIME_SIMULATIONS
                        Time to be used in CORA reachability analysis as final time for simulations
  --folder_output FOLDER_OUTPUT
                        Relative path in the folder results where the output will be saved
  --additional-regions-fname ADDITIONAL_REGIONS_FNAME
                        Path to the additional regions file