From 7039112e41e4b6f5087a05bb3a651f2ec36acbae Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Tue, 24 Sep 2019 11:34:38 +0200 Subject: [PATCH] tut12: mention X[!] * doc/org/tut12.org (Final notes): Here. --- doc/org/tut12.org | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/doc/org/tut12.org b/doc/org/tut12.org index 1a77dc74f..a4acb3248 100644 --- a/doc/org/tut12.org +++ b/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.