Error with NuSMV

Question

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 succeeded.

score 2 · Accepted Answer · answered Apr 06 '17 at 08:05

2

The problem is that you are using an LTL operator within a CTL formula.

In CTL, you have two options to talk about the next state:

AX P : along all outgoing paths, in the next state P holds
EX P : along at least one of the outgoing paths, in the next state P holds

See this picture:

As a side note, you have a syntax error on line 6 because you are assigning a Bool to an integer variable. You might want to change x = 10 into 10 first, then change the domain of values for variable x and add some exhaustive conditions to that case ... esac construct.

answered Apr 06 '17 at 08:05

Patrick Trentin

7,126
3
23
40

I think it is an LTL spec that is expected (but I'm not 100 %). Something like `LTLSPEC AG P != WRITE K -> AG K = X K` or in English almost a tautology: If P never changes K then K stays the same. How can I formalize that? – Niklas Rosencrantz Apr 06 '17 at 10:46
1

@DjDac it's fine, if you want to write an *LTL formula*, then you should use `G` instead of `AG`. You should first formalise `P` and `K`. – Patrick Trentin Apr 06 '17 at 10:49
For my application I think I need three models (three modules): `Proc` (process), `Mem` (memory) and `UART` (connector). I want to prove that `K` in the memory (`Mem`) stays the same if `Proc` doesn't write to `K`. I don't know yet how I create three or more modules with shared variables but I'll try. I still get error every time I try to use `X` for instance the following generates a parser error `LTLSPEC G state != stop -> K = X K`. I'm going to ask a new question perhaps if it still doesn't work today. I'm reading the manual pages and the user manual for NuSMV but there aren't many examples – Niklas Rosencrantz Apr 06 '17 at 11:42
1

@DjDac You are getting an error because it's written in the wrong way: `X` is an operator over a Boolean property, you cannot put an equality sign there. What you should write is: `LTLSPEC G state != stop -> K = old_K`, where old_K is conveniently defined. – Patrick Trentin Apr 06 '17 at 11:45
Thanks for the help. The following compiled `LTLSPEC G state != read -> K <-> X K` – Niklas Rosencrantz Apr 06 '17 at 11:46
I settle for this `LTLSPEC G proc != write-K -> old-K = K` because I know no way of expressing "`WRITE K` " in NuSMV. It compiled and gave a counterexample so at least I have a code outline and defined what I want to prove. Now my next question is how I can share data between models if I make three different models. – Niklas Rosencrantz Apr 06 '17 at 12:00
1

@DjDac Did you take a look at the slides I linked you the other day? there should be plenty of examples :) – Patrick Trentin Apr 06 '17 at 12:05
Thanks for the help. I just wrote two exercises to learn NuSMV. It's getting clear but I also find it difficult because I don't know how to make a function or a method, I know only the `next` of variables. I'm going to read all I can. – Niklas Rosencrantz Apr 06 '17 at 12:07
1

@DjDac there's no function or method, you should think of it as a way to describe a circuit: instead of encoding a plus function, you encode an adder 'circuit' that does just that – Patrick Trentin Apr 06 '17 at 12:10
I'm eager to know. I read the slides and write SMV code to know also how I can use shared variables or similar way to share data between different models. I should create three models: Mem (memory), Proc (process) and UART (the connector). I want to prove `LTLSPEC G proc != write-K -> old-K = K` where proc is the process and `K` belongs to the other model which is the memory. I think it could be appropriate to use the dot `.` such as `mem.k` and `mem.old-k` but I'm not there yet. I should learn all the basics and fast because I want to get done with my project by May or June. – Niklas Rosencrantz Apr 06 '17 at 12:39
Let us [continue this discussion in chat](http://chat.stackoverflow.com/rooms/140075/discussion-between-patrick-trentin-and-dj-dac). – Patrick Trentin Apr 06 '17 at 12:41

Error with NuSMV

1 Answers1