2

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 of the interaction that I want to check, but just one particular finite trace (the values of all variables in all states).

Is there any way in which I could specify this in NuSMV? I basically want to input one of the models that NuSMV outputs as counterexamples:

-> State: 1.1 <-
a = TRUE
b = FALSE
-> State: 1.2 <-
a = FALSE
-> State: 1.3 <-
a = TRUE

And verify it. Or is NuSMV the wrong tool for this?

Thanks!

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
adivinanza
  • 31
  • 4
  • Your question is not clear to me. You have a 'bogus' trace or a 'bogus' state? Why cannot you formalise the 'bogus' trace into a NuSMV model? where does your difficulty lie? Could you edit your question and provide the full extent of your source code? – Patrick Trentin Sep 21 '16 at 14:41
  • 1
    Yes, I actually could formalize the trace into a NuSMV model (I only had to specify each state with a variable), but I only realized after the question was posted. Sorry, I was really not seeing it. Thanks for the answer!! – adivinanza Sep 22 '16 at 15:44
  • I would suggest you to to answer your own question with a detailed example of your code and solution, it might be helpful for others. – Patrick Trentin Sep 22 '16 at 16:00

1 Answers1

1

After some thinking, I found a solution to encode a particular trace in a NuSMV model. It's quite simple, the trick is to use one variable for each state of the trace.

For example, I wanted to encode an interaction, and I wanted only the last uttered message to be true in each state. If the interaction to encode is ['a','b','a'], the NuSMV model would be:

MODULE main
VAR
a : boolean;
b : boolean;
state : {s0,s1,s2};

ASSIGN
init(a) := FALSE;
init(state) := s0;
next(a) := 
    case
        state = s0 : TRUE;
        state = s1 : FALSE;
        state = s2 : TRUE;
    esac;
next(b) := 
    case
        state = s0 : FALSE;
        state = s1 : TRUE;
        state = s2 : FALSE;
    esac;
next(state) := 
    case
        state = s0 : s1;
        state = s1 : s2;
        state = s2 : s2;
    esac;

I hope maybe it's useful for someone!

adivinanza
  • 31
  • 4