Mercurial > hg > Members > kono > Proof > automaton

annotate a13/smv/test2.smv @ 218:689be82c08fa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 21 Jun 2021 19:22:06 +0900
parents 0e8a0e50ed26
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
127
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 MODULE counter_cell(carry_in)
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2 VAR
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 value : boolean;
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 ASSIGN
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 init(value) := FALSE;
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 next(value) := value xor carry_in;
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 DEFINE
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 carry_out := value & carry_in;
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 MODULE main
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 VAR
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 bit0 : counter_cell(TRUE);
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 bit1 : counter_cell(bit0.carry_out);
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 bit2 : counter_cell(bit1.carry_out);