nusmv - 如何将最后一部分（**一盏灯只能进行 10 次转换**）添加到这个 NUSMV 代码中？

Question

问题图片

如何将最后一部分（一盏灯只能进行 10 次转换）添加到此代码中？

MODULE light (other)
VAR

state:{r, y, g};
ASSIGN
init(state) := r;
next (state) := case
        state = r & other =r: {r, y};
        state = y : g;
        state=g : {g, r};
        TRUE : state;
    esac;

MODULE main
VAR
tl1 : process light(tl2.state);
tl2 : process light (tl1.state);

标签： nusmv