Contract-based Heterogeneous Analysis and Systems Exploration
After building the sources, two tools are available: Chase and EPStool.
It is the main tool of the framework. It takes as input a problem specification expressed using the CHASE Specification Language and analyzes its consistency. In the present version, a TuLiP-compatible Python specification is formulated as shown, for instance, in
demo/Terraswarm/specs (without timing specifications) and
demo/Timing/specs (with timed specifications).
chase -i input_file.txt [ -o output_file.py] [-V]
To print the help:
$> chase -h
- -i Specifies the
.txtinput file containing the specification.
- -o Specifies the python output file. Default: input file with extension
- -V Enables verbose mode.
To execute (in verbose mode) the
chase tool on a simple example, go to the main directory of Chase and type
./bin/chase -i demo/Terraswarm/specs/template_0_synthesizable.txt -o out.py -V
This tool requires a file specifying the architecture of the EPS and a file with the system requirements expressed using a set of patterns (templates). Examples of architectural specifications can be found in
./demo/EPS/architecture_specs/. Examples of system requirements can be found in
$> epstool -a Architecture_specs -b Behaviors_specs -o outfile [-p]
$> epstool -h
- -a Architecture specs file
- -b Dynamics specs file
- -o Output file
- -p Use “physical” contactors with delay
For instance, to execute
epstool on a simple example, type
./bin/epstool -a demo/EPS/architecture_specs/template_0_topology.txt -b demo/EPS/dynamic_specs/template_0_synthesizable_nc.txt -o out.py
In the current version, the execution of
epstool generates a TuLiP-compatible Python specification. Considering the previous examples, the
out.py file can be executed as follows:
$> python out.py
However, it is possible to support a set of options while executing a generic
file.py generated by
epstool, as shown below.
python file.py -g -f GRAPHIC_REPRESENTATION_FILE -i -p PYTHON_IMPLEMENTATION_FILE
To print the help:
python file.py -h
-h: Shows the help message.
-g, --graphical: Produces a graphical representation of the finite state machine of the controller if the specification is realizable. Disabled by default.
-i, --implement: Produces a Python implementation of the controller FSM. Disabled by default.
-p PYTHON_FILE: _Specifies the path of the output Python file containing the controller FSM. It is allowed only if
-i, --implementare used. The default value is
-f GRAPHIC_FILE: _Specifies the path of the output graphic file with the controller FSM. It is allowed only if
-g, --graphicalare used. The default value is
graphical.py. The supported graphic formats (specified by the file name) are:
eps, dot, jpg, and
For instance, type the following command to generate both the graphical (
eps file) and Python implementation of the discrete control strategy from
out.py, generated as shown above
$> python out.py -g -f fsm.eps -i -p fsm.py