replace == with <-> in examples

to conform with tulip temporal logic syntax
and to work with gr1c
ignore absence of ts initial states in examples
new func: add_initial_states to use after discretize

The function abstract.discretization.discretize keeps track of atomic propositions (APs) during discretization.
The resulting transition system (TS) is labeled with these APs.
If continuous initial conditions are specified using polytopes labeled as atomic propositions, then the initial states of this TS can be marked, as the preimage of AP labels.

This requires that the AP used for each initial polytope be true only there.
This restriction can be avoided by using additional propositions and polytopes dedicated to defining initial conditions (i.e.: duplicate polytopes if so needed)

An alternative is implementing separate tracking of initial conditions during discretization.
replace (a -> b) with (!a || b)

to defer implementing replacement of (a -> b) by ((not a) or b) when evaluating a formula using eval in tulip.spec.form._eval_formula