Mercurial > hg > Members > kono > Proof > automaton

annotate a13/smv/test10.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 3be1afb87f82
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 main
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 y : 0..15;
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(y) := 0;
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 TRANS
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 case
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 y=7: next(y)=0;
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 TRUE : next(y) = ((y + 1) mod 16);
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 esac
139
3be1afb87f82 add utm
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
11 LTLSPEC G ( y=4 -> X y=5 )