nusmv - nuXMV 初学者帮助

Question

我是学习 nuXMV 的新手，希望有人能帮助我。我正在尝试从 UPAAL 实现灯示例，只是为了学习如何使用这个工具。

所以我想做的是这个例子：

我知道下面的代码不起作用，但这就是我走了多远。我不知道如何模拟例如用户的按钮按下。

@TIME_DOMAIN continuous

MODULE main
    VAR 
        off : boolean;  
        on : boolean; 
        bright: boolean;
    c: clock;
    press : boolean;
    LTLSPEC G F off;
    
    INIT off = TRUE & on = FALSE & bright = FALSE & c = 0 & press = FALSE;

    ASSIGN next (press) := !press; 

    TRANS
    case
        off & press : on & !off & !press;
        on & (c > 5) & press : off & c = 0 & !on & !press;
        on & (c <= 5) & press : bright & !on & !press;
        bright & press : off & !bright & !press;
        esac;

如果有人知道如何对其进行编码 - 有一个示例可以指导它会很好:)