Функциональный модуль в NuSMV не может использовать входные переменные в качестве параметров,
Как решить эту проблему без изменения IVAR на VAR.
Например, следующий код:
MODULE main
IVAR
p1 : boolean;
p2 : boolean;
VAR
x : boolean;
f1:Fun(p1,p2);
INIT
x = FALSE;
ASSIGN
next(x) := f1.y;
MODULE Fun(p1,p2)
VAR
y : boolean;
ASSIGN
y := p1 & p2;
Итак, возникает проблема с входными переменными.
Как с этим бороться?Значит ли это, что в NuSMV мы не можем объявить модули с параметрами входных переменных ??
Большое спасибо!