diff --git a/regression/smv/modules/module_argument1.desc b/regression/smv/modules/module_argument1.desc new file mode 100644 index 000000000..7e6baa5ac --- /dev/null +++ b/regression/smv/modules/module_argument1.desc @@ -0,0 +1,8 @@ +CORE +module_argument1.smv + +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring +-- diff --git a/regression/smv/modules/module_argument1.smv b/regression/smv/modules/module_argument1.smv new file mode 100644 index 000000000..e046990d9 --- /dev/null +++ b/regression/smv/modules/module_argument1.smv @@ -0,0 +1,15 @@ +-- from the NuSMV 2.7 manual + +MODULE main + VAR + a : bar; + m : foo(a); + +MODULE bar + VAR + q : boolean; + p : boolean; + +MODULE foo(c) + DEFINE + flag := c.q | c.p;