如何在NuSMV中创建简单的Kripke模型? [英] How to create a simple Kripke model in NuSMV?
问题描述
我目前正在对LTL(线性时间逻辑)和CTL(计算树逻辑)进行一些理论研究.我是NuSMV的新手,我很难创建一个简单的Kripke结构.
I am currently doing some theoretical research in LTL (Linear-time Temporal Logic) and CTL (Computation Tree Logic). I am new to NuSMV and I have difficulty to create a simple Kripke structure.
我的结构是M =(S,R,L),其中S = {s0,s1,s2}是可能状态的集合,R是过渡关系,使得:s0-> s1,s0-> s2, s1-> s0,s1-> s2和s2-> s2,并且L是每种状态的标记函数,定义如下:L(s0)= {p,q},L(s1)= {q,r},并且L(s2)= {r}.我使用的是Huth和Ryan在计算机科学中的逻辑"教科书中描述的符号.我尝试了以下两个代码:
My structure is M = (S, R, L) where S = {s0, s1, s2} is the set of possible states, R is a transition relation such that: s0 -> s1, s0 -> s2, s1 -> s0, s1 -> s2, and s2 -> s2, and L is the labeling function for each state defined by: L(s0) = {p, q}, L(s1) = {q, r}, and L(s2) = {r}. I am using notations describe in Logic in Computer Science textbook by Huth and Ryan. I have tried two following codes:
第一个代码:
MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0, s1, s2};
ASSIGN
init(state) := s0;
next(state) :=
case
state = s0 : {s1, s2};
state = s1 : {s2};
state = s2 : {s2};
esac;
init(p) := TRUE;
init(q) := TRUE;
init(r) := FALSE;
next(p) :=
case
state = s1 | state = s2 : FALSE;
esac;
next(q) :=
case
state = s1 : TRUE;
state = s2 : FALSE;
esac;
next(r) :=
case
state = s1 : FALSE;
state = s2 : TRUE;
esac;
SPEC
p & q
第二个代码:
MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0, s1, s2};
ASSIGN
init(state) := s0;
next(state) :=
case
state = s0 : {s1, s2};
state = s1 : {s2};
state = s2 : {s2};
esac;
init(p) := TRUE;
init(q) := TRUE;
init(r) := FALSE;
next(p) := !p;
next(q) :=
case
state = s0 & next(state) = s1 : q;
state = s0 & next(state) = s2 : !q;
state = s1 & next(state) = s0 : q;
state = s1 & next(state) = s2 : !q;
esac;
next(r) :=
case
state = s0 & next(state) = s1 : r;
state = s0 & next(state) = s2 : r;
state = s1 & next(state) = s0 : !r;
state = s1 & next(state) = s2 : r;
esac;
LTLSPEC
p & q
出了点问题,我得到了以下消息:案例条件并不详尽".这是什么意思?如何解决我的问题?
Something was wrong and I got this message: "case conditions are not exhaustive". What does it mean? How do I fix my problem?
推荐答案
因为您必须为每种情况输入其默认值". 第一个代码:
Because you must enter for each case also its "default". The first code:
MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0, s1, s2};
ASSIGN
init(state) := s0;
next(state) :=
case
state = s0 : {s1, s2};
state = s1 : {s2};
state = s2 : {s2};
TRUE : state;
esac;
init(p) := TRUE;
init(q) := TRUE;
init(r) := FALSE;
next(p) :=
case
state = s1 | state = s2 : FALSE;
esac;
next(q) :=
case
state = s1 : TRUE;
state = s2 : FALSE;
TRUE : q;
esac;
next(r) :=
case
state = s1 : FALSE;
state = s2 : TRUE;
TRUE : r;
esac;
SPEC
p & q
和第二个代码:
MODULE main
VAR
p : boolean;
q : boolean;
r : boolean;
state : {s0, s1, s2};
ASSIGN
init(state) := s0;
next(state) :=
case
state = s0 : {s1, s2};
state = s1 : {s2};
state = s2 : {s2};
TRUE : state;
esac;
init(p) := TRUE;
init(q) := TRUE;
init(r) := FALSE;
next(p) := !p;
next(q) :=
case
state = s0 & next(state) = s1 : q;
state = s0 & next(state) = s2 : !q;
state = s1 & next(state) = s0 : q;
state = s1 & next(state) = s2 : !q;
TRUE : q;
esac;
next(r) :=
case
state = s0 & next(state) = s1 : r;
state = s0 & next(state) = s2 : r;
state = s1 & next(state) = s0 : !r;
state = s1 & next(state) = s2 : r;
TRUE : r;
esac;
LTLSPEC
p & q
这篇关于如何在NuSMV中创建简单的Kripke模型?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!