Как решить проблему с ошибкой IVAR в NuSMV

Question

Функциональный модуль в 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 мы не можем объявить модули с параметрами входных переменных??

Большое спасибо!