Structure of BT library

The BT library is currently structured as follows:

• the file bt.v defines three modules:

  • BT_SIG collects all the parameters (as of now it contains only the set of skills, other stuff may be added later)
  • BT_binary is a parametric module over BT_SIG which contains a possible implementation of the BT data type (with binary nodes only);
  • BT_general is another parametric module over BT_SIG which contains another possible implementation of the same data type (trees with arbitrary branching).

• in the example files you can find how to concretely instantiate such modules:

  • load the library with the command Require Import bt
  • specify a concrete set of skills, as in the ex_skills module
  • define a module my_bt as the instantiation of (e.g.) BT_binary over the "concrete" module ex_skills
  • at this point you can define concrete examples of BTs (over the specified set of skills); it is convenient to add a directive Import my_bt in order to avoid using annoying qualified names (e.g. my_bt.Skill instead of Skill, etc.)