Stack Overflow
Stack Overflow

Questions tagged [nuxmv]

19 questions
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
0 answers

How to identify deadlock conditions in the model containing infinite domain variable?

"check_fsm" command is used in nuxmv shell for checking deadlock conditions in model containing finite domain variables. But in case of models containing infinite domain variables like integers with no range or real variable the model can't be built…
vishudh
  • 21
  • 1
2
votes
1 answer

How to interpret the differnce in results of check_property & msat_check_ltlspec_bmc counterexamples

I created a generic SMV program and checked a pair of LTL properties using both check_property and msat_check_ltlspec_bmc. One property is found to be true with both commands. The other property, instead, gives a counter-example of 14 states with…
Ranjana N
  • 59
  • 5
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

nuXmv how does it know in initial state that (AF p) & (AF w) is false

I have a question concerning nuXmv solution. I have a simple graph where the initial state is s1 and there are two arcs from s1, one leads to s2, the other to s3. From s2 and s3 there is one arc leading to s1. This is the program in nuXmv which…
Joanna
  • 154
  • 2
  • 13
2
votes
1 answer

NuXMV use of Real numbers

I am using nuXmv on a work that I am developing, and I am having troubles using Reals. Supose I have the program: MODULE main VAR t : Real; r : 0..5000; ASSIGN init(t):=0; init(r):=0; TRANS case r>=500 :next(r)=0 & next(t)=0 &…
Daniel Soares
  • 23
  • 4
1
vote
2 answers

Four-Knights Puzzle in nusmv/nuxmv

Does anyone have code for Four-Knights Puzzle written in smv (nusmv or nuxmv)? I describe the problem with a grid, but when I tried to write the constraints/moves, I got errors like: line 35: recursively defined: S1 in definition of next(S3) at line…
אברהם וספיר רביב
  • 21
  • 2
1
vote
1 answer

4 in a row with NUSMV

I'm trying to create a 4 in a row implementation in NuSMV. Unfortunately I am new to NuSMV and I have difficulty to creating it. I have tried to define all the winning cases for player 1 and have used 2D array to represent the grid. Now im getting…
georgi georgiev
  • 11
  • 1
1
vote
1 answer

nuXmv syntax error when using variable instead of integer

I have a model in muXmv, where I initialize with a range of values like - VAR x : 0..100; ASSIGN init(x) := 10..50; this works perfectly fine. However, when I use variable instead of values, ASSIGN init(x) := LB..UB; DEFINE LB := 10; …
Sneha Sahu
  • 33
  • 8
1
vote
1 answer

Determining when two boolean functions are equivalent?

Problem Given two boolean functions f1(a,b) and f2(a,b,c) with a,b and c booleans, I'd like to know if there exists a value of c such that for any combinations of a et b f1(a,b)=f2(a,b,c). For example if f1(a,b)=a AND b and f2(a,b,c)=a AND b AND c,…
f1f2
  • 23
  • 3
1
vote
1 answer

syntax errors in model checking with nuXmv

Now there are two options for customer, phone call and sms to clinic to book an appointment with doctor. The phone call or sms need to deliver to phone attender or reception, then do the next.... Well as we know, the phone call and sms can…
UD.Cole
  • 45
  • 8
1
vote
1 answer

Error: Impossible to build a BDD FSM with infinite precision variables

I just installed nuXmv and wanted to try out the example growing-counter-integer from the examples folder. When I try to run the command: build_model, I get the error message: file growing-counter-integer.smv: line 30: Impossible to build a BDD…
Alex
  • 13
  • 1
  • 5
1
vote
1 answer

Different results from check_property and msat_check_ltlspec_bmc in NuXMV

The following property is true with check_property but msat_check_ltlspec_bmc gives counterexample. The result of latter one seems to be correct."G (((tt >= 7) -> G ((FlagLO = FALSE)))) IN module". how do we explain this? I tried this with slightly…
Ranjana N
  • 59
  • 5
1
vote
1 answer

How to interpret the Result of msat LTL commands of NuXMV

I am using NuXMV for checking LTL properties using msat_check_ltlspec_bmc command on a fairly large model. The result shows no counterexample found within the given bounds. Do I interpret it as that property is True. Or it can alternatively mean…
Ranjana N
  • 59
  • 5
1
vote
1 answer

syntax error nested NEXT operator in NuSMV

I try to use NuSMV to check my model and here is the code. However, when I input NuSMV kernel.smv in the shell, it occur an error file kernel.smv: line 16: nested NEXT operators: next(_b) in definition of next(_cond) in definition of next(tx.fired)…
jiahao he
  • 15
  • 3
1
2