This reverts commit 3746d38c.

This reverts commit 84c88b53.

Fix MiniSAT build error

See merge request !1

If a formula E [ (a, ...) C a ] was given, it was translated into
E [ a U EZ [ (a, ...), (!a, FALSE)]], which always evaluates as false.
Now, it is instead translated into  E [ a U EZ [(a, ...), (TRUE, a) ] ].

In some files it was still refered to CTL^f, this is now changed to
ESFCTL

This reverts commits 54fabb2a,
4f3e9d1f,
684d39b5.

EZ [(p_1, q_1),..., (p_n, q_n)]
  = νY./\^n_{i=1} [EX E[ Y U (p_i /\ Y) ] \/ (q_i /\ EX Y)]

- Example: CTLFSPEC EM [ TRUE, EX TRUE, EF TRUE ] | EM [ FALSE ]
- Implementation not complete, but model checking works

Instead of the states where E [a G b] holds, the states where b holds
have been used to generate a trace.