Stack Overflow
Stack Overflow

Questions tagged [nusmv]

NuSMV is a model checking software free for non-commercial and academic purposes. It is used to verify and prove hardware and software.

NuSMV is a model checking software free for non-commercial and academic purposes. It is used to verify and prove hardware and software.

93 questions
6
votes
1 answer

building NuSMV 2.6 from source, make utility on ubuntu

I am trying to build NuSMV on Ubuntu 17.04,using cmake utility. Used cmake tool to create make file, but when I try to use make utility it gives the error Error 1 CMakeFiles/Makefile2:824: recipe for target…
Sharjeel Ahmed
  • 439
  • 1
  • 3
  • 11
4
votes
0 answers

Generate different possible counterexamples in NuSMV

I wish to know if there is a way to generate different possible counterexamples for a given LTL formula in NuSMV. If we need to generate counterexample for an LTL formula, it generates one for us. But the one generated by NuSMV may not be the most…
user_1_1_1
  • 903
  • 1
  • 12
  • 27
3
votes
2 answers

How to check LTL satisfiability using NuSMV?

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…
gigabytes
  • 3,104
  • 19
  • 35
3
votes
0 answers

Internal representation of Enumeration Types in NuSMV/NuXMV

why is there a significant performance dropdown when representing a 16-bit signed integer variable as an intervall (-32768..32767) in comparison to fixed length bit arrays? Inspecting the pre-processed NuSMV/NuXMV model one can observe that the…
optional
  • 2,504
  • 4
  • 18
  • 30
2
votes
1 answer

Can Kripke structures have guards?

I have a simple kripke structure, where I have 3 states, with the following transitions: s1 --> s2 s2 --> s1 s1 --> s3 s3 --> s3 s1 is the only initial state. I do not want the loop s1 to s2 be repeated more than a certain amount (say twice). In…
User 19826
  • 509
  • 2
  • 5
  • 13
2
votes
0 answers

Is there any tools or codes to translate the BPEL into NuSMV code?

Is there any tools or codes to translate the BPEL into NuSMV code? I have found the paper Modelling and verification of BPEL business processes, but there is no tools or codes provided.
yu chen
  • 21
  • 1
2
votes
0 answers

nuXmv empty initial set of states for LTL formula

I'm using nuXmv 1.1.1 to model check the following finite state machine. MODULE main VAR node : {_0_0,_1_0,_1_1,_1_2,_1_3,_2_0}; DEFINE setParentThis_r_ := case TRUE : FALSE; esac; setParent_r_ := case node=_1_3 :TRUE; TRUE…
Davidbrcz
  • 2,335
  • 18
  • 27
2
votes
0 answers

Induction by assume-guarantee with nuSMV

I have an asynchronous symmetric ring-shaped protocol with 5 processes that satisfies a given property. I want to prove (or get counterexample) that the property is true for protocols with 6 number of processes and more; that is ∀n.φ(n) I…
mirzanahal
  • 167
  • 2
  • 12
2
votes
1 answer

Exploration of State Space in NuSMV Source

I am working on a program correction/synthesis project. My task is to obtain an error trace (counter-example), locate it in the complete state space, and repair the model at that location. I want to implement this as a NuSMV extension. I have been…
Brishna Batool
  • 445
  • 3
  • 15
2
votes
1 answer

xSAP error passing an smv model

I was trying to pass to xSAP (version 1.2.0) an smv model, but I got this error panda@jakul:~/Desktop$ python /home/panda/Desktop/xSAP/scripts/extend_model.py -v /home/panda/Desktop/brca.smv /home/panda/Desktop/brca.fei Traceback (most recent call…
panda
  • 163
  • 2
  • 9
2
votes
1 answer

Check CTL specification in SMV

When I try to check "EG (!s11included & !s10included)" in SMV, it is reported false and gives a counter example as follows, which I think on the contrary it support this CTL specification. Is there something wrong with my CTL specification? --…
firefighter
  • 25
  • 3
2
votes
1 answer

Reason for difference in number of reachable states

I verify an 8-bit adder with this code. When I print the number of reachable states are 1 if the main module is empty and 2^32 if the entire main module is included. What makes this difference in reported number of reachable states? For a 4-bit…
Niklas Rosencrantz
  • 25,640
  • 75
  • 229
  • 424
2
votes
1 answer

Error with NuSMV

MODULE main VAR x : 0 .. 2; ASSIGN init (x) := 2; next (x) := case x = 2 : x = 10; esac; SPEC AG x = 2 -> AG X x = 20 at token "X": syntax error - Why syntax error? I try to use the keyword X but never…
Niklas Rosencrantz
  • 25,640
  • 75
  • 229
  • 424
2
votes
1 answer

NuSMV passes wrong specification

I am new to NuSMV and CTL and was trying simple Examples. I have 3 states A, B, and C and there is a transition from A-> B I modeled it in NuSMV and want to check if there is any execution path from B to A. Eventhough I have not defined such…
karthi
  • 2,762
  • 4
  • 30
  • 28
2
votes
1 answer

Use model checker to check one particular trace

I'm using LTL to define rules for open interaction protocols. I then want to check if a particular interaction follows the specification, or if any rule was broken. My immediate approach was to use NuSMV, but the problem is that I don't have a model…
adivinanza
  • 31
  • 4
1
2 3 4 5 6 7