Skip to content

Commit cba30a1

Browse files
committed
SMV: test for module instance as module argument
This adds a test from the SMV manual, in which a module instance is passed as argument to another module.
1 parent 371bb9a commit cba30a1

File tree

2 files changed

+23
-0
lines changed

2 files changed

+23
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
module_argument1.smv
3+
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
--
Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
-- from the NuSMV 2.7 manual
2+
3+
MODULE main
4+
VAR
5+
a : bar;
6+
m : foo(a);
7+
8+
MODULE bar
9+
VAR
10+
q : boolean;
11+
p : boolean;
12+
13+
MODULE foo(c)
14+
DEFINE
15+
flag := c.q | c.p;

0 commit comments

Comments
 (0)