rm parser using pyparsing

because it is not supported any more and lex yacc is a standard tool that can parse strictly more languages, and more efficiently.
pep8, mostly rm trailing whitespace
mv simple property gr1 converters from spec.form to spec.gr1_fragment

because that module contains utilities for converting non-gr1 formulae to the gr1 fragment. Otherwise spec.form is bloated w/o good reason.

The relevant tests were also moved to their own script file.
rm method: GRSpec.sym_to_prop

because it is superseded by the syntactic manipulation utilities that are safer to use.
It replaces symbols using a lexical search with regular expressions, which does not distinguish between string literals and variable names. Working on the AST is safer.

Another motivation is to reduce confusion as to which method the user should pick (because the AST manipulation methods cover this functionality, for example GRSpec.sub_values).
rm function: spec.form.mutex, use synth.mutex or synth.exactly_one instead

because they allow finer control over the intended constraint.
The module spec.form contains mainly classes for representing GR(1) specifications in a structured way.
rm method: GRSpec.to_smv because it is long now defunct

and so if ever reimplemented, it will need to be rewritten from scratch. Also, it will reside elsewhere.
mv spec.form tests from spec_test to form_test

because the spec subpackage is larger and tests are easier to deal with if organized per module. Note that the test for the method GRSpec.sym_to_prop has been retained commented, so that it can be updated to test GRSpec.sub_values and other relevant methods or functions.
assert is a statement, not a function

so rm parentheses, because they are redundant and visually distracting.
rm pyparser from spec.parser
rm LTLException

because it is not used in an essential way.
mv language translation backends to the new module: `spec.translation`

to reduce the complexity of GRSpec and make it independent of specific tools. Tulip parsers LTL, it stores GR(1) specs in `GRSpec`, uses syntactic manipulation on a common AST (to be updated in one of the following commits), and when a translation is need, this AST is mapped to another ("isomorphic") AST that has different `flatten` methods, suited for the target language.

This also liberates from the Babylonian tendency of having differently named flatteners for each language (`to_gr1c`, `to_jtlv`, …). They make the data structures more difficult to deal with, violating the recommendation by Alan Perlis to have a large number of functions that operate on a few, fundamental data structures.

Each language's AST nodes have a different operator map attribute that they inherit from their parent abstract base class `Node`. So to produce subclasses that inherit from the updated parent `Node`, a node factory function will be defined in `spec.ast` and is used in `spec.translation` to create a node factory for each language.

The refactored `spec` package has a clear separation between the parser and AST manipulation frontend, and the flattening (translation) backends for the various languages. This makes it easier to add new formats w/o the danger to affect existing ones, as well as import from tulip in some other package and reuse the base AST node classes and factories to create new ones.

Also note that `spec.translation` is using some syntactic AST manipulation utilities from the `spec.transformation` module (to be created).
extract syntactic AST manipulation functions and Tree class to new module `spec.transformation`

because they are separate utilities that operate on AST graphs and need no be mixed with the modules that define AST node classes, nor GR(1) specifications. They are independent, general-purpose utilities.

The class `spec.ast.LTL_AST` has been renamed to `spec.transformation.Tree`, and significantly restructured (for example it does not need to worry about translations any more).

Note that the methods `LTL_AST.sub_values` and `LTL_AST.sub_constants` have been moved to functions of the same name in `spec.transformation`.

The `Tree` class has methods `from_recursive_ast` and `to_recursive_ast` for conversions from and to recursively defined AST (see below).

Rationale
=========
Note that as of 89920b64bb9ddc5d6946c7bd79f053e875cfabf3 the AST node classes formed a recursively defined tree, not a graph data structure as those in `networkx`, i.e., one that contains easily-accessible information for traversing it in either direction w/o too much extra code.

Those were converted to the current ones, that are only used as nodes in a `networkx` graph (user defined classes are hashable with their `id` as their `__hash__`). The reason was to make syntactic manipulations easier (since they occur several times throughout processing of formulae). Having AST nodes that recursively define a tree (with attributes like `operand`, `left`, and `right`) and use those as nodes of a `networkx` graph was deemed confusing and error-prone. However, `networkx` graphs are slightly less efficient when it comes to flattening, and some operations are still easier with the recursive definition, especially defining new transformations.

So for the benefit of simplicity, uniformity and to encourage resuse of the AST node factories, the AST node classes will be converted back to a recursive definition. The syntactic manipulations are significantly cleaner by using a `networkx` graph for traversing and modifying the tree.

For this reason, before syntactic manipulation, a `networkx` graph is constructed over a recursively defined AST, to be used as a "scaffold" for changes. During those changes, the underlying recursively defined AST is not touched (i.e., attributes like `operand`, `left`, `right` of the nodes belonging to the input tree are read-only). When the transformations are complete, the `networkx` scaffold is used to produce a new recursively defined AST, i.e., fresh node objects are created, and connected based on the transformed `networkx` graph (i.e., their attributes like `operand`, `left`, and `right` are set based on the edges of the final `networkx` graph).

This makes manipulation clean, and separate from everything else.
If one prefers to write a function that operates directly on the recursive AST, perhaps because that particular operation does not need to traverse the tree in both directions, then they can simply not use the module `spec.transformation`.
rm _eval methods from AST nodes

because they are not used anywhere, since flattening to python and compiling to `code` objects is faster.
the `operator` attribute need not be a property

because these substitutions will be performed by the lexer, as will be explained in the next commit message. Besides that, we're all consenting adults here (BDFL).
rm node subclasses that do not provide additional methods

and are not otherwise essential for general use. Check the attribute `Operator.operator` instead if you need to distinguish between different operators.
rewrite the core AST node classes to simplify and uniformize

and make subclassing easier. Also, they are now produced by a factory function, to allow changes of the abstract base class `Node` to be inherited by its subclasses.

Encoding operators by a single character stored in `Operator.operator` is much more succinct and easier to check, than creating a different class for each one. The latter increases inhomogeneity of AST classes, making reading them, reusing them, writing functions that manipulate them, and subclassing convoluted, tedious, and error-prone. Alan Perlis applies again: simpler classes can be manipulated by more functions with less difficulty.

Lexical substitution of operators must be performed by the lexer --- *not* by the AST classes. So token rules like eventually, that recognizes both `<>` and `F`, must be implemented with token methods in the lexer, that for example recognizes both `<>` and `F`, but returns only `F`. The lexer is the appropriate tool designed for this job.

Note that using methods instead of plain regular expressions for some token rules affects the precedence, and so they need to be re-ordered, because `ply` maintains the order of token rule functions the same as they appear in the lexer source code. For example "EVENTUALLY" would shadow "False" (stealing the `F` from it).
Add some unit tests to guard against such cases in the future.

The operator map is useful for translations and a node factory is used, so that other languages can change the operator map for the `Node` abstract base class and have that change inherited also by the other nodes.

The operator `==` is removed from the lexer, because it can only cause sorrow.

The _eval methods are not used anywhere, because flattening to python and compiling to `code` objects is faster. So they are removed.

The maps[lang][self.op] are not replaced by a change of `opmap` that happens in `spec.translation` by writing new node class factories.
shift code
update yacc to use new AST nodes
mv some `spec.form` functions to methods of `GRSpec`

and update them to use the relocated and refactored AST transformation utilities. Note that function `_finite_domain2ints` has been renamed to `GRSpec.str_to_int`, because that communicates more readily its purpose.
update functions and methods in `form` to use `spec.transformation`