Hi Tony, tony mancill <tmanc...@debian.org> writes: > 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.)
Version 3.4.13 had -DNXT disabled by default. It has been enabled by default since version 3.4.14 (in 2002) without any mention in Spin's ChangeLog. There isn't really anything to fix, except proper usage of the tool. The verifiers that Spin generate use a partial-order reduction (POR) technique to reduce the state space, and this requires the specification to be stutter-invariant. That specification can be given to Spin either as an LTL formula or as a never claim. If the LTL formula does not use the next operator, it is guaranteed to be stutter-invariant. Else, when the specification uses X or when a never claim is given, Spin will simply assume the specification to be stutter-invariant, and it is the user's responsibility to compile the verifier (not Spin itself) with -DNOREDUCE to disable POR when that isn't the case. Disabling X doesn't actually remove all problems, since you can still pass a stutter-sensitive never claim, forget to use -DNOREDUCE, and get garbage result. Another reason to allow X by default is that several tools rely on Spin to translate LTL into Büchi automata, but do not use it for model checking (i.e., POR isn't used). This usage is probably less important nowadays, as there are better alternative to translate LTL into Büchi automata, but that's actually my use case.
