IntroductionSpecificationFormatData FilesExtensions |
FormatEach instance is defined by two files: one for describing the atoms, actions, events and the initial system state, and other for describing the LTL formula that must hold in the goal state. The instance file has the following format.<number of atoms> atom1 atom2 ... atomN <number of atoms that are true in the initial state> atom_initialstate1 atom_initialstate2 ... atom_initialstateK <number of actions + number of events> <action/event name 1> <type - "A" for action, "E" for event> <number of preconditions> <number of negative effects> atom1 atom2 ... atomL <number of positive effects> atom1 atom2 ... atomJ <number of negative effects> atom1 atom2 ... atomV ... <action/event name M> <type - "A" for action, "E" for event> <number of preconditions> <number of negative effects> atom1 atom2 ... atomL <number of positive effects> atom1 atom2 ... atomJ <number of negative effects> atom1 atom2 ... atomV As for the formula file, the LTL condition is written in a natural form. Example: G(!breakM1) & G(!breakM2) & G(!breakM3) & F(generateP1P2) Back to the beginning. |