Use model checker to check one particular trace

Question

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!

Answer 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!