tulip-control/tulip-control — pull request #108 by johnyf (2014-09-29 04:14:20+00:00)
Title: Strategy

Add:
- syntactic manipulations on the AST
- subtree substitutions
- string literals with integers
- `spec.form.check_for_undefined_identifiers`
- `Const`, `Operator` AST node
- `LTL_AST` class
- flattening of Boolean formulas to `python` code
- `synth.determinize_machine_init` to handle interpretation of `ALL_INIT` for simulation, i.e., when the initial state is known. It is needed to avoid passing non-deterministic transducers to simulation functions.
- function `strip_ports` to remove auxiliary vars, like dependent Boolean vars
- update `tulip` LTL syntax in `doc`
- `ltl2ba` interface
- `graphviz` to `install.sh`
- `json` configuration file for `logging` of `tulip` (e.g., hides the parser debug output - quite verbose)

Changes:
- double quotes must enclose string literals
- double quotes: backward compatibility function `spec.form.infer_constants` added to do this when called. Checks for ambiguity and raises `Exception` if any found.
- rewrite AST classes
- AST is now a `networkx.DiGraph` for easy traversal
- that forced AST nodes to be hashable themselves, and thus cannot have field referring to the AST graph they belong to. So the recursive visitor had to become external (instead of integrated in the AST node classes). Now it is collected at a single place, a few lines. (Experimented with iterative instead of recursive visitor, but that is not as fast or readable).
- replace custom `dot` dump with `pydot`
- optionally plot `type` of `AST` nodes, preserve left-to-right tree ordering
- cache parsed AST and flattened formulas in `GRSpec`, with garbage collection
- optimize flatteners based on timing measurements with `cProfile` and `line_profiler`
- make the LTL lexer and parser classes, to allow for instantiation and avoid global vars. Don't recreate a parser for each parse
- make syntax maps for each tool more complete
- mv conversion of loaded strategies to transducers to `synth`. So interfaces share it, instead of duplicating it
- rewrite the substitution of string literals with integer values for string variables inside specifications
- rewrite eval of initial conditions to find initial states, using `python` and `eval` to create `code` objects (=compiled `python` code) for the Boolean formula of initial conditions
- state variables for machines deprecated for now, because that implies transducers that unfold, hence are in a sense symbolic. Transducers produced by synthesis are explicit until now, so wait until such a feature is needed.
- allow integers vars with singleton or 2-element domains for `gr1c`
- allow integer graph states for transition systems passed to `synth`
- merge, simplify and rewrite several functions in `synth`
- `print` moves during random transducer simulation
- rm `show` argument from `PPP.plot`
- rm `transys.executions`
- check `pydot` version at runtime
- raise `Exception` if `jtlv` returns strategy with `#?#` as value of a variable.

Experimental:
- marking automata as having symbolic edge guards (i.e., Boolean formulas as strings)