Skip to content

Using TACoS

Jump to bottom
Till Hofmann edited this page Oct 13, 2022 · 8 revisions

TACoS has a C++ API, which can be used by library consumers, as well as a protobuf interface, mainly intended as text input format. For more details, visit the separate pages that explain the APIs:

TACoS main binary

The main binary tacos reads a plant and a specification from protobuf txt files, runs the search, and creates a controller. It can also optionally visualize the search graph and the resulting controller, and debug the search interactively.

You need to specify at least the following:

  1. the input timed automaton (the plant) as a proto file
  2. the specification of undesired behavior as a proto file
  3. the actions that are under control of the controller

For the plant and the specification, see the Protobuf documentation for details how to write the proto files. The controllable actions are directly given on the command line. Assuming the plant file is examples/railroad/plant.pbtxt and the specification is examples/railroad/spec.pbtxt, you can synthesize a controller as follows:

./build/src/app/tacos \
  -p examples/railroad/plant.pbtxt \
  -s examples/railroad/spec.pbtxt \
  -c start_open -c finish_open -c start_close -c finish_close

This will run the synthesis on the plant examples/railroad/plant.pbtxt with specification examples/railroad/spec.pbtxt and controllable actions start_open, finish_open, start_close, and finish_close.

By default, the tool synthesizes a controller, but does not save or display the resulting controller. To write the controller to a proto file, add -o controller.pbtxt to the call, e.g.,:

./build/src/app/tacos \
  -p examples/railroad/plant.pbtxt \
  -s examples/railroad/spec.pbtxt \
  -c start_open -c finish_open -c start_close -c finish_close \
  -o controller.pbtxt

You can also visualize the controller with dot:

./build/src/app/tacos \
  -p examples/railroad/plant.pbtxt \
  -s examples/railroad/spec.pbtxt \
  -c start_open -c finish_open -c start_close -c finish_close \
  --visualize-controller railroad_controller.png \
  --hide-controller-labels

This will create a rendered dot graph railroad_controller.png. You may also use pdf or dot as output format. The option --hide-controller-labels hides the node labels. This makes the controller more readable, but omits some information.

You can also visualize the search graph, which is particularly useful for debugging:

./build/src/app/tacos \
  -p examples/railroad/plant.pbtxt \
  -s examples/railroad/spec.pbtxt \
  -c start_open -c finish_open -c start_close -c finish_close \
  --visualize-search-tree railroad_search.png

Finally, you may also investigate the search tree interactively:

./build/src/app/tacos \
  -p examples/railroad/plant.pbtxt \
  -s examples/railroad/spec.pbtxt \
  -c start_open -c finish_open -c start_close -c finish_close \
  --visualize-search-tree railroad_debug.pdf \
  --debug

This will first complete the search and then allow you to selectively unfold the search tree, while updating railroad_debug.pdf on every iteration. The tool will guide you through the debugging process.

Clone this wiki locally