repositories
/
master.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
up',
[master.git]
/
ar
/
assignments
/
marble.smv
1
MODULE main
2
VAR
3
a : 0..100;
4
c : 0..20;
5
INIT
6
a = 1 & c = 0
7
TRANS
8
case
9
c<20 : next(c) = c+1;
10
TRUE : next(c) = c;
11
esac & (
12
case
13
a<100 : next(a) = a+1;
14
TRUE : next(a)=a;
15
esac |
16
case
17
a<=50 : next(a) = 2*a;
18
TRUE : next(a)=a;
19
esac)
20
LTLSPEC G !(a = 100 & c = 8)