On Wed, Sep 25, 2024 at 11:39:02AM +0200, Alexandre Duret-Lutz wrote: > Package: spin > Version: 6.5.2+dfsg-1 > Severity: normal
Hello Alexandre, > When I compile Spin manually, without changing anything to its > makefile, it supports the "X" (next) operator. For instance: > ... > However the version shipped with Debian does not: > My understanding is that this is because Src/makefile has > CFLAGS?=-O2 -DNXT -Wall -pedantic I started looking into why this operator requires a compile flag at all. I believe it goes back to this comment in the documentation: > ==== Version 3.0.6 - 16 December 1997 ==== > > - fixed an error in the processing of logical OR in the presence of > the X operator in LTL formulae -- this only affected the outcome of a > translation if Spin was compiled with -DNXT to enable the LTL > next-time operator (this is not enabled by default, because it > jeopardizes compatibility with the partial order reductions) I don't see a subsequent update in the documentation indicating that the problem was resolved, but I suspect the fix can be inferred by the fact that upstream enables it by default. (Still, it would be nice to have package tests to verify that enabling the feature doesn't introduce a regression.) Nonetheless, I am inclined to enable it with the next upload. Thank you for the bug report. tony
signature.asc
Description: PGP signature
