tut12: mention X[!]

* doc/org/tut12.org (Final notes): Here.

doc/org/tut12.org

@@ -226,7 +226,7 @@ State: 3 {0}
 --END--
 #+end_example
 
-* Final note
+* Final notes
 
 Spots only deal with infinite behaviors, so if you plan to use Spot to
 perform some LTLf model checking, you should stop at step 3.  Keep the
@@ -238,3 +238,13 @@ Alternatively, if your Kripke structure is already equiped with some
 you could replace =alive= by =!dead= by using ~ltlfilt
 --from-ltl="!dead"~ (from the command-line), a running
 =from_ltlf(f, "!dead")= in Python or C++.
+
+When working with LTLf, there are two different semantics for the next
+operator:
+- The weak next: =X a= is true if =a= hold in the next step or if
+  there are no next step.  In particular, =X(0)= is true iff there are
+  no successor.  (By the way, you cannot write =X0= because that as an
+  atomic proposition: use =X(0)= or =X 0=.)
+- The strong next: =X[!] a= is true if =a= hold in the next step *and*
+  there must be a next step.  In particular =X[!]1= asserts that
+  there is a successor.