我正在制作一个图的模型，其中消息通过节点之间的通道进行路由，以完成家庭作业。
(基本上，消息只包含目标节点的id，节点可以创建消息并通过预定义的路由表对其进行路由，每个通道一次可以包含一条消息，目标是找到死锁。(
问题是在添加了大约10个节点(我需要14个(之后，NuSMV在选择初始状态时陷入了困境，即使所有通道都应该为0。我不知道它为什么会卡住(对于10个节点，pick_state需要几秒钟的时间，模拟几乎是即时的(。是否有一些环境变量我应该更改，或者我的模型中是否存在一些问题？
这是代码(我还是个初学者(：
-- Gives next channel id for node i and msg destination j
MODULE route(i,j)
DEFINE
-- out '0' implies no route
out :=
case
j = 0 : 0; -- empty message
i = j : 0; -- already at destination
i = 1 : 1;
i = 2 : 2;
i = 3 :
case
j in {1,2,12,13,14} : 6;
TRUE : 3;
esac;
i = 4 :
case
j in {1,2,12,13,14} : 21;
j in {3,5} : 4;
TRUE : 7;
esac;
i = 5 : 5;
i = 6 : 8;
i = 7 : 9;
i = 8 :
case
j in {1,2,12,13,14} : 17;
j in {3,4,5,6,7} : 20;
TRUE : 10;
esac;
i = 9 : 11;
i = 10 : 12;
i = 11 : 13;
i = 12 :
case
j = 13 : 14;
j = 14 : 18;
TRUE : 16;
esac;
i = 13 : 15;
i = 14 : 19;
TRUE : 0;
esac;
-- Node with id, at most 4 in and 3 out channels with known ids
-- also a new 'channel' for creating new msgs
MODULE node(id, new, in1, in2, in3, in4, out1, out2, out3, out1_id, out2_id, out3_id)
VAR
r : route(id,new); -- route for new msg
r1 : route(id,in1); -- route for msg on channel 1
r2 : route(id,in2); -- route for msg on channel 2
r3 : route(id,in3); -- ...
r4 : route(id,in4);
TRANS
-- out occupied or (free and ( stay free or pull from input channel if route matches ))
(out1 != 0 | (out1 = 0 & (next(out1) = 0 | (r1.out = out1_id & next(out1) = in1 & next(in1) = 0)
| (r2.out = out1_id & next(out1) = in2 & next(in2) = 0)
| (r3.out = out1_id & next(out1) = in3 & next(in3) = 0)
| (r4.out = out1_id & next(out1) = in4 & next(in4) = 0)
| (r.out = out1_id & next(out1) = new & next(new) = 0)))) &
(out2 != 0 | (out2 = 0 & (next(out2) = 0 | (r1.out = out2_id & next(out2) = in1 & next(in1) = 0)
| (r2.out = out2_id & next(out2) = in2 & next(in2) = 0)
| (r3.out = out2_id & next(out2) = in3 & next(in3) = 0)
| (r4.out = out2_id & next(out2) = in4 & next(in4) = 0)
| (r.out = out2_id & next(out2) = new & next(new) = 0)))) &
(out3 != 0 | (out3 = 0 & (next(out3) = 0 | (r1.out = out3_id & next(out3) = in1 & next(in1) = 0)
| (r2.out = out3_id & next(out3) = in2 & next(in2) = 0)
| (r3.out = out3_id & next(out3) = in3 & next(in3) = 0)
| (r4.out = out3_id & next(out3) = in4 & next(in4) = 0)
| (r.out = out3_id & next(out3) = new & next(new) = 0)))) &
-- in empty or ( msg at destination or ( msg should be routed and (wait or push to out channel by route )))
(in1 = 0 | (in1 = id & next(in1) = 0) | (in1 != id & in1 != 0 & (next(in1) = in1
| (r1.out = out1_id & out1 = 0 & next(out1) = in1 & next(in1) = 0)
| (r1.out = out2_id & out2 = 0 & next(out2) = in1 & next(in1) = 0)
| (r1.out = out3_id & out3 = 0 & next(out3) = in1 & next(in1) = 0)))) &
(in2 = 0 | (in2 = id & next(in2) = 0) | (in2 != id & in2 != 0 & (next(in2) = in2
| (r2.out = out1_id & out1 = 0 & next(out1) = in2 & next(in2) = 0)
| (r2.out = out2_id & out2 = 0 & next(out2) = in2 & next(in2) = 0)
| (r2.out = out3_id & out3 = 0 & next(out3) = in2 & next(in2) = 0)))) &
(in3 = 0 | (in3 = id & next(in3) = 0) | (in3 != id & in3 != 0 & (next(in3) = in3
| (r3.out = out1_id & out1 = 0 & next(out1) = in3 & next(in3) = 0)
| (r3.out = out2_id & out2 = 0 & next(out2) = in3 & next(in3) = 0)
| (r3.out = out3_id & out3 = 0 & next(out3) = in3 & next(in3) = 0)))) &
(in4 = 0 | (in4 = id & next(in3) = 0) | (in4 != id & in4 != 0 & (next(in4) = in4
| (r4.out = out1_id & out1 = 0 & next(out1) = in4 & next(in4) = 0)
| (r4.out = out2_id & out2 = 0 & next(out2) = in4 & next(in4) = 0)
| (r4.out = out3_id & out3 = 0 & next(out3) = in4 & next(in4) = 0)))) &
(new = 0 | (new = id & next(new) = 0) | (new != id & new != 0 & (next(new) = new
| (r.out = out1_id & out1 = 0 & next(out1) = new & next(new) = 0)
| (r.out = out2_id & out2 = 0 & next(out2) = new & next(new) = 0)
| (r.out = out3_id & out3 = 0 & next(out3) = new & next(new) = 0))))
MODULE main
DEFINE
M := {1,3,11};
VAR
c1 : 0..14;
c2 : 0..14;
c3 : 0..14;
c4 : 0..14;
c5 : 0..14;
c6 : 0..14;
c7 : 0..14;
c8 : 0..14;
c9 : 0..14;
c10 : 0..14;
c11 : 0..14;
c12 : 0..14;
c13 : 0..14;
c14 : 0..14;
c15 : 0..14;
c16 : 0..14;
c17 : 0..14;
c18 : 0..14;
c19 : 0..14;
c20 : 0..14;
c21 : 0..14;
new1 : 0..14;
new2 : 0..14;
new3 : 0..14;
new4 : 0..14;
new5 : 0..14;
new6 : 0..14;
new7 : 0..14;
new8 : 0..14;
new9 : 0..14;
new10 : 0..14;
new11 : 0..14;
new12 : 0..14;
new13 : 0..14;
new14 : 0..14;
-- NODE ID, NEW , IN1, IN2, IN3, IN4, OUT1 OUT2 OUT3 [ OUT IDS ]
n1 : node(1 , new1 , c16, 0 , 0 , 0 , c1 , 0 , 0 , 1 , 0 , 0 );
n2 : node(2 , new2 , c1 , 0 , 0 , 0 , c2 , 0 , 0 , 2 , 0 , 0 );
n3 : node(3 , new3 , c2 , c5 , 0 , 0 , c3 , c6 , 0 , 3 , 6 , 0 );
n4 : node(4 , new4 , c3 , c20, 0 , 0 , c4 , c7 , c21, 4 , 7 , 21);
n5 : node(5 , new5 , c4 , 0 , 0 , 0 , c5 , 0 , 0 , 5 , 0 , 0 );
n6 : node(6 , new6 , c7 , 0 , 0 , 0 , c8 , 0 , 0 , 8 , 0 , 0 );
n7 : node(7 , new7 , c8 , 0 , 0 , 0 , c9 , 0 , 0 , 9 , 0 , 0 );
n8 : node(8 , new8 , c9 , 0 , 0 , 0 , c10, c17, c20, 10, 17, 20);
n9 : node(9 , new9 , c10, 0 , 0 , 0 , c11, 0 , 0 , 11, 0 , 0 );
n10 : node(10, new10, c11, 0 , 0 , 0 , c12, 0 , 0 , 12, 0 , 0 );
n11 : node(11, new11, c12, 0 , 0 , 0 , c13, 0 , 0 , 13, 0 , 0 );
n12 : node(12, new12, c13, c15, c19, 0 , c14, c16, c18, 14, 16, 18);
n13 : node(13, new13, c14, 0 , 0 , 0 , c15, 0 , 0 , 15, 0 , 0 );
n14 : node(14, new14, c6 , c17, c18, c21, c19, 0 , 0 , 19, 0 , 0 );
INIT
c1 = 0 &
c2 = 0 &
c3 = 0 &
c4 = 0 &
c5 = 0 &
c6 = 0 &
c7 = 0 &
c8 = 0 &
c9 = 0 &
c10 = 0 &
c11 = 0 &
c12 = 0 &
c13 = 0 &
c14 = 0 &
c15 = 0 &
c16 = 0 &
c17 = 0 &
c18 = 0 &
c19 = 0 &
c20 = 0 &
c21 = 0 &
new1 = 0 &
new2 = 0 &
new3 = 0 &
new4 = 0 &
new5 = 0 &
new6 = 0 &
new7 = 0 &
new8 = 0 &
new9 = 0 &
new10 = 0 &
new11 = 0 &
new12 = 0 &
new13 = 0 &
new14 = 0
TRANS
(next(new1 ) = 0 | (1 in M & next(new1 ) in M)) &
(next(new2 ) = 0 | (2 in M & next(new2 ) in M)) &
(next(new3 ) = 0 | (3 in M & next(new3 ) in M)) &
(next(new4 ) = 0 | (4 in M & next(new4 ) in M)) &
(next(new5 ) = 0 | (5 in M & next(new5 ) in M)) &
(next(new6 ) = 0 | (6 in M & next(new6 ) in M)) &
(next(new7 ) = 0 | (7 in M & next(new7 ) in M)) &
(next(new8 ) = 0 | (8 in M & next(new8 ) in M)) &
(next(new9 ) = 0 | (9 in M & next(new9 ) in M)) &
(next(new10) = 0 | (10 in M & next(new10) in M)) &
(next(new11) = 0 | (11 in M & next(new11) in M)) &
(next(new12) = 0 | (12 in M & next(new12) in M)) &
(next(new13) = 0 | (13 in M & next(new13) in M)) &
(next(new14) = 0 | (14 in M & next(new14) in M))
带有标记id 的图形图像
您可以使用go_bmc和bmc_pick_state而不是go和pick_state。
如果出于某种原因需要使用OBDD，则可以将选项-dynamic指定为NuSMV，并启用变量的动态重新排序。
在我的机器上，为您的模型选择初始状态在这两种情况下都会变得更快。