Proposition YAML File - VerifiableRobotics/LTL_stack GitHub Wiki

Proposition YAML file defines files that correspond to each proposition. Here is an example of a proposition YAML file.

In this example, we have one input (environment proposition) person and one output (system proposition) move. person and move are proposition names in the LTL slugs file.

The description of other fields in the file is as follows.

REQUIRED for controller execution

  • node: name of the proposition node. It does not have to be the same as the proposition.
  • node_publish_topic: topic name that this node is publishing to in connection with the provably-correct controller. It follows the format (/example_name/inputs/proposition name in slugs). (For an environment (input) proposition)
  • node_subscribe_topic: topic name that this node is subscribing to from the provably-correct controller determine an actuation status. It follows the format (/example_name/outputs/proposition name in slugs). (For a system/robot (output) proposition)

REQUIRED for automatic generation of proposition launch file

  • pkg: package name that the ROS program sits in
  • filename: file name of the ROS program
  • parameters(optional): if the ROS program is taking in parameters, you can specify them here.

Note that following this convention allows you to easily generate a launch file for all proposition nodes but it is not necessary.

Generating Proposition YAML File

Option 1: Write this file manually

Option 2: Use an rqt gui to create the file

  1. Start all the ROS nodes to connect with the controller (finite-state-machine) synthesized from LTL. Each node should have a topic of type Bool for communication with the controller.
  2. Run rqt --standalone rqt_grounding_and_analysis. You should see the GUI below without the entries of propositions.

  1. To display the entires, load a .slugsin file (A).
  2. Now you should see all the propositions in the .slugsin file in the GUI. From the dropdown box (C), you can choose a node from those you have started that corresponds to a proposition.
  3. Afterwards, you also need to specify the topic in the node to communicate with the controller (D). For inputs, this topic publishes boolean values to the controller. For outputs, the topic subscribes information from the controller.
  4. Continue this process for all the propositions and save the file at the end (E).