update 3b fixed

[ar1516.git] / a2 / src / 3b.smv

diff --git a/a2/src/3b.smv b/a2/src/3b.smv
new file mode 100644 (file)
index 0000000..f88fc04
--- /dev/null
+++ b/a2/src/3b.smv
@@ -0,0 +1,47 @@
+MODULE main
+VAR
+-- 0=b,1=c,2=d,3=e,4=f
+p0: {b,c,d,e,f};
+p1: {b,c,d,e,f};
+p2: {b,c,d,e,f};
+p3: {b,c,d,e,f};
+p4: {b,c,d,e,f};
+p5: {b,c,d,e,f};
+m: 0..4;
+INIT
+p0=b & p1=c & p2=d & p3=e & p4=f & p5=b & m=0
+TRANS
+(
+       next(m)=1 &
+       next(p0)=p1 &
+       next(p1)=p2 &
+       next(p2)=p0 &
+       next(p3)=p3 &
+       next(p4)=p4 &
+       next(p5)=p5
+) | (
+       next(m)=2 &
+       next(p0)=p0 &
+       next(p1)=p2 &
+       next(p2)=p3 &
+       next(p3)=p1 &
+       next(p4)=p4 &
+       next(p5)=p5
+) | (
+       next(m)=3 &
+       next(p0)=p0 &
+       next(p1)=p1 &
+       next(p2)=p3 &
+       next(p3)=p4 &
+       next(p4)=p2 &
+       next(p5)=p5
+) | (
+       next(m)=4 &
+       next(p0)=p0 &
+       next(p1)=p1 &
+       next(p2)=p2 &
+       next(p3)=p4 &
+       next(p4)=p5 &
+       next(p5)=p3
+)
+LTLSPEC G !(p0=b & p1=d & p2=c & p3=e & p4=f & p5=b)