chase

Contract-based Heterogeneous Analysis and Systems Exploration


Project maintained by chase-cps Hosted on GitHub Pages — Theme by mattgraham

<– Go back to the main page

Tools

After building the sources, two tools are available: Chase and EPStool.

Chase

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).

Usage

chase -i input_file.txt [ -o output_file.py] [-V]

To print the help:

$> chase -h

Parameters:

  • -i Specifies the .txt input file containing the specification.
  • -o Specifies the python output file. Default: input file with extension .py rather than .txt.
  • -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

EPSTool

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 ./demo/EPS/dynamic_specs/.

Usage:

$> epstool -a Architecture_specs -b Behaviors_specs -o outfile [-p]

$> epstool -h

Parameters:

  • -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

Backend

In the current version, the execution of chase and 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 chase or epstool, as shown below.

Usage:

python file.py -g -f GRAPHIC_REPRESENTATION_FILE -i -p PYTHON_IMPLEMENTATION_FILE

To print the help:

python file.py -h

Parameters:

  • -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, --implement are used. The default value is automaton.py.
  • -f GRAPHIC_FILE: _Specifies the path of the output graphic file with the controller FSM. It is allowed only if -g, --graphical are used. The default value is graphical.py. The supported graphic formats (specified by the file name) are: eps, dot, jpg, and png.

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

<– Go back to the main page