mcrl2 交通灯变色问题

如何解决mcrl2 交通灯变色问题

我正在尝试使用 mcrl2 解决交通灯问题。我不知道我的代码是否 100% 正确，但它可以编译。

基本上我有 3 种颜色和 3 个交通灯，使用此代码我可以切换它们的颜色，但是我想做出限制，例如，如果一个交通灯是绿色，则其他交通灯不能更改为任何颜色，它们只能更改它们的颜色当绿灯变成黄灯时。

    sort
        Color = struct green | red | yellow;

    map
        next: Color -> Color;
    
    eqn
        next(green) = yellow;
        next(yellow) = red;
        next(red) = green;
    
    act
        toRed,toGreen,toRedYellow,toYellow;
    
    proc
        Lighter1 (c : Color) = (c == green) -> toYellow.Lighter1(next(c))
                             +(c == yellow) -> toRed.Lighter1(next(c))
                             +(c == red) -> toGreen.Lighter1(next(c));
    
        Lighter2 (c : Color) = (c == green) -> toYellow.Lighter2(next(c))
                             +(c == yellow) -> toRed.Lighter2(next(c))
                             +(c == red) -> toGreen.Lighter2(next(c));
    
        Lighter3 (c : Color) = (c == green) -> toYellow.Lighter3(next(c))
                             +(c == yellow) -> toRed.Lighter3(next(c))
                             +(c == red) -> toGreen.Lighter3(next(c));
    init
        Lighter1(green) || Lighter2(red) || Lighter3(green);