3

I'm trying to use NuSMV as a satisfiability checker for LTL formulae, i.e. I want to know if there exist a model for a given formula. I know that NuSMV can be used for this purpose as well, both because it is theoretically possible and because I see it cited in a lot of papers that deal with satisfiability (one of them claims also that NuSMV is one of the fastest satisfiability checkers out there).

I see that with NuSMV comes a tool called ltl2smv that apparently translates an LTL formula into an SMV module, but then I don't know how to use the output. Giving it directly to NuSMV gives back an error message about "main" being undefined, so I suppose I have to define a main module and use the other in some way. Since I've never used NuSMV as a model checker I have no idea how its language works and the User Guide is overwhelming given that I only need this specific use case, which, by the way, is not mentioned anywhere in said guide.

So how can I use NuSMV to check the satisfiability of an LTL formula? Is there a place where this use case is documented?

Niklas Rosencrantz
  • 25,640
  • 75
  • 229
  • 424
gigabytes
  • 3,104
  • 19
  • 35

2 Answers2

4

Have a look at the chapter about LTL model checking in NuSMV's user manual. It comes with an example how LTL specifications can be expressed in a module and checked:

MODULE main
  VAR
    ...
  ASSIGN
    ...
  LTLSPEC <LTL specification 1>
  LTLSPEC <LTL specification 2>
...

NuSMV checks if the specifications hold for all possible paths. To check if there exists a model (i.e. path) for your formula, you can enter the negation and the model checker will give you a counter-example for it if it exists. The counter-example would then be an example for your original formula.

danielp
  • 1,179
  • 11
  • 26
  • Ok, so the LTL formula is put into the LTLSPEC directive. The ltl2smv tool is not related to this? What's its purpose? – gigabytes Jan 21 '16 at 22:44
  • @gigabytes: It seems that it is for NuSMV's internal use, see [this page](http://nusmv.fbk.eu/NuSMV/progman/v25/html/ltlExt.html). – danielp Jan 21 '16 at 23:51
  • I see.... Can you kindly provide a minimal working example in the answer, please? – gigabytes Jan 22 '16 at 08:26
  • I have currently no working NuSMV installed. But the manual's example would find a model for `!G (proc1.state = entering -> F proc1.state = critical)`. – danielp Jan 22 '16 at 15:00
  • Yes, in the meantime I've managed to make it work from your answer and the linked manual section. Thank you :) – gigabytes Jan 22 '16 at 15:55
0

One way is to use PolSAT. This takes as input an LTL formula, and feeds it to a number of different LTL solvers. This is usually faster than just using NuSMV alone. If you replace the NuSMV binary with /bin/false and run ./polsat 'Gp & F X ~ p' it will abort and leave behind a file ../NuSMV/tmpin.smv containing something like:

MODULE main
VAR
Gp:boolean;
p:boolean;
LTLSPEC
!(((Gp)&(F (X (!(p))))))

(Note that PolSAT interpreted Gp as a single variable). You can then run NuSMV directly with the command ../NuSMV/nusmv/NuSMV < ../NuSMV/tmpin.smv.

If you want to install PolSAT, it can presently be downloaded from https://lab301.cn/home/pages/lijianwen/. v0.1 has a bit of difficulty on modern machines, you may need to downgrade bison to version 2.7 (See e.g. https://askubuntu.com/questions/444982/install-bison-2-7-in-ubuntu-14-04).

gmatht
  • 835
  • 6
  • 14