tulip-control/tulip-control — pull request #95 by johnyf (2014-08-01 21:06:02+00:00)
Title: Convert gr1

Work in progress, but already contains useful features, so better to merge now and not when every planned feature has been implemented.

New features:

- export graphs in `dot` format with `tikz` annotations suitable for conversion using [`dot2tex`](https://github.com/kjellmf/dot2tex) and inclusion in `latex` with package [`dot2texi`](https://github.com/kjellmf/dot2texisty).
- add sound and complete function to generate `GR(1)` subformulae corresponding to:
- eventually `<>p`
- response `[](p -> <>q)`
- until `p U q`
- add sound but incomplete function to generate `GR(1)` subformulae corresponding to:
- stability `<>[]p`
- add syntax check for recognizing a fragment of LTL that is convertible to GR(1).
- add conversion functions `moore2mealy` (exact) and `mealy2moore` (exact is impossible)
- implement guided `MealyMachine` simulation, remove random simulation (a better replacement is a separate function that would read a `MealyMachine`, get the input definitions and generate a random input sequence: this will lead to cleaner code design).
- add support to define default values of typed labelings of `LabeledDiGraph`
- add methods `TypedDict.is_consistent` and `LabeledDiGraph.is_consistent` to check consistency of labeling after restricting the codomain of admissible label values. (e.g., removing some atomic proposition)
- add `GameGraph` class - under dev

Changes:

- use `dict` instead of `list` for defining typed labeling of a `LabeledDiGraph`
- rm alias `Mealy`, because it's not significantly shorter than `MealyMachine`
- rename `FTS.project` -> `FTS.projection` for consistency with naming convention of built-in `set`
- use new default labeling mechanism to initialize a valid labeling of a transition system by empty sets (of atomic propositions). Note that in a sense there is no absolute "default" for initializing sets, but at least an empty set is the minimal element in the partial order induced by the subset relation.
- improve print formatting for transition systems
- stop using `OrderedDict` for machine port definitions
- `LabeledDiGraph.states.post` with no argument returns the set of initial states
- import `matplotlib` and `IPython` only where needed inside `transys`, in order to significantly reduce its import time when no exports, or saving to `dot` are used.