Reputation: 31
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!
Upvotes: 2
Views: 159
Reputation: 31
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!
Upvotes: 1