evaluation framework for integrator chains domain

[vraman]

Create a script that parses an LTL formula into a Buchi or Rabin automaton and checks that an input string satisfies the specification. Should interface with the trial data from tdstat.py. The script should take as input a time duration for the trial and output success or failure based on appropriately defined acceptance criterion where not obvious (e.g. for liveness properties).

[slivingston]

Note that the integrator_chains domain uses only LTL formulae that can be expressed through two basic reach-avoid templates. As such, we could use a task specification syntax that is accordingly restricted and thus avoid the need for Rabin automaton construction.

[slivingston]

@vraman What do you think about my recommendation of using a restricted syntax? It could be used for an initial implementation and be supplemented or replaced by a design involving Büchi or Rabin automata later.

[vraman]

I agree with the suggestion of using a restricted syntax for an initial implementation.